Clash Formal - Provable cybersecurity for Cyberagentur

Security tokens and smart cards, correct by design

Smart cards with mathematically proven security properties. QBayLogic’s Clash Formal is part of Ecosystem formally verifiable IT (EvIT), the research mission of Germany’s Agentur für Innovation in der Cybersicherheit (Cyberagentur).

Talk to an engineer

The challenge

Security today is a cycle of shipping, finding flaws, and patching. Cyberagentur’s EvIT mission replaces that cycle with proof. It covers every level of the stack, hardware and software together, rather than one layer at a time.
Formal verification tools target functional programs, which execute one step after another. Circuit designs are intrinsically parallel. So those tools do not carry over.
Verifying Haskell programs is well trodden ground. Verifying a hardware design together with the interface it exposes to software is not. That is why the programme names the interface as a research area in its own right.

The approach

Clash and Haskell share one language front-end and one type system. Hardware, the interface and software therefore live in a single environment. A proof about the software still holds for the circuit, because no translation step sits in between.
A strong type system captures safety and security requirements early, during design itself. Otherwise they surface in test, which is too late. Cyberagentur calls the result correct-by-design.
We build formal verification frameworks straight into the compilers. SAIL describes the semantics of instruction set architectures. Proof assistants such as Coq connect through dedicated interfaces.

The results

Clash 2.0 will be the first release where developers use formal verification tools naturally, inside their normal workflow.
A working demonstrator proves the features: a security token and an advanced smart card system. Both carry formally verified security properties.
Documentation, training material and published research keep the results in the open. So the existing Haskell and Clash community gains from the work too.

Find out more at the official project page:

clash-formal.org

OUR CLIENTS

Trusted by some of the most innovative teams in the world

• Free-space secure communication • Cryptography • Quantum communication • Bittide / synchronization • Satellite communication

Why QBayLogic?

QBayLogic stands out for its ability to harness the power of both software and digital hardware design. Our Clash software-to-hardware compiler, based on the Haskell programming language, is a prime example of our innovative approach.

This unique expertise made us the ideal fit for Cyberagentur’s ambitious EvIT project.