Learn how we apply and advance Formal Verification in the Centre
1 minute
In contrast to testing, formal verification ensures the correctness and security of software by constructing mathematical proofs that consider all possible executions of a program, even in the presence of a malicious attacker.
Verification is thus a rigorous technique to increase trust in software.
Our centre applies verification both to software designs and to concrete programs.
On both levels, we advance verification techniques and tools, and apply them to the solutions developed in the centre such as SOAP and ADEM.
For example, our goal for ADEM is to prove that an asset is deemed protected only if ADEM successfully checked all necessary requirements for the associated emblem. The resulting proof will increase trust that ADEM provides the required security guarantees.
We advance formal verification in the following projects:
ADEM is a proposal for a digital emblem and was developed at the Centre for Cyber Trust. A digital emblem is the digital equivalent to the protective, physical emblems of the red cross, red crescent, and red crystal. Follow the link of ADEM to learn more.
Digital emblems are cryptographically signed objects and as such must be verified. We implemented prototypes doing just that. The Programming Methodology and Information Security groups, both members of the Centre, collaboratively supervised a student thesis in which we formally verified the prototype’s verification code.
Security protocol implementations are obiquitious. We use them daily to perform electronic payments, communicate with friends and coworkers, and they are even present in our electronic passports.
However, designing and implementing security protocols is notoriously difficult. Since security protocols aim to secure communication against malicious attackers, usually active ones, all possible attacks have to be considered at design and implementation time. Subtle bugs, like forgetting a simple comparison check, can render an implementation completely insecure.
Tamarin is a state-of-the art, automated protocol verifier that was used to prove real-world and complex protocols secure, for example, TLS 1.3 or 5G. Nevertheless, Tamarin only supports a limited induction mechanism. Induction is required to handle loops and unbounded data structures, which become more and more common in modern protocols such as in Signal and Certificate Transparency.
In the Centre for Cyber Trust, we currently explore a new induction mechanism for Tamarin that implements so-called cyclic proofs.
Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
Go is targeted at high performance applications running in potentially distributed settings and on multicore machines. Hence, Go provides some built-in concurrency primitives, like channel-based communication. Gobra is intended to verify correctness and security properties of such programs, scaling to substantial codebases.
Read More Visit our project website! Gobra’s initial publication is available here. Gobra is open-source.
