PROTECT - Proving Next Generation Secure Systems
PROTECT wants to use innovative methods of formal verification to raise IT security to a new level and sustainably strengthen trust in digital systems.
The project members are:
- German Research Center for Artificial Intelligence (DFKI)
- RWTH Aachen University,
- Cryspen SARL ,
- German Informatics Society ,
- RPTU Kaiserslautern,
- LUBIS EDA GmbH,
- University of Lübeck
Together, the PROTECT partners are developing solutions to make IT systems more resistant to cyber attacks against companies and public institutions. The approach is based on three strengths of the partners involved:
- Bottom-up instead of top-down. We combine the existing approaches of the partners involved, combining existing strengths instead of forcing project partners into a one-size-fits-all corsett. At the same time, this approach allows users to select the appropriate methods for their use case.
- Open source and open science. Our work is published as open source or open access, to make it as widely accessible as possible.
- Research-driven. All partners are well-established in their respective fields, and contribute this research excellence to the project.
Contributions to Formal Verification
The focus of the PROTECT project is security on the hardware/software interface. The key contributions are:
• Our partner Cryspen is developing tools to verify Rust programs, including the Hax toolchain and a verified cryptographic library for Rust.
• Partners RWTH Aachen and DFKI are developing virtual prototypes for early development and verification of software. They will be providing virtual prototypes of all reference systems, and investigate methods for seamless generation and verification of security properties using SAIL as an ISA specification language
• Partners RPTU Kaiserslautern, Universität zu Lübeck and Lubis EDA are developing methods to establish a secure micoarchitecture as a root of trust. Using formalized threat models, they develop security mechanisms across the HW/SW interface for a secure-by-construction design.
Demonstration Systems
PROTECT will deliver virtual prototypes of reference systems of increasing complexity, based on the open-source RISC-V architecture to showcase the methods. Starting with a basic system (RISC-V 32 bit without extensions) without an operating system, the project partners develop a medium system (RISC-V 32 bit with extensions) with a micro-kernel (such as seL4) and basic libraries (e.g. a crypto-library developed in Rust) which can be found in embedded settings, and a large sytem (RISC-V 64 bit) with a full operating system (such as Linux) used e.g. as a server. As they scale up the systems, they scale up the verification methods, allowing us to verify even large systems, with decreasing verification coverage if need be.
Community Building
PROTECT and ÖvIT aim to improve the applicability of formal verification. Networking for research and development is essential for this. The German Informatics Society (GI) operates networking and cooperation programmes to highlight synergies between project partners. The goal is to build an ecosystem for users, applicants and developers.
