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 <jgarb...@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." > > > > 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 -- coreboot@coreboot.org To unsubscribe send an email to coreboot-le...@coreboot.org
