Ask Me Anything with Kathleen Fisher
summary
A DARPA program builds vehicles with formally specified components and runs red-team wireless attacks every 18 months; after replacing ad-hoc code with formal-methods generated code the red team cannot remotely take over the quadcopter, and on a larger Little Bird helicopter the seL4 microkernel partitions prevent a root-privileged malicious partition from breaking out during an in-flight test with pilots. An industrial proof pipeline for TLS maps high-level proofs to C and runs automatically about 967 times with only 3 manual fixes, showing scalable automation.
AI-written summary · about
chapters (13)
- 0:00Intro
- 2:05About Kathleen
- 8:09Helicopter Software Verification Project
- 12:31Formal Methods Training
- 16:19Improving Proof Automation
- 19:04Research
- 21:21DSLs
- 25:02Solutions
- 28:05Favorite roles
- 34:35From academia to industry
- 38:40Advice for switching roles
- 42:57Choosing tools
- 45:02Projects
related talks
24mDefeating the Transparency Feature of DBI
32mPanel Discussion: The AI Kernel...
56mProof Assistants At the Hardware-Software Interface
28mHelion: A High-level DSL for Kernel Authoring
16mTooling Design and Lessons Learned from Systematic Evaluations of the Preservation of(…)
59mTutorial: High Level Sail Overview
57mResearch on Different Time Horizons (and an Example with Machine-Checked Proofs)
20mFSLH: Flexible Mechanized Speculative Load Hardening