Foundations of Hardware-Software Leakage Contracts

What it is

Jan Reineke's tutorial-style paper formalizing hardware-software leakage contracts. The fetched text covers the motivation, the architecture/microarchitecture models, and the start of the contract definition. The page cuts off at the definition of contract atoms, so the secure-programming (Section 4) and verification/synthesis material is not in what was fetched.

How it works

Contract as an observation trace. A contract interprets a program instruction by instruction and emits observations. Two executions an attacker can distinguish must produce different contract traces. The paper's example contract is: "for every multiplication the second operand leaks and for every memory access the memory address leaks."

Worked examples under that contract (Fig. 1).

• (b) input * secret: vulnerable, since the trace exposes the secret operand.
• (d) Mem[secret] then Mem[input]: vulnerable, since the trace exposes both addresses.
• (a) secret-dependent busy-wait: vulnerable, because the traces differ in length.
• (c) secret-dependent branch returning 23 or 42: judged secure under this contract, which exposes no branch observations.
• (e) the Spectre V1 variant: also judged secure, since the traces are independent of secrets.

(c) and (e) are secure under this particular contract only. The paper notes (c) leaks on most in-order pipelines via the branch outcome or instruction-cache effects, and (e) leaks on speculative processors. A contract that does not model branch outcomes or speculation therefore does not describe those machines. The paper does not discuss this in the fetched portion.

Formal pieces.

• An architecture is (ArchState, Isa), with one transition per instruction.
• A microarchitecture is (ImplState, Impl), with one transition per cycle. ImplState = ArchState × µArchState.
• Functional correctness uses ISA compliance (Wang et al.) via a retirement predicate φ.
• A contract is a set of atoms. Each atom is a pair (π_A, φ_A): an applicability predicate over architectural state and a leakage function that gives the exposed observation.
• Soundness: a microarchitecture satisfies a contract if it captures all leaks.

Preconditions / Affected

• Secure programming under a contract is only meaningful if the target microarchitecture satisfies (is sound for) that contract.
• Satisfaction is practically coupled to functional correctness, so the paper says non-trivial contracts cannot be satisfied by an incorrect implementation.
• Formal ISA specs are a practical prerequisite. ARM publishes a machine-readable ARMv8-A model in ASL. x86 is only informally specified, and no academic formalization has been adopted by Intel or AMD.
• Verification research targets open RISC-V cores, because commercial microarchitectures are closed source.

Caveats

• The paper states vendors do not release microarchitectural specs detailed enough to guarantee security.
• It argues side-channel security cannot be achieved purely in hardware: example (a) leaks on any microarchitecture.
• Nothing actionable is given in the fetched text: no tool, command, benchmark, or verified processor. The verification and synthesis techniques are only promised for Sections 3-4, which were not retrieved.