Assignment 2 - SVF-tools/Software-Security-Analysis GitHub Wiki

Assignment-2 folder layout

../Assignment-2
|-- CPP
|   |-- Assignment-2.cpp
|   |-- Assignment-2.h
|   |-- CMakeLists.txt
|   |-- Z3SSEMgr.cpp
|   |-- Z3SSEMgr.h
|   `-- test-sse.cpp
|-- Python
|   |-- Ass2_helper.py
|   |-- Assignment2.py
|   |-- CMakeLists.txt
|   |-- Main.py
|   `-- Test.py
`-- Tests
    `-- testcases
        `-- sse
            |-- test1.c
            |-- test1.ll
            |-- test2.c
            |-- test2.ll
            |-- test3.c
            `-- test3.ll

1. Get the latest code template

Before coding, update your local repository:

cd "$HOME/Software-Security-Analysis"
git pull

if you use pysvf, update pysvf

pip install pysvf -U  # or: pip install -U pysvf --force-reinstall

Make sure to switch your program to ass2 before coding.

2. Assignment 2 task

- Implement the following methods of class SSE in Assignment_2.cpp or Assignment_2.py

Method	Description
SSE::reachability	Control-flow reachability analysis starting from the entry (GlobalICFGNode) of the program. More here
SSE::collectAndTranslatePath	Collect each program path from the entry to each assertion of the program. More here
SSE::handleCall	Translate callPE in a context-sensitive manner
SSE::handleRet	Translate retPE in a context-sensitive manner
SSE::handleBranch	Translate branch intraICFGEdge and evaluate the branch condition and return true if the branch evaluated is feasible, otherwise infeasible
SSE::handleNonBranch	Translate AddrStmt, CopyStmt, LoadStmt, StoreStmt, GepStmt, CmpStmt into constraints

SSE::reachability

The method differs from Assignment-1 only in the first argument which is ICFGEdge* rather than ICFGNode*.

Ensure the algorithm terminates on recursive programs. Recursion can be handled in two ways: either treat a call to an already active function as a recursive back edge and stop expanding it, or allow recursive calls to unfold up to a fixed bound (K). The first approach explores each recursion at most once per DFS call chain, similar to loop handling in Assignment 1, while the second provides more path coverage but still guarantees termination. The first approach suffices for our internal marking.

Non-recursive call chains should still be traversed context-sensitively without bounding.

SSE::collectAndTranslatePath

In this function, you will need to:

1. Add each path into the paths set
2. Call translatePath to convert each path into Z3 expressions. Note that translatePath returns true if the path is feasible, infeasible otherwise.
3. Each branch edge on a path must be evaluated to determine its feasibility. If a branch is infeasible, the translation can terminate early; otherwise, the corresponding branch condition should be added to the solver. During ICFG reachability analysis, remember to remove the branch-condition constraints from the solver when backtracking to explore another path.
4. If a path is feasible, you will need to call assertchecking to verify the assertion (which is the last ICFGNode of this path).

Run Tests

For C++, you can refer to this section
For Python, you can refer to this section

Submitting Your Work

For C++, you can refer to this section
For Python, you can refer to this section

3. Configuration, Debug and visualize ICFG

For C++, you can refer to this section
For Python, you can refer to this section