Writing a constraint-based static analysis for C programs with LLVM and Datalog.
In this lab, you will implement a constraint-based analysis to detect exploitable divide-by-zero bugs. A bug is exploitable if hackers can control inputs or environments, thereby triggering unintended behaviors (e.g., denial-of-service) through the bug. For example, a recently reported divide-by-zero bug in the Linux kernel can be exploitable and crash the system; another example was the Log4Shell incident. You will design a static analysis that detects such bugs by combining reaching definition analysis and taint analysis using a datogon engine, souffle.
The skeleton code for Lab8 is located under
We will frequently refer to the top level directory for Lab 8 as
lab8 when describing file locations for the lab. Open the
lab8 directory in VSCode following the Instructions from Course VM document
The following commands set up the lab, using the Cmake/Makefile pattern seen before.
/lab8$ mkdir build && cd build /lab8/build$ cmake .. /lab8/build$ make
The above command will generate an executable file ‘constraint’ in build directory that extracts facts about the program that will be used by
to check if the input program has an exploitable divide-by-zero bug:
/lab8$ cd ./test /lab8/test$ clang -emit-llvm -S -fno-discard-value-names -c simple0.c /lab8/test$ mkdir -p simple0/input simple0/output /lab8/test$ ../build/constraint simple0.ll ./simple0/input /lab8/test$ souffle -F ./simple0/input -D ./simple0/output ../src/analysis.d
After completing the lab implementation, you should see the instruction that could potentially cause a divide-by-zero in
In this lab, you will design a reaching definition analysis and taint analysis using datalog.
The main tasks are to design the analysis in the form of logical rules as a Datalog program, and implement a function that extracts logical relations form a test program in the form of Datalog facts for each LLVM instruction.
We will then use the datalog rules with the facts you extracted from each instruction in a program to find any exploitable divide-by-zero errors.
In short, the lab consists of the following tasks:
analysis.dlfor taint analysis.
Extractor.cppthat extracts Datalog facts from LLVM IR
Instructionand dumps them to appropriate
.factsfiles. Detailed instructions provided in comments.
The skeleton code in
Extractor.cpp provides the definitions of various functions that will help you dump the necessary Datalog relations declared in
Here we will explain what each of the datalog relation mean.
The relations for def and use of variables are as follows:
def(var, inst): Variable
varis defined at instruction
use(var, inst): Variable
varis used in instruction
The relations for the reaching definition analysis are as follows:
kill(curr_inst, old_inst): Instruction
curr_instkills definition at instruction
next(curr_inst, next_inst): Instruction
next_instis an immediate successor of instruction
in(inst, def_inst): Definition at defining instruction
def_instmay reach the program point just before instruction
out(inst, def_inst): Definition at defining instruction
def_instmay reach the program point just after instruction
Note that the
kill relation can be derived by using the
def relation by writing a Datalog rule.
The relations for the taint analysis are as follows:
taint(inst): There exists a function call at intruction
instthat reads a tainted input.
edge(from, to): There exists an immediate data-flow from instruction
Path(from, to): There exists a transitive tainted data-flow from instruction
sanitizer(inst): There exists a function call at intruction
instthat sanitizes a tainted input.
div(denom, inst): There exists a division operation at instruction inst whose divisor is variable denom.
alarm(inst): There exists a potential exploitable divide-by-zero error at instruction inst.
Assume that input programs may contain function calls to
sanitizer that read and sanitize a tainted input, respectively.
The final output relation for potential bug reports is
You will use these relations to build rules for the definition analysis and taint analysis in
Recall that, in LLVM IR, values and instructions are interchangable.
Therefore, all variables X, Y, and Z are an instance of LLVM’s
Assume that input C programs do not have pointer variables.
Therefore, we abuse pointer variables in LLVM IR as their dereference expressions.
Consider the following simplified LLVM program from a simple C program
int x = 0; int y = x;:
x = alloca i32 ; I0 y = alloca i32 ; I1 store i32 0, i32* x ; I2 a = load i32, i32* x ; I3 store i32 a, i32* y ; I4
We ignore alloca instructions and consider that each store instruction defines the second argument.
In the case of the above example, you should have
I0 corresponds to
x in LLVM IR and
I2 defines the variable
Likewise, consider each load instruction uses the argument.
In the example, you should have
addDef(I3,I3) because load instructions define a non-pointer variable which is represented as the instruction itself in LLVM.
Finally, you should have
addDef(I1,I4) for instruction
You will write your Datalog rules for taint analysis in
src/analysis.dl using the relations above.
Please refer to the souffle’s documentation for the datalog language and its syntax.
Here’s a quick example to help you get started.
Consider an example Datalog rule:
A(X, Y) :- B(X, Z), C(Z, Y).
It adds a rule which says that there is a relation
there is a relation
X and some
Z and there is also a
C between that
You will need to implement the function
Extractor.cpp to extract Datalog facts for each LLVM instruction.
The skeleton code provides a couple of auxiliary functions in
lab8/src/Utils.cpp help you with this task:
void addX(const InstMapTy &InstMap, ...)
Xdenotes the name of a relation. These functions add a fact to the facts file for
InstMapthat encodes each LLVM instruction as an integer. This map is initialized in the
vector<Instruction*> getPredecessors(Instruction *I)
bool isTaintedInput(CallInst *CI)
CIreads a tainted input or not.
bool isSanitizer(CallInst *CI)
CIsanitizes a tainted input or not.
For debugging, after you run
constraint you can inspect the
./test/simple0/input for files containing the extracted relations.
Input programs in this lab are assumed to have only sub-features of the C language as follows:
sanitizerin a special way which represents their actions as described previously.
Your analyzer should run on LLVM IR. For example:
/lab8$ cd ./test /lab8/test$ make loop0
If the input program has exploitable divide-by-zero errors, then you should see entries in
Once you are done with the lab, you can create a
submission.zip file by using the following command:
lab8$ make submit ... submission.zip created successfully.