Ecosystem Formally Verifiable IT – Provable Cybersecurity (EvIT)
IT systems are becoming more complex and prone to security-critical errors. Many vulnerabilities can be traced back to a few fundamental errors. Common programming and testing methods can prevent and detect many errors in hardware and software, but not all of them.
This is where EvIT comes in: We use formal verification and mathematical-logical methods. This allows us to prove that an IT system is completely free of security gaps that would violate previously defined security properties. The desired security properties are formally recorded, and hardware and software are consistently created in such a way that the properties are mathematically provably fulfilled. Formally verified software and hardware are verifiably secure and error-free within the scope of the specifications. This makes them particularly suitable for use in critical infrastructure systems such as ICT, mobility, or military systems.
EvIT aims to establish a network for research, application, and development in the field of formal verification. In building a scientific community, experts will connect with young professionals and interested parties from industry to advance the applicability of formal verification in a targeted manner. We invite interested parties to become members of our ecosystem.
"Testing shows the presence, not the absence of bugs" (Dijkstra, 1969). Formal verification operates on a different level than testing: it examines the source code completely and at the most fundamental level. This eliminates errors and vulnerabilities from the outset.
The “Ecosystem of verifiable IT - provable cybersecurity” (EvIT) program aims to research and develop technologies, methods and tools for end-to-end formally verified software and hardware components. Formal verification is intended to be applied automatically to more complex systems. The basic research required for this will extend over the next five to ten years. Formal verification requires in-depth expert knowledge, but is rewarded with the security benefits of bug-free software and hardware: Reliable systems protect customers from dangerous errors and malicious external access. To ensure that the transfer from the prototype to, for example, the control of critical infrastructure, cars or industrial plants is successful, developers should exchange ideas and network with commercial providers and users in an ecosystem.
Verified security: Logic proofs can be used to prove that code is error-free. This enables both security and safety for the end product.
Reduced costs: Verified software and hardware does not have to be maintained again. This eliminates the need for test cycles and recalls if bugs are discovered. The workload in this field is reduced.
No external access: The absence of bugs means an absence of vulnerabilities through which an attack from outside would be possible. The American DARPA, for example, together with Trustworthy Systems (seL4 team at UNSW), has built an unhackable, remote-controlled drone in practical tests.
EvIT is composed of five different projects, each with its own focus on formal verification. It covers hardware and software verification, System on Chip design, multikernel configuration and the further development of verification tools. These cover hardware and software verification, SoC design, multicore configuration, and the further development of verification tools.
Formula V
A complete verification of an IT system with hardware and software in a consistent evidence system. The unique selling point of Formula-V is its gap free proof, which extends from the hardware to the operating system and the program.
PROTECT
A consistently verified IT system with hardware and software consisting of verified individual components and proof of security properties in their composition (compositional “bottom-up” approach). Special attention is paid to protection against side-channel attacks. Implementation is carried out using virtual prototyping and follows the “security by design” approach.
Dyvercon
The extension of the certified seL4 microkernel to a dynamically updatable multicernel configuration with practical performance.
Clash Formal
The extension of formal verification tools in a functional programming language for circuit designs to include end-to-end verification together with the software.
PISTIs-V
The expansion and comprehensive formal verification of the highly modular LionsOS operating system (usable in automobiles, aircraft, automated machines), protection against timing attacks, verified real-time behavior, and isolation of untrustworthy applications in the system.