Program Analysis with Satisfiability Modulo Theories (SMT) Solvers for Bug Hunters - Part 1

software-verification
debugging
sast
coding
offdev
smt
code-reviews
Tags: #<Tag:0x00007f389e4a2df0> #<Tag:0x00007f389e4a2cb0> #<Tag:0x00007f389e4a2b70> #<Tag:0x00007f389e4a2a30> #<Tag:0x00007f389e4a28f0> #<Tag:0x00007f389e4a27b0> #<Tag:0x00007f389e4a2670>

#1

This is part 1 of a blog series about Program Analysis with Satisfiability Modulo Theories (SMT) Solvers for Bug Hunters.


I took a class in Advanced Tool Development with SMT Solvers with Sean (Vertex.re) in London. Here is a little revue as a preface for some of the future posts on this blog.

My interest in program verification with SMT solvers started in 2012ish. - For bug hunting purposes. Many of the modern approaches appear practical, and some even claim to support automated exploit development… I was at Defcon in 2016, when they had the Cyber Grand Challenge (CGC).

My takeaway is, that some level of assistance should be practical, even on my hobbyist’s scale, and that SMT solvers and other formal methods can provide that.


Program Analysis with Satisfiability Modulo Theories (SMT) Solvers for Bug Hunters

Boolean SAT example.

##Summary:

Motivation

This little post may help to understand KLEE {1}, angr {2}, manticore {3} and other projects. I think a mid-term effect of these approaches becoming OpenSource and part of a larger discussion will be, that we are going to see more debugging extensions and IDEs with helpful features to support development with a perspective driven by program analysis.

At the moment I’d comfortably place the topic in between applied research and software engineering. In the following I’ll have a focus on software security applications.

References

{1} KLEE is useful to execute program code symbolically and to explore the state space practically
{2} angr is a CTF-driven development, focused on binary analysis with symbolic execution and SMT solvers
{3} manticore is an OpenSource project, which may aim to become a concrete symbolic (concolic) execution engine for bug hunting purposes

Terminology

Each field has its own way to use certain terms. Here are my short definitions in plain English.

Symbolic?

The term “symbolic” as it is common in program analysis may be used to define objects, that represent one or more concrete values.

Symbolic Execution / SymEx

The key idea has also been formulated by James C. King, CACM 1976. A Symbolic Executor executes a program, tracking the Symbol State. If the execution path depends on an unknown constraint, we fork the executor; ideally.

Ideally in symbolic execution the program can take any feasible path.

During symbolic execution, the program state consists of symbolic values; for some memory locations.

Path Condition

During symbolic execution we aim to determine if certain forumlae are satisfiable (SAT).

For example: is a particular program point reachable? If you have used IDA Pro and performed basic block coverage with the Debugger, you have dynamically solved a reach-ability problem.

What if you could just ask a model of the program, not execute the program at all, and archive the same answer? In a more complete way, because even if you have an advanced fuzzer, like AFL, you may still need to execute a lot of test cases to have a reasonably complete measurement of the path-conditions and how they affect the given reach-ability problem.

The idea is to use a powerful SMT / SAT solver to generate the input from a Model instead. SAT stands for SATisfiability. SMT stands for Satisfiability Modulo Theories, as in ($SAT)^2$.

SMT

An SMT instance is a formula that extends the Boolean SAT logics (see the motivation picture) with operators and data-types. Like fixed-size bit-vectors, arithmetic, linear and real scalar types, recursive data-types, tuples… lambda expressions, dependent types…

SMT Solvers like Z3 {1} or STP {2} have a lot of features to reason about semantics of a program effectively. We “just” need to build Models.

References

{1} Microsoft Z3 on GitHub
{2} STP constaint solver

SMTLIB Models

SMTLIB is an expression language, similar to LISP. It can be used to build Models, which can be explored via SMT solvers.

In the training there was an exercise to model 2 basic x86 assembly instructions in SMTLIB to find out what is in eax afterwards:

add eax, ebx
add eax, ecx

