The next presentation will be by Fabien Choteau.
He will give an introduction on formal verification and will learn us how to mathematically prove
this error box in your software. Thank you. I need the timer because I have quite a lot
of things to say. Hi everyone, I'm Fabien and yet today I want to talk about formal verification,
open source formal verification. First the disclaimer, I'm not an expert in formal verification,
but I'm a user of this technology. What I'm an expert at is embedded software, but I
use formal verification and I will explain later our work in a company that's developing
some formal verification solutions. If we look at what Wikipedia says, formal verification
is the act of proving or disproving the correctness of intended algorithms using formal methods
of mathematics. So in practice, what does that mean? Let's take a very trivial example.
If we look at this line of code and we want to prove that it's correct, that it never
fails. First we will have to look at what can go wrong. So for instance here we can say
well there's potentially a division by zero, right? That's bad. So if we want to prove
that the line is correct, we have to prove that x minus 10 is different from zero, which
in terms means we have to prove that x is different than 10. This is known as a verification
condition, something that has to be true for our program to be correct. Now if we look
at this line of code in a context, just a trivial example, here we see that there is
an if statement that's guarding the expression. So we know that x is always different from
10 and therefore we know that there's no possible division by zero in this piece of
code. So that was easy, right? But now let's look at another very trivial piece of code.
Are you able to spot all the verification conditions? Are you able to check that they
are respected or not? This is actually very, very difficult. Most programmers will know
some of the things that can go wrong. Most of the time we will forget what they are.
I'm looking at you, integral flow. And so that's why programming correctly is very difficult
for human beings because we are not able to keep in mind all the verification conditions
and play with them and check them all the time. Again, this is a very simple piece of
code. And so what formal verification is, and in particular, automatic formal verification,
well the goal is to have tools that will extract the verification conditions from the code
and then run a mathematical proof to check that they are respected. And so today I want
to talk about one framework for automatic formal verification, which is called Spark.
So Spark is both a set of tools and a language to perform automatic formal verification.
So on the tool side, we have different tools that are working together to achieve this
goal. The first one is Gnatt Prove. It's developed by the company I work for, Aida Core. It's
going to take Spark code as the input and translate it to another language called YML.
Then we have this, the tool itself, Y3, developed by Inria in France. It's a research institute
which, again, translates the code and extract the verification conditions and call the different
solvers, which are on the right here, to ask them to prove the verification conditions.
So we have different solvers that will have properties on different kinds of algorithms,
Altergo, CVC5, Z3. And so this full tool chain is open source and developed by different
entities, as I mentioned. And so the solvers, for instance, they are not only used for Spark,
they are used for other formal verification frameworks, but all of them work together
in this framework. And so on the other side, Spark is also a language. And actually Spark
is a subset of the Aida programming language. And so the question you may ask is, why would
you use Aida? Why would you use a subset of Aida for formal verification? So I'm going
to take just two simple examples. Why Aida is great for when you want to do formal verification?
Well, this language provides a lot of specification power. The developers can express very precisely
what they want from the program, from the code, which then the formal verification framework
will be able to check. Just a simple example, if you program in any other language, if you
want to have in your application a percentage value, for instance, for the completion of
a process or whatever, usually we'll say, OK, my percentage is a float. And I'm going
to say I'm going to use the value from 0 to 1. And if you are an extremely good programmer,
you're going to write that in a comment. Like, you know, my lowest value is 0, my highest
value is 1. And that's just a comment. And then if five years down the line, you want
to say, oh, actually, it's better if it's from 0 to 100. What happens to the comment?
Maybe you update it. Maybe you don't. How do you make sure that everything, all the code
is updated to follow this new rule? That's very difficult to maintain. So one example
with Aida, you just define your own type and you say it's a float. It's a new float. It's
a different kind of float. That has only valid value between 0 and 1. And so what's great
here is that the solvers that will try to prove the code, they get a lot of information
from here. First, they will add verification conditions when you try to cast from a regular
float to this percentage value. Because if the value is not within the range, that's
a bug in your program. And you want to know it. Also, you can extract information. Like,
if you take two percentage value and you multiply them, you also know that the result is between
0 and 1. And so in turn, that means a lot of information for the provers to do their work.
And so they will be able to more automatically reason and prove that the program is correct.
Another example is the contract-based programming of Aida. So you can have preconditions and
postconditions on your subprograms. So precondition is something that has to be true when you
call the function or the procedure. Postcondition is something that has to be true when you
return from the subprogram. So very simple example here with the stack. We implement
the stack. We have functions to know if the stack is full or if it's empty. And we implement
the push. And obviously, well, not obviously, but in this API, we say it doesn't make sense
to push something on the stack if the stack is already full. So never do that. That's
the contract that the procedure is asking from the caller. And then the implementation
says if you push something on the stack, well, it's not empty anymore at the return.
And so with Spark, what's great here is that you have formal verification both on the
caller side. So Spark will prove that you never call the push function when the stack
is full. And on the implementation side, it's going to prove that when you return from
the push function, the stack is never empty. And so that's going into functional correctness
verification, which means your software is doing what it's supposed to do and only what
it's supposed to do. And so with the integrated pre and post conditions in ADA and other features
that I don't have time to mention, well, this makes ADA a very great language for formal
verification. So why should I care about Spark and I would say formal verification in general?
So with Spark, you can have mathematical proof that there is no possible vulnerabilities
in your application for any possible inputs. That means no buffer overflow, no division
by zero, no integral overflow and so on. If you go beyond and you use contracts, you can
also prove, as I mentioned, the functional correctness. So the program does what it's
supposed to do and only what it's supposed to do. And in terms, that means you can avoid
some of the testing efforts because, for instance, unit testing is more or less trying to achieve
the same goal. So if you already have a mathematical proof that the functional correctness of your
code, you don't need to do unit testing anymore. And so you're going to save time on that.
Recently we published a case study from NVIDIA. So a few years ago, the NVIDIA security team
was questioning their methodology for security and how to achieve their goals in terms of
security. And so they said testing security is pretty much impossible. You cannot test
all possible combinations of all possible values for your application. And so they decided
to try provability. And they selected Spark as an experiment. And now they are deploying
more and more Spark in the GPU. So if you get the latest, greatest NVIDIA GPU, there
should be some Spark-proven code embedded in the firmware, which lets them actually focus
on other parts of the security on more interesting verifications and more interesting properties,
security properties of the application. They don't have to deal with buffer overflows and
integers overflows. All the low-level stuff, it's already taken care of. And they can focus
on more interesting points. So now let's do some proof. So for the A9 Spark programming
language, we have this package manager called Alire. So here are a few instructions to make
your first and prove your first piece of Spark code. So you don't know then install the package
manager. So from the command line, we start by creating a project or a crate with Alire
in it. We enter the directory. We add the net prove tool suite as a dependency. So it's
going to download everything and set it up for you. Then we write some piece of code.
So you can recognize our very nice equation here. Just for the declaration of the X constant,
it doesn't matter what it is. I'm just taking an integer value that Spark doesn't know.
So just to make sure I'm not cheating or anything. We go to the console again. We run a net
prove. And so a net prove will tell us, well, there might be a division by zero error at
these points. So as you can see, the message is pretty clear. Actually, it can be even
better than that because the tool can provide counter examples. So if we add the switch,
counter examples on, net prove will say division by zero might fail, for instance, when X equals
10. And so that's pretty easy to fix. We just add this if statement. And we run the tool
again. And that's it. We proved our first piece of code. So as you can see, it was easy.
If you want to try and learn a little bit of Spark, we have an online website. So learn.edocore.com.
Online interactive website. So you don't even have to install what I showed before just
to learn and try the tool sheets. So there's different chapters and one specific to Spark.
So that's one way to get started. And for those who wondered, just the piece of code
before, there are seven potential bugs or errors in this one. So I'll let you as an
exercise to fix this one. Thank you very much.
Thank you for the presentation. Let me unwrap you with a shot.
Perhaps someone might have a question about that.