Skip to content

Contract Tracing
Module rvzr/model.py
Public interface Model
Inputs TestCaseProgram, InputData
Outputs CTrace

Model

The Model executes test cases according to a leakage contract and produces contract traces (CTraces). These represent the information expected to leak during execution, including speculative execution.

Revizor supports two model backends:

  • Unicorn: This backend is based on the Unicorn CPU emulator. It implements the contract by hooking into instruction execution and memory access events. Documentation is provided in Unicorn Backend.
  • DynamoRIO: This backend uses DynamoRIO for dynamic binary instrumentation. It instruments the test case to insert hooks for tracing and speculation simulation. Documentation is provided in DynamoRIO Backend.

Both implement the same interface defined by the abstract Model class.

Contract Trace Representation

A CTrace is a sequence of typed observations representing leaked information:

CTrace
  └─ List[CTraceEntry]
       ├─ mem    Memory address
       ├─ pc     Program counter
       ├─ val    Data value
       ├─ reg    Register value
       └─ ind    Indirect branch target

CTraces use xxhash for fast equality checking, enabling efficient grouping into equivalence classes.