nordisk/heimdall

Part 2 of 5 of docs/v2/graph-filter.md (generated; edit the source)

3. Graph mode (new)

Step 2. The static analysis gives the graph

The graph is Mímir's lossless graph, and this design assumes it exists. It is defined in the graph plan (nornir docs/v2/mimir/exec-graph-plan.md at 03662cb4). This design uses:

• Nodes: the boundary sites B, one per call of a foreign function or raw syscall, per instance of the code (plan §4.1, §8). λ(s) comes from the libc map. Arguments are given where the code fixes them, for the same eleven calls the profiler records (plan §4.4).
• Edges: Next, with First(e) per entry (plan §4.3; files exec.nodes, exec.edges).
• Entries: main, each thread and task body, each signal handler (plan §4.5). The async executor is ordinary code in the graph, and a coroutine keeps its yield points (plan D2). So where two futures can run in either order, Next holds both orders.
• The projection { λ(s) : s reached } has the shape of today's graph.json (plan §4.6). Static mode's step 2 reads it unchanged. One graph serves both modes.

"1:1 with the code" means the Rust code. A C function is one node whose λ is a set (plan D4); section 10 says what follows from that.

Step 1. The profiler checks the graph

The profiler runs the program as today and also records, per thread, which call follows which (section 7). A pair (a, b) means: b is the next call after a in the same thread. Base-set and vDSO calls are not seen and are in no pair. Two numbers, on nodes and on pairs:

Obs  = classes observed          Static  = ⋃ λ(s) over reached sites
Obs₂ = pairs observed            Static₂ = { (a, b) : ∃ (s, s') ∈ Next, a ∈ λ(s), b ∈ λ(s') }
                                           ∪ { (a, b) : a, b ∈ λ(s), s can make several calls }

soundness   S  = |Obs  ∩ Static|  / |Obs|       S₂ = |Obs₂ ∩ Static₂| / |Obs₂|     must be 1.0
precision   P  = |Obs  ∩ Static|  / |Static|    P₂ = |Obs₂ ∩ Static₂| / |Static₂|  rises with coverage

An empty denominator is "no data", never 1. "Before anywhere in the run" would not work as the definition of a pair: in a loop, every call comes before every other after one round.

Every difference is a finding:

The goal: the static analysis gets so good that profiling only confirms it, 100 %. S = S₂ = 1.0 is required before a graph is enforced. P and P₂ reach 1.0 only for code the runs fully cover.

Step 3. The graph filter

The three parts.

The floor is the filter of section 2: always = I ∪ F, never = everything else. The brokered set is what the broker serves today: the open calls (openat, openat2, and on x86_64 open and creat), socket, connect, bind, listen, accept, accept4, io_uring_setup, sends with MSG_FASTOPEN, and exec (crates/heimdall-broker/src/filter.rs:27-44, 64-96). Today the broker opens files and sockets itself, lets exec continue, and refuses the others (broker.rs:409-427).

The decision. A position is the set of sites the thread's last call can have come from. It is a set because the kernel side sees a call's class and not its site, and two sites can make the same call. A thread's state is a stack of positions: its own entry at the bottom, and one frame on top for each signal handler that is running on it.

frame f = (e, P, last)     an entry e, the position P on it, the class of the frame's last call
state of thread t          ⟨f₀ … f_k⟩, at most 8 frames;  f₀ = (the thread's entry, {ε}, none)
H                          the signal-handler entries of the graph

step_e(P, c) = { s' : c ∈ λ(s') ∧ ( (ε ∈ P ∧ s' ∈ First(e)) ∨ ∃ s ∈ P : (s, s') ∈ Next
                                    ∨ (s' ∈ P ∧ s' can make several calls) ) }

decide(⟨f₀ … f_k⟩, event), on the top frame f_k:
  call c ∈ I                     valid; no position moves; rt_sigreturn pops f_k when k > 0
  call c, step(P_k, c) ≠ ∅       valid; P_k := step(P_k, c), last_k := c             (next)
  call c = last_k                valid; nothing moves             (again: the self-edge s → s)
  signal delivered, handler h    h ∈ H and k < 7: push (h, {ε}, none);  otherwise invalid
  thread created                 the parent's clone is a next step to a spawn site of the graph;
                                 the child starts as ⟨(the entry that site spawns, {ε}, none)⟩
  anything else                  an INVALID STEP

allowed(stack) = I ∪ { c : decide(stack, call c) is valid }

