RedLeaf: Towards An Operating System for Safe and Verified Firmware

HotOS 2019 screenshot

Abstract

RedLeaf is a new operating system being developed from scratch to utilize formal verification for implementing provably secure firmware. RedLeaf is developed in a safe language, Rust, and relies on automated reasoning using satisfiability modulo theories (SMT) solvers for formal verification. RedLeaf builds on two premises: (1) Rust’s linear type system enables practical language safety even for systems with tightest performance and resource budgets (e.g., firmware), and (2) a combination of SMT-based reasoning and pointer discipline enforced by linear types provides a unique way to automate and simplify verification effort scaling it to the size of a small OS kernel.

Citation

Vikram Narayanan, Marek Baranowski, Leonid Ryzhyk, Zvonimir Rakamaric, Anton Burtsev
RedLeaf: Towards An Operating System for Safe and Verified Firmware
Proceedings of the 17th Workshop on Hot Topics in Operating Systems (HotOS), 37--44, doi:10.1145/3317550.3321449, 2019.

BibTeX

@inproceedings{2019_hotos_nbrrb,
  title = {RedLeaf: Towards An Operating System for Safe and Verified Firmware},
  author = {Vikram Narayanan and Marek Baranowski and Leonid Ryzhyk and Zvonimir Rakamaric and Anton Burtsev},
  booktitle = {Proceedings of the 17th Workshop on Hot Topics in Operating Systems (HotOS)},
  publisher = {ACM},
  pages = {37--44},
  doi = {10.1145/3317550.3321449},
  year = {2019}
}

Acknowledgements

We thank the anonymous HotOS reviewers. This material is partially based upon work supported by Intel and the National Science Foundation under grants number 1837127 and 1837051.