"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.

#OSFC #OSFC2024 #TockOS #RustLang

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.

#OSFC

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.

#OSFC

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.

https://github.com/flux-rs/flux

#RustLang #OSFC #OSFC2024 #Flux

This type of refinement on variables that flux provides is called "liquid types", or types + decidable logical predicates.

#OSFC

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.

#OSFC

In Summary, Rust + Tock OS Architecture + Lightweight verification is a solution to provide safe firmware.

#OSFC #RustLang #TockOS

In answer to a question, Samir shows that Flux uses an SMT solver (Z3) to do the verification of all invariants.

And it can also be combined with runtime invariant checks (assert), which flux understands.

#OSFC #Flux

@Aissen Thanks I did not know about Tock OS :-) I'm quite familiar with this hardware real-time framework RTIC: https://rtic.rs/2/book/en/

I'll check this out for sure. Will the presentation be available online at some point?

@jarkko It will be, later today, at https://godsped.com/safe-firmware/

@jarkko there was also a question about the difference with Hubris (another Rust RTOS from @oxidecomputer ) which you might have heard about.

A few company already use Tock, like Google, Microsoft, and others. It has been available for 10 years, and stable for a few years already.

#TockOS #OSFC

@Aissen @oxidecomputer Cool. I'll need to ping my friend Phil who works at Oxide Computer and ask about that. Did not know about it.

I think Rust is really good cure for stuff that has been previously written with C on bare metal (with no OS whatsoever).