Uncategorized

Practical Symbolic Execution and SATisfiability Module Theories (SMT) 101

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

 

Standard

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

w

Connecting to %s