41128 - Summary

1. Introduction to Software Analysis and Verification

1.1 Main question and Purpose

Week 1 - 3

Purpose

• Main question
  • Why do we need software analysis?
• Large programs can contain problems such as:
  • memory leaks
  • buffer overflows
  • uninitialised variables
  • use-after-free errors
  • security vulnerabilities
• It is difficult for developers to manually examine every possible path in a program containing thousands or millions of lines.
• Software analysis therefore uses algorithms and tools to automatically reason about program behaviour.

1.2 Static analysis versus dynamic analysis

Static analysis	Dynamic analysis
Examines code without running it	Examines the program while it runs
Attempts to consider all possible paths	Only observes paths executed by the test inputs
Can find problems before deployment	Finds problems that actually occur during execution
May produce false alarms	May miss untested problems
Used heavily in this subject	Examples include testing, fuzzing and sanitizers

• A helpful way to remember this:
  • Static: “What might happen?”
  • Dynamic: “What happened during this execution?”

1.3 Software analysis versus software verification

• The slides distinguish them by their goal:
  • Software analysis: tries to find whether a bug may exist.
  • Software verification: tries to prove that a program satisfies its specification and that certain bugs cannot occur.

For example:

assert(x > 0);

The assertion is a small specification saying:

“Whenever execution reaches this line, x must be greater than zero.”

A static verification tool attempts to determine whether this assertion can ever fail without actually running the program.

The two larger subject projects

Project 1: Static taint checker

It tracks untrusted information from a source to a sink.

It needs:

1. C/C++ programming
2. LLVM IR
3. graph representations
4. control-flow analysis
5. data-flow analysis
6. taint-path detection and visualisation

Project 2: Static symbolic execution

It reasons about possible values and program conditions to determine whether assertions can fail.

It needs:

1. LLVM IR and code graphs
2. control-flow reachability
3. constraint generation
4. a constraint or assertion solver

---

2. LLVM and SVF

Purpose of 2A and 2B

Purpose 2A

• Main question
  • How can an analysis tool understand C or C++ code consistently?
  • Directly analysing source code is difficult because source languages contain many complicated constructs.
  • Therefore, Clang translates C/C++ into a simpler, standard representation called LLVM Intermediate Representation, or LLVM IR.

Purpose 2B

• Main question
  • How do we turn LLVM instructions into structures that analysis algorithms can easily use?
• LLVM IR is more manageable than C++, but it still contains many instruction types and compiler details.
• SVF provides another abstraction called SVFIR:

LLVM IR → SVFIR → code graphs → analysis algorithms

• SVFIR is built from LLVM IR. It does not independently replace LLVM IR.

2A. LLVM Compiler and LLVM IR

What is LLVM IR?

LLVM IR is:

lower-level than C/C++ higher-level than machine code strongly typed language-independent structured into modules, functions, basic blocks and instructions designed to support compiler optimisation and program analysis

For example, a source-code expression:

a = b + c * d;

might be separated into simpler instructions:

t = c * d
a = b + t

Each instruction performs a small operation. That makes relationships between values easier for an analysis tool to follow.

Static Single Assignment — SSA

LLVM IR generally uses Static Single Assignment form.

It means each LLVM variable is assigned only once.

Normal code:

x = 1;
x = x + 2;

SSA-style representation:

x1 = 1
x2 = x1 + 2

LLVM IR Scopes and Identifier

1. LLVM IR structure and scopes

Module
├── Global variables
└── Functions
    ├── Arguments
    └── Basic blocks
        └── Instructions

---

• Module
  • A module represents one complete LLVM IR file or compilation unit.
  • It contains:
    • Global variables
    • Function definitions
    • Function declarations

Example

@counter = global i32 0

define i32 @main() {
    ret i32 0
}

Here, @counter and @main belong to the module.

---

• Function
  • A function contains:
    • Function parameters
    • One or more basic blocks
    • Local identifiers used by its instructions

define i32 @add(i32 %x, i32 %y) {
entry:
    %result = add i32 %x, %y
    ret i32 %result
}

• In this example:
  • @add is the function.
  • %x and %y are arguments.
  • entry is a basic block.
  • %result is a local identifier.

---

• Basic block
  • A basic block is a continuous sequence of instructions.
  • A basic block:
    • Has one entry point
    • Runs instructions from top to bottom
    • Ends with a terminating instruction such as ret, br, or switch

entry:
    %result = add i32 %x, %y
    ret i32 %result

• Both instructions belong to the entry block.

2. LLVM identifiers: @ versus %

• LLVM uses prefixes to show the scope of an identifier.

Prefix	Meaning	Scope	Examples
@	Global identifier	Entire module	@main, @swap, @counter
%	Local identifier	Current function	%a, %b, %result
No prefix with :	Basic-block label	Current function	entry:, if.then:

---

• Global identifiers: @
  • Functions and global variables normally use @.

@number = global i32 10

define i32 @main() {
    ret i32 0
}

• @number is a global variable.
• @main is a global function name. They can be referenced from other functions in the module.

---

• Local identifiers: %
  • Function parameters and instruction results use %.

define i32 @double(i32 %value) {
entry:
    %result = mul i32 %value, 2
    ret i32 %result
}

• %value and %result only exist inside @double.
• Another function may also have a %result; this is allowed because each function has its own local scope.

Common LLVM IR instructions

• You do not need to memorise the entire LLVM language, but you should recognise: | LLVM instruction | Simplified meaning | | ---------------- | ------------------------------------------------- | | alloca | Create stack storage | | load | Read from memory | | store | Write to memory | | call | Call a function | | ret | Return from a function | | br | Branch to another basic block | | icmp | Compare integer values | | phi | Combine values arriving from different paths | | getelementptr | Calculate the address of a field or array element |

2B. SVFIR and Code Graphs

Main question and What is SVFIR?

Main question

• Main question
  • How do we turn LLVM instructions into structures that analysis algorithms can easily use?
• LLVM IR is more manageable than C++, but it still contains many instruction types and compiler details.
• SVF provides another abstraction called SVFIR:

LLVM IR → SVFIR → code graphs → analysis algorithms

• SVFIR is built from LLVM IR. It does not independently replace LLVM IR.

What is SVFIR?

