Industry of the Future
Program safely in Rust with the Why3 proof assistant
Date:
Changed on 06/03/2024
Popular among some of the Internet's major players, the Rust programming language is gradually replacing C. The advantage of Rust is that it helps to prevent memory-related errors, which are responsible for 70% of security breaches. But when writing a critical program it still has to be verified, which is where proof assistants come in. Developed by the Toccata project team, Why3 is a verification tool that is currently making all the headlines in the industrial sphere. What sets it apart are its speed and how easy it is to use. And thanks to a brand new software program called Creusot, Why3 is now capable of verifying programs written in Rust.
On 4 June 1996 the rocket Ariane 5 took off for the first time from Kourou. 36 seconds after ignition, on the computer for the inertial navigation system, one digital value exceeded the memory space allocated to store it. A minor bug that no one had picked up on during development. Denied information, the autopilot broke down, and the rocket veered off its flight path, which resulted in it self-destructing.
This infamous accident illustrates how even the smallest errors in critical software can lead to disaster. In a world that is now totally digital, these critical software programs control all manner of things, from regulating the movement of trains and controlling secure transactions to activating surgical machinery, coordinating telephone networks and supervising nuclear power plants.
It is therefore essential that they do not contain any bugs, but this is easier said than done. In 1996 it took 16 engineers three years to verify the 90,000 lines of code for the software used to control an automated line on the Paris metro. But programs have become so sophisticated, so complex and so large that this sort of “manual” labour is no longer really feasible.
It would be impossible for a developer to verify millions of lines of code individually, which is why tools are needed to automate this task. Known as proof assistants, they are based on a branch of mathematics known as formal methods. At an international level Inria has been a pioneer of these proof assistants, beginning with the success of Coq. Used worldwide and boasting solid theoretical foundations, this is a highly powerful tool for expressing mathematical complexity. However, expertise is required in order to use it and developers must direct the process themselves, step-by-step.
Why3: automated program verification
Then another tool emerged: Why3. Devised by researchers from the Toccata project team, a joint undertaking involving the Inria Saclay centre, Université Paris-Saclay and the CNRS within the Formal Methods Laboratory (LMF - Laboratoire des méthodes formelles), with support from CEA-List, this platform is targeted more at the industrial sphere than at mathematicians. It provides a quick and easy method of program verification. And crucially from a business perspective, it's cheaper to run - verification can often swallow up big budgets.
Third parties can also use the platform to run other software used to verify programs written in other languages. One such example of this is Adacore. Their application Spark is connected to Why3 in order to verify programs written in Ada, a language that is frequently used in aeronautics. Similarly, the CEA's List laboratory created Frama-C, an application which employs Why3 to verify programs written in C.
Creusot for verifying programs written in Rust
A new software program has just emerged within this ecosystem: Creusot. Devised by Xavier Denis as part of his PhD with Toccata co-directed by Claude Marché (Inria) and Jacques-Henri Jourdan (CNRS), it also connects to Why3, only this time its purpose is to verify programs written in Rust. The use of this language is now widespread for the development of critical programs, meaning this highly strategic utility is likely to attract the attention of a whole host of companies.
The heart of the matter: memory management. This is a crucial aspect of program reliability. “According to a study carried out by Microsoft, 70% of security breaches in applications written in C are caused by memory bugs”, explains Xavier Denis. “This language was developed in the 1970s. It doesn't generate new memory for storing tables or any other sort of structure. That’s up to the developer, who has to determine how much memory they allocate. But this is a task that humans aren't well suited to. They simply aren't capable of doing it. At first it seemed easy. You allocated memory and then you freed it up. Sometimes without realising it you try to access memory that has already been freed up, and it now contains something else. People are accessing information they shouldn't be, including passwords.” Of course, there are tools for limiting this problem, but they have a serious impact on system performance.
Rust first appeared in 2015, supported by the Mozilla Foundation. “Its aim is to combine the best of two worlds: to prevent the sort of security bugs you get with C without the extra cost of memory management. This language is designed in such a way as to prohibit any memory bugs presented to it using its type system. It knows when it can allocate memory and when it can release it, checking each time to make sure that the programmer is asking it to produce an executable.” Key to Rust’s success is the fact that it does this without slowing the process down. “Rust has since been adopted by major companies including Amazon, Facebook, Google and Microsoft.” It is also used in the browser Firefox and the Android operating system and, of course, in the world of cybersecurity.
But despite the advantages of this language, programs are not totally risk-free. Creusot was designed to verify that programs have been corrected, featuring two innovative mechanisms for this purpose. This research culminated in the publication of a paper in October 2022.
Two key innovations
Creusot employs two new methods for the verification of programs written in Rust. The first relates to what are known as memory mutations. “Memory management is probably the main activity of any program. Programs take values, store them to read later and, most importantly, modify them. These are mutations. When programmers carry out mutations incorrectly, that’s when the problems start.”
To limit such occurrences, Rust employs the use of a type system. The idea is that: “each part of the memory belongs to a variable from the program, but just one. They’re linked. A given variable, X, will be the only one that can change a given part. Sometimes, however, this can be too restrictive, and so the program lends memory. The programmer can use this memory to do things, but they will need to pay back the loan later.” The problem is that “when you want to verify a program which contains loans, you have indirection. Say you have a value X, then you take out a loan Y. Then there is a change to Y. In this case you need to remember that the value in X is now different. That’s what makes verification so tricky.”
Creusot overcomes this obstacle through the use of prediction. “Instead of looking for an update, an estimate is made from the outset as to what the value for X will be when Y gives us it. There’s a sort of predetermination. A prediction is made in the knowledge that that is going to happen. The theoretical concept was launched in 2020 by other researchers. We applied it to a more realistic context by developing this method with a view to incorporating it into a completed tool.”
The second scientific contribution relates to systems of traits, also known as type classes. “Programs contain different types of information: whole numbers, floating point numbers, lists, and so on. But there are certain operations we might want to define. We may want to compare two whole numbers to see if they are equal, for example. The issue here is that this equality function cannot be correctly defined. If it takes any two objects and says that they are equal, there is no information available on what it is that is being compared. This gave us the idea for these type classes which tell us how to compare two lists or two whole numbers.”
“This method makes it possible to isolate operations in order to structure code, particularly on a large scale. It already exists in Rust. For an equality function it will say 'true’ or ‘false’. But there is nothing to prevent inconsistent results from being produced. Creusot can be used to verify that this function is actually returning an equality result. A developer can then use this function in their program as it has been verified. They can assume that it will work as it should, and they don't even need to know the specific type.”
Retaining program performance
The first person to use the new tool was a Master’s student. “He had just used Rust to write a boolean formula solver, which he was then able to verify using Creusot. His verified solver had essentially the same level of performance as an unverified solver, showing that performance can be retained without the need for any compromise.”
Scientific research, meanwhile, is still ongoing. “There are certain properties of Rust that we don't yet know how to manage, but hopefully we can address that. This is a major area of research. A new PhD was started recently on this subject.” As for Xavier Denis, he is focusing more and more on the user experience. “There are thousands of details to sort out before we can move from a research prototype to a tool that is ready for industrial use.” Making this all the more important is the fact that some companies have already been downloading Creusot to give it a try...