Formal verification: how a 400 year old mathematical idea could transform cybersecurity

Estimated reading time: 5 minutes

As software systems grow more complex, computer scientists need robust methods to test their reliability and performance. Now, they are starting to use complex maths to make code ultra-secure…

The technology sector is keen on the phrase: software is eating the world. It's easy to see why. Today, industry of every type runs on software – from automotive and healthcare to heavy industry and finance. 

But, as every user of a laptop or smartphone knows, software can malfunction. Computer code frequently contains programming errors, which can lead to systematic failures. When your computer stops working, this is annoying. But system failure in a power plant? Or a transport system? Or a bank? This can be critical.

So the big question is: how to address software errors and vulnerabilities?

One method is testing. And this is how most contemporary software development works. Software developers write code, and use integration tests to identify bugs.  They then rewrite the software accordingly. 

But today's code bases are vast. And every new update can introduce fresh errors; the problem compounds as the scale of the code base increases. To use more technical language, testing is limited by the combinatorial complexity of test cases and their relevance.

Happily, there is a complementary technique: in addition to testing, developers can use maths. How? By applying a technique known as formal verification (FV).

Formal Verification: from academic theory to mitigating risks in industrial applications

The roots of this idea actually go back hundreds of years, when application of 'formal reasoning' on complex systems was explored by the 17th-century German mathematician Gottfried Wilhelm Leibniz. He proposed that any intellectual discourse could be described using mathematical language within certain rules.

Over the centuries the idea was developed by other mathematicians such as Godel and Turing. When the computer age began in the second half of the 20th century, software engineers began to ponder a new question: could they reason all possible behaviours of a system based on a mathematical description of all possible scenarios? If they could, their applications would be free from the coding errors that introduce bugs, hacks, and attacks.

Put simply, the benefits of FV in computer science can be summarised as follows;

•    It's exhaustive. FV can in theory provide a 100% guarantee of the absence of bugs and security issues 

•    FV dramatically reduces the cost of software maintenance, which was estimated at $2 trillion in 2020 in the US only.

•    It is compliant. The reliability introduced by FV can help organisations to comply with the highest assurance levels of industrial certification.

Early examples of FV in computer programming emerged in the 1970s as a handful of projects demonstrated that formal verification could be applied to real-world software systems, not just theoretical models. In 1998, there was a high-profile example, when the RATP project used formal verification to test the software underlying the automatic train operating system for the first driverless metro line 14 in the city of Paris.

There were other experiments but today, 50 years later, the deployment of FV remains limited. This is because of a number of fundamental obstacles. They include: 

•    Scalability: Large, complex codebases demand considerable modelling effort and computational resources to be verified.

•    Abstraction: It's hard to create accurate formal models representative of real-world systems especially when they are not designed with verification in mind.

•    Time and cost: The above challenges make FV time-consuming and expensive. This can delay product releases or development cycles.

•    Expertise: There is a limited number of skilled professionals in formal methods

•    Integration: Incorporating FV into agile or rapid development cycles is limited by the scalability and time and cost issues.

•    Tool limitations: There is a lack of user-friendly tools available to programming engineers without advanced expertise in formal verification.

The good news is that tech firms and academic researchers are now working hard to solve some of the above challenges. This is especially crucial in industries such as aerospace, defence, automotive, and critical infrastructure. These are sectors that rely on secure elements and safety-critical identity components, where errors or vulnerabilities can have severe consequences.
 

Academia and industry pool their expertise

A fine example of recent progress is the collaboration between French innovation institution CEA and Thales Research and Technology. In 2015, they set up the FormalLab unit to research the use of FV in cybersecurity. The partners were aware that a bold new approach was needed to address the growing sophistication of cybercrime. Indeed, just a year before the project was announced the Heartbleed bug had showed that 17% of the Internet’s secure servers were believed to be vulnerable to attack.

Marko Erman, Chief Technical Officer of Thales, said at the launch: “At Thales, we believe that the future lies in natively secure solutions, with cybersecurity built into every level — the overall architecture, the network and, importantly, the software, especially the application modules used for communications and data encryption. In this field, FormalLab is breaking with conventional cybersecurity practices to better defend against constantly changing cyberthreats.”

To accelerate their work, the FormalLab researchers jointly applied and improved a semi-automated formal approach based on the Frama-C Platform. It is a set of tools that help programmers analyse and verify the correctness of C code. The formal approach aims  to prove complex security properties whose specification and verification cannot be fully automated. Effectively, it can guarantee that code doesn’t contain any software bugs that could cause software vulnerabilities.

In their experiments, the Thales and CEA researchers combined their use of FRAMA-C with automated static application security testing (SAST) tools. For Adel Djoudi, a Formal Methods Expert at Thales’s Digital Identity and Security businesses, the collaboration with academic researchers has been essential to the progress of the project. 

Attention turns to the JavaCard virtual machine 

In2021, Thales’s Digital Identity and Security businesses , Thales Research and Technology and CEA reached another milestone – successfully applying FV in the area of smart cards. Given the near-universal use of smart cards for sensitive applications such as payment and identity, this was an important project. So here the researchers used FRAMA-C on the underlying JavaCard virtual machine that ensures the necessary isolation properties inside a card. The implementation contained over 7,000 lines of C code, and successfully proved more than 52,000 instantiations of security properties. 

It was the world's first formal verification of the actual C implementation of a JavaCard VM code using FRAMA-C. And this pilot project attained the EAL7 certification awarded by the French certification body ANSSI. This is the highest level of Common Criteria CC certification (Common Criteria for Information Technology Security Evaluation). It certifies that “a formally verified and tested system is resistant to a high-level attacker.”

Thales believes its work on the application of FV to smart cards can pave the way for new breakthroughs in cyber security – and also give it a head start on its competitors. Djoudi says: “The smart card is a fertile environment for the application of formal verification, because a lot of testing has been done already without it. By adding formal verification we can get close 100 percent level of security. This is critical because we develop identity products for governments and their citizens, which requires the maximum level of assurance. So far, we are the only company in the market to achieve EAL7 certification level. And that was possible  thanks to our formal verification approach. This really distinguishes us from our competitors.”