Provable Security in Embedded Systems: Verification Work in Tock OS

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.

I am a graduate student at UC San Diego working on verifying Tock OS, an OS for embedded systems written in Rust. Tock OS is widely used for root-of-trusts. Tock supports process isolation.

Verification allows a path to eliminating million dollar bugs and make sure your system behaves the way you expect. Formal methods are going to make sure that we can trust systems. We show that verifying your software is possible with low line-of-code overhead.

Testing code such as timers/alarms is very error prone and requires invasive instrumentation or imagining every possible edge case. I will show how you can statically analyze your code with formal methods. At compile time, you know your code does not violate any properties and works correct in every possible execution. I will show you some crazy bugs I have discovered in timing code that can be completely eliminated.

Content of the talk:

• What is Tock OS
  • OS for resource contrained systems (microcontrollers) written in a high level language
  • used in industry by Google, HP, WD
• Software Verification is here
  • Now is the time for verifying our systems are safe. We are using Verus and Flux to prove that system guarantees of isolation and correctness are met.
  • Verifying properties of our Rust OS has low overhead and does not require reimplementing the whole system. Rust+verification eliminates memory errors and logic errors for critical systems such as the root-of-trust use case.
• Our Approach
• Examples of bugs caught
  • Developers have more confidence in implementing optimizations and accepting code changes in PRs.
  • I have found bugs that are virtually impossible to find by reading the code. We will take a look at previous security bugs in Tock, how we came up with system properties to verify, and show how these problems are now impossible produce.
• Some technical explanation on how verification works and the methods we have used.
• Verification
  • Formal methods have been coming for a long time, and they are here to stay. With our work, I hope to show that proving system properties is doable for a microkernel. I will show our future work and paths for current software to become more safe and more understable via formal methods.
• Tock is open source! Freely use it for whatever you want.