Home / Unlabelled / HeapHopper - A Bounded Model Checking Framework For Heap-implementations

HeapHopper - A Bounded Model Checking Framework For Heap-implementations


HeapHopper is a bounded model checking framework for Heap-implementations.

Setup
sudo apt update && sudo apt install build-essential python-dev virtualenvwrapper
 git clone https://github.com/angr/heaphopper.git && cd ./heaphopper
 mkvirtualenv -ppython2 heaphopper
 pip install -e .

Required Packages
build-essential python-dev virtualenvwrapper

Required Python-Packages
ana angr cle claripy IPython psutil pyelftools pyyaml

Examples
# Gen zoo of permutations
 heaphopper.py gen -c analysis.yaml
 
 #  Trace instance
 make -C tests
 heaphopper.py  trace -c tests/how2heap_fastbin_dup/analysis.yaml -b tests/how2heap_fastbin_dup/fastbin_dup.bin
 
 # Gen PoC
 heaphopper.py poc -c tests/how2heap_fastbin_dup/analysis.yaml -r tests/how2heap_fastbin_dup/fastbin_dup.bin-result.yaml -d tests/how2heap_fastbin_dup/fastbin_dup.bin-desc.yaml -s tests/how2heap_fastbin_dup/fastbin_dup.c -b tests/how2heap_fastbin_dup/fastbin_dup.bin
 
 # Tests
 cd tests
 # Show source
 cat how2heap_fastbin_dup/fastbin_dup.c
 # Run tests
 ./run_tests.py
 # Show PoC source
 cat pocs/malloc_non_heap/fastbin_dup.bin/poc_0_0.c
 # Run PoC
 ./run_poc.sh pocs/malloc_non_heap/fastbin_dup.bin/bin/poc_0_0.bin

Publication
This work has been published at the 27th USENIX Security Symposium.
You can read the paper here.
Cite:
@inproceedings {heaphopper,
 author = {Eckert, Moritz and Bianchi, Antonio and Wang, Ruoyu and Shoshitaishvili, Yan and Kruegel, Christopher and Vigna, Giovanni},
 title = {HeapHopper: Bringing Bounded Model Checking to Heap Implementation Security},
 booktitle = {27th {USENIX} Security Symposium ({USENIX} Security 18)},
 year = {2018},
 address = {Baltimore, MD},
 url = {https://www.usenix.org/conference/usenixsecurity18/presentation/eckert},
 publisher = {{USENIX} Association},
 }



Source: feedproxy.google.com
HeapHopper - A Bounded Model Checking Framework For Heap-implementations HeapHopper - A Bounded Model Checking Framework For Heap-implementations Reviewed by Anonymous on 2:12 PM Rating: 5

Tags