SVFIR = SVFValue + SVFVar + SVFStmt + Code Graphs

• In simpler language:
  • SVFValue: wrapper around an LLVM value
  • SVFVar: a program variable or memory object
  • SVFStmt: a relationship or operation between variables
  • Code graph: puts those items into a graph that an algorithm can traverse
• SVFIR simplifies complicated LLVM operations into a smaller number of analysis-friendly statements.

Important SVF statements

SVF statement	Simplified meaning
AddrStmt	p = &object
CopyStmt	p = q
LoadStmt	p = *q
StoreStmt	*p = q
GepStmt	Address of an array element or structure field
PhiStmt	Value comes from one of several paths
BranchStmt	Conditional control flow
CallPE	Pass actual arguments into function parameters
RetPE	Pass a returned value back to the caller

The three most important graphs: "Call Graph", "Control-Flow Graph and ICFG", "Program Assignment Graph — PAG"

1. Call Graph

A call graph provides a function-level view.

• Node = function
• Edge = one function may call another

---

• It answers:
  • “Which functions can call which other functions?”
• It does not show every statement inside the functions.

2. Control-Flow Graph and ICFG

• A CFG describes the possible execution order of statements inside one function.
• An Interprocedural Control-Flow Graph, or ICFG, connects control flow across functions.
  • Node = instruction or statement
  • Edge = possible next execution step
• It answers:
  • “Can execution move from statement A to statement B?”

The ICFG is the graph used in Week 3.

3. Program Assignment Graph — PAG

• The PAG represents relationships between variables and memory objects.
  • Node = variable or memory object
  • Edge = assignment, load, store, address relationship, etc.
• It helps answer:
  • “How can a value move from one variable or memory location to another?”

The PAG becomes particularly important for data-flow and pointer analysis.

---

3. Control Flow and Interprocedural Analysis

3.1 Main question and Purpose

Purpose

• Main question
  • Where can program execution go?
• Before analysing data, we need the possible execution paths through a program.

3.2 Control Flow Graph (CFG)

A CFG represents possible execution paths inside one function.

• Node = instruction or basic block
• Edge = possible execution transition

For example:

if (x > 0)
    y = 10;
else
    y = 20;

print(y);

3.3 Intra-procedural versus interprocedural analysis

Intra-procedural	Interprocedural
Stays inside one function	Crosses function boundaries
Uses a CFG	Needs a call graph and an ICFG
Enough for local control flow	Needed for real programs that call other functions

Intra-procedural

Interprocedural

3.4 Call Graph

A call graph shows which functions may call other functions. Week 2B already introduces it as the function-level view. Week 3 uses it for interprocedural analysis.

It answers:

• “Which functions can call which other functions?”

For example:

main() {
    foo();
}

foo() {
    bar();
}

Indirect calls

Sometimes the target is not obvious:

fp();

If pointer analysis determines pts(fp) = {foo, bar}, the possible call targets are:

3.5 ICFG

ICFG = Interprocedural Control Flow Graph.

It extends control-flow analysis across functions.

main() {
    foo();
}

Important SVF ICFG nodes:

Node	Purpose
FunEntryICFGNode	Function entry
FunExitICFGNode	Function exit
CallICFGNode	Function call
RetICFGNode	Return site
IntraICFGNode	Normal instruction

• Key takeaway
  • CFG → control flow inside a function
  • Call graph → relationships between functions
  • ICFG → detailed control flow across functions

---

4. Data Dependence and Pointer Analysis

4.1 Main question and Purpose

Purpose

• Main question
  • Where can data go?
• Week 3 asked where execution can go. Week 4 asks how values move, especially through pointers and memory.

For example:

x = 10;
y = x;

There is a data dependence because y uses the value defined by x:

4.2 Why pointers make data dependence difficult

*p = 50;
x = *q;

Does x depend on the first statement? We do not know until we know whether p and q could point to the same memory.

If p and q both point to A:

then the store through p can affect the load through q, so there is a possible data dependence.

4.3 Pointer basics

int a = 10;
int *p = &a;

Expression	Meaning
a	value of a
&a	address of a
p	address stored in p
*p	value at the address p points to

• Therefore:
  • a and *p are values
  • &a and p are addresses

4.4 The four important pointer operations

Code	Operation	Meaning
p = &a	Address	p points to a
q = p	Copy	copy address from p to q
q = *p	Load	read the value or pointer stored through p
*p = q	Store	write a value or pointer through p

• Easy memory rule
  • p = &a → address
  • q = p → copy address
  • q = *p → read / load
  • *p = q → write / store

q = p versus q = *p

int a = 10;
int *p = &a;

Copy copies the address:

int *q = p;

Both p and q point to a.

Load copies the value:

int q = *p;

So:

• q = p → copy address
• q = *p → read value

Store

int a = 10;
int *p = &a;
int q = 50;

*p = q;

Because p points to a, *p = q means a = q.

• Before: p → a = 10, q = 50
• After: p → a = 50, q = 50

4.5 Points-to sets and alias analysis

A points-to set contains the possible memory objects a pointer may reference.

• pts(p) = {a} means p may point to a.
• pts(p) = {a, b} means p may point to a or b.

Two pointers may alias if they may reference the same memory object.

If:

• pts(p) = {A, B}
• pts(q) = {B, C}

then pts(p) ∩ pts(q) = {B}, so they may alias.

• General rule
  • If pts(p) ∩ pts(q) ≠ ∅, they may alias.
• This helps determine whether a store through one pointer can affect a load through another.

4.6 PAG / SVFIR

The Pointer Assignment Graph (PAG) / SVFIR represents pointer and value constraints. Week 2B already introduces the PAG; Week 4 uses it for pointer analysis.

p = &a;
q = p;

After pointer analysis:

• pts(p) = {a}
• pts(q) = {a}

Therefore p and q may alias.

4.7 Andersen's pointer analysis

Andersen analysis calculates what each pointer can possibly point to.

It processes the constraints in the PAG / SVFIR and propagates points-to information.

p = &a;
q = p;
r = q;

• Start
  • pts(p) = {a}
  • pts(q) = {}
  • pts(r) = {}
• Propagate along p → q → r
• Final
  • pts(p) = {a}
  • pts(q) = {a}
  • pts(r) = {a}

