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).
Recording will be posted here once available
Find 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
