datalog

name

datalog

description

Souffle Datalog for binary analysis. Use this skill when writing, debugging, or reasoning about Datalog rules and fact schemas for binary program analysis — especially rules over MLIL-SSA facts extracted from Binary Ninja. Trigger on: writing .dl files, Souffle syntax questions, defining Datalog relations for binaries, composing taint/reachability/lifecycle queries, fact schema design, debugging Souffle errors, or any task involving Datalog-based reasoning over disassembled code.

Souffle Datalog for Binary Analysis

This skill covers writing Souffle Datalog programs for the BinCodeQL project — a query engine that reasons over facts extracted from Binary Ninja's MLIL-SSA intermediate representation.

Souffle Syntax Quick Reference

Type Declarations

Souffle uses .type for custom types and .decl for relation declarations.

// Subtypes (recommended — catches cross-relation mistakes)
.type Address <: unsigned
.type Symbol <: symbol
.type Version <: unsigned
.type ArgIndex <: unsigned
.type Offset <: number

// Relations use typed columns
.decl Function(name: Symbol, addr: Address)
.decl Def(func: Symbol, var: Symbol, ver: Version, addr: Address)

Rules

// Basic rule: head :- body.
Reaches(a, b) :- CallEdge(a, b).
Reaches(a, c) :- Reaches(a, b), CallEdge(b, c).

// Negation (requires stratification — negated relation must be fully computed first)
Unused(f) :- Function(f, _), !CallEdge(_, f).

// Disjunction (multiple rules for same head)
InputSource(f, v, ver) :- Call(f, "read", addr), ActualArg(addr, 0, _, v, ver).
InputSource(f, v, ver) :- Call(f, "recv", addr), ActualArg(addr, 1, _, v, ver).

IO Directives

// Input facts from TSV files (one file per relation in the fact directory)
.input Function(IO=file, filename="Function.facts", delimiter="\t")
.input Def(IO=file, filename="Def.facts", delimiter="\t")

// Output query results
.output TaintedSink(IO=file, filename="TaintedSink.csv", delimiter="\t")

// Shorthand (uses relation name as filename, tab-delimited)
.input Function
.output TaintedSink

Aggregation and Arithmetic

// Count, min, max, sum
CallCount(f, n) :- f = caller, n = count : CallEdge(caller, _).

// Bounded recursion isn't needed — Souffle does fixed-point automatically
// but watch for Cartesian blowups in joins

Components (Modules)

.comp TaintAnalysis {
    .decl Source(func: Symbol, var: Symbol, ver: Version)
    .decl Sink(func: Symbol, addr: Address, arg: ArgIndex)
    .decl Flow(src_f: Symbol, src_v: Symbol, dst_f: Symbol, dst_v: Symbol, dst_ver: Version)

    // Rules here...
}

// Instantiate
.init taint = TaintAnalysis

Important Souffle Behaviors

• Fixed-point evaluation: recursive rules iterate until no new tuples. No explicit loop needed.
• Stratification: negation and aggregation require the negated/aggregated relation to be fully computed in a prior stratum. Souffle checks this at compile time.
• No duplicates: relations are sets, not bags. Same tuple inserted twice = stored once.
• Symbol type: interned strings. Use for function names, variable names.
• Unsigned type: non-negative integers. Use for addresses (hex values are just numbers).
• Number type: signed integers. Use for offsets that can be negative.

Running Souffle

# Interpreted mode (faster startup, good for interactive/small programs)
souffle -F fact_dir/ -D output_dir/ program.dl

# Compiled mode (compiles to C++ first — faster execution on large fact sets)
souffle -F fact_dir/ -D output_dir/ -c program.dl

# With parallel threads
souffle -F fact_dir/ -D output_dir/ -j4 program.dl

# Show warnings (useful for debugging unused relations)
souffle -F fact_dir/ -D output_dir/ -w program.dl

Key flags:

• -F <dir>: fact directory (where .facts/.csv input files live)
• -D <dir>: output directory (where output relations are written)
• -c: compile to C++ before running (slow start, fast execution)
• -j <N>: number of parallel threads
• -p <file>: profile output (for performance debugging)

BinCodeQL Fact Schema

Facts are extracted from Binary Ninja MLIL-SSA output. Read references/fact-schema.md for the complete schema with all columns and types.

Core Relations (extracted)

Relation	Source	Purpose
Function(name, addr)	list_methods	All functions in the binary
Import(name, addr)	list_imports	Imported symbols (libc, etc.)
Export(name, addr)	list_exports	Exported symbols
Def(func, var, ver, addr)	MLIL-SSA LHS	Variable definition site
Use(func, var, ver, addr)	MLIL-SSA RHS	Variable use site
Call(caller, callee, addr)	MLIL-SSA call stmt	Function call edge
ActualArg(call_addr, idx, param, var, ver)	MLIL-SSA call args	Argument at call site
ReturnVal(func, var, ver)	MLIL-SSA return	Return value
PhiSource(func, var, def_ver, src_var, src_ver)	MLIL-SSA phi	SSA phi node sources
MemRead(func, addr, base, base_ver, offset)	MLIL-SSA load	Memory load
MemWrite(func, addr, target, offset, mem_in, mem_out)	MLIL-SSA store	Memory store
AddressOf(func, var, ver, target)	MLIL-SSA &	Address-of expression
CFGEdge(func, from_addr, to_addr)	MLIL-SSA branch/goto	Control flow edge

SSA Property

The key insight: in MLIL-SSA, Def(f, x, 3, ...) and Use(f, x, 3, ...) refer to the same definition because SSA versioning is unique per definition. This makes def-use chains trivial:

// In SSA, same (var, version) = same definition. No reaching-definition analysis needed.
DefUsePair(func, var, ver, def_addr, use_addr) :-
    Def(func, var, ver, def_addr),
    Use(func, var, ver, use_addr).