Flow insensitivity

Classic Andersen analysis is flow-insensitive.

p = &a;
q = &b;

r = p;
r = q;

At actual runtime, r = p makes r point to a, then r = q overwrites that, so r ends pointing to b.

Andersen generally collects both possibilities:

• pts(r) = {a, b}

because it does not distinguish statement order in its overall points-to result. It says: somewhere in the analysed program, r may receive the address of a or b.

4.8 Fixed point

Andersen repeatedly propagates information until nothing new can be added.

When nothing new can be added, it has reached a fixed point.

4.9 Week 4 summary

Week 4’s purpose is to determine how values can flow, especially through pointers and memory.

---

5. Information Flow Tracking and Taint Analysis

5.1 Main question and Purpose

Purpose

• Main question
  • Can a particular piece of information flow from a source to a sink?
• Week 5 combines Weeks 3 and 4. This is information-flow tracking.

5.2 Source, tainted data, and sink

A source is where interesting or untrusted data originates.

Examples include user input, network input, file input, and environment data.

x = getUserInput();

If getUserInput() is a source, x becomes tainted.

Tainted data is data originating from a source that we want to track.

x = source();
y = x;
z = y;

A sink is a sensitive operation where tainted data may be dangerous.

Examples include SQL execution, OS command execution, file operations, and network output.

system(x);

If a valid flow from source to sink exists, the analyser may report a potential vulnerability.

Simple taint analysis

x = source();
y = x;
sink(y);

Therefore the source can reach the sink.

5.3 Why Weeks 3 and 4 are needed

Why Week 4 is needed

Pointers hide data movement through memory:

int input = source();

int a;
int *p = &a;
int *q = p;

*p = input;

int x = *q;

sink(x);

Week 4 determines:

• pts(p) = {a}
• pts(q) = {a}

so p and q alias. Week 5 can then find:

Without pointer analysis, the analyser may not know that the store through p can affect the load through q.

Why Week 3 is needed

Real programs contain function calls.

void process(int x) {
    sink(x);
}

int main() {
    int input = source();
    process(input);
}

Week 3’s call graph and ICFG tell us how execution moves between these functions.

5.4 Context sensitivity

Suppose the same function is called multiple times:

foo(tainted);
foo(safe);

A context-sensitive analysis remembers which call led into the function.

• Correct
  • Call A → foo → return A
  • Call B → foo → return B
• Incorrect
  • Call A → foo → return B

The incorrect matching creates an impossible execution path and may cause false positives.

Call stack

Context can be understood using a stack.

main() {
    foo();
}

foo() {
    bar();
}

• Call foo → stack [foo]
• foo calls bar → stack [foo, bar]
• bar returns → [foo]
• foo returns → []

This helps match calls with their correct returns.

5.5 SVFG

SVFG = Sparse Value-Flow Graph.

It represents relevant value-flow relationships:

• Where was a value defined?
• Where can that value flow?
• Where can it be used?

The SVFG lets analyses such as taint analysis traverse value-flow paths.

Direct versus indirect value flow

Direct:

x = source();
y = x;

Indirect through memory:

*p = x;
y = *q;

If Week 4 determines that both p and q point to A:

This is an indirect memory-based flow.

5.6 Analysis process

A simplified taint-analysis process:

For interprocedural analysis, the traversal must also respect valid call/return contexts.

5.7 Connecting Weeks 3, 4 and 5

	Week 3	Week 4	Week 5
Focus	Control flow	Data dependence	Information flow
Question	Where can execution go?	Where can data and pointers go?	Can source reach sink?
Main graph	CFG / ICFG	PAG / SVFIR	SVFG
Important analysis	Interprocedural analysis	Andersen pointer analysis	Taint analysis
Key concepts	Call, return, entry, exit	Points-to, alias, load/store	Source, sink, taint
Purpose	Find valid execution paths	Find data dependencies	Find security / information flows

• One sentence per week
  • Week 3: find the possible execution paths through and between functions.
  • Week 4: find how data and pointers relate, including hidden memory dependencies caused by aliasing.
  • Week 5: use those relationships to determine whether specific information can flow from a source to a sink.

5.8 Complete example

void process(int *q) {
    int x = *q;
    sink(x);
}

int main() {
    int input = source();
    int a;
    int *p = &a;
    *p = input;
    process(p);
}

Week 3 — Control flow

Execution can reach process() and the sink.

Week 4 — Data dependence

int *p = &a;

gives pts(p) = {a}. When p is passed to process, q can point to the same object:

Therefore:

Week 5 — Information flow

There is a valid source-to-sink information flow.

---

6. Program Verification Against Software Vulnerabilities

6.1 Main question and Purpose

Purpose

• Main question
  • What real software vulnerabilities can happen, why they happen, and what conditions should be checked to prevent them?
• The lecture groups vulnerabilities into memory-safety errors, arithmetic errors, tainted-input problems, injection problems, and side-channel attacks.
• The slides repeatedly use assertions to check important safety conditions before continuing execution.

6.2 Memory leak

A memory leak occurs when dynamically allocated memory is not freed along a program execution path.

List *list = new List();

If the program never properly deletes all allocated memory, the leak remains.

• Why it matters
  • Over time, the program may consume more and more memory.
• Secure idea
  • Make sure every allocated object is eventually freed.

Relation to Week 3

Memory leaks depend on execution paths. Week 3 asks where execution can go.

Control-flow analysis can help determine whether there is some path where allocated memory is never released.

6.3 Null pointer dereference

A null-pointer dereference happens when the program dereferences a pointer whose value is NULL or nullptr, often causing a crash.

Student* student = findStuRecord(id);

printf("%s", student->name);

findStuRecord() may return nullptr. Then student->name tries to access memory through an invalid pointer.

• Secure idea
  • Check before dereferencing:

assert(student != nullptr);

Relation to Week 4

Week 4 asks what a pointer can point to. Week 6 adds: is the pointer valid before we dereference it?

Week 4’s pointer analysis is directly useful here.

6.4 Dangling pointer / use-after-free

A dangling pointer is a pointer that no longer refers to a valid memory object, often because that object has already been freed.

char *ptr = malloc(SIZE);

free(ptr);

logError(ptr);

