Abstract
The constant-time discipline is a software-based countermeasure used for protecting high assurance cryptographic implementations against timing side-channel attacks. Constant-time is effective (it protects against many known attacks), rigorous (it can be formalized using program semantics), and amenable to automated verification. Yet, the advent of micro-architectural attacks makes constant-time as it exists today far less useful.
This paper lays foundations for constant-time programming in the presence of speculative and out-of-order execution. We present an operational semantics and a formal definition of constant-time programs in this extended setting. Our semantics eschews formalization of microarchitectural features (that are instead assumed under adversary control), and yields a notion of constant-time that retains the elegance and tractability of the usual notion. We demonstrate the relevance of our semantics in two ways: First, by contrasting existing Spectre-like attacks with our definition of constant-time. Second, by implementing a static analysis tool, Pitchfork, which detects violations of our extended constant-time property in real world cryptographic libraries.
Methodology
- A model to incorporate speculative execution.
- Abstract machine: fetch, execute, retire.
- Reorder buffer => out-of-order and speculative execution
- Directives can be initiated to model the detailed schedule of the reordered micro-ops
- Observations are also modeled in such process to mimic the leakage visible to the attacker
- Modeled instructions:
op,fence,load,store,br,call,ret
Artifact
- Symbolic execution based on angr
- Schedule the worst case reorder buffer => maximize potential leakage
- Can indeed found threat
Comments
- Are the threats confirmed by the developers?
- Is the model formalized in a proof checker?
- Execution time of instructions is not modeled? (or need not to be modeled?)