Formula-V aims to create a fully formally verified system that meets the highest standards of security, privacy, and trustworthiness. To achieve this, the project integrates both software and hardware verification, laying a solid foundation for the digital technologies of tomorrow.

The project members are:

• Barkhausen Institut gGmbH
• Kernkonzept GmbH,
• Ferrous Systems GmbH,
• Fraunhofer AISEC,
• TU Dresden,
• TU Berlin

Formula-V uses formal methods, such as mathematical and logical reasoning, to ensure that systems behave exactly as specified. This goes beyond traditional testing, providing mathematical proof of correctness and eliminating entire classes of bugs and vulnerabilities before systems are deployed. The project embeds security and correctness at the design stage, advocating for the co-design of hardware and software with formal verification in mind from the outset. 

A key element of the project is the creation of a unikernel, a minimalist operating system architecture designed to run a single application. By incorporating only the necessary components, such as minimal file system support and networking capabilities, the design reduces the attack surface and optimizes performance. Each layer of the unikernel is subjected to formal verification, enabling rigorous guarantees of correctness and robustness across the system.

Verified parts of the Unikernel:

• File system and network stack, including drivers
• CHERI-based memory isolation for unverified code
• RISC-V processor, verified based on SAIL semantics
• Compiler for verified unikernel composition

To reach its goal, Formula-V set the following targets:

• Verified Unikernel Platform in Rust and Coq: Developing a unikernel written in Rust to meet high-performance demands, with formal verification carried out primarily in Coq. Verification targets include core components like the file system and network stack, along with their drivers. This provides a robust foundation for secure, minimalistic application environments.
• CHERI-Based Isolation for Unverified Code: Supporting the execution of unverified code securely by integrating CHERI capabilities. These are used to enforce fine-grained memory safety, allowing unverified components to run in isolation. The RISC-V base is formally verified based on semantics defined in SAIL.
• Hardware-Level Security with Formal Countermeasures: Introducing formally verified countermeasures against side-channel and transient execution attacks on the processor level. These are directly embedded into the hardware design and proven secure, further strengthening the overall system integrity.
• Automated Tooling for Unikernel Composition: Emphasizing automated tooling to ease unikernel development. A formally verified compiler adds isolation for unverified components where formal memory-safety guarantees are missing.
• Description of the most significant anticipated results of the project: The primary innovation of Formula-V is a gap-free formal proof encompassing the entire system from hardware to application logic. It delivers a unique, end-to-end approach to secure system development.