After free(ptr), the memory object is gone. Using ptr again is use-after-free.

• Secure idea
  • A defensive pattern shown in the lecture is:

free(ptr);
ptr = nullptr;

Relation to Week 4

Week 4 understands ptr → object A. Week 6 adds object lifetime:

Knowing where a pointer points is not enough; we also care whether the object still exists.

6.5 Buffer overflow

A buffer overflow occurs when the program writes more data than a buffer can hold and overwrites adjacent memory.

char *p = malloc(n);
int y = n;

p[y] = 'a';

If the buffer has n elements, valid indexes are 0 ... n-1. p[n] is outside the allocated area.

• Secure idea
  • Check the index before writing:

assert(y < n);

Relation to Weeks 3 and 4

• Week 3 helps determine whether execution can reach the dangerous access.
• Week 4 helps reason about the memory object being accessed.
• Week 6 asks: is the actual memory access valid?

6.6 Integer overflow

An integer overflow occurs when a calculation produces a value outside the range that the integer type can represent.

Easy definition: the result is too large to fit inside the integer type.

For unsigned integers, the lecture shows wrap-around behaviour:

• UINT_MAX + 1 = 0
• UINT_MAX + 2 = 1
• UINT_MAX + 3 = 2

Why it is dangerous

size = nresp * sizeof(char*);

If the real result is huge but the multiplication overflows:

The lecture gives an OpenSSH example where multiplication overflow leads to a heap buffer overflow.

• Secure idea
  • Check the value before the dangerous arithmetic or allocation:

assert(nresp <= userDefinedSize / sizeof(char*));

The lecture recommends checking the size before allocation.

6.7 Division by zero

A division-by-zero error occurs when the divisor becomes zero.

return totalTime / numRequests;

If numRequests = 0, the operation is invalid.

• Secure idea

assert(numRequests > 0);

before performing the division.

6.8 Tainted information flow

Tainted data means data that comes from an untrusted source, such as user or network input.

Week 6 explains that malicious input can cause unexpected behaviour, information leakage, or attacks.

char *pMsg = packet_get_string();

ParseMsg((LOGIN_MSG_BODY *)pMsg);

The lecture example shows attacker-controlled data influencing a loop bound and recommends checking it against a safe limit.

Relation to Week 5

This is a direct continuation of Week 5.

Week 5 tracks SOURCE → taint → value flow → sink.

Week 6 asks: what vulnerability can occur if that tainted value reaches an unsafe operation?

6.9 Code injection

Code injection happens when input that should only be treated as data becomes part of executable code or a command.

cin >> user_id;

system(command + user_id);

Expected: user_id = "05" produces cat user_info/05. If malicious command syntax is included in the user input, system() may execute unintended commands. The lecture identifies lack of validation before system() as the problem.

• Secure idea
  • Validate the input before passing it to system().
  • The lecture checks that the user ID contains numeric input before execution.

Relation to Week 5

This is another source-to-sink problem:

• Week 5 detects: tainted flow → system()
• Week 6 interprets: possible code injection

6.10 Format string vulnerability

A format string vulnerability occurs when user input is interpreted as formatting instructions rather than ordinary data.

Easy definition: user-controlled data becomes printf instructions.

Safe:

printf("%s", userInput);

• "%s" → format
• userInput → data

Vulnerable:

printf(userInput);

Now userInput is treated as format instructions. If the user provides %s%s%s%s, printf() may interpret those sequences as instructions to read string arguments that were never supplied. This can cause invalid memory access or a crash.

Relation to Week 5

6.11 SQL injection

SQL injection happens when user input is directly combined into an SQL query and changes the query’s meaning.

txtUserId = getRequestString("UserId");

txtSQL =
    "SELECT * FROM Users WHERE UserId = "
    + txtUserId;

The slides show that specially crafted input can modify the condition so that the database returns unintended records.

Relation to Week 5

SQL injection is another practical consequence of unsafe information flow.

6.12 Side-channel / timing attack

A side-channel attack occurs when secret information leaks through some observable program behaviour rather than through normal program output.

A timing attack uses how long the program takes as the observable information.

for (...) {
    if (guess[i] != password[i])
        return false;
}

Suppose the password is CAT123. An attacker may infer that more characters are correct because the program takes longer before returning:

• XXXXXX → fails quickly
• CXXXXX → slightly slower
• CAXXXX → even slower
• CATXXX → slower again

• Secure idea
  • Compare all characters instead of returning immediately:

for (i = 0; i < length; i++)
    result &= (ca[i] == cb[i]);

The goal is a constant-time comparison for a fixed input length.

Relation to Week 5

Week 5 mainly studies explicit value flow: variable → variable → sink.

Timing attacks show that information can also escape indirectly:

This extends information flow beyond normal data-flow edges.

6.13 Role of assertions

Assertions state: this condition must be true before continuing.

assert(student != nullptr);
assert(y < n);
assert(numRequests > 0);
assert(nresp <= safeLimit);

The important idea is not just the word assert, but the safety condition being checked.

6.14 Connecting Weeks 3–6

Week	Main question	How Week 6 uses it
Week 3	Where can execution go?	Find paths that reach dangerous operations or miss cleanup
Week 4	Where can pointers / data go?	Understand memory objects, pointer accesses and aliases
Week 5	Can information flow from source to sink?	Track tainted input into dangerous operations
Week 6	What vulnerability can happen?	Identify real bugs and the safety checks needed

Week 3 → Week 6

Week 3 gives the paths. Week 6 identifies a memory leak.

Week 4 → Week 6

Week 4 understands p → memory A. Then:

free(p);
*p = 10;

Week 6 identifies use-after-free.

Week 5 → Week 6

input = source();
system(input);

Week 5 finds SOURCE → input → SINK. Week 6 interprets the unsafe tainted flow as code injection.

6.15 Cheat sheet

Vulnerability	Remember
Memory leak	Allocated memory is never freed
Null dereference	Use *p when p == nullptr
Use-after-free	Use memory after it has been freed
Buffer overflow	Write outside buffer bounds
Integer overflow	Number does not fit its integer range
Division by zero	Divisor becomes 0
Tainted information flow	Untrusted data travels through the program
Code injection	User data becomes executable command or code
Format string	User data becomes printf instructions
SQL injection	User input changes an SQL query
Timing attack	Secrets leak through execution time

