The Project ​

Cloud computing and ultra-fast communication infrastructures are the driving forces behind the profound digitization of society. The "Internet of Things" (IoT) connects physical objects – from autonomous vehicles to medical devices to smart grids – to the internet. However, to make this technology safe and trustworthy, new standards for privacy, integrity, and security must be established. Especially in a world where IoT systems are becoming increasingly autonomous, developing trustworthy and formally verified systems is crucial to prevent misuse and attacks.

Our project addresses this challenge by building a fully formally verified unikernel-based platform that serves as a new foundation for trustworthy IoT and cloud systems. We combine modern systems programming in Rust with state-of-the-art formal verification in the Rocq prover to create an integrated software and hardware stack with mathematically proven security, safety, and reliability guarantees. With a special focus on automation and usability, our project makes verified system development accessible to a broader community and aims to establish formal verification as a standard in future systems design.

Project Duration: 12/2024 - 12/2028

Project Coordination ​

Barkhausen Institut gGmbH ​

Formula-V is coordinated by the Barkhausen Institut (BI), an internationally recognized research institute conducting cutting-edge research on the trustworthiness of networked electronic systems. In an interdisciplinary and international team, we are jointly pursuing the goal of building a reliable foundation for the Internet of the future and enabling trust in digital technologies.

Project Partners ​

Ferrous Systems ​

Founded in 2018 in Berlin, Ferrous Systems is the leading provider of Rust-based software solutions for embedded and safety-critical systems. The company plays a key role in advancing Rust for use in regulated industries through the development of Ferrocene, the first open-source Rust compiler toolchain qualified to meet the highest automotive, industrial and medical standards. Ferrous Systems is an active contributor to the Rust Project and the embedded Rust ecosystem, and collaborates closely with industry partners to deliver reliable, memory-safe software solutions for high-assurance systems worldwide. It also offers training, consulting and long-term support to help development teams adopt Rust with confidence.

Fraunhofer AISEC ​

The Fraunhofer Institute for Applied and Integrated Security AISEC is considered one of the world-leading institution for applied research in cybersecurity. More than 230 highly qualified researchers develop customized security concepts and solutions for commercial businesses and the public sector, boosting the overall competitiveness of clients and partners. Fraunhofer AISEC designs solutions for enhanced data security and effective defense against cybercrimes such as corporate espionage and tampering attacks. The institute's portfolio ranges from embedded and hardware security, automotive and mobile security to security solutions for industry and automation. In addition, the cutting-edge test labs at Fraunhofer AISEC allow for evaluating the security of networked and embedded systems, hardware and software products as well as cloud and web-based services.

Kernkonzept ​

Kernkonzept is a specialist in secure and safe virtualization and operating-system technology, based in Dresden. Built on their own open-source L4Re technology – a scalable, microkernel-based operating system and hypervisor platform accredited up to GERMAN GEHEIM and Common Criteria EAL 4+ certified – they deliver system solutions with a minimal attack surface, real-time capabilities, and robust virtualization support. The deeply experienced operating-system engineers tailor these solutions to meet the demands of safety-critical markets like automotive, as well as high-assurance security, cloud servers, and embedded systems. Kernkonzept is dedicated to supporting customers with comprehensive, customized architectural consulting and engineering services to drive their success.

TU Berlin ​

TU Berlin is one of the leading research institutions in Germany and a member of the "Berlin University Alliance" excellence initiative. The research of the "Software and Embedded Systems Engineering" group primarily focuses on the design and quality assurance of embedded systems.

TU Dresden ​

The Seniorprofessorship Operating System Group at TU Dresden, led by Prof. Hermann Härtig, has been researching and developing operating system concepts for over 30 years. With a primary focus on microkernel-based systems, the group has made significant contributions on the areas of real-time, system security, virtualization and usability of microkernel-based systems. The group developed several variants of L4-based microkernel systems as well as the tile-based M3 security architecture. Several spin-offs out of the group contribute to an active operating system scene in Dresden.

Funding Acknowledgement ​

This project is financed by the Agentur für Innovation in der Cybersicherheit GmbH (Cyberagentur) as part of the program Ecosystem Formally Verifiable IT – Provable Cybersecurity (EVIT).

Contact ​

Project Manager: Dr.-Ing. Sebastian Ertel sebastian.ertel@barkhauseninstitut.org