Tag: Z3

Practical Symbolic Execution and SATisfiability Module Theories (SMT) 101

~ hucktech ~ Leave a comment

https://twitter.com/fdiskyou/status/998133894351343616

Practical Symbolic Execution and SATisfiability Module Theories (SMT) 101

May 19, 2018 • By rui

Finding bugs is hard, reverse engineering is hard. Constraint solvers are the heart of many program analysis techniques, and can aid Fuzzing, and software verification.

This post contains a few hands-on experiments with Z3, a high performance theorem prover developed at Microsoft Research by Leonardo de Moura and Nikolaj Bjorner. With KLEE, a Symbolic Execution Engine built on top of the LLVM compiler infrastructure developed by Cristian Cadar, Daniel Dunbar, and Dawson Engler. And, angr, a binary analysis framework developed by the Computer Security Lab at UC Santa Barbara and their associated CTF team, Shellphish.[…]

http://deniable.org/reversing/symbolic-execution

 

BootStomp: Android bootloader vulnerability finder

~ hucktech ~ Leave a comment

BootStomp is a boot-loader bug finder. It looks for two different class of bugs: memory corruption and state storage vulnerabilities. For more info please refer to the BootStomp paper. To run BootStomp’s analyses, please read the following instructions. Note that BootStomp works with boot-loaders compiled for ARM architectures (32 and 64 bits both) and that results might slightly vary depending on angr and Z3’s versions. This is because of the time angr takes to analyze basic blocks and to Z3’s expression concretization results.[…]

https://seclab.cs.ucsb.edu/academic/publishing/#bootstomp-security-bootloaders-mobile-devices-2017

https://github.com/ucsb-seclab/BootStomp/blob/master/tools/huawei_tools/oeminfo_exploit.py

https://github.com/ucsb-seclab/BootStomp

print “[!] Usage: “ + sys.argv[0] + “ <oeminfo.img> <exploit_oeminfo.img>\n“

Lots of links to read at the end of the github readme web page.