Weeks 3–5 teach you how to follow program execution and data. Week 6 uses that knowledge to recognise unsafe program behaviour and software vulnerabilities.

---

7. Code Verification and Predicate Logic

7.1 Main question and Purpose

Purpose

• Main question
  • Given a pre-condition and a program, can we prove that a safety assertion always holds?
• Weeks 3–6 analyse what a program can do. Week 7 checks whether what it does is correct / safe.
• The slides take program paths and SVF statements, translate them into logical formulas, and check each path.

Week	Main question	Connection to Week 7
Week 3 — Control flow	Where can execution go?	Gives the program paths that can be checked
Week 4 — Data dependence	Where can data / pointers go?	Gives relationships between values along those paths
Week 5 — Information flow	Can data flow from source to sink?	Identifies important flows that may need verification
Week 6 — Vulnerabilities	What can go wrong?	Introduces safety conditions such as assert(index < size)
Week 7 — Verification	Can we prove the safety condition holds?	Converts paths + assertions into logic and checks them

7.2 Formal verification

Formal verification means proving whether code satisfies a given specification using mathematical logic.

The lecture describes this as translating the specification and implementation into logical formulas, then using theorem-proving tools to check them.

7.3 Specification: pre-condition and post-condition

In this subject, specifications are embedded in the source code using assume and assert. The slides express this with Hoare logic:

P { prog } Q

Part	Meaning
P	Pre-condition — assumption before the program
prog	Program being checked
Q	Post-condition — assertion that should hold afterward

assume(x > 0);    // P

y = x + 1;        // program

assert(y > 0);    // Q

If x > 0 before execution, running the program should guarantee y > 0.

7.4 Main verification question

Week 7 asks:

Given the pre-condition and the program, will the assertion always hold?

assume(100 > x && x > 0);

if (x > 10) {
    y = x + 1;
}
else {
    y = 10;
}

assert(y >= x + 1);

Here:

• P = 100 > x > 0
• Q = y >= x + 1

7.5 Check each program path

This is where Week 3 control flow becomes important. The example has two paths:

Path 1

x > 10
y = x + 1

Assertion: y >= x + 1

Because y = x + 1, the assertion holds on this path.

Path 2

x <= 10
y = 10

Try x = 10. Then y = 10, but:

y >= x + 1
10 >= 11  ✗

So x = 10 is a counterexample. The lecture identifies this same counterexample for the else path.

7.6 Counterexample

A counterexample is:

A valid input that makes the required assertion fail.

Instead of trying every possible input (x = 1, x = 2, …, x = 99), we ask a solver:

Does any valid input exist that breaks the assertion?

That question becomes the logical verification formula.

7.7 Convert code into logical formulas

Each program path is translated into constraints. The slides state that the SVFStmts from each program path are translated into a logical formula ϕ, then each path is checked.

Path 1 formula

P
AND
x > 10
AND
y = x + 1

Path 2 formula

P
AND
x <= 10
AND
y = 10

7.8 How we search for a bug

The required property is:

P ∧ Program → Q

If the pre-condition holds and the program executes, then the post-condition should hold.

To search for a bug, the lecture instead looks for:

P ∧ Program ∧ ¬Q

7.9 SAT and UNSAT

A solver checks whether a logical formula has a solution.

SAT — Satisfiable

There is at least one set of values that makes the formula true.

Example: x > 5 AND x < 10 has a solution x = 7, so the formula is SAT.

The lecture says an automated prover returns a model when a formula is satisfiable.

UNSAT — Unsatisfiable

No values can satisfy the formula.

Example: x > 10 AND x < 5 is impossible, so the formula is UNSAT.

For the bug formula P ∧ Program ∧ ¬Q:

7.10 Propositional logic

Before predicate logic, Week 7 reviews propositional logic.

A proposition is a statement that is either TRUE or FALSE.

Example:

• P = "x > 10"
• Q = "y < 5"

Logic	Meaning	Code equivalent
P ∧ Q	AND	P && Q
P ∨ Q	OR	P || Q
¬P	NOT	!P
P → Q	If P then Q	implication

Inference example

if (x > 10 && y < 5)
    z = 15;

Let:

• P1 = x > 10
• P2 = y < 5
• Q = z = 15

Then (P1 ∧ P2) → Q:

P1
P2
──────
Q

This is a basic inference pattern.

7.11 Why propositional logic is not enough

Propositional logic treats x > 10 as one whole statement P. It does not analyse the internal relationship between x, >, and 10.

The slides explain that propositional logic has limited ability to represent properties, relationships, or statements about all or some objects.

Programs contain many relationships:

• x > 10
• y < x
• index < size
• result = x + 1

Therefore we need something more expressive: predicate logic.

7.12 Predicate logic / first-order logic

Predicate logic extends propositional logic with:

• variables
• predicates
• relationships
• quantifiers

One-variable predicate

R(x): x > 5

• x is a variable
• x > 5 is a predicate / property

If x = 6, then R(6) is 6 > 5, which is TRUE.

Two-variable predicate

R(x, y): x > y

R(10, 5) is 10 > 5, which is TRUE.

This is why predicate logic is useful for analysing program variables.

7.13 Quantifiers

Predicate logic introduces two important symbols.

∀ — Universal

Means for all / every. ∀x = for every x.

In verification:

The assertion should hold for all valid inputs.

∃ — Existential

Means there exists / at least one. ∃x = there exists some x.

In bug finding:

Does one input exist that breaks the assertion?

The slides define ∀ as all / every and ∃ as some / there exists.

Safety:
∀ valid inputs → assertion holds

Bug finding:
∃ input → assertion fails

7.14 Knowledge base — KB

The Predicate Logic slides use KB for Knowledge Base:

The collection of logical constraints / facts extracted from the program.

Example:

KB:
x > 10
y = x + 1

Q:
y > 10

We ask KB ⊢ Q ?

Given everything in KB, must Q also be true?

The lecture describes this as asking whether Q is true in every situation that satisfies the constraints in KB.

7.15 Theorem provers

Doing this manually becomes impractical because programs contain too many paths, variables, logical relationships, and assertions.

