Trustworthy software in the real world
summary
SMACCMPilot is a BSD licensed high‑assurance quadcopter autopilot that compiles 8k lines of autopilot code plus 10k lines of drivers into about 40k C and runs on small embedded RAM budgets. The talk claims formal proofs scaleable enough to eliminate classes of bugs citing seL4 (9k C lines, 13 person‑years, ~$127/line), demonstrates ivory for memory‑safe code and compile‑time metaprogramming, and shows practical testing tools like American Fuzzy Lop and symbolic execution finding real defects.
AI-written summary · about
chapters (26)
- 0:00Intro
- 1:24trusted: quadcopters
- 2:05trusted: spacecraft
- 3:17trusted: pacemakers
- 3:57"trustworthy" software
- 4:27kinds of assurance case
- 7:35machine-checkable coding standards
- 9:27runtime countermeasures
- 11:08fuzz testing
- 12:52symbolic execution
- 14:05randomized property testing
- 16:04proving properties
- 18:27pros and cons of property proofs
- 21:01equivalence proofs
- 24:08cyber-physical systems
- 24:19software vulnerabilities with physical consequences
- 24:36capitalism strikes again
- 25:06state of the art, May 2015
- 25:58DARPA HACMS program: air team
- 26:34embedded systems tough environments
- 28:05Ivory: a safe subset of
- 29:57Ivory: also great for metaprogramming
- 33:19Tower composition framework
- 34:55seL4: provable process isolation
- 37:07better living through formal methods
- 38:43questions?
related talks
01h 03mKEYNOTE: From quadcopters to helicopters
16mRISC-V Based Secure Flight Computer System
10mDemo: Secure and Open Source RISC-V Based Flight Computer
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
12mRISC V A New Zero Trust Model for Cyber Resilient Avionics
49mCompiling to preserve our privacy
01h 19mCrashing Drones and Hijacked Cameras: CyberTrust Meets CyberPhysical
33mU-Boot in the Fast Lane: Developing a Safety Test Framework for Automotive Applicati...