A naive model could look like this (of course I would never… :slight_smile: ):

Program Bad Model
add eax, ebx (= eax (bvadd eax ebx))
add eax, ecx (= eax (bvadd eax ecx))

At least the (s look like LISP, so that point is covered.

In Models we use each variable only once. eax is reused. Bad. But if we just rename them the two expressions aren’t related. We are looking for the result of eax afterwards. So… both expressions need to be True; we need to AND them.

Program Model
(and
add eax, ebx (= eax1 (bvadd eax_in ebx_in))
add eax, ecx (= eax2 (bvadd eax1 ecx_in))
)

The _in suffix indicates that the variable gets input from the outside.

In SMTLIB you need to set the logic type etc. I recommend that you check out the version 2 of the standard {1}. For bug hunting we usually use QF_BV, because we need Bitvector extraction when we are dealing with x86 register addressing (EAX, AX, AH, AL)

References

{1} SMTLIB standard reference

Programming a Model

Modern SMT solvers have APIs, so that you can use Java, C, Python etc. to express the Models. Here is an example snippet with Python 2.7 and Z3.

import z3

x_int =  z3.Int('x')
y_int = z3.Int('y')
eax_bitv = z3.BitVec('eax1', 32)
z3.solve(x + y < 10)

The usual and more structured approach is to use z3.Solver() as an object, and to add the variables one by one. The issue is, that there will be many variables.

Binary Translation

In order to automatically build and extract Models, binary translations to Intermediate Languages (ILs) are common.

manitcore does not use an IL or IR, in order to remain simpler.

mcsema: x86 -> LLVM IL

mcsema {1} looks like an interesting project, that can help to translate arbitrary x86 (for example) binaries to LLVM IL. I requires IDA Pro or Binary Ninja as a disassembler.
Latter seems to have its own IL, but you cannot access the API headlessly without an enterprise license. Due to this (and many other artificial Binary Ninja hoops you have to jump through) I recommend to stick to IDA Pro in general, for the time being.

OpenREIL

OpenREIL {2} uses a variant of the REIL IL, and the Capstone framework.

The overall problem with REIL in opposite to LLVM is, that the code gets very long. For Abstract Interpretation this can be okay, because you evaluate the IL automatically with a parser. Due to this you want a simple expression, so that your parser grammar is easy to handle.

angr's PyVex

VEX is an IL, which has been created for Valgrind. angr has a Python binding {3} for VEX, which may be suitable for modeling. VEX-like ILs have also been used by projects, such as Bitblaze.

References

{1} mcsema framework for lifting x86, amd64, and aarch64 program binaries to LLVM bitcode

{2} OpenREIL is open source library that implements translator and tools for REIL (Reverse Engineering Intermediate Language)

{3} PyVex exposes Valgrind’s VEX to Python

Revue

Although I put some emphasis on reverse engineering and bug hunting here, it seems to be possible to do Whitebox Fuzzing in the form of concrete symbolic (concolic) execution. Approaches like this have helped Microsoft’s secure coding initiatives. Much more than Static Application Security Testing (SAST).

Static Code Analysis often confuses developers, because 80% of the indicated bugs can be False Positives.
Abstraction, in SAST, can let us scale and model all possible runs of a program, but due to limited resources we have to balance precision and scalability. Many parts of a program can be data-flow sensitive, context-sensitive, path-sensitive, resource-sensitive, timing-sensitive… Often there is a mismatch between developer expectations and SAST tool performance, due to this.

Whitebox Fuzzing and Concolic Testing may be a better fit, because testing is common in Agile (Build, Test, Release, Deploy) cycles. If bugs get detected during testing, they can be concretely investigated. Of course the problem with testing here is, that the exploration needs to be balanced with the resource constraints.

In the near future I hope to get a build of mcsema to be able to generate specific models for certain functions. :wink: But building some of these tools isn’t straight forward. OpenREIL has a WinDBG extension, which looks interesting. Before these aspects are relevant, some of my personal hands-on examples need to find their way into some blog posts.