Proof Assistants At the Hardware-Software Interface

on YouTube ↗56m

" summary

A working FPGA testbed implements a verified Internet of Things light bulb with an Ethernet card, a processor and software stack written in calk and proved with a Coq library comi and Bedrock compiler; a RISC‑V style spec (a small Haskell subset) anchors correctness so an infinite family of optimized processors (any number of cores, cache sizes) is proved to match the spec. Spectre-style timing leaks are addressed by a machine‑code symbolic executor that verifies Salsa20 compiled by GCC and by a new blue spec/KOICA clocking approach that preserves cycle‑by‑cycle timing. Industry uptake begins via a startup product line.

AI-written summary · about

" chapters (28)

1. 0:00Intro
2. 2:26Specification?
3. 3:36Key Layers of End-to-End Proof
4. 4:32Outline
5. 6:33An Open Instruction Set
6. 12:06Many Interpretations of Parameter Functions
7. 13:03Surprising Hardware Security Vulnerabilities
8. 15:22The Naive Solution - Turning Off Speculation
9. 16:01Community Response?
10. 18:37Programming: Software vs. Hardware
11. 21:41Threads & Shared Memory A Convenient (?) Fiction
12. 23:00Surprise: Not an "Array", a Distributed System!
13. 23:54A Cartoon View of Digital Hardware Design
14. 26:21Bluespec-Style Hardware Coding
15. 27:53Rules & Schedules
16. 29:31Bluespec-Style Modularity
17. 30:18A La Process Calculus
18. 31:11Stepwise Refinement
19. 32:17Proved for a Multicore Processor & Memory Sys.
20. 32:55Disappearing Specs
21. 37:01Less Leaky Software
22. 37:30Two Main Approaches to HW/SW Timing Security
23. 42:28Proved for a Simple Processor
24. 43:34Beware the Demonic Scheduler!
25. 44:33Ask the Developer for a Tree Scheduler
26. 46:38Enclaves: Goals & Nongoals
27. 48:07Phrasing Security
28. 48:50Conclusion

" related talks

• 24mStrong Formal Verification For RISC V: From Instruction Set Manual To RTLAdam Chlipala · 7th RISC-V Workshop 2017
• 21mThe New Verification Ecosystem that Supports RISC-V Verification fo...Lee Moore, John Sotiropoulos · RISC-V Summit 2022
• 09mBreaking the RISC-V Processor Customization Barrier with Formal VerificationSven Beyer · RISC-V Summit Europe 2024
• 21mMaking Concurrent Hardware Verification SequentialAdam Chlipala, Thomas Bourgeat, Jiazheng Liu · PLDI 2025
• 57mResearch on Different Time Horizons (and an Example with Machine-Checked Proofs)Adam Chlipala · PLMW @ PLDI 2025
• 11mDemo: More Than Point Tools: RISC-V SolutionsLarry Lapides · RISC-V Summit North America 2024
• 29mTowards Formally Verified Just-In-Time CompilationAurèle Barrière · CoqPL 2020
• 31mFormal SpecificationThomas Bourgeat · 8th RISC-V Workshop Barcelona 2018