SMT

Satisfiability Modulo Theories

Satisfiability modulo theories is the body of math that enables manticore to answer questions about program state. Some examples of when SMT is leveraged by Manticore include

• When branching, deciding if a given branch can be taken.
• When adding integers together, deciding if an integer overflow is possible
• When executing a transaction, deciding if the contract is capable of receiving payment (caller has less value than they started with).

Z3

Z3 is the SMT solver leveraged by Manticore. Z3 takes problems described in terms of smtlibv2 formula and returns SAT, UNSAT or UNKNOWN. SAT indicates that assignments for all variables were found that makes the formula evaluate to true. When a satisfying assignment is discovered by Z3 it produces a "model" containing all assignments. If satisfying assignments isn't possible z3 returns UNSAT. In certain circumstances Z3 may also give up and return UNKNOWN. For the work being done by Manticore, UNKNOWN is a rare result however, be aware undecidable problems do exist.

smtlibv2

Smtlibv2 is a standardized way to describe SMT problems to SMT solvers. It can be very challenging to read. Smtlibv2 expressions are composed of prefix s-expressions where

SAT

(declare-fun a () (_ BitVec 32))
(assert (bvsgt a #x0000000a))

(bvsgt is shorthand for BitVector Signed Greater Than.)

This formula asks the question, for a given 32 bit signed integer a, can it have a value greater than 0xa(10). Z3 says SAT and returns the model:

(model
  (define-fun a () (_ BitVec 32)
    #x0000000b)
)

Which is an assignment to a of 11 that satisfies the constraint that a must be greater than 10.

UNSAT

1: (declare-fun a () (_ BitVec 32))
2: (assert (= a #x00000001))
3: (assert (= a #x00000002))

1. A symbolic variable a is created representing a 32 bit quantity.
2. A constraint is added such that a must be equal to 1
3. A constraint is added such that a must be equal to 2

No satisfying assignment can exist because a 32 bit quantity can not simultaneously be equal to 1 and 2. This formula is UNSAT.

Making UNSAT useful

The UNSAT result is often exactly what you want your formula to evaluate to. It's typically how you will "prove" there are no bad states. Using Manticore you will ask for satisfying assignments that would violate a desirable property. If Manticore returns UNSAT you have a mathematical guarantee of your property holding true.

Consider the following example where we prove a quality of two's complement integers.

(declare-fun a () (_ BitVec 32))
(assert
  (=
    (=
      (bvneg a)
      (bvadd (bvnot a) #x00000001)
    )
    false
  )
)
(check-sat)

The property being validated is that a number's negative, is equal to its binary negation plus 1 or ( -a == ~a + 1 ).

The way we prove this fact is by asking for an assignment that makes this expression false or ( -a == ~a + 1 )==false. If no such assignment can be made ( ie, z3 returns UNSAT), it means that for all 32 bit integers, ( -a == ~a + 1 ) holds.

SMT in Manticore

If you want to manually inspect the SMT formula produced by Manticore you can find it in the mcore_* directories inside files ending in .constraints. Like the examples in this document the .constraints contain two types of statement, declare-fun which is the declaration of a variable or result of a calculation and assert which imposes a constraint on the solver. When you use Manticore to check for specific software behaviors you'll in effect be adding asserts.