Get Started with Open Source Formal Verification
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 542 | |
| Author | ||
| License | CC Attribution 2.0 Belgium: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/61617 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
|
00:00
Formal verificationCore dumpSoftwareOpen sourceMathematicsAlgorithmFormal verificationOpen sourcePresentation of a groupExpert systemSoftware bugLine (geometry)Set theoryFormal languageProof theoryCondition numberChainDifferent (Kate Ryan album)Category of beingCodeMathematicsAlgorithmMultiplication signComputer programComputer programmingSoftware frameworkDivision (mathematics)Statement (computer science)Fiber bundleComputer animation
05:15
Programming languageSubsetFormal verificationComputer animation
05:35
Core dumpGlass floatRange (statistics)Stack (abstract data type)Natural numberBoolean algebraFunction (mathematics)SoftwareInformation securityoutputFunctional (mathematics)Proof theorySoftware testingFormal verificationFocus (optics)Logical constantIntegerPhase transitionMathematical analysisEmpennageMountain passPermianComputer programmingContent (media)Formal languageMaxima and minimaInformation securityoutputProcedural programmingFunctional (mathematics)Software testingSoftware developerLatent heatVector potentialError messageComputer programmingSoftware frameworkDesign by contractCartesian coordinate systemComplete metric spaceImplementationFormal verificationFormal languageSoftwareProof theoryBitWebsitePower (physics)PreconditionerUnit testingTerm (mathematics)InformationBuffer overflowMultiplication signObservational studyCategory of beingCASE <Informatik>CodeLine (geometry)Process (computing)Different (Kate Ryan album)Condition numberSoftware bugResultantVulnerability (computing)Buffer solutionDivision (mathematics)CounterexamplePoint (geometry)Level (video gaming)Data managementProjective planeDirectory serviceCombinational logicMereologyIntegerDampingVideo game consoleMessage passingStatement (computer science)WeightSuite (music)Nichtlineares GleichungssystemDeclarative programmingComputer animation
15:05
Program flowchart
Transcript: English(auto-generated)
00:14
The next presentation will be by Fabien Chouteau. He will give an introduction on formal verification.
00:22
And we'll learn as how to mathematically prove that there are bugs in your software, so. Thank you. You push this to start? Yeah, thanks. Okay, I need the timer because I have quite a lot of things to say, so. So hi, everyone, I am Fabien,
00:40
and yet today I want to talk about formal verification, open source formal verification. So first a 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 I work in a company that's developing formal verification solutions.
01:04
So 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?
01:20
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.
01:42
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 turn means we have to prove that x is different than 10. This is known as a verification condition,
02:02
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,
02:23
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?
02:41
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, Integra workflow.
03:01
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 very simple piece of code. And so what formal verification is, in particular, automatic formal verification.
03:24
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
03:42
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
04:00
that are working together to achieve this goal. The first one is GNAB Prove. It's developed by the company I work for, Edecor. It's gonna take Spark code as the input and translate it to another language called YML. Then we have this, the tool itself, Y3,
04:20
developed by the INRIA in France. It's a research institute, which gonna, again, translate 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.
04:42
And 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,
05:00
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 Ada programming language.
05:22
And so the question you may ask is, why would you use Ada, why would you use a subset of Ada for formal verification? So I'm gonna take just two simple examples. Why Ada is great for
05:41
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.
06:02
Just simple example, if you program in any other language, if you want to have in your application percentage value, for instance, for the completion of a process or whatever, usually we'll say, okay, my percentage is a float, and I'm gonna say, I'm gonna use the value from zero to one.
06:23
And if you are an extremely good programmer, you're gonna write that in a comment, like, you know, my lowest value is zero, my highest value is one. 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 zero to 100.
06:40
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 Ada, 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 zero and one.
07:05
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.
07:22
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 zero and one. And so in terms, that means a lot of information for the provers to do their work.
07:41
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 Ada. So you can have preconditions and post-conditions
08:02
on your sub-programs. So precondition is something that has to be true when you call the function or the procedure. Post-conditions, something that has to be true when you return from the sub-program. So very simple example here with the stack.
08:20
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
08:42
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.
09:01
So Spark will prove that you never call the push function when the stack is full. And on the implementation side, it's gonna prove that when you return from the push function, the stack is never empty. And so that's going into functional correctness
09:23
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
09:42
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.
10:04
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
10:22
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,
10:41
you don't need to do unit testing anymore. And so you're gonna 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
11:03
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 combination of all possible values for your application. And so they decided to try provability and they selected Spark as an experiment.
11:22
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
11:41
of the security on more interesting verifications and more interesting security properties of the application. They don't have to deal with buffer overflows and integers overflow, all the low level stuff it's already taken care of and they can focus on more interesting points.
12:00
So now let's do some proof. So for the ADA and Spark programming language, we have this package manager called Alire. So here are a few instructions to make your first, improve your first piece of Spark code. So you don't know then install the package manager.
12:22
So from the command line, we start by creating a project or crates with Alire in it. We enter the directory. We add the net proof tool suite as a dependency. So it's gonna download everything and set it up for you. Then we write some piece of code. So you can recognize our very nice equation here.
12:46
Just for the declaration of the X constants, doesn't matter what it is. I'm just taking an integral value that Spark doesn't know. So just to make sure I'm not cheating or anything,
13:00
we go to the console again, we run net proof. And so net proof will tell us, well, there might be a division by zero at this point. 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.
13:21
So if we had the switch, counter examples on, net proof will say, division by zero might fail. For instance, when X equals 10. And so that's pretty easy to fix. We just add these if statements and we run the tool again and that's it.
13:41
We proved our first piece of code. So as you can see, it was easy. Okay, if you want to try and learn a little bit of Spark, we have an online website. So learn.edicar.com, online interactive website.
14:02
So you don't even have to install what I showed before, just to learn and try the tool sheets. So there are 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,
14:21
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.
14:43
Well, thank you for the presentation. Let me unwrap you with a...