Providing evidence for the security properties of hardware/software codesigns
summary
Argument: end-to-end proofs need empirical validation for real devices. The team builds an FPGA prototype of VRASED on an MSP430 core, uses F proofs of crypto from HACL and a NuSMV-checked hardware monitor, and still finds concrete failures: attacker-controlled initial stack pointer, a timing side channel in the wrapper, and a DMA-monitoring bug that leaks key bytes. Formal guarantees (memory safety, functional correctness, secret independence) hold locally but integration mismatches break them; recommend case studies, attack competitions and falsifiable assumptions*.
AI-written summary · about
chapters (19)
- 0:00Introduction
- 2:50Overview
- 4:20The introduction
- 6:20The field of secure compilation
- 8:45How low should we go
- 9:58The role of the lower layer
- 13:47Providing evidence for adequacy
- 17:03Models
- 19:00Secure Compilation
- 20:59Systems
- 27:54Case Studies
- 28:57Hacklestar
- 35:52Hackelstar assumptions
- 38:08Hackelstar overview
- 39:50Hardware Security Monitor overview
- 42:27Hardware Security Monitor examples
- 44:22Addressing dismissive comments
- 46:34Conclusion
- 50:27Questions
related talks
12mHardware Verification of Timing Side Channel Freedom in the Spectre Era
24mVerification of Hardware and Software with Fuzzing and Proofs
24mSystem Level Security Verification of RISC V Based SoCs
59mNationally Critical Infrastructure needs Secure Hardware
01h 13mHardware-Software Contracts for High Assurance with Applications to Side-Channel Security
44mHardware Security By Design
25mDemystifying remote attestation
01h 04mSoftware Verification meets Real-World Cryptography