Compile time techniques for safer firmware
Published:
Provable Security in Embedded Systems: Verification Work in Tock OS
Tock OS secures millions of devices and uses language, architectural, and formal techniques to statically enforce system guarantees. This talk will go over how the Tock operating system eliminates many bugs that plague other OSes at compile time. I will demonstrate how we are mitigating logic bugs in Tock OS by using lightweight formal verification (Flux).
Watch now
Watch on YouTube Watch on Vimeo
Slides
Find the pdf of the slides and the source code for the slides and demo in this repo.
Connect with us!
Tock: safe embedded operating system
- Tock is open source!
- tockos.org
- Join Tock Slack, Matrix, and verification mailing list
Flux: scalable Rust verification
Proving should be as easy as programming
Share the presentation permalink: godsped.com/safe-firmware
I want to credit the amazing support and work on this project done by Pat Pannuto, Nico Lehmann, Evan Johnson, and Ranjit Jhala.
I must to give an enormous thanks to OSFC for sponsoring me to present. If you found this presentation interesting, you should consider going to the next OSFC!
