Class: SeccompTools::Symbolic::Executor

Inherits:
Object
  • Object
show all
Defined in:
lib/seccomp-tools/symbolic/executor.rb

Overview

Symbolic executor for classic BPF (the byte-code seccomp filters are written in).

A normal interpreter (see SeccompTools::Emulator) runs a program once with concrete inputs and follows the one path those inputs select. A symbolic executor instead keeps the inputs unknown (Expr) and explores every path through the program at once. Wherever the program branches, it walks both sides, remembering on each side the Constraint that made that branch taken. When a path reaches a return, the executor records a Leaf: the value returned plus the exact list of conditions that lead there. The collection of leaves is a complete, input-independent description of what the program does.

The machine model is classic BPF: two registers (A and X), 16 scratch-memory slots, and a read-only input buffer addressed by byte offset. Jumps are always forward, so a single walk with a visited-set terminates and never loops.

Examples:

# instructions come from `SeccompTools::Disasm.to_bpf(raw, arch).map(&:inst)`
leaves, truncated = SeccompTools::Symbolic::Executor.new(instructions).run
leaves.first.ret   #=> an Expr describing the returned value
leaves.first.path  #=> the Array<Constraint> under which it is returned

Defined Under Namespace

Classes: Leaf

Constant Summary collapse

STEP_CAP =

Upper bound on the number of states visited, so a pathological program cannot make the walk run unboundedly. When hit, #run stops early and reports truncated.

100_000
SPLIT =

Maps a comparison operator to the pair of Constraint operators implied on the taken and not-taken branches (e.g. a >= test learns >= if taken, < if not).

{
  :== => %i[== !=],
  :> => %i[> <=],
  :>= => %i[>= <],
  :& => %i[set unset]
}.freeze

Instance Method Summary collapse

Constructor Details

#initialize(instructions) ⇒ Executor

Returns a new instance of Executor.

Parameters:

  • instructions (Array<Instruction::Base>) —

    The program to execute, as SeccompTools::Disasm.to_bpf(raw, arch).map(&:inst). Only the duck-typed #symbolize method is used, so any classic-BPF instruction set works.



51
52
53
 
# File 'lib/seccomp-tools/symbolic/executor.rb', line 51

def initialize(instructions)
  @instructions = instructions
end

Instance Method Details

#run ⇒ Array(Array<Leaf>, Boolean)

Walks every path and returns the reachable leaves.

Leaves whose path condition is self-contradictory (e.g. A == 1 and A == 2 on the same word) are dropped - a conditional jump forks both ways regardless of feasibility, so the walk can construct paths that can never happen at runtime. See #feasible? for exactly what can (and deliberately cannot) be proven contradictory.

Returns:

  • (Array(Array<Leaf>, Boolean)) —

    The feasible leaves, and whether the walk was truncated at STEP_CAP.



63
64
65
66
 
# File 'lib/seccomp-tools/symbolic/executor.rb', line 63

def run
  leaves, truncated = walk
  [leaves.select { |leaf| feasible?(leaf.path) }, truncated]
end