Formally verified hardening of C programs against hardware fault injection
summary
Implements two control-flow hardening transforms over CompCert RTL and proves two properties in Coq proofs: semantic preservation (no behavior change without faults) and robustness under a fault-extended RTL semantics (any single fault is either detected or produces no observable effect). The pipeline integrates into CompCert, adds a new RTL pass framework, and is evaluated with Lazart symbolic fault injection: with optimizations off no single-fault escapes, with optimizations on some single-faults reappear but are mitigated by opaque copies; two-fault scenarios remain.
AI-written summary · about
chapters (9)
- 0:00Fault injection attacks
- 2:28Countermeasures
- 7:51CompCert compiler implementation
- 13:09Syntactic transformation
- 15:18Robustness proof
- 20:56End-to-end verification
- 23:00Compiler optimizations impact
- 24:25Future work
- 26:20Q&A
related talks
28mMemory simulations, security and optimization in a verified compiler
15mMy Journey in Secure Compilation
01h 13mHardware-Software Contracts for High Assurance with Applications to Side-Channel Security
24mVerification of Hardware and Software with Fuzzing and Proofs
12mAutomated Synthesis of Verified Firewalls
20mFSLH: Flexible Mechanized Speculative Load Hardening
01h 08mProviding evidence for the security properties of hardware/software codesigns
28mProving Memory Access Violations in Isabelle/HOL