Thanks for sharing this. On Fri, May 17, 2019 at 6:44 PM ron minnich <rminn...@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-le...@coreboot.org > -- Tech III * AppControl * Endpoint Protection * Server Maintenance Buncombe County Schools Technology Department Network Group ComicSans Awareness Campaign <http://comicsanscriminal.com>
_______________________________________________ coreboot mailing list -- coreboot@coreboot.org To unsubscribe send an email to coreboot-le...@coreboot.org
