Enschede-based Qbaylogic will join forces with international research teams and industry partners to revolutionize digital security. In the Ecosystem Formally Verifiable IT – Provable Cybersecurity (EVIT) project, they plan to tackle the challenge of creating systems that are mathematically proven to be secure from the ground up. The German government agency for cybersecurity innovation, Cyberagentur, has committed 42 million euros to the initiative.
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 to make formal verification possible for more complex systems, in an automated fashion. The initial project will run for five years, with the possibility of a five-year follow-up.
Current IT security follows a predictable but problematic pattern. Hackers discover vulnerabilities, developers create patches and the cycle continues with new vulnerabilities emerging. The EVIT partners want to break the cycle. “Instead of playing this endless game of cat and mouse with hackers, we’re developing technologies that allow us to mathematically prove the security of systems before they go live,” explains Felix Klein of Qbaylogic. “This represents a complete paradigm shift in how we think about system security.”
Qbaylogic’s open-source Clash technology plays a central role in the initiative. Based on Haskell, a functional programming language, it provides a robust foundation for creating hardware designs with verifiable security using functional programming techniques. Efforts are focused on enhancing the Clash compiler to support comprehensive formal verification of hardware designs, creating new tools that bridge the traditional gap between hardware and software verification and developing practical, industry-ready solutions that make formal verification techniques accessible to everyday developers.
To prove the real-world viability, Qbaylogic will develop a fully verified smartcard system. “It’s a relatively simple system that everyone understands – think of your bank card or ID card – but one where security is absolutely critical,” Klein explains. “If we can prove that we can make such a system completely secure, we’ve made a significant breakthrough.” The team will verify every component of the smartcard system, from the low-level hardware to the high-level software interfaces. This comprehensive approach will demonstrate how different verification techniques can work together to create a completely secure system.
All technologies Qbaylogic develops during the project will be freely available. These include new verification tools and methodologies, the complete smartcard system implementation, documentation and best practices, as well as integration guides for existing development workflows.
