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." > > https://dl.acm.org/citation.cfm?id=3321449
"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. _______________________________________________ coreboot mailing list -- [email protected] To unsubscribe send an email to [email protected]