The subject therefore focuses on automated theorem-prover tools rather than manual mathematical proofs.

7.16 SAT versus SMT solver

Solver	Handles	Example
SAT	Boolean / propositional formulas	P ∧ Q, P ∨ ¬Q
SMT	Richer expressions with values and arithmetic	x > 10, y = x + 1, index < size

The slides describe SMT as an extension / generalisation of SAT for richer formulas, and identify Z3 as the SMT solver used in this subject.

7.17 Week 7 overall process

7.18 Cheat sheet

Concept	Meaning
Formal verification	Use logic to verify program correctness
Specification	What the program should guarantee
Pre-condition P	Assumption before execution
Post-condition Q	Assertion after execution
Hoare form	P {prog} Q
Counterexample	Input that makes Q fail
Proposition	Statement that is true or false
Predicate	Property / relation involving variables
∧	AND
∨	OR
¬	NOT
→	implies
∀	for all
∃	there exists
KB	Known program constraints
SAT	Formula has a solution
UNSAT	Formula has no solution
SMT	Solver for richer arithmetic / logic constraints
Z3	SMT solver used in this subject

Most important thing to remember

Weeks 3–6:
Find paths, data flows and vulnerabilities.

Week 7:
Turn those program behaviours and
safety requirements into logic
and check whether they can fail.

Week 7 = Path + Program Constraints + Assertion → Logical Formula → Solver → Counterexample or no counterexample.

---

8. Software Verification and Z3 Theorem Prover

8.1 Main question and Purpose

Purpose

• Main question
  • How do we turn program code into logical constraints, then use Z3 to check whether those constraints can actually happen?
• The slides focus on manually translating source code into Z3 expressions, understanding the Z3 solver, and using the provided Z3Mgr APIs.

8.2 What is Z3?

Z3 is an SMT solver developed by Microsoft Research. It is used for software verification, static checking, testing, and other analysis tasks.

Give me some logical rules, and I will check whether there is any possible solution.

Slide example

Constraints:

x > 10
y = x + 1

Z3 can choose x = 11, y = 12. Those values are possible, so the result is sat.

8.3 SAT, UNSAT and UNKNOWN

Z3 returns one of these results when checking a formula.

Result	Easy meaning
sat	At least one solution exists
unsat	No solution can satisfy all constraints together
unknown	Z3 cannot determine the answer

SAT   = possible
UNSAT = impossible

SAT example

x = 10
x > 5

Possible, so sat.

UNSAT example

x = 10
x = 20

Impossible, so unsat.

8.4 Important Z3 commands

Command	Meaning
declare-const	Create a variable
declare-fun	Create a function
assert	Add a constraint
check-sat	Check if constraints are satisfiable
get-model	Show one possible solution
eval	Evaluate a value using the solution

Example

(declare-const x Int)
(assert (> x 10))
(check-sat)

Meaning:

• create integer x
• require x > 10
• ask Z3 whether this is possible

Answer: sat.

8.5 Understanding Z3 syntax

Z3 usually writes expressions as (operator value1 value2) instead of normal C/C++ style.

C/C++	Z3
x > 10	(> x 10)
x == 10	(= x 10)
x + 1	(+ x 1)
x != y	(not (= x y))

(assert (= y (+ x 1)))

simply means y = x + 1.

8.6 assert

In Z3, assert means:

Add a rule that must be true.

(assert (> x 10))
(assert (= y (+ x 1)))

Z3 now needs to satisfy both:

x > 10
AND
y = x + 1

Every new assert adds another condition.

8.7 Uninterpreted functions

An uninterpreted function is a function where Z3 does not know its internal implementation.

For f(x), Z3 may only know that f accepts an Int and returns an Int. It does not care about the code inside f.

Same input, one output — SAT

f(10) = 1

Possible, so sat.

Same input, two outputs — UNSAT

f(10) = 1
f(10) = 2

Impossible, because the same function with the same input cannot return two different values. Result: unsat.

Different inputs, same output — SAT

x != y
f(x) = f(y)

This can still be sat, because different inputs are allowed to produce the same output.

8.8 Arithmetic and types

Z3 supports common arithmetic and comparison operations such as +, -, *, /, <, >, <<, >>, &, and |.

Operands should use compatible types. The slides warn against mixing types without explicit conversion.

If a is Int and b is Float, combining them directly may cause a sort mismatch.

This is similar to LLVM IR, where types such as i32, i64, float, and double matter.

8.9 ite — if then else

Z3 represents conditional expressions using ite(condition, trueValue, falseValue).

if (condition)
    result = trueValue;
else
    result = falseValue;

ite(x > 10, 20, 0)

means: if x > 10 then result = 20, else result = 0.

The slides use ite for comparisons and branches.

Connection to control flow

Earlier weeks modelled a branch as two paths. Week 8 can represent that mathematically:

ite(x, trueValue, falseValue)

8.10 Arrays — store and select

Z3 arrays are important because they can be used to represent memory.

Operation	Meaning	C-like	Z3 idea
store	Write a value into an array / memory location	a[x] = y	store(a, x, y)
select	Read a value from an array / memory location	z = a[x]	select(a, x)

STORE  = write
SELECT = read

8.11 push and pop

Think of these as:

• push = save the current solver state
• pop = restore the previous solver state

The slides explain that push creates a new scope and pop removes the assertions added since the matching push.

Temporary constraint

x > 0

PUSH
    x = 10
    check-sat
POP

Back to:
x > 0

The temporary constraint x = 10 disappears after pop.

Why this is useful for branches

You can analyse true and false paths separately so constraints from different paths are not mixed together:

PUSH
assert(x > 10)
analyse TRUE path
POP

PUSH
assert(x <= 10)
analyse FALSE path
POP

8.12 Z3Mgr

The subject provides a wrapper called Z3Mgr to make Z3 easier to use from the assignment code.

API	Meaning
getZ3Expr(...)	Create a Z3 expression
getMemObjAddress(...)	Create / address a memory object
getGepObjAddress(...)	Create an address with an offset
addToSolver(...)	Add a constraint
resetSolver()	Clear constraints
solver.check()	Check SAT / UNSAT
getEvalExpr(...)	Evaluate an expression
printExprValues()	Print expression values

