"An integer overflow caused $370M to vaporize in 40 seconds."
When a rocket exploded in flight because of two simultaneous integer overflow in independently written systems.
Luckily the industry has learned from this, right? Not really, with some Boeing planes having to be rebooted every 51 days to prevent catastrophically wrong information being shown to pilots.
This is Samir's talk on Tock OS, or how to secure firmware at compile time.
In TockOS, drivers are called Capsules, written in safe-rust, and selected to be built-in (and trusted) at compile-time. Every capsule has static memory usage.
Capsules are isolated from each other: they can be buggy, and won't crash the system.
While the OS is written in Rust, and this solves many issues, Logic Bugs still exist. And in general those are difficult to find.
And to address this, "lightweight formal verification" is used, with a tool called Flux.
Flux is formal verification tool that allows progressive verification of existing code. It uses Rust macros to add conditions on input and output variables of a function: preconditions and postcondition invariants.
This type of refinement on variables that flux provides is called "liquid types", or types + decidable logical predicates.
Samir also used Flux to catch a bug on an rv32 microcontroller where a process was attempting to access a memory region it didn't have the right to. And this can be caught at compile time.
In Summary, Rust + Tock OS Architecture + Lightweight verification is a solution to provide safe firmware.
Anisse
Jarkko Sakkinen