{"id":3028,"date":"2023-09-06T09:49:18","date_gmt":"2023-09-06T07:49:18","guid":{"rendered":"https:\/\/www.cyberagentur.de\/projects\/ecosystem-formally-verifiable-it-provable-cybersecurity-oevit\/"},"modified":"2026-04-28T11:07:33","modified_gmt":"2026-04-28T09:07:33","slug":"evit","status":"publish","type":"project","link":"https:\/\/www.cyberagentur.de\/en\/programs\/evit\/","title":{"rendered":"Ecosystem Formally Verifiable IT \u2013 Provable Cybersecurity (EVIT)"},"content":{"rendered":"
    \n
  1. \n Status:<\/span>\n Project phase<\/span>\n<\/li>\n <\/ol>\n

    Background<\/h3>\n\n

    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. <\/p>\n\n

    Aim<\/h3>\n\n

    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. <\/p>\n\n

    Disruptive Risk Research<\/h3>\n\n

    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. <\/p>\n\n

    Projects<\/h6>\n\n

    <\/p>\n\n

    Formula-V (A foundational platform for fully-formally-verified systems design)<\/summary>\n

    Contractors: <\/strong>Barkhausen Institut (Dresden), TU Dresden, TU Berlin, Kernkonzept GmbH, Ferrous Systems GmbH, Fraunhofer AISEC<\/p>\n\n\n\n

    Project duration: <\/strong>12\/2024-12\/2028<\/p>\n\n\n\n

    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. <\/p>\n<\/details>\n\n

    PROTECT (Proving Next-Generation Secure Systems)<\/summary>\n

    Contractors: <\/strong>DFKI (Bremen), RWTH, Cryspen SARL, Lubis EDA GmbH, Gesellschaft f\u00fcr Informatik, RPTU Kaiserslautern, Universit\u00e4t zu L\u00fcbeckProject duration: <\/strong>12\/2024-12\/2028Project websites: <\/strong>DFKI<\/a>, German Informatics Society<\/a><\/p>\n\n\n\n

    PROTECT focusses on a compositional bottom-up-strategy, where different formalisms and approaches are combined into one unified system.The development of the project\u2019s 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. <\/p>\n<\/details>\n\n

    Dynamism, performance, and proof for complex cyber-physical systems<\/summary>\n

    Contractors: <\/strong>Kry10 (Wellington, NZ), Proofcraft (Sydney)<\/p>\n\n\n\n

    Project duration: <\/strong>08\/2024-08\/2028<\/p>\n\n\n\n

    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. <\/p>\n<\/details>\n\n

    Clash Formal (Provably Secure and Safe System Design with Clash)<\/summary>\n

    Contractor: <\/strong>QBayLogic (Enschede, NL)<\/p>\n\n\n\n

    Project duration: <\/strong>07\/2024-07\/2028Project website: <\/strong>QBayLogic<\/a><\/p>\n\n\n\n

    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. <\/p>\n<\/details>\n\n

    PISTIs-V (Protected Integrity and Security of Transmissions Integrating seL4 and RISC-V)<\/summary>\n

    Contractors: <\/strong>PlanV GmbH (Munich), UNSW Sydney, University of Gothenburg<\/p>\n\n\n\n

    Project duration: <\/strong>09\/2024-09\/2027Project website: <\/strong>PISTIs-V<\/a><\/p>\n\n\n\n

    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. <\/p>\n<\/details>\n\n

    Preliminary studies<\/h6>\n\n

    The \u00d6vIT call for tenders was based on the \u00d6vIT preliminary studies, which examined the research needs in the subject area in five batches.<\/p>\n\n

    Lot 1: Software Verification
    <\/summary>\n

    Contractor:<\/strong> FZI Forschungszentrum Informatik (Bernhard Beckert, Oliver Denninger, Jonas Klamroth, Max Scheerer, J\u00f6rg Hen\u00df)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. <\/p>\n\n\n\n

    Download \u00d6vIT preliminary studies lot 1 software<\/a><\/strong><\/p>\n<\/details>\n\n

    Lot 2: Hardware Verification
    <\/summary>\n

    Contractor: <\/strong>Rheinland-Pf\u00e4lzische Technische Universit\u00e4t (Wolfgang Kunz, Dominik Stoffel, Johannes M\u00fcller, 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. <\/p>\n\n\n\n

    Download \u00d6vIT preliminary studies lot 2 hardware<\/a><\/strong><\/p>\n<\/details>\n\n

    Lot 3: Verification of Software-Hardware Interfaces<\/summary>\n

    Contractor<\/strong>: <\/strong>Deutsches Forschungszentrum f\u00fcr K\u00fcnstliche Intelligenz GmbH (Christoph L\u00fcth, 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. <\/p>\n\n\n\n

    Download \u00d6vIT preliminary studies lot 3 ISA<\/a><\/strong><\/p>\n<\/details>\n\n

    Lot 4: Formal Security Guarantees for Trustworthy Hardware Supply Chains
    <\/summary>\n

    Contractor:<\/strong> Hensoldt Cyber GmbH (Dominik Sisejkovic, Lennart M. Reimann, Maja Malenko, Rainer Leupers)<\/p>\n\n\n\n

    Download \u00d6vIT preliminary studies lot 4 supply chains<\/a><\/strong><\/p>\n<\/details>\n\n

    Lot 5: Community and Ecosystem Development for Formal Verification of Basic IT
    <\/summary>\n

    Contractor<\/strong>: Hensoldt Cyber GmbH, ESMT BerlinFor 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. <\/p>\n\n\n\n

    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. <\/p>\n\n\n\n

    Download \u00d6vIT preliminary studies Lot 5 Community building<\/a><\/strong><\/p>\n<\/details>\n","protected":false},"excerpt":{"rendered":"

    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 […]<\/p>\n","protected":false},"featured_media":2946,"template":"","class_list":["post-3028","project","type-project","status-publish","has-post-thumbnail","hentry"],"acf":[],"yoast_head":"\nEcosystem Formally Verifiable IT \u2013 Provable Cybersecurity (EVIT) - Cyberagentur<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.cyberagentur.de\/en\/programs\/evit\/\" \/>\n<meta property=\"og:locale\" content=\"en_GB\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Ecosystem Formally Verifiable IT \u2013 Provable Cybersecurity (EVIT) - Cyberagentur\" \/>\n<meta property=\"og:description\" content=\"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 […]\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.cyberagentur.de\/en\/programs\/evit\/\" \/>\n<meta property=\"og:site_name\" content=\"Cyberagentur\" \/>\n<meta property=\"article:modified_time\" content=\"2026-04-28T09:07:33+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.cyberagentur.de\/wp-content\/uploads\/2024\/08\/Oevit.jpg\" \/>\n\t<meta property=\"og:image:width\" content=\"2304\" \/>\n\t<meta property=\"og:image:height\" content=\"1792\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/jpeg\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Estimated reading time\" \/>\n\t<meta name=\"twitter:data1\" content=\"9 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\\\/\\\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/programs\\\/evit\\\/\",\"url\":\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/programs\\\/evit\\\/\",\"name\":\"Ecosystem Formally Verifiable IT \u2013 Provable Cybersecurity (EVIT) - Cyberagentur\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/programs\\\/evit\\\/#primaryimage\"},\"image\":{\"@id\":\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/programs\\\/evit\\\/#primaryimage\"},\"thumbnailUrl\":\"\\\/wp-content\\\/uploads\\\/2024\\\/08\\\/Oevit.jpg\",\"datePublished\":\"2023-09-06T07:49:18+00:00\",\"dateModified\":\"2026-04-28T09:07:33+00:00\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/programs\\\/evit\\\/#breadcrumb\"},\"inLanguage\":\"en-GB\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/programs\\\/evit\\\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-GB\",\"@id\":\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/programs\\\/evit\\\/#primaryimage\",\"url\":\"\\\/wp-content\\\/uploads\\\/2024\\\/08\\\/Oevit.jpg\",\"contentUrl\":\"\\\/wp-content\\\/uploads\\\/2024\\\/08\\\/Oevit.jpg\",\"width\":2304,\"height\":1792,\"caption\":\"Oevit\"},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/programs\\\/evit\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Ecosystem Formally Verifiable IT \u2013 Provable Cybersecurity (EVIT)\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/#website\",\"url\":\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/\",\"name\":\"Cyberagentur\",\"description\":\"\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\\\/\\\/www.cyberagentur.de\\\/en\\\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"en-GB\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Ecosystem Formally Verifiable IT \u2013 Provable Cybersecurity (EVIT) - Cyberagentur","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/www.cyberagentur.de\/en\/programs\/evit\/","og_locale":"en_GB","og_type":"article","og_title":"Ecosystem Formally Verifiable IT \u2013 Provable Cybersecurity (EVIT) - Cyberagentur","og_description":"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 […]","og_url":"https:\/\/www.cyberagentur.de\/en\/programs\/evit\/","og_site_name":"Cyberagentur","article_modified_time":"2026-04-28T09:07:33+00:00","og_image":[{"width":2304,"height":1792,"url":"https:\/\/www.cyberagentur.de\/wp-content\/uploads\/2024\/08\/Oevit.jpg","type":"image\/jpeg"}],"twitter_card":"summary_large_image","twitter_misc":{"Estimated reading time":"9 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/www.cyberagentur.de\/en\/programs\/evit\/","url":"https:\/\/www.cyberagentur.de\/en\/programs\/evit\/","name":"Ecosystem Formally Verifiable IT \u2013 Provable Cybersecurity (EVIT) - Cyberagentur","isPartOf":{"@id":"https:\/\/www.cyberagentur.de\/en\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.cyberagentur.de\/en\/programs\/evit\/#primaryimage"},"image":{"@id":"https:\/\/www.cyberagentur.de\/en\/programs\/evit\/#primaryimage"},"thumbnailUrl":"\/wp-content\/uploads\/2024\/08\/Oevit.jpg","datePublished":"2023-09-06T07:49:18+00:00","dateModified":"2026-04-28T09:07:33+00:00","breadcrumb":{"@id":"https:\/\/www.cyberagentur.de\/en\/programs\/evit\/#breadcrumb"},"inLanguage":"en-GB","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.cyberagentur.de\/en\/programs\/evit\/"]}]},{"@type":"ImageObject","inLanguage":"en-GB","@id":"https:\/\/www.cyberagentur.de\/en\/programs\/evit\/#primaryimage","url":"\/wp-content\/uploads\/2024\/08\/Oevit.jpg","contentUrl":"\/wp-content\/uploads\/2024\/08\/Oevit.jpg","width":2304,"height":1792,"caption":"Oevit"},{"@type":"BreadcrumbList","@id":"https:\/\/www.cyberagentur.de\/en\/programs\/evit\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.cyberagentur.de\/en\/"},{"@type":"ListItem","position":2,"name":"Ecosystem Formally Verifiable IT \u2013 Provable Cybersecurity (EVIT)"}]},{"@type":"WebSite","@id":"https:\/\/www.cyberagentur.de\/en\/#website","url":"https:\/\/www.cyberagentur.de\/en\/","name":"Cyberagentur","description":"","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.cyberagentur.de\/en\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"en-GB"}]}},"_links":{"self":[{"href":"https:\/\/www.cyberagentur.de\/en\/wp-json\/wp\/v2\/programme\/3028","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.cyberagentur.de\/en\/wp-json\/wp\/v2\/programme"}],"about":[{"href":"https:\/\/www.cyberagentur.de\/en\/wp-json\/wp\/v2\/types\/project"}],"version-history":[{"count":13,"href":"https:\/\/www.cyberagentur.de\/en\/wp-json\/wp\/v2\/programme\/3028\/revisions"}],"predecessor-version":[{"id":5789,"href":"https:\/\/www.cyberagentur.de\/en\/wp-json\/wp\/v2\/programme\/3028\/revisions\/5789"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.cyberagentur.de\/en\/wp-json\/wp\/v2\/media\/2946"}],"wp:attachment":[{"href":"https:\/\/www.cyberagentur.de\/en\/wp-json\/wp\/v2\/media?parent=3028"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}