Foundations of Hardware-Software Leakage Contracts

The gist: Hardware-software leakage contracts are an emerging security abstraction that characterizes side-channel leakage at the ISA level, enabling programmers and compilers to generate code provably resistant to side-channel attacks without explicitly reasoning about microarchitecture <ref:2610.20754#pg6>.

The Problem of Microarchitectural Attacks

Microarchitectural attacks such as Spectre and Meltdown undermine security by exploiting software-visible side effects of microarchitectural optimizations like caches and speculative execution <ref:2610.20754#pg9>. These features, including caches, deep pipelines, and various forms of speculation, are implemented to increase performance but may have software-visible side effects <ref:2610.20754#pg10>. Attacks exploit the fact that instructions may have vastly different execution latencies depending on the context in which they are executed. Measuring latencies of instruction or of entire programs thus allows attackers to gain information about the execution context, which may in turn depend on secret data <ref:2610.20754#pg4>.

Leakage Contracts as a Security Abstraction

Hardware-software leakage contracts aim to fill the void left by Instruction Set Architectures (ISAs) being ill-suited for secure programming because they abstract from microarchitectural details and fail to reflect their security consequences <ref:2610.20754#pg8>. These contracts specify at the ISA level what information a program may leak, serving as a rigorous foundation for writing programs that are resistant against microarchitectural attacks <ref:2610.20754#pg9>. They also provide a specification for hardware designers to ensure that microarchitectures do not introduce unintended and undocumented side channels <ref:2610.20754#pg9>. An informal contract might state, “For every multiplication the second operand leaks and for every memory access the memory address leaks” <ref:2610.20754#pg10>.

Formalizing Architectures and Microarchitectures

Architectures are modeled as state machines that define how execution progresses through a sequence of architectural states, formally defined as a pair (ArchState, Isa) where Isa: ArchState → ArchState is a transition function. Microarchitectures are modeled as state machines that define how the processor’s state evolves at cycle granularity, represented by a pair (ImplState, Impl) where Impl: ImplState → ImplState is a transition function modeling execution over one cycle. Microarchitectural states consist of an architectural part σArch and a microarchitectural part σµArch modeling components like caches and predictors.

Contract Atoms and Traces

Leakage contracts are defined as sets of contract atoms, which correspond to basic units of leakage. A contract atom is formally a pair A = (πA, ϕA), where the applicability predicate πA determines whether a contract atom is applicable in a given architectural state, and the leakage function ϕA specifies what information from the architectural state is exposed when the atom is applicable. A set of atoms S induces a contract LCS, which is a function from architectural states to sets of contract observations. The contract trace, LCS(Isa∗(σ)), denotes the sequence of contract observations associated with the execution Isa∗(σ).

Contract Satisfaction and Secure Programming

