Formal Verification: How We Come to Trust the Systems Around Us
Sayan Mukherjee has joined IITB Trust Lab as a Senior Research Scientist working in the area of Formal Verification. His research focuses on formally verifying real-time, and stochastic systems. More recently, he is also working on techniques originating from Formal Verification, that can aid in building trust in AI-based systems, by improving their explainability. In this article he takes us through the motivation for, and fundamental ideas of Formal Verification, why it is crucial, and its intersection and overlap with the overarching idea of Digital Trust.
In 1994, Thomas Nicely, a number theory professor in Virginia, working with prime numbers, suddenly realized that some numbers that he was computing were wrong. Was there a bug in his algorithm? His code? No, neither. What was going wrong then? Turns out, the bug resided in the chip sitting inside his computer!
In order to speed up floating point divisions, Intel’s brand new Pentium series microprocessors used a method that consulted a lookup table containing roughly thousand entries. Now, due to an error in a script, five of these entries were missing.
Whenever the division algorithm would try to fetch these missing entries, the resulting value would be wrong. But this error was a very particular one: as per some estimates, this error could occur once in about 9 billion divisions. The issue, it was argued, was supposed to unsettle very few people in the world (you can read about the problem in detail here).
Others put the odds differently. IBM’s estimate for the error occurring in practice turned out to be much higher, leading them to stop the shipment of their machines containing the affected chip. The story of the issue became big news in the popular press, and ultimately, Intel had to recall all the chips back by the end of 1994 and this cost them around $475 million. All because 5 entries in a rather large table were missing! Intel spent the next decade fixing its workflow so that such costly mistakes could be avoided.
Imagine someone computes many (billions, let’s say) random divisions using the affected chip. In all likelihood, they may never encounter the bug. As was the practice back then, Intel must have also tested their chip by simulating it numerous times, before deploying them. Unfortunately, they must have never hit the bug in those simulations. This perhaps led them to be fairly confident that the chip is indeed correct, until a mathematician found a very very particular execution where the chip failed!
Simulation can therefore never provide the ultimate guarantee of correctness. The fix that Intel counted on, was to formally prove that the chip computes the division correctly. A proof would cater to all possible computations, not merely a few billion! By 2009, this effort was extensively adopted inside Intel, and this was documented in a paper – appearing at a top Formal Verification conference – Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation.
So How Do You Prove A System Is Correct?
In today’s world, we are growing more and more used to (perhaps, even dependent on) systems that are governed by automatic components, such as those chips. A bug in the floating point division computation may or may not affect us all in our daily lives, but what if there is an obscure bug residing in the software of my heart-rate monitor that can somehow show I am fine when I am not? What if the braking system in an automatic car fails to push the brake in an emergency, because somehow a corner case was missed while designing the braking mechanism? Medical devices, alarm modules, autonomous vehicles, avionics: we have systems around us that we cannot afford to get wrong.
Trust in a system increases when we know that the system is doing what it is supposed to do, not just most of the time, all the time. Unfortunately, but somewhat unsurprisingly, coming up with correct systems is an immensely hard task. So when humans (with or without AI) build systems, bugs can easily creep in.
So what can we do to make a system trustworthy? A standard technique for detecting bugs in a system is to test it, before deploying it in practice. Even though this is a popular and well used approach, it fails to provide guarantees across executions not encountered during the testing phase. As the famous Computer Scientist Edsger W. Dijkstra had said: “Program testing can be used to show the presence of bugs, but never to show their absence!”
How do we show that a system is bug-free? Instead of executing a system and seeing what happens, Formal Verification studies an umbrella of techniques, grounded in rigorous mathematics, that treats the system as a mathematical object and attempts to prove that under every possible input, the system-under-study cannot produce an undesired outcome.
In this article, we will consider one of the well-celebrated Formal Verification techniques, called Model Checking. Given a property (generally called, a specification) of the system that the user desires, the goal in model checking is to prove that the system-under-study satisfies the specification, on all of its executions. In other words, the goal is to verify the system against a given specification.
Now, Model checking a system typically involves two primary steps:
(i) modelling the system one wants to verify into a mathematical abstraction; and
(ii) formalizing the specification one wants to verify.
Modelling The System
For the first step, generally systems are modelled using automata. These are graph-like structures that are able to classify whether an execution is feasible in a system or not; in other words, these can represent exactly the set of all feasible executions of a system.
As an example, consider a (simplified) model of an ATM: here, the user inserts their (debit/credit) card, enters an amount they want to withdraw, followed by their PIN. Then the bank verifies whether the PIN is correct or not, and sends a response (succ or fail). If it returns succ, then money is disbursed and the session gets terminated. On the other hand, if the PIN fails, then the session terminates. This behaviour of the ATM can be captured using the automaton drawn below.
The circles in the image are called states of the automaton, the arrows are the transitions; the transitions are labelled with events that the system (that is the ATM) can observe. At any given time, the automaton resides in one of its states.
At the beginning, it starts in the blue state, then it moves from one state to another depending on the event that happens next. Note that, if we take a sequence of transitions of this automaton, they lead to a feasible execution of the ATM. For example:
insert_card > enter_amt > enter_pin > succ > disburse
is a valid execution of the ATM. Whereas, an invalid execution:
insert_card > enter_amt > disburse
is not a feasible sequence of transitions in the automaton. If the automaton reaches the red state, then it denotes a failed (but feasible) execution; if it reaches the green state, it denotes the successful completion of one withdrawal.
Modelling The Specification
For the second task, first, note that natural language – e.g. English – is ambiguous! Writing a specification in natural language is therefore not suitable for formal analysis, since the same specification could possibly be interpreted in different ways. An example specification for the ATM model, can be that “a fail should not be followed by a disburse”.
But there can be two meanings of this:
(i) a fail is not followed by a disburse in the next step; or
(ii) a fail is never followed by a disburse ever in the future.
We can see that perhaps the first option is what is intended by the specification, however, one could also misinterpret this with the second option. To circumvent this issue of ambiguity, specifications are formalized in mathematical logic.
Amir Pnueli introduced Temporal Logics. These are structured specification languages for specifying the temporality of events, such as ‘a fail is not followed by a disburse in the next step’, or ‘a bad event never happens’, ‘the system always emits safe signals’, ‘the robot does not fall into a hole until it reaches its target’ etc.
Once a specification is formalized as a logical formula (in some suitable logical formalism), one can again come up with an automaton that captures all the executions (without worrying about which executions are feasible in the system) satisfying the formula. For example, if we take the first interpretation of the given specification, we can draw the following automaton.
Here e1 denotes all the events other than fail (that is: insert_card, enter_amt, enter_pin, succ, disburse, terminate), and e2 denotes all the events other than fail and disburse. If you look at it long enough, you will realize that all the executions of this automaton are the sequences of events where a fail is not followed by a disburse in the next step.
Once the system and the specification are modelled as suitable automata, the task of verification boils down to checking that the set of feasible executions of the systems is contained in the set of all executions that satisfy the specification. This implies there exists no feasible execution of the system that can violate the specification! This is exactly the guarantee we were looking for. (You may have already realized that for the ATM example above, this inclusion indeed holds for the selected specification, hence the modelling of the ATM is correct with respect to the specification.)
Amir Pnueli won the ACM Turing award in 1996 for introducing Temporal Logics; Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis, won the ACM Turing award in 2007 for introducing Model checking – ACM Turing award is the highest award accorded in Computer Science.
The Guarantee, And Where It’s Going
Model checking provides a much stronger guarantee than traditional techniques such as testing, as this certifies the system against all of its possible behaviours. With respect to a given specification, this is perhaps the ultimate correctness guarantee we can aim for. But, these techniques are computationally intensive: for large systems these can take a long time to run. That said, these are generally used pre-deployment, so in most cases we can afford to give them the time they require. Making verification techniques more efficient, so that larger systems can be verified, remains an active area of research.
Formal verification has been deployed successfully in the real world, most notably in the hardware industry, and progressively more in software as well. Leading companies now maintain dedicated teams that apply a layer of formal verification to their production flow before their solutions are deployed in practice.
Today, one of the most active areas of research in this direction is the verification of AI-based systems. These systems are extremely capable, but they come with almost no guarantees about their behaviour. If I ask it to polish the draft of this article, I can read its changes myself and be reasonably sure. But, if I ask a coding agent to write me a long program, how sure can I be that what it produced is indeed correct? Researchers are now working in both directions: using formal methods to explain how an AI-based system behaves, thereby certifying what the system will or will not do, and using AI to make formal methods scale.
From Probable to Provable Trust
The same idea is now behind a lot of what we call digital trust. Take EMV, the standard behind the chip-and-PIN cards we all carry, its specification runs over 2000 pages! Buried somewhere in there was a flaw that let an attacker pay without knowing the PIN. Researchers found it by building a formal model of the protocol and checking it with a tool called Tamarin. And once the standard was fixed, they used the same model to prove that the fix actually worked (you can find more details here).
Thus, Formal Verification offers a mathematical foundation for that trust. Rather than sampling a system’s behaviour through testing, it uses logic, model checking and other techniques to prove that the system meets its specification – under all possible inputs, in all possible executions.