getEvalExpr() checks the solver, retrieves a model if the constraints are satisfiable, and evaluates the requested expression in that model.

8.13 Main translation rules

The slides show how SVF statements map into Z3 constraints.

SVF statement	C-like meaning	Z3 idea
AddrStmt	p = &a	give p an address
CopyStmt	p = q	p == q
LoadStmt	p = *q	load value from memory
StoreStmt	*p = q	store value into memory
GepStmt	p = &q[i]	address + offset
PhiStmt	merge path values	choose value from executed path
BranchStmt	if / else	use ite(...)
UnaryOp	!p	unary logic
BinaryOp	r = p + q	equivalent Z3 operation
CmpStmt	p > q etc.	comparison
Call / Return	function call	use scope + value passing

Important examples

p = q
→ p == q

r = p + q
→ r == p + q

if (x)
    r = p
else
    r = q
→ r == ite(x, p, q)

8.14 Why SSA is important

The slides state that code being translated should be in SSA form, such as SVFIR.

a = 1;
a = 2;

If Z3 sees both assignments as the same variable, it interprets them as a must equal 1 and a must equal 2, which is unsat.

SSA gives each assignment its own version:

a1 = 1
a2 = 2

This is why earlier LLVM / SVFIR work matters in Week 8.

8.15 Scalar translation example

The slides use:

int a;
int b;

a = 0;
b = a + 1;

assert(b > 0);

This becomes approximately:

a = 0
b = a + 1
b > 0

Z3 checks whether all of these conditions can be true. Yes: a = 0, b = 1, so sat.

The slides show the full flow from C code → Z3Mgr → Z3 formulas → solver.

8.16 Memory example

The slides also use:

int* p;
int x;

p = malloc(...);
*p = 5;
x = *p;

assert(x == 5);

The logic is:

• p points to a memory location
• *p = 5 writes 5 into the memory pointed to by p
• x = *p reads that value from memory
• therefore x = 5, and assert(x == 5) is consistent with the constraints

The slides model memory using a Z3 array and use store / load operations around that memory map.

8.17 How Week 8 connects to previous weeks

Earlier concept	Connection to Week 8
LLVM / SVFIR	Provides the program representation to translate
SSA	Makes assignments suitable for logical formulas
ICFG	Helps identify executable paths
Pointer analysis	Helps reason about addresses and memory
Load / Store	Become Z3 memory operations
Branches	Can become ite expressions / path constraints
Data / taint flow	Determines how information moves
Assertions	Become properties that can be checked using constraints

So Week 8 is where many earlier concepts start coming together.

8.18 Cheat sheet

Concept	Meaning
Z3	SMT solver used to solve logical constraints
SAT	A solution exists
UNSAT	No solution exists
UNKNOWN	Z3 cannot determine the result
assert	Add a constraint
check-sat	Ask Z3 if all constraints can be satisfied
get-model	Show one solution
ite	if-then-else
select	Read from array / memory
store	Write to array / memory
push	Save solver state
pop	Restore solver state
SSA	Each variable definition has its own version
Z3Mgr	Wrapper used in this subject to interact with Z3

Main translations

p = q
→ p == q

r = p + q
→ r == p + q

if / else
→ ite(...)

*p = q
→ store to memory

p = *q
→ load from memory

a[i]
→ select

a[i] = value
→ store

The slides finish by asking you to understand the Z3 formula format, understand Z3Mgr, review the Assignment 3 examples, complete the quizzes, and implement manual code-to-Z3 translation.

Week 8 is about translating program behaviour into logical constraints so Z3 can determine whether that behaviour is possible.

---

9. Assertion-based Verification Using Static Symbolic Execution

9.1 Main question and Purpose

Purpose

• Main question
  • How do we automatically check whether an assertion can fail using Static Symbolic Execution (SSE) and Z3?
• Instead of running a program with one real input, SSE uses symbolic values.
• This lets the analysis reason about many possible inputs at once.

Normal execution                 Symbolic execution
────────────────                 ──────────────────
int x;                           int x;
y = x + 1;                       y = x + 1;

x = 5                            x = symbolic
y = 6                            y = x + 1

9.2 Overall Week 9 workflow

Source Program
     ↓
ICFG finds possible paths
     ↓
Follow one path
     ↓
Read SVF statements
     ↓
Translate statements into Z3 constraints
     ↓
Reach assertion
     ↓
Negate the assertion
     ↓
Ask Z3
     ↓
SAT or UNSAT

The ICFG is used because symbolic execution needs to know which sequence of statements forms a valid execution path.

9.3 Assertion checking

Suppose:

assert(y >= x + 1);

The assertion is:

Q: y >= x + 1

To find a bug, we ask:

Can the assertion be false?

So we check NOT Q, which becomes:

y < x + 1

Result	Meaning
unsat	No counterexample exists — assertion is safe on this path
sat	A counterexample exists — assertion may fail

The slides verify assertions by checking the path constraints together with the negated assertion.

9.4 Example: one path

Program:

if (x > 10) {
    y = x + 1;
}

assert(y >= x + 1);

For this path:

x > 10
y = x + 1

To search for an assertion failure:

x > 10
AND
y = x + 1
AND
y < x + 1

But if y = x + 1, then y < x + 1 would mean:

x + 1 < x + 1

That is impossible, so the result is unsat. This path cannot violate the assertion.

9.5 Why ICFG is used again

ICFG answers:

Which program paths are possible?

Example:

if (x > 10)
    y = x + 1;
else
    y = 10;

ICFG gives two paths:

Path 1                      Path 2
──────                      ──────
x > 10                      x <= 10
   ↓                           ↓
y = x + 1                   y = 10
   ↓                           ↓
assert                      assert

Week 9 then checks each path separately.

Part	Role
ICFG	Finds the route
SSE	Understands the values on the route
Z3	Checks whether the route can break the assertion

9.6 Translating statements into Z3

The later slides explain how to convert different program statements into Z3 expressions.

Program instruction
       ↓
SVF statement
       ↓
Z3 constraint

9.7 CmpStmt — comparison

CmpStmt represents comparisons such as x == y, x != y, x > y, and x <= y.

Example:

b = (x == y);

Symbolically:

b = if x == y then 1 else 0

In Z3:

b == ite(x == y, 1, 0)