A microarchitecture Impl satisfies a contract LCS for attacker Atk if the attacker cannot infer more about the initial architectural state by observing Impl’s executions than what is revealed through the contract’s observations. This is formalized as Definition 2, requiring that for all states σ, σ′ with σµArch = σ′µArch and LCS(Isa∗(σArch)) = LCS(Isa∗(σ′Arch)), we have Atk(Impl∗ (σ)) = Atk(Impl∗ (σ′). Contract satisfaction is tightly connected to functional correctness, as microarchitectural execution must be consistent with the prescribed architectural execution for non-trivial leakage contracts.

Verifying and Synthesizing Contracts

There are methods to verify contract satisfaction, such as using inductive invariants synthesized using the Houdini algorithm or explicit state model checking. Alternatively, some recent work aims to synthesize software-level characterizations of microarchitectural leakage, such as ConjunCT and VeloCT, which determine a set of safe instructions that can be invoked with secret arguments without timing leaks. Furthermore, tools like Scam-V and Revizor are used to scrutinize post-silicon commercial processors by searching for inputs that are contract indistinguishable under one contract but distinguishable under a weaker one.

Secure Programming Paradigms

Secure programming aims to prevent confidential data from leaking to an attacker, which can be captured as non-interference w.r.t. a contract LCS. If a program is non-interferent w.r.t. a contract and the microarchitecture satisfies this contract, then non-interference transfers to the microarchitecture. This framework allows for capturing both sandboxing and constant-time programming paradigms as non-interference w.r.t appropriate policies and contracts.

Conclusion and Future Challenges

Leakage contracts act as a bridge between hardware and software, serving as a foundation for secure programming and a specification for the development of underlying microarchitectures. Significant open challenges remain, particularly on the hardware side regarding how to design complex high-performance processors that provably satisfy useful leakage contracts. This includes developing contract-aware hardware design methodologies and formalizing how data-independent timing instructions can be interpreted as leakage contracts. Future work may involve binary-level analysis platforms like Binsec for contract verification.

How it works

The paper introduces hardware-software leakage contracts as a new security abstraction to address the limitations of ISAs in reflecting microarchitectural security consequences <ref:2610.20754#pg9>. These contracts characterize side-channel leakage at the ISA level, enabling programmers and compilers to generate code provably resistant to side-channel attacks without needing explicit knowledge of the microarchitecture <ref:2610.20754#pg9>. They also provide a specification for hardware designers to ensure microarchitectures do not introduce unintended and undocumented side channels <ref:2610.20754#pg9>.

Key Components

The formalization models architectures as state machines defining execution through architectural states (ArchState) and microarchitectures as state machines defining evolution at cycle granularity using ImplState, which combines an architectural part with a microarchitectural part. Contract atoms are defined as pairs (πA, ϕA), where πA is the applicability predicate over ArchState and ϕA is the leakage function specifying what information from the architectural state is exposed. The contract LCS is then defined by evaluating each applicable atom in S according to LCS(σ):= ΣϕA(σ) (πA, ϕA) ∈ S ∧ πA(σ).

Contract Satisfaction

Contract satisfaction requires that for any two initial states that coincide in their microarchitectural components, if the contract traces are identical, then the attacker traces must also be identical. This is formalized as Definition 2, ensuring that the contract exposes at least as much information about the execution as an attacker can infer from its observations on the microarchitecture.

Decoupling Concerns

Theorem 1 shows that if a microarchitecture correctly implements an architecture, then contract satisfaction and microarchitectural contract satisfaction are equivalent. This decoupling allows for testing and verification to focus either on security or functional correctness. Secure programming is achieved by ensuring a program is non-interferent w.r.t a contract, which, combined with contract satisfaction, guarantees non-interference w.r.t the attacker on the microarchitecture.

1. Bold Header: ISA-Level Security Abstraction

This involves creating formal specifications for instruction sets that characterize side-channel leakage at the ISA level, enabling programmers and compilers to generate code that is provably resistant to side-channel attacks—without having to explicitly reason about the microarchitecture.

2. Bold Header: Provable Side-Channel Resistance

AI systems can be developed with formal guarantees by defining contracts based on instruction operands, such as the informal contract: For every multiplication the second operand leaks and for every memory access the memory address leaks. This allows verification tools to ensure that execution traces are independent of any secrets when a program is non-interferent w.r.t. a contract LCS.

3. Bold Header: Microarchitectural Contract Enforcement

The system can be designed such that it satisfies microarchitectural contract satisfaction (Definition 4), meaning Atk(Impl) = LCS(Implϕ), which ensures that the attacker cannot infer more about the initial architectural state by observing Impl’s executions than what is revealed through the contract’s observations.

4. Bold Header: Non-Interference Transfer

Secure programming can be achieved by ensuring that if Atk(Impl) = LCS(Isa) and P ⊢ NI(π,LCS(Isa)), then P ⊢ NI(π, Atk(Impl)), allowing security to be verified at the contract level rather than requiring explicit reasoning about the underlying hardware.

5. Bold Header: Speculative Leakage Mitigation

The system can incorporate speculative noninterference and speculative constant-time notions to detect and prevent leaks from speculative execution, addressing vulnerabilities like Spectre by modeling speculation explicitly in the architectural execution.