• Every call the floor lets through is followed, the always calls too. So the order of all calls is checked, at the cost of one small program run per call and no context switch.
• Brokered calls are followed too. Seccomp ends a brokered call that the supervisor answers itself, so it never reaches the entry tracepoint. The follower steps it at the exit tracepoint, which the kernel runs for every call (section 8, kernel facts).
• Again. The kernel can restart an interrupted call: the same call enters the kernel a second time, or restart_syscall does for a timed wait. A program can also retry after EINTR. So the same call again from the same position is always valid. A restart needs no handler; a stop or io_uring task_work is enough (crates/heimdall-seccomp/src/base.rs:10).
• Signals. A handler can start between any two calls of a thread. The follower sees the kernel's signal-delivery tracepoint, which carries the handler's address, and pushes that handler's entry on top of the interrupted position. Calls inside the handler follow the handler's part of the graph. A second signal nests one more frame. rt_sigreturn pops, and the thread continues from the interrupted position, where the interrupted call may come again. restart_syscall and rt_sigreturn are base-set calls: never invalid, and they move no position, except that rt_sigreturn pops.
• The stack is bounded: 8 frames, the thread's own and 7 handlers. A ninth is an invalid step. So is a handler the graph does not have.
• Threads. A new thread's first frame is the entry the graph gives for its spawn site (the plan's spawn marks, §2.3, §4.5). The parent must be at a position with an edge to that site. A spawn the graph does not have is an invalid step.
• Async. Position is per kernel thread. A worker thread's entry is the executor's loop, and each task's poll body is a callee of it, so at a scheduling point allowed is the union over the tasks that can run. That is sound and costs precision. Task tags written by the program are not used: an attacker in the process can write them.
• Widening. Only dyn and fn-pointer call sites are widened, and only to the vtables and pointers the reached code creates (plan §3.3). A reached C function that the boundary map has no answer for is not widened to every call. It is a finding that blocks graph mode for that program, which stays in static mode.
• In the kernel, the stack lives in task-local storage (a hash map keyed by thread where a kernel lacks it), and Next in a map. eBPF cannot walk a set of sites, so the loader makes the graph deterministic first: one state id per reachable position, and a map from (state, class) to state. A graph that outgrows the map is refused at load. The loader also maps each handler's address to its entry, from the program's symbols.

Enforce and Audit are a field of the policy.

• Enforce. An invalid step kills the process (bpf_send_signal).
• Audit. An invalid step is written to a ring buffer and counted, and the call runs. Audit never returns an error to the program, because that would change its behaviour. Audit is how a new graph is tried on a real workload first.

The kill is late by at most one call. At the entry tracepoint the follower cannot stop the call. The invalid call itself runs, and the thread never returns to user space. The floor guarantees that this one call is a call the static filter allows anyway. Where an LSM hook exists for the operation (open, connect, bind, exec, mmap), the refusal comes before the call: the follower marks the thread at the entry, and the hook refuses while the mark is set.

Four properties, each a property test:

(G1) every run of the code is valid: each frame's calls follow its entry's graph (pairs ⊆ Static₂),
     while handlers start between any two calls, nest and return, and an interrupted call comes again
(G2) graph mode is never wider than static mode: the floor answers first, and allowed(stack) ⊆ I ∪ Static
(G3) the base set is never invalid, at any stack, and it moves no position (rt_sigreturn only pops)
(G4) Audit changes nothing in the program: no call fails, and no call waits for user space

What falls out of the graph.

• Phases are regions of the graph: before the entry's serving loop, the loop, after it (plan §4.5). Once the position is in the loop no path leads back, so setup calls are no longer in allowed.
• Budgets are sites outside every loop. A site on no cycle of Next that makes one call can be passed once per path, plus the same call again in place. "io_uring_setup at most N times" is the number of such sites on the longest path. A site in a setup loop can repeat while the position is in that loop, and never after.

This replaces the earlier design of the two deleted plans: named phases, a stacked filter per mark, and counted "pledge budgets", with no order inside a phase. That design was a workaround for a lossy graph that had no order. With the 1:1 graph, phases and budgets are not separate mechanisms. They fall out of following the graph.

Dataflow, graph mode

 code ─► Mímir (lossless MIR, instances) ─► mimir-exec ─► (2) THE GRAPH  exec.nodes, exec.edges
                                                               │   B, λ, First, Next; arg facts
                    ┌──────────────────────────────────────────┤
                    ▼                                          ▼
 runs ─► (1) PROFILER  per thread: pairs (a, b)        import + validate, digest
              │  Obs, Obs₂                                     │
              ▼                                                ▼
         graph check: S, P, S₂, P₂, findings ─────►  accepted only with S = S₂ = 1.0
              │ findings                                       │ loader: states, maps
              ▼                                                ▼
   analyzer fix + test  /  add a run        (3) AT THE SYSTEM-CALL ENTRY, for every call
   (back to Mímir or to the runs)
                                             seccomp floor (static mode's filter)
                                                never    → KILL
                                                brokered → USER_NOTIF ─► supervisor: open, inject fd
                                                always   → ALLOW
                                                    │ every call the floor let through
                                                    ▼
                                             graph follower (eBPF): stack(t), decide
                                                valid   → the position advances
                                                invalid → Enforce: kill    Audit: log, count, run
                                                    │
                                                    ▼
                    signed record: mode, Enforce or Audit, floor digest, graph digest, violations

Next: part 3 of 5, raw: https://www.gunnar.rs/nordisk/heimdall/raw/docs/v2/graph-filter-parts/part-3.md