- Status: Project phase
Background
As IT systems become increasingly complex, they also become more vulnerable to security-critical errors. Many of the most dangerous vulnerabilities in IT systems stem from a few fundamental issues. Conventional programming and testing methods can help avoid and identify many errors in hardware and software, but they are not foolproof.
This is where formal verification comes into play: using mathematical-logical methods, it is possible to prove that an IT system is completely free of security vulnerabilities that would violate previously defined security properties. Desired security properties are formally specified, and hardware and software are created in such a way that the properties can be mathematically proven to be fulfilled throughout.
However, the techniques involved require specialised knowledge even from computer scientists. Additionally, the methods for hardware and software of today’s complexity are not easy to use or to run in an automated way. Formal methods are currently used separately for hardware and software, often focusing on specific aspects of a system. There is currently no holistic approach 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.
The goal is for researchers to make formal verification possible for more complex systems, and in an automated fashion. The necessary basic research will be performed over a period of five to ten years, so that a follow-up project is expected to be necessary after the initial project of five years’ duration from 2024.
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 aim to bring systems with provable cybersecurity into widespread use, preventing security gaps from occurring in deployed hard- and software the first place. At the same time, the “Cybersecurity by design” approach should be more widely adopted. 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 provide a strong incentive for IT providers to quickly transfer the results into applications and products.
Projects
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.