Common Binary Analysis Patterns

1. Call Graph Reachability

Reaches(a, b) :- Call(_, a, _), Call(_, b, _), a = b.  // reflexive (wrong)
// Correct:
Reaches(a, b) :- Call(a, b, _).
Reaches(a, c) :- Reaches(a, b), Call(b, c, _).

// "Can main reach dangerous_func?"
.output Reaches
// Then check: Reaches("main", "dangerous_func") in output

2. Taint Flow (Input to Sink)

// Sources: return values from input functions
TaintVar(func, var, ver) :-
    Call(func, callee, addr),
    Import(callee, _),
    DangerousInput(callee),
    Def(func, var, ver, addr).   // the return value def

// Propagation through SSA assignments
TaintVar(func, var2, ver2) :-
    TaintVar(func, var1, ver1),
    Use(func, var1, ver1, addr),
    Def(func, var2, ver2, addr).

// Propagation through phi nodes
TaintVar(func, var, def_ver) :-
    TaintVar(func, src_var, src_ver),
    PhiSource(func, var, def_ver, src_var, src_ver).

// Interprocedural: caller arg → callee parameter
TaintVar(callee, param_var, param_ver) :-
    TaintVar(caller, arg_var, arg_ver),
    Call(caller, callee, call_addr),
    ActualArg(call_addr, idx, _, arg_var, arg_ver),
    // Need formal parameter mapping (callee's first Def of param at entry)
    FormalParam(callee, idx, param_var, param_ver).

// Sink detection
TaintedSink(func, call_addr, callee, idx) :-
    TaintVar(func, var, ver),
    Call(func, callee, call_addr),
    ActualArg(call_addr, idx, _, var, ver),
    DangerousSink(callee, idx).

// Configuration: which functions are sources and sinks
DangerousInput("read").
DangerousInput("recv").
DangerousInput("fread").
DangerousSink("memcpy", 2).   // size argument
DangerousSink("strcpy", 1).   // source argument
DangerousSink("sprintf", 2).  // format argument
DangerousSink("system", 0).   // command argument

3. Resource Lifecycle (Use-After-Free)

// Track allocations
Allocated(func, var, ver, addr) :-
    Call(func, callee, addr),
    AllocFunc(callee),
    Def(func, var, ver, addr).

// Track frees
Freed(func, var, ver, addr) :-
    Call(func, callee, addr),
    FreeFunc(callee),
    ActualArg(addr, 0, _, var, ver).

// Use-after-free: a variable that was freed is later used
// (simplified — real check needs path sensitivity or CFG ordering)
PotentialUAF(func, use_addr, free_addr, var) :-
    Freed(func, var, ver_free, free_addr),
    Use(func, var, ver_use, use_addr),
    ver_use >= ver_free,  // approximate: later version used after free
    use_addr != free_addr.

AllocFunc("malloc"). AllocFunc("calloc"). AllocFunc("realloc").
FreeFunc("free").

4. Struct Field Access Tracking

// Who writes to offset 0x10 of a buffer?
FieldWrite(func, addr, target, 0x10) :-
    MemWrite(func, addr, target, 0x10, _, _).

// Who reads from it?
FieldRead(func, addr, base, 0x10) :-
    MemRead(func, addr, base, _, 0x10).

5. Shortest Call Path (with path length)

PathLen(a, b, 1) :- Call(a, b, _).
PathLen(a, c, n+1) :- PathLen(a, b, n), Call(b, c, _), n < 20.  // depth bound

ShortestPath(a, c, m) :- m = min n : PathLen(a, c, n).

Common Mistakes

1. Forgetting .input directives — Souffle won't read fact files unless told to. Every base relation needs .input.

2. Cartesian joins — A rule like R(x, y) :- A(x), B(y). produces |A|×|B| tuples. Always join on shared variables.

3. Unstratifiable negation — You can't negate a relation that depends (transitively) on the rule's own head. Souffle will report an error.

4. Type mismatches — If you declare Def(func: Symbol, ...) but try to join with a relation using unsigned for the same column, Souffle will reject it. Keep types consistent.

5. Missing base cases in recursion — Every recursive rule needs a non-recursive base case. Reaches(a,c) :- Reaches(a,b), Edge(b,c). alone won't produce anything — you need Reaches(a,b) :- Edge(a,b). as the base.

6. Address representation — MLIL-SSA addresses are hex strings in MCP output but should be stored as unsigned integers in Souffle. Convert during extraction (int("0x40a8b0", 16) in Python).

MLIL-SSA Statement Types

When extending the fact schema or debugging extraction, refer to the 10 MLIL-SSA statement types. Read references/mlil-ssa-grammar.md for the full grammar with regex patterns.

Quick summary:

Type	Pattern	Facts Generated
Assignment	var#N = expr	Def + Uses from RHS
Conditional	if (cond) then L1 else L2	CFGEdge ×2 + Uses
Goto	goto L @ addr	CFGEdge
Phi	var#N = ϕ(x#1, x#2)	Def + PhiSource per source
Return	return expr	ReturnVal + Uses
Call	ret#N, mem#M = func(args) @ mem#J	Call + Def + ActualArg + Use
MemRead	var#N = [base + off].sz @ mem#K	MemRead + Def + Use
MemWrite	tgt:off @ mem#J -> mem#K = val	MemWrite + Def(mem) + Use
AddressOf	var#N = &symbol	Def + AddressOf
NoReturn	noreturn	skip or NoReturn marker

Reference Files

• references/fact-schema.md — Complete fact schema with all column types, IO directives, and example .facts file format
• references/mlil-ssa-grammar.md — Full MLIL-SSA grammar with regex patterns for each statement type