"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."
Thanks for sharing this.
On Fri, May 17, 2019 at 6:44 PM ron minnich rminnich@gmail.com 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 _______________________________________________ coreboot mailing list -- coreboot@coreboot.org To unsubscribe send an email to coreboot-leave@coreboot.org
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.
well, I was not going to announce this until september, but events are moving faster than planned, and the paper forced my hand. I started looking into some new paths for firmware a few years back by messing about with the Rust-based tock kernel. It taught me a lot.
The project I will be more publicly announcing at the OSFC is called oreboot. oreboot is coreboot without 'C'. It's a downstream fork of coreboot. I started with coreboot because there's a huge amount of value in coreboot's directory layout, its many tools, and documentation, that should not be discarded
but, in oreboot: - I remove all the C code - I remove all Intel chipsets since the days of intel source code support are long gone - I remove anything that depends on a binary blob - and anything that tries to support binary blobs
And that's just a start. But a lot of stuff is gone.
The first target is RISCV-SPIKE, as that lightweight CPU has made so much possible in the last 5 years (including the idea of RAMPAYLOAD).
We could use some Rust expertise (I can barely spell C, must less Rust); if this interests you, please let me know. I don't want to clutter this list with oreboot discussions, so we may want to keep it separate unless there is interest.
Possibly at the workshop in 2 weeks we can spend some time establishing the proper way to code for oreboot.
Thanks
ron
On Mon, May 20, 2019 at 9:54 AM Jacob Garber jgarber1@ualberta.ca wrote:
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.
-
Jacob Garber -
R S -
ron minnich