ite means if-then-else.

CmpStmt = comparison

The slides translate comparison operators such as ==, !=, >, >=, <, and <= into Z3 expressions.

9.8 BinaryOpStmt — calculation

BinaryOpStmt represents arithmetic or bitwise operations.

Example:

z = x + y;

becomes:

z = x + y

SVF operation	Meaning
Add	+
Sub	-
Mul	*
SDiv	/
SRem	%

BinaryOpStmt = calculation

The slides show these operations being translated into Z3 constraints.

9.9 Simple example using CmpStmt and BinaryOpStmt

Program:

y = x;
b = (x == y);
z = x + y;

assert(z == 2 * x);

Symbolic meaning:

y = x
b = ite(x == y, 1, 0)
z = x + y

To search for failure, check z != 2*x:

y = x
AND
z = x + y
AND
z != 2*x

Because y = x, then z = x + x = 2*x, so z != 2*x is impossible. Result: unsat.

The slide uses this example to show that the assertion has no counterexample.

9.10 Memory operations

Week 9 also handles pointers and memory.

int* p;

p = malloc(...);
*p = x + 5;
y = *p;

assert(y == x + 5);

Normal execution may use a real address such as p = 0x1234. Symbolic execution instead uses a virtual address:

p = symbolic memory address

Then:

*p = x + 5   →   Memory[p] = x + 5
y = *p       →   y = Memory[p]

Therefore y = x + 5.

The slides model allocated memory using virtual addresses instead of real runtime addresses.

9.11 AddrStmt, StoreStmt, LoadStmt

These are easier if you translate the names into normal programming operations.

SVF statement	Meaning	Example
AddrStmt	Get an address	p = &x
StoreStmt	Write to memory	*p = 10
LoadStmt	Read from memory	y = *p

AddrStmt                 StoreStmt                LoadStmt
────────                 ─────────                ────────
p = &x                   *p = 10                  y = *p
   ↓                        ↓                        ↓
p points to x            write 10 into memory     read value from memory

The Week 9 algorithms handle these three memory operations directly.

9.12 Relation to earlier pointer analysis

Earlier pointer analysis asked:

What can p point to?

Example:

p = &x;

might produce:

pts(p) = {x}

Week 9 asks something different:

What symbolic value is stored at the memory location p points to?

Earlier:
pointer → object

Week 9:
pointer → object → symbolic value

9.13 GepStmt — field or array access

GepStmt is used to locate something inside a larger object.

struct st {
    int a;
    int b;
};

If p->b is accessed, symbolic execution needs an address for field b.

p
│
▼
┌─────────────┐
│ a           │
├─────────────┤
│ b  ← target │
└─────────────┘

GepStmt = find the address of a field or array element

The slide models fields using a base object plus a field offset, giving each field its own virtual address.

9.14 Struct example

Program:

struct st {
    int a;
    int b;
};

struct st* p = malloc(...);

q = &(p->b);
*q = x;

int k = p->b;

assert(k == x);

Step by step:

p
↓
struct object

q
↓
points to field b

Then *q = x means p->b = x, and k = p->b means k = x. So assert(k == x) is safe.

9.15 Function calls — push() and pop()

When symbolic execution enters another function, Z3 temporarily saves the current solver state.

Caller
  │
  │ push()
  ▼
Callee function
  │
  │ analyse function
  ▼
return
  │
  │ pop()
  ▼
Caller continues

Call	Meaning
push()	Save current constraint state
pop()	Restore previous constraint state

The Week 9 call and return algorithms use Z3's solver stack in this way.

9.16 Branch checking

Before following a branch, symbolic execution checks whether that branch is possible.

Current knowledge:

x = 5

Branch:

if (x > 10)

Check:

x = 5
AND
x > 10

Z3 returns unsat. Therefore this branch cannot happen, and the analysis does not continue down this path.

The slide's handleBranch algorithm temporarily adds the branch condition and checks satisfiability.

9.17 Z3 has two main jobs in Week 9

Job 1: Check whether a path is possible

Path constraints
      ↓
Z3
      ↓
SAT   → possible path
UNSAT → impossible path

Job 2: Check whether an assertion can fail

Path constraints
+
NOT assertion
      ↓
Z3
      ↓
SAT   → counterexample exists
UNSAT → no counterexample

Be careful: SAT is not always bad.

Context	Meaning of SAT
Branch checking	Path is possible
Assertion checking	Assertion can fail

The meaning depends on what constraints you gave Z3.

9.18 Easy way to remember all statement types

Category	Statements	Meaning
Values	CmpStmt, BinaryOpStmt	Comparison and calculation
Memory	AddrStmt, LoadStmt, StoreStmt	Address, read, write
Objects	GepStmt	Field or array element
Control flow	Branch, Call, Return	Where execution goes

9.19 Cheat sheet

                 PROGRAM
                    │
                    ▼
                  ICFG
          find execution paths
                    │
                    ▼
          Static Symbolic Execution
                    │
       ┌────────────┼────────────┐
       │            │            │
       ▼            ▼            ▼
   Values        Memory      Control Flow
 CmpStmt       AddrStmt       Branch
 BinaryOp      LoadStmt       Call
               StoreStmt      Return
               GepStmt
       │            │            │
       └────────────┼────────────┘
                    ▼
             Z3 constraints
                    │
                    ▼
             Reach assertion
                    │
                    ▼
            Add NOT assertion
                    │
                    ▼
                 Z3 Solver
                /         \
              SAT        UNSAT
               │           │
               ▼           ▼
       Counterexample   No counterexample
       may exist        on this path

Concept	Meaning
SSE	Static Symbolic Execution — reason about many inputs using symbols
ICFG	Finds feasible program paths to check
Negated assertion	NOT Q — used to search for a counterexample
CmpStmt	Comparison → often ite(...) in Z3
BinaryOpStmt	Arithmetic / bitwise calculation
AddrStmt	Get an address
StoreStmt	Write to memory
LoadStmt	Read from memory
GepStmt	Address of a field or array element
push / pop	Save / restore solver state around calls
Branch check	Temporarily add branch condition and ask Z3

Week 9 uses the ICFG to find program paths, symbolically translates each SVF statement into Z3 constraints, and checks whether any feasible path can violate an assertion.