On Fri, May 17, 2019 at 03:43:43PM -0700, ron minnich wrote:
"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."
"To make things worse, modern firmware is fundamentally insecure. The software engineering technology behind the platform firmware has remained unchanged for decades. Modern firmware is developed in a combination of low-level assembly and an unsafe programming language, namely C. (Several rare exceptions demonstrate applications of fuzzing and symbolic execution [24,40].) Typical firmware both ad-heres to multiple low-level hardware specifications and implements functionality of a minimal OS, i.e., implements multiple device drivers and sometimes even provides support for file systems and network protocols [27,28,43]. Due to such inherent complexity, bugs and vulnerabilities are routinely introduced in the omni-privileged firmware."
Is there interest in using more formal methods in Coreboot? For example, I know gfxinit is written in Ada SPARK, and certainly some of the Coverity bugs I look at would benefit from using a stricter programming language.