Parametric types, and turning a concrete interpreter to a symbolic one without modifying it

2017-04-29

TL;DR;

By making the intermediate language interpreter parametric in the type of monad, I could write a concrete interpreter, and then turn it into a fully symbolic one without modifying it.

While I am quite proud of this trick, this will certainly not be released, as it is just a toy. But keep a eye on BinCAT, which should be released soon, and really looks promising (with an IDA plugin!).

Introduction

I just spend quite a few hours in the previous weeks toying with symbolic execution and automated constraint solving for compiled programs. That was a lot of fun, and I can't deny that throwing all the constraints to the SMT solver and getting the solution of a (very simple) crackme felt like magic.

I found an extremely cute way to implement symbolic execution by completely reusing the code of a concrete interpreter, which is described at the end of this post.

As an introduction, here is a toy example for symbolic execution, using the IL I developed:

Set (Rg EAX) 0
If (EReg EBX :== 0x12345678) [Set (Rg EAX) 1] []
If (EReg ECX :== 0xabcde)    [Set (Rg EAX) (EReg EAX :+ 1)] []

In this case, the EAX register will only be equal to 2 if EBX == 0x12345678 and ECX == 0xabcde when the program starts. I wrote a toy symbolic execution engine that converts such problems to a set of constraints that is then fed to an SMT solver.

How it works is approximately:

Decode a binary program into a set of instructions
Write a function that describe the semantics of each instruction, using an intermediate language (IL)
Write an interpreter for this IL, that is able to collect constraints as it runs through the program
Find the desired end-state of your program, along with the related constraints, and try to solve them!

Intermediate representation

In order to get started, I had to define an intermediate representation (IL), which is a language that is used to describe the semantics of individual instructions. A well known language is REIL, but I really don't like how it is designed, especially with regards to its imperative feeling.

For example, here is how they define mov ah, al:

00000000.00     AND         R_EAX:32,             ff:8,           V_00:8
00000000.01     AND         R_EAX:32,      ffff00ff:32,          V_01:32
00000000.02      OR           V_00:8,             0:32,          V_02:32
00000000.03     SHL          V_02:32,             8:32,          V_03:32
00000000.04      OR          V_01:32,          V_03:32,         R_EAX:32

Note how temporary registers are created to hold the result of each step of computation. With my IR, which is heavily borrowed from BinCAT, it looks like:

Set (Rg EAX)
  ( EReg EAX :& 0xffff00ff :| ( (EReg EAX :<< Constant 8) :& 0xff00 ) )

The statements of the IL are listed here:

data Statement arch where
    Set    :: Extend width (RegType arch) => Lval arch width -> Expr arch width -> Statement arch
    If     :: Expr arch Bool -> [Statement arch] -> [Statement arch] -> Statement arch
    Jmp    :: Expr arch (RegType arch) -> SegmentType arch -> Statement arch
    Call   :: Expr arch (RegType arch) -> SegmentType arch -> Statement arch
    Return :: Statement arch
    Nop    :: Statement arch
    Halt   :: Statement arch
    Debug  :: String -> Statement arch -> Statement arch

As for the Expr arch a data type, I went for a large GADT. Most examples I have seen are very weakly typed, where all the values are unsigned words of some width. For this reason, they require specific IMUL, IDIV and IMOD instructions for signed operations.

I decided to go full GADTs, with stuff like:

data Expr arch a where
  (:+)     :: Num a
           => Expr arch a -> Expr arch a -> Expr arch a
  (:*)     :: Num a
           => Expr arch a -> Expr arch a -> Expr arch a
  (:/)     :: (Integral a, SDivisible (SBV a))
           => Expr arch a -> Expr arch a -> Expr arch a
  (:>)     :: (SymWord a, Integral a)
           => Expr arch a -> Expr arch a -> Expr arch Bool
  ...

And a typeclass-based explicit type conversion system:

  SignExt    :: (Extend a b, Integral a)        => Expr arch a -> Expr arch b
  ZeroExt    :: (Extend a b, Integral a)        => Expr arch a -> Expr arch b
  Truncate   :: (Truncate a b, Integral a)      => Expr arch a -> Expr arch b
  ToSigned   :: (Signop a, Integral a)          => Expr arch a -> Expr arch (Signed a)
  FromSigned :: (Signop a, Integral (Signed a)) => Expr arch (Signed a) -> Expr arch a

For example, here is the translation of the EBPF LsAbsB rg imm instructions, which loads a packet byte into a 64bit register:

let byte :: Expr EBPF Word8
    byte = Addr ( ZeroExt (Constant (Resolved imm)) ) Packet
in  Set (Rg rg) (ZeroExt byte)

Not how the size of the memory access is defined by its type, and so is everything else. This is however not all roses here, as the following prevents a proper Eq instance:

    (:>)     :: (SymWord a, Integral a) => Expr arch a -> Expr arch a -> Expr arch Bool

