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.