Mini KINT

Implementing the essential functionalities of KINT (OSDI'12) using LLVM-14.

Quick Start

mkdir -p build && cd build
# Recommend to remove VSCode's C++ plugin and use its ClangD plugin.
cmake .. -DCMAKE_BUILD_TYPE=Debug -DCMAKE_EXPORT_COMPILE_COMMANDS=1

Run Test

Run unit test and get raw output of LLVM-lit:

cd build
make check

Run unit test and get analysis of the test result:

cd build
make check &> test.log
LOG=test.log python3 ../tests/statistics.py

Add your own test cases:

Put your c code test file under tests/manual and add following comments in the header of the new test file to trigger automatic testing.

// RUN: clang-14 -O0 -Xclang -disable-O0-optnone -emit-llvm -S %s -o %t.ll
// RUN: opt-14 -load-pass-plugin=%builddir/mkint/MiniKintPass.so -passes=mkint-pass -S %t.ll -o %t.out.ll

// RUN: BEFORE=%t.ll AFTER=%t.out.ll python3 %testdir/llvm_lite.py TestMKint.test_IR_correct
// RUN: BEFORE=%t.ll AFTER=%t.out.ll python3 %testdir/llvm_lite.py TestMKint.test_i_annoted

Then use the same commands used in running unit tests.

Worklist

• (Basic::Logger) add logger library for debugging and checking;
• (Basic::Z3) integrate Z3 environment in CMake;
• (Feature::TaintAnalysis) Taint/sink annotation and broadcasting (WIP)
  • Taint source and sink mark;
  • Taint broadcasting;
• Per-function range analysis;
  • Backedge analysis;
  • Binary operator;
  • Branch handling;
  • Unary operator;
  • Casting (if have time);
• Cross-function range analysis;
• Constraint solving;
• Error type marking;

Bound checking

Consider the following cases for all integer expressions.

• overflow: observe if expr > MAXLIM or expr < MINLIM;
• div-by-zero: observe if div(x, y) that y == 0;
• shift: observe if shift(a, b) that b >= nbits;
• array index: observe if arr[idx] that idx < 0;
• impossible branch: e.g., ask a uint to be smaller than 0;

Use SMT solver to determine if these are possible and mark plausible ones (the solution must be related to observable variables).

Range analysis (interval analysis)

Find out observable variables outside of current functions:

• Function arguments;
• Function return value;
• Global variables;
• Range of observable variables for each block.

Analyze their ranges and apply it in eventual solving.

Taint Analysis

Is this bug related to untrusted input.

• Taint sources: arguments of functions whose names start with sys_ or __mkint_ann_.
• Sinks: kmalloc:0, kzalloc:0, vmalloc:0, etc.

Known Issues

(M1-LLVM-13-Homebrew) For LLVM-13 installed from Homebrew M1 Monterey stable, the program will crash on ConstantRange::extendSigned but it is fine on Linux machines. This looks like a LLVM bug.