There is no way to write it:

instance Eq a => Eq (Expr arch a) where
   a == b = case (a,b) of
              (x1 :+ y1, x2 :+ y2) -> x1 == x2 && y1 == y2 -- OK
              (x1 :> y1, x2 :> y2) -> -- can't write an implementation! The types of x1 and x2 are not known to be identical :(

That might be solved by writing specific versions of the comparison operators, such as:

    GT8  :: Expr arch Word8  -> Expr arch Word8  -> Expr arch Bool
    GT16 :: Expr arch Word16 -> Expr arch Word16 -> Expr arch Bool
    GT32 :: Expr arch Word32 -> Expr arch Word32 -> Expr arch Bool
    GT64 :: Expr arch Word64 -> Expr arch Word64 -> Expr arch Bool

But it is clearly not very elegant ...

Interpreting the IL

I decided to have the following milestones when interpreting the IL:

A basic interpreter for concrete programs and memory. That means that the while program state is known when the program starts, and it is possible to explore that way a single possible execution path.
An interactive interpreter, that would work a bit like a debugger. This proved useful, not to debug the analyzed program, but my own program ;)
Symbolic values, introduced in place of the concrete ones. The interpreter should work as before.
Start abstracting some program state, and have the debugger interactively ask the user how to translate symbolic expressions into concrete values.
Finally, run all possible execution paths, collecting constraints.

Step 1 - concrete values

There isn't much to say about this. The following data structures are required in order to emulate a program:

The EmulInfo arch structure holds data such as which register is the instruction pointer, how to handle a jump, etc.
The AState arch structure holds the program state, that is registers and memory.

Once this was done, it was trivial to write an interpreter for the IL. I also wrote enough support for the EBPF architecture in order to solve one of the SSTIC 2017 challenge steps.

Step 2 - interactive interpreter

I used haskeline with optparse-applicative. The latter is kind of well suited for the task of defining commands and parsing parameters, even though the help text really looks too much like that of a command line utility. I still have to integrate tab-completion.

Step 3 - symbolic values

This is how my symbolic value type looks like:

data MemR arch a
  = Unresolved (Expr arch a)
  | Resolved a
  | Unk (SegmentType arch) (RegType arch)

So a symbolic value of type a can either be:

an arbitrary expression of type Expr arch a
a known, concrete value of type a
a reference to a memory address, representing an unknown zone of memory at program start

For now, all registers hold concrete values when the program starts, so the UnkReg constructor is not necessary. Now that values can be unresolved, the expression evaluation function can't have the following type:

evalExpression :: ...  => Expr arch a -> m a

The actual type becomes:

evalExpression :: ...  => Expr arch a -> Eval arch (Either (Expr arch a) a)

This means this can return either a fully evaluated value, or an unevaluated (but perhaps simplified) expression.

Symbolic memory was the biggest headache, as even memory reads could alter the program state! Indeed, a memory read that is 8bits wide at address 5 and another that is 32 bits wide at address 4 are related. In order to make sure this would not go unnoticed, each memory read of a new unknown memory address alters the program state so that subsequent reads could reference the same variable.

Another big pain point was having all the unaligned / endianity changing accesses right.

Step 4 - abstracting program state

This is where things get interesting, but problems start to arise. The most illustrative example is the conditional statement:

    If     :: Expr arch Bool -> [Statement arch] -> [Statement arch] -> Statement arch

The first argument represents a boolean condition. The second is the list of statement to be executed if that condition is true (the then branch), and the third if it is false (the else branch).

Unfortunately, resolving the boolean condition could result in an unevaluated expression! In order to be able to decide which branch must be executed, it must be reduced to a concrete Bool. For this reason, I made the following functions primitives of the Eval monad:

solveBool :: Expr arch Bool -> Eval arch Bool
solveAddr :: Expr arch (RegType arch) -> Eval arch (RegType arch)

(solveAddr is for jumps, so that the interpreter could determine where to go next.)

And now the If statement can be evaluated like:

evalStatement :: forall arch. (Ord (Register arch), Eq (RegType arch)) => Statement arch -> Eval arch ()
evalStatement s = do
   ...
   case s of
      If b th el -> do
          x <- evalExpression b >>= either solveBool pure
          mapM_ evalStatement $ if x then th else el
      ...

Here, the evalExpression b expression has type Eval arch (Either (Expr arch Bool) Bool)). With the help of the solveBool function, it is possible to turn the dreaded unresolved expression into a proper boolean.

But now, how to run the Eval monad?

This is the signature of the runEval function, which translates an Eval arch a expression into an arbitrary monad:

runEval :: Monad m
  => (Expr arch Bool -> m (Eval arch Bool))                     -- ^ resolving boolean choices
  -> (Expr arch (RegType arch) -> m (Eval arch (RegType arch))) -- ^ resolving addresses
  -> EmulInfo arch                                              -- ^ architecture specific data
  -> AState arch                                                -- ^ program state
  -> Eval arch a                                                -- ^ Eval action to run
  -> m ( Either (EmulError arch) (a, AState arch)
       , [EmulationTrace arch]
       )

The return result is a bit obscure at first. It includes a list of emulation traces (in particular, the state of the emulation at each instruction), and the result of the evaluation. The evaluation could fail (and return an EmulError arch), or succeed (and return the expected a, along with an updated program state).

As can be guessed, the first two arguments are used to implement the solveBool and solveAddr functions.

In the case of a simple interpreter, where all program state is know and evalExpression always returns the Right result, the following function can be used:

trivialSolve :: Monad m
             => Expr arch x
             -> m (Eval arch x)
trivialSolve e =
  return $ case e ^? _RConstant of
    Just x -> return x
    Nothing -> throwError (Misc "trivialSolve failed :(")

Note that the runEval function is parametric in the type of monad, and related to the type of the provided solveBool and solveAddr implementations.

Step 5 - actual symbolic execution

Let's look back at the introductory example:

Set (Rg EAX) 0
If (EReg EBX :== 0x12345678) [Set (Rg EAX) 1] []
If (EReg ECX :== 0xabcde)    [Set (Rg EAX) (EReg EAX :+ 1)] []

Symbolic execution would work that way:

Update the program state, setting EAX to 0.
Create two states:
- Set EAX to 1, assorted with the constraint EReg EBX :== 0x12346789, and branch again:
  - Set EAX to 2, assorted with the constraint EReg ECX :== 0xabcde.
  - Set EAX to 1, assorted with the constraint EReg ECX :!= 0xabcde.
- Set EAX to 0, assorted with the constraint EReg EBX :!= 0x12346789, and branch again:
  - Set EAX to 1, assorted with the constraint EReg ECX :== 0xabcde.
  - Set EAX to 0, assorted with the constraint EReg ECX :!= 0xabcde.

So if I am interested in the outcome where EAX is equal to 2, I should solve the following constraints set:

EReg EBX :== 0x12346789
EReg ECX :== 0xabcde

Now how to implement this without changing the interpreter? It turned out to be surprisingly easy! The branching can be handled using the list monad, and the constraint collection using the writer monad:

symbEvalBool :: Expr arch Bool -> LT.ListT (Writer [Expr arch Bool]) (Eval arch Bool)
symbEvalBool e = case e ^? _RConstant of
      Just b -> return (return b)
      Nothing ->  (lift (tell [e])     >> return (return True))
              <|> (lift (tell [Not e]) >> return (return False))

Conclusion

My toy program currently works as long as there are not too many branches. It solves the first (easy) part of the "don't let him escape" problem of the 2017 SSTIC challenge:

$ ./sstic2017-symbolicsolve
Initial packet content:
P/00000000 ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? 02 ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ??    ??????????????.?????????????????
P/00000020 ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ??    ????????????????????????????????

Symbolic exectution of all paths ...

10 possible executions

Interesting states:
  * ffffffff
    - not(zeroExt(P/0000000c,[Word16->Word64]) != 0x800)
    - not(zeroExt(P/00000017,[Word8->Word64]) != 0x11)
    - not(zeroExt(P/00000024,[Word16->Word64]) != 0x539)
    - not((zeroExt(P/00000010,[Word16->Word64]) + 0xfffffff8 - 0x8) << 32 >> 32 != 0x10)
    - not(zeroExt(P/0000001e,[Word8->Word64]) & 0xff != 0x4c)
    - not(zeroExt(P/0000001f,[Word8->Word64]) & 0xff != 0x55)
    - not(zeroExt(P/00000026,[Word32->Word64]) << 32 | zeroExt(P/0000002a,[Word32->Word64]) != 0x456443724d66417d)
    - not(zeroExt(P/00000022,[Word32->Word64]) << 32 >> 32 != 0x42765751)
    - not(zeroExt(P/00000020,[Word16->Word64]) & 0xffff != 0x4d7b)

Solution 1:
Updated packet content:
P/00000000 ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? 08 00 02 ?? 00 20 ?? ?? ?? ?? ?? 11 ?? ?? ?? ?? ?? ?? 4c 55    ????????????...?. ?????.??????LU
P/00000020 4d 7b xx xx xx xx xx xx xx xx xx xx xx 7d ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ??    M{xxxxxxxxxxx}??????????????????

Rerun, with the updated packet content, and retrieve the new EBPF map content:
map[0] = 00000001
map[1] = bd89a8ae
map[2] = ba9bbc8d

Note that the initial packet is not fully unknown, as I had to set a concrete value to a field that is used for indexed memory accesses. However, the second part of the problem involves a lot of conditional expressions, resulting is something like $2^115$ possible states.

What is amusing is that my current plan for fighting state explosion will have a direct application in the gamebook solving series. More to come soon!

Hbtvl