RedLeaf: Towards An Operating System for Safe and Verified Firmware

RedLeaf: Towards An Operating System for Safe and Verified Firmware
复制标题

DOI：
10.1145/3317550.3321449
复制
发表时间：
2019-05
期刊：
Proceedings of the Workshop on Hot Topics in Operating Systems
影响因子：
--
通讯作者：
Vikram Narayanan;Marek S. Baranowski;L. Ryzhyk;Zvonimir Rakamaric;A. Burtsev
Vikram Narayanan;Marek S. Baranowski;L. Ryzhyk;Zvonimir Rakamaric;A. Burtsev
中科院分区：
其他
文献类型：
--
作者：
Vikram Narayanan;Marek S. Baranowski;L. Ryzhyk;Zvonimir Rakamaric;A. Burtsev

文献摘要

被引文献

相似文献

Redleaf是一种新的操作系统，将从从头开始开发，以利用正式验证来实现可证明的安全固件。 Redleaf是用安全的语言开发的，生锈，并依赖于使用满意度模型理论（SMT）求解器进行正式验证的自动推理。 Redleaf在两个前提下建立：（1）Rust的线性类型系统即使对于具有最紧张的性能和资源预算（例如固件）的系统，以及（2）基于SMT的推理和由线性类型执行的指针纪律的组合，也可以实用语言安全。提供了一种独特的方法来自动化和简化验证工作，将其扩展到小型OS内核的大小。
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.