Provable Security in Embedded Systems: Verification Work in Tock OS

Main Room,

Learn about the cutting edge work that is happening in verifying isolation guarantees and timer correctness in Tock OS. Tock is an operating system written in Rust for low-power microcontrollers. You will learn about our progress proving that isolation guarantees are met by the system using formal methods.