Hardware-Software Contracts for High Assurance with Applications to Side-Channel Security
summary
Presents three concrete hardware–software contracts and their implementations: the ASP execution contract plus compiler passes form Cerberus, a software-only defense that runs on current Intel/ARM-like hardware with LLVM passes (stack privatization, register cleaning, minimum-fence insertion) and reports 7–21% overhead on crypto; the ProtISA/Protean contract lets software program a hardware-tracked protection set via a one-bit prefix and two hardware mechanisms (pro_delay/pro_track) to achieve comprehensive, programmer‑transparent protection; and leakage functions plus SynthLC use template-driven LTL property generation and model checking to extract verified leakage signatures and reverse‑engineer leakage contracts (modulo bounded model checking limits).
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:23Hardware side-channel attacks
- 3:53Constant time leakage contracts
- 8:08Transient execution and Spectre
- 12:43Hardware-software cooperation
- 15:53Cerberus: Spectre defense
- 28:28Limitations of Cberus and motivation for Proteum
- 30:32Proteum: Transparent defense
- 41:08SynthLC: Verifying contracts
- 55:16Broader implications
- 57:50Q&A
related talks
18mHardware-Software Codesign for Mitigating Spectre
01h 08mProviding evidence for the security properties of hardware/software codesigns
23mHardware security for critical national infrastructure
21mSecuring Tomorrow’s Hardware: Dual-State Models in the AI Era
12mHardware Verification of Timing Side Channel Freedom in the Spectre Era
46mRethinking Architectures and Abstraction for a World Where Security Improvements Matter More than Performance Gains
44mHardware Security By Design
06mRISC-V Spotlight: Avoiding Murphy's Law and Satan's Law Without Selling your Soul