- Status: Project phase
Background
IT systems are becoming increasingly complex and therefore more susceptible to security-critical errors. Many of the most dangerous vulnerabilities of IT systems can be traced back to a few fundamental problems. Common programming and testing methods can prevent and find many errors in hardware and software, but not all of them. This is where formal verification comes into play: these are mathematical and logical methods that can be used to prove that an IT system is completely free of security vulnerabilities that would violate previously defined security properties. To do this, the desired security properties are formally defined and the hardware and software are consistently created in such a way that the properties can be mathematically proven to be fulfilled. However, the methods used require specialist knowledge, even from computer scientists. In addition, the procedures for hardware and software of today’s complexity are not easy or automated to apply. Formal methods are currently carried out separately for hardware and software, and often only for individual aspects. There is currently no holistic procedure that can prove the correct implementation of an entire IT ecosystem.
Aim
The EVIT program aims to research and develop technologies, methods, and tools for end-to-end formally verified software and hardware components. It also seeks to establish an ecosystem of developers and users. To this end, researchers aim to make formal verification automatically applicable to more complex systems in the future. The necessary basic research will extend over a period of five to ten years and can only be completed in a follow-up project.
Disruptive Risk Research
The new, end-to-end approach aims for wider adoption by emphasizing easier-to-use, automated, and modular methods and tools. Active community building is a key aspect of the program. From a scientific and technological perspective, the research program is highly ambitious and risky. A project for the holistic verification of complex hardware and software has not yet been successfully realised. If successful, common security vulnerabilities in many IT systems can be addressed during development already, regardless of whether the software and hardware being developed are standard office systems or whether they are hardened IT for critical infrastructure or national security. The results should lead to the widespread use of systems with demonstrable cyber security that prevent security vulnerabilities from occurring in the first place. At the same time, the “cybersecurity by design” approach is to be disseminated more widely. The new knowledge and the emerging ecosystem will directly strengthen Germany’s technological sovereignty. A federal procurement policy that formulates such an approach as a requirement would also be a strong incentive for IT providers to quickly transfer the results into applications and products.
Projects
Formula-V (A foundational platform for fully-formally-verified systems design)
Contractors: Barkhausen Institut (Dresden), TU Dresden, TU Berlin, Kernkonzept GmbH, Ferrous Systems GmbH, Fraunhofer AISEC
Project duration: 12/2024-12/2028
The aim of Formula-V is a fully formally verified IT system based on a unikernel operating system. The core goal is to verify software and hardware within the same verification tool set.
The verification efforts of the unikernel include the file system and the network stack with their respective drivers. The semantics of a RISC-V processor and the implementation of the unikernel will be transferred into Rocq (the proof assistant formerly known as Coq) for formal verification. Furthermore, countermeasures against side-channel and transient execution attacks will be introduced. To simplify the development of verified unikernels, a special focus lies on more automated tools for formal verification.
PROTECT (Proving Next-Generation Secure Systems)
Contractors: DFKI (Bremen), RWTH, Cryspen SARL, Lubis EDA GmbH, Gesellschaft für Informatik, RPTU Kaiserslautern, Universität zu Lübeck
Project duration: 12/2024-12/2028
Project websites: DFKI, German Informatics Society
PROTECT focusses on a compositional bottom-up-strategy, where different formalisms and approaches are combined into one unified system.
The development of the project’s reference system will be based on a RISC-V core which will be modelled with virtual prototypes (VPs). This allows early co-design and verification of software and hardware. New formal verification techniques for the HW and the HW/SW interface will allow to avoid transient execution side channel attacks.
The reference system is planned to have minimal complexity at the outset (RISC-V 32 bit, no operating system) and move to a medium size system (RISC-V 32 bit, Unikernel or Micro-Kernel based OS with Crypto module). In the ideal case, this can be extended to verifying (at least partially) a large system (RISC-V 64 bit, multi-core, Linux-class operating system).
An important part in this project is the community building, to design and facilitate a community of researchers, hardware and software developers and practitioners from industry.
Dynamism, performance, and proof for complex cyber-physical systems
Contractors: Kry10 (Wellington, NZ), Proofcraft (Sydney)
Project duration: 08/2024-08/2028
This project targets multi-core dynamically updatable systems, using formal methods to provide assurance. This project aims to develop a reference platform based on the seL4 microkernel, including a software development kit, a supported hardware configuration and a demonstration system to support industry transition. Additionally, tools and techniques supporting development and evaluation of critical cyber-physical system designs will be developed.
Clash Formal (Provably Secure and Safe System Design with Clash)
Contractor: QBayLogic (Enschede, NL)
Project duration: 07/2024-07/2028
Project website: QBayLogic
Clash Formal leverages the functional hardware description language Clash in combination with the functional programming language Haskell for the creation of safe and secure correct-by-design hardware, hardware-to-software interfaces and software within a single all-in-one description language and development environment. One goal is the direct integration of formal verification frameworks, like the language SAIL for describing the semantics of instruction set architectures as well as interfaces for proof assistants such as Coq into the Clash/Haskell compilers. The results finally are used to create a security token and an advanced smart card system demonstrator with formally verified security properties.
PISTIs-V (Protected Integrity and Security of Transmissions Integrating seL4 and RISC-V)
Contractors: PlanV GmbH (Munich), UNSW Sydney, University of Gothenburg
Project duration: 09/2024-09/2027
Project website: PISTIs-V
PISTIs-V aims to develop a reference embedded system that demonstrates end-to-end security and safety proofs and can serve as a starting point for industrialization. It is based on Lions OS, a new operating system built on the formally verified seL4 microkernel. The project will provide an approach to developing drivers for LionsOS and verify the drivers against a verified implementation of the device hardware. It will also verify other critical hardware components, including the fence.t instruction, a hardware mechanism enabling complete time protection, implemented in the CVA6 RISC-V processor. The verified properties of LionsOS will include proof that untrusted components can be confined, i.e. unable to leak information, including through microarchitectural timing channels, and moreover the schedulability of mixed-criticality real-time systems. A core aim of PISTIs-V is the easy re-verification of new drivers and policy modules required for porting the system to new platforms or adapting to new use cases; this will be enabled using push-button verification techniques.
Preliminary studies
The ÖvIT call for tenders was based on the ÖvIT preliminary studies, which examined the research needs in the subject area in five batches.
Lot 1: Software Verification
Contractor: FZI Forschungszentrum Informatik (Bernhard Beckert, Oliver Denninger, Jonas Klamroth, Max Scheerer, Jörg Henß)
Formal software verification methods can verify both functional and non-functional properties of software systems. In contrast to methods such as testing or debugging, they can guarantee that a software system does not exhibit any behavior that violates a certain property. As a result, they achieve a higher level of confidence. Formal verification of software has a long history in research, but has never made the transition to widespread industrial application. This study presents the state of the art in formal verification of software systems and makes recommendations for improving the state of the art and its industrial application.
Lot 2: Hardware Verification
Contractor: Rheinland-Pfälzische Technische Universität (Wolfgang Kunz, Dominik Stoffel, Johannes Müller, Mohammad R. Fadiheh)
This study provides an overview of methods of formal hardware verification with regard to relevant security goals for the basic IT elements in hardware at the microarchitecture level. From an analysis of common hardware weaknesses and the relevant security requirements for microarchitectures, we derive the aims of sign-off security verification. The study relates these aims to the state of the art in formal hardware verification and describes strengths and weaknesses of different methods and methodologies. This leads to research recommendations for the formal security verification of hardware.
Lot 3: Verification of Software-Hardware Interfaces
Contractor: Deutsches Forschungszentrum für Künstliche Intelligenz GmbH (Christoph Lüth, Dieter Hutter, Milan Funck, Jan Zielasko)
We report on the state of the art in the field of formal verification at the interface between hardware and software. After a systematic review of the literature of the last ten years, we can give an overview of the existing verified systems and verification tools. Verification methods have matured with verified operating system kernels, compilers and hardware, but there are still significant gaps, especially in terms of security; we describe these research needs and suggest directions for future research efforts.
Lot 4: Formal Security Guarantees for Trustworthy Hardware Supply Chains
Contractor: Hensoldt Cyber GmbH (Dominik Sisejkovic, Lennart M. Reimann, Maja Malenko, Rainer Leupers)
Lot 5: Community and Ecosystem Development for Formal Verification of Basic IT
Contractor: Hensoldt Cyber GmbH, ESMT Berlin
For the digital technological sovereignty of the Federal Republic of Germany, it is important to have demonstrably secure, high-performance alternatives to existing basic IT systems from third-party providers in order to be able to implement cyber-resilient complex IT systems in security-critical areas. The development of demonstrably secure basic IT and its application must be promoted by a corresponding ecosystem to be established.
The establishment and management of a suitable developer and user community is an important step on the way to an “ecosystem of trustworthy IT” with formally verified hardware and software. This paper examines the question of how a corresponding “formal verification of basic IT” community can be established and managed. To this end, the success and failure factors and the state of the art of building and managing such a community are examined in a literature review. The insights gained – supplemented by statements from an expert survey and observations of case studies – serve as a basis for developing a possible procedure for building and managing a developer and user community for “Formal Verification of Basis IT” (roadmap) and a vision for a future ecosystem growing from this.
If you are interested in the documents relating to the preliminary studies, please contact our library directly: bibliothek@cyberagentur.de.