KEYNOTE: From quadcopters to helicopters

on YouTube ↗01h 03m

" summary

DARPA’s HACMS program demonstrates that co-developed formal methods can harden vehicles: researchers replace RTOS and flight code with seL4 microkernel and domain-specific generated C, use CompCert verifying C compiler, Isabelle/Coq proofs and SAT/SMT automation, and produce ~80k lines of high‑assurance code in 16 months. A red team with full documentation fails to take over the quadcopter and later the Boeing unmanned little bird; initial DARPA budget is about $70M for the program.

AI-written summary · about

" chapters (4)

1. 0:00Start
2. 33:51Formal Method Based Tools
3. 42:25Performance Consequences
4. 48:31Lessons Learned

" related talks

• 39mTrustworthy software in the real worldJamey Sharp · Open Source Bridge 2015
• 41mKeynote:Bend the Machine: The Hacker Path to Autonomy in the Real WorldDavid Brumley · CODE BLUE 2025
• 44mThe seL4 Foundation – growing through upheavalGernot Heiser · linux.conf.au 2022
• 15mHACCLE: Metaprogramming for Secure Multi-Party ComputationTiark Rompf, Roopsha Samanta, Donghang Lu, Aniket Kate, Yuyan Bao, Benjamin Delaware, Qianchuan Ye, Kirshanthan Sundararajah, Christopher Wagner, Nouraldin Jaber, Jeremiah Blocki, Raghav Malik, Christina Garman, Fei Wang, Mohammad Hassan Ameri, Alexander Seto, Pierre-David Letourneau, Benoit Meister, Jonathan Springer, Milind Kul · GPCE 2021
• 16mRISC-V Based Secure Flight Computer SystemShreekant Thakkar · RISC-V Forum: Security 2021
• 01h 19mCrashing Drones and Hijacked Cameras: CyberTrust Meets CyberPhysicalJeannette M. Wing · USENIX Security '16
• 17mLow Code/No Code Design Paradigm for Multi-OS CockpitsPhilipp Michel · emBO++ 2023
• 01h 05mKeynote: Can we reason about the security of concurrent systems code?Peter Sewell · PriSC 2024