Code Satisfiability

Code Satisfiability - Achievable in constrained contexts.

Code Validity - Very difficult, I haven't found much academic work that tackles that successfully.

When we want to thoroughly test code, specifically for security vulnerabilities. We have a couple of options:

There is lots of academic work being done on code satisfiability, lots of amazing work. However there appears to be duplication of implementations in the academic world.


Thesaurus check:

Dynamic Symbolic Execution Concolic Testing (Or as I liked to call it "Mixed symbolic and concrete testing")

The aim of Concolic/Dynamic... is to deal with the path explosion that comes from testing every valid state of variables in symbolic execution.


One of the key strategies, outlined well by the KATCH paper is to use a regression suite to allow you concretely execute a binary up to the vicinity of the code under test, after which you can symbolically execute. This limits the search space which helps to deal with the path explosion issue.

To take a step back to the basics of how to symbolically execute a piece of code, you can either take one of 2 approaches: Translate source code to an abstract syntax tree, then walk that to generate SMTLIB2 compliant language like Z3 or STP to execute the function symbolically.

"AST Approach"

Ideally using something like ANTLR to do the AST generation as there are ANTLR grammars available for nearly all the popular source code languages.

Or we have the option to use the abstraction of LLVM or Binary Analysis Platform (BAP), which is the most popular with the existing academic tools.</p> "bitcode Approach"

Adding in the LLVM Intermediate Representation (IR) abstraction removes the maintenance overhead of the grammar transform work, the LLVM IR is walkable similar to an AST.

References: