MiniKLEE Development Plan

[xuruiyang2002]

We propose to build a toy symbolic executor for teaching purpose.

Objective

Currently there are two types of symbolic execution:

• Concolic Testing: Starting execution with random inputs, and after execution, constructing a new path condition pc₁ using the path condition pc₀ of the current path (by negating the last condition) and solving pc₁ to get a new input I₁ to explore the new path, and repeating the process. As in CREST and DART Our current experiment is of this type.

• Execution-Generated Testing (EGT): Fork symbolic execution at each conditional branch (if both directions are feasible), maintain multiple partial paths, and coordinate their execution simultaneously. As in EXE, SPF, and KLEE. This is the type of implementation that is currently desired.

We are going to implement a toy EGT symbolic executior which currently has the following features/weakness:

• Can only analyze single-main program, just basic-block level (avoid dealing with stack frames). For example:

  
  int main() {
  int a = 1;
  int b;
  symbolic(b);
  int c = a + b; 

if (c == 1000) { bug(); } else { printf(‘Pass’) } return 0; }

- Can only Support a subset of LLVM Operations such as `Add`, `Sub`, `Alloca`, `Load`, **`Br`** _et al_, others we leave to future
- To Be Determined

[xuruiyang2002]

Build Framework Based on LLVM

• [x] Refining the miniklee toolchain
• [x] Building LLVM-based static analysis framework.

Version: dd6b3c535fd72202f720cdd2944f6380cc2b0840

[xuruiyang2002]

Model Control-flow

There are two issues to be carefully considered:

• How to model control-flow?

  • [x] PC: pointer to next instruction
  • [x] PrevPc: previous program counter
  • [x] Constraints: the path constraints collected when symbolic exploring
  • [x] Symbolic Memory Array: maintain and update status of each variables
  • [x] Stack Frame Not currently supported

• Which instruction should take into consideration?

  • [x] Load/Store
  • [x] Neg
  • [x] Add/Sub
  • [x] Br: unconditional/conditional, transfer control flow cross bacis blocks
  • [x] Ret
  • [x] Cmp
  • [x] Call (Although we don't deal with call, we should skip debug function, like this 3c8441e2fa979d549c472edddcda2c6816c05e1c)
  • [x] Ret

Now we have modeled the interpretive skeleton (at commit point c597e4300fa1161315a59c9c8ddc1c45de7c109b), next is interpreting the semantics of each instruction.

At commit c597e4300fa1161315a59c9c8ddc1c45de7c109b, miniklee could fetch and analyze each at basic block level (which means transfer control flow in main function), and return successfully.

[xuruiyang2002]

Interpret Control-flow

• [x] How to implement make symbolic? Refer to klee_make_symbolic in klee We defer it to later.
• [x] How to represent symbolic variable?: Model various llvm operations by building corresponding expression class:
  • [x] Expr: base class
  • [x] ConstantExpr
  • [x] NonConstantExpr
  • [x] AddExpr/SubExpr/MulExpr/SDivExpr/UDivExpr
  • [x] CmpExpr: Signed less/larger/equal expressions
  • [x] others like ref and ref cnt

At commit point 4cf6fc292265ce2cf2bde71d579fdff2f4ed8952, we have alreay built the basic assisted frameworks to represent and operate symbolics.

The current number of all lines (for cpp and h files) is 900+ lines

• [x] How to interpret instructions?
  • [x] Alloca/Load/Store
  • Interpret Alloca: executeAlloca: map Instruction to Expr
  • Interpret Store: executeMemoryOperation(state, isWrite = true, address, value, target = 0)
  • Interpret Load: executeMemoryOperation(state, isWrite = false, address, value = 0, target)
  • [x] Neg: No need to deal with it.
  • [x] Add/Sub
  • [x] Br: unconditional/conditional, transfer control flow cross bacis blocks
  • [x] Ret
  • [x] Cmp
  • [x] Call: no need to deal with it.

[xuruiyang2002]

Implement TinySolver

After modeling and interpreting the semantics of each instruction (c2dfc9fd2e60ad73d358fb77e8006182c34d399b), we arrive at the most exciting part: forking when branching. This means that when encountering a branch, the symbolic executor invokes a solver to solve the constraints it has collected during path exploration.

To keep things simple and reduce complexity, as well as to make development life less painful, we have decided not to integrate the Z3 solver into our toolchain. Instead, we implement a naive solver that can handle simple equations and inequalities involving only addition and subtraction.

UPDATE: So far, TinySolver has been completed, and we can use it to solve any linear equations (with only addition and subtraction).

[xuruiyang2002]

Generate Test Case and Handle Errors

With TinySolver completed (c3e2a82560d33193ad8d62afd09e83d01ee2b9c5), we can now solve linear equations involving only addition and subtraction. This marks the end of the MiniKLEE development journey.

Last but but the least thing to do: generate test case and handling errors.