Skip to content

Home

Jump to bottom
Andrew Brown edited this page Mar 31, 2026 · 12 revisions

A tool to uncover and resolve the effects of weak memory on an aarch64 binary executable.

Approach

The approach the rif tool takes is:

  • Import the binary and lift it. End with a CFG of basic-blocks for the specified function.

  • Insert all instructions & basic-blocks into datalog.

    • Instructions are "ordered" based on where they fall within basic-blocks, and also by basic-block topological ordering within the control flow graph.

  • Datalog generates a relation between two instructions if theyare "reorderable"

    • This does not care about the execution context (i.e. if at runtime two registers carry the same pointer value), only the static syntax
    • Only memory operations are considered reorderable because we don't care about non-memory-operations.

  • Retrieve this relation.

  • For every reorderable pair

    • Decide, based on a user-provided spec, which aspects of the state are relevant. This is, essentially, partitioning the state based on uninterpreted predicates appearing in the specification. For more info on the spec, see Usage.

    E.g. for secret write, the spec is "secret(shared) ==> locked(lock)". So, the relevant aspects of the state are whether something is secret, whether something is locked, whether a memory-addressing-instruction aliases "shared", and whether a memory-addressing-instruction aliases "lock".

    • Generate all realistic combinations of these aspects of the state. E.g. both instructions will not alias the same "shared" or "lock" variable.

    • Further discharge possible precondition combinations based on an in-order execution. If the instructions do not uphold the guarantee when executing in-order, the precondition is assumed to be wrong. wrong

    • For all the valid precondition combinations, now, perform the verification that out-of-order behaviour is a subset of in-order behaviour.

Note that rif is agnostic to the particular logic in use. For example, the wpif logic makes use of gamma variables: these do not exist in rif

Syntax Guided Synthesis (SyGuS)

Syntax Guided Synthesis is the approach of solving SMT-like problems. Essentially, given some specification, can the tool produce a function that fulfils this specification? For more info on SyGus, read this.

Also, skolemisation is an approach to particular problems of the form "For all a,b, there exists x such that ...". Essentially, rather than supposing the existence of an 'x', you may write "There exists f(1,2) such that for all a,b, such that ..." and then within the '...', you can use f(a,b) in lieu of 'x'. You are moving the existential quantifier outside the forall by supposing the existence of a function returning 'x', rather than x itself.

In combination, SyGuS + skolemisation enables a particular approach to solving the SMT problems that RIF needs.

In general, RIF problems are of the form "For all out-of-order prestates, there exists a way for the in-order execution to still get to the same post-state(s)". The exact formal phrasing is dependent on the context, language, etc. that you're working with.

Skolemisation lets us express this as "There exists a function F, such that for all out-of-order prestates, the in-order execution gets to the same post-state(s), and F(state) represents the middle-state it goes via".

Now, we can use SyGuS to actually request that the solver invent the function F. In most cases, doing this (with SyGuS) will be easier than attempting to see if an SMT tool will deal with a "Forall a, Exists b" problem.

Problems

  • Spec language is hard to define on a per-instruction level. Reorder read with "take lock": how do I express what the "read" is? Taking a value from mem -> reg is hard to express.

  • Spec language is hard to define in general. "Rely that x goes to some power of 2" is hard (expressed currently as X goes to 2 ^ ???). "Rely that X goes to some secret value" is harder.

  • Compilers may optimise in a way that reintroduces concrete values. I.e. "write 0 to lock" could become str r1, [r0] (storing value r1 into memory-at-R0) and we would notice, via taint-analysis, that if r0 aliases lock, we should generate pre-states where r1 is locked or not-locked. However, what about str wzr [r0]? (wzr is the zero register that always containts 0.) This appears in ASL semantics as "Mem.set ( R0 , 0000000... )". Do we need to generate predicates for all "RHS of mem.set's" including immediates?

Future Work

  • Combine with BinCaml pipeline

    • Integrate Rob's pipeline semantics
    • Identify reordering on a sub-instruction level: instructions can reorder (pipelining) or memory operations can reorder (caching, dispatching)

  • Custom sliding-window to discern reorderable pairs instead of datalog

    • Configurable pipeline length? Configurable cache behaviour?
    • See above: consider sub-instruction reordering behaviours?
    • Avoid datalog quadratic blowup when adding more rules (e.g. x;y -> before(x,y) but x;y;z -> before(x,y);before(y,z);before(x,z))
      • Sub-point: potentially this is not the exact problem with datalog, however, for ~1000-instruction functions, datalog clearly becomes a bottleneck.

  • Nick's concept

    • Integrate wp / rg verification with the tool (sort of)
    • Inject rely/guar calls between all instructions
    • do WP pass to collect "required preconditions"
    • Start in a pre-state where these are true

Suggested approach:

  • Intake bincaml IR. Side quest: instruction address mappings (or custom non-BASIL frontend) for bincaml?

  • Develop mapping between Rob's pipeline semantics and bincaml IR statements/expressions

    • Side quest: some reordering is instruction-level (fetch/decode pipelining) and some is microarch-level (writing, caching, dispatch). It would be interesting to look at which approaches are more precise/scalable. Developing a good way to deal with this & testing it against a real ARM processor could be cool? possibly a paper?

  • Do sliding-window analysis system over IR w/r/t above mapping

    • possibly another paper? "analysis tool that is able to highlight reorderable instructions based on verified pipeline semantics"
    • Side quest: a good way of modelling (extensive) caches? e.g. L1/L2/L3 -- configure by cache line size? Eviction? Depending on which CPU the code runs on?
    • Could use a RISC-V verilog implementation for full-fidelity modelling
    • following this line of thinking, could reach out to ARM(?), research opportunities w/r/t use of their verilog models

  • Could rely on / augment bincaml infrastructure for WP pass

    • Side quest: boogie backend (or other backend) for bincaml (this is already being worked on IIRC?)
    • bincaml has to turn things into assertions anyway, so re-use this info, static analysis passes, etc
    • basically re-use everything that bincaml does, but on top of inserting assertions, do WP passes to determine the actual preconditions

  • Possibly retain state-splitting approach for more detailed error summaries

    • All relevant predicates that aren't already provided by the WP pass
    • e.g. secret write: rely: secret(x) ==> locked(y) | guar: secret(x) ==> x isn't printed may still need to partition state space by whether or not Y is locked Would produce better output if so: "this fails when Y is not locked but succeeds when it is locked"
    • The goal is to eliminate "I can't prove X because I don't know Y". The solver should always know Y or ~Y, in order to be able to tell the user which specific cases are problematic.

  • Dispatch problem to CVC5 as this tool does

    • The solver stuff that rif does is pretty watertight; it's the setup beforehand that could be massively improved

Clone this wiki locally