Proving the Correctness of GNAT Light Runtime Library
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.
Moy, Yannick
As a programming language, Ada offers a number of features that require runtime support, e.g. exception propagation or concurrency (tasks, protected objects). The GNAT compiler implements this support in its runtime library, which comes in a number of different flavors, with more or less capability. The GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, with an Operating System or without it (baremetal). It contains around 180 units focused mostly on I/O, numerics, text manipulation, memory operations. Variants of the GNAT light runtime library have been certified for use at the highest levels of criticality in several industrial domains: avionics (DO-178), space (ECSS-E-ST40C), railway (EN 50128), automotive (ISO-26262). Details vary across certification regimes, but the common approach to certification used today is based on written requirements traced to corresponding tests, supported by test coverage analysis. Despite this strict certification process, some bugs were found in the past in the code. An ongoing project at AdaCore is applying formal proof with SPARK to the light runtime units, in order to prove their correctness: that the code is free of runtime errors, and that it satisfies its functional specifications. So far, 30 units (out of 180) have been proved, and a few bugs fixed along the way (including a security vulnerability). In this talk, I will describe the approach followed, what was achieved, and what we expect to achieve.
 Hello, I'm going to talk about the project I've been working on for the past six months with my colleague Pierre-Alexandre Bazin about proving the correctness of the Gnatt Light Runtime Library. So what is this Gnatt Runtime Library? That's what we called previously at the decor the zero footprint ZFP or Revenscar SFP or SERT Runtime. So now it's divided between the light runtime and a more encompassing embedded runtime. And this light runtime is targeted that's embedded platforms. So we have 77 platforms supported right now. Most of them are bare metal with a variety of chips ARM, Leon, PowerPC, RISP5, X86 and X86 64 bits. And sometimes with an S on top, so like PyCoS or X-Wars. And the units of that runtime are ready for certification. So a subset of these have been already certified for use in various projects in avionics, in space, in railway, in automotive, subject to the suitable certification documents. So like DO178 for avionics, ECSS for space, EN51284 railway and ISO26262 for automotive. So you can say that the units in that runtime are this subject to a high degree of scrutiny with proper specifications put in place and test suites and reviews etc. So you can build this runtime based on the project that you have available truly on GitHub in BB runtimes where it takes the sources from the DCP3 and the net sources subdirector. So just to give you a tour quickly of these units in the net light runtime, if I take the X86 64 bits version, because of course for each version you have different number of units. And here it has 182 spec files. And I'm only counting the spec files here because some of them are just spec files, but some of them are bodies and some of them are instantiations of generics. So they have spec plus bodies, but declared just as a spec file. So between all of these 182 files, you have of course support for the ADAS standard library. So that's the A-iPhone something files and the I-iPhone something files for interfaces. So you have here a carton string handling, you have some Nurex library, you have support for assertions and exceptions, but in this runtime there's no propagation of exceptions, it's only local or calling the last-hand handler. And there's interfaces with C. You have also a little bit of the Gnats user library, so we have a few G-something files, it's mostly for I-O. And you have many files that deal with the support for features of the language, so the Gnat runtime library, so you have 104 T as dash something files. And so here you have support for various attributes like tick image, tick value, tick width, attributes of floating point numbers. You have support for I-fed collaborations, especially on fixed points and floats and explanations, including contagious and some Nurex, and support for tasking. So all of that. Now I'm going to talk about proof. So proof using the Spark tool. It's a formal verification tool doing two kinds of analysis, one called flow analysis and one called proof. And proof is the most involved whether it asks provers about the validity of some formulas which entail the correction of the code. And so here you can see very briefly a depiction of the architecture of the Spark tool, where it starts from the complete left inside an editor, where you can see the codes. And at the bottom you can see here some Spark codes say assigning a value 42 in index one of array A. And through some codes, part of it which is shared with the compiler, what I called the Gnat here, we transform that code into a YML from intermediate form. So that's this code in the middle which represents the assignment on the left. And which is represented by this question mark in the middle, which is the symbol of the Y3 platform. And this platform dedicated to proof programs then generates formulas. So you can see an example of a bit of a formula in this SMT lip syntax on the bottom right. And these formulas are dispatched to various provers, in particular automatic provers like AlphaGo, CVC4 and D3, which are all included in the Spark technology. Okay. So in Spark, we emphasize the fact that proof is not an all or nothing endeavor. So you can start at some bottom level, which we call the stone level, where you have only the guarantees of having a better, safer subset of the language. And then you can go up the scale here with the bronze level for checking constraints of data and information flow and making sure that everything is initialized. Silver level is about making sure that there are no runtime errors, particularly no CW in the codes. At the goal level, you can start proving key integrity properties, whether it's there really to safety or security. And at the platinum level, you can prove fully functionally the code. And so typically, the platinum level is applied to a much smaller subset of the codes than what's, than where you can apply lower levels. And the main target, usually the silver level, so absence of contenders. But here in this project, we're going to target this platinum level, so fully functionally describing the behavior and proving that the code complies with this specification. So first, a little motivating example for this project. And so we're going back to 2012, when we were adding support for big integers in that, so mathematical integers inside the compiler, was motivated by a feature in Spark to allow intermediate computations without overflows. So we do them using full mathematical possibilities to ignore the possibility of overflows in some proof. And implementation was done by the late great developer, Robert DeWor, so founder of Hedycorp, and used to always be for this multi precision division. So we have integers in a number of machine integers. So you have array of machine integers to represent large integers. And this algorithm is described in the art of computer programming, volume two. So we use the second edition from 1981. And this will have an port Slater, that's why I'm mentioning it here. At the time, so the reviewer told him that in the code that he had written, there was a possible overflow in this large piece of code, this large expression. But Robert, knowing that he had implemented the code from Knuse's book correctly, and assuming that the book was correct, was not convinced by this possibility of an overflow, and asked for an actual issue. So the reviewer went back to the codes and finally came up with this example. So try this long multiplication division, which corresponds to activating this expression leading to an overflow. And indeed, Robert recognized that the true results was different from the computation in the codes given by Knuse. So what happened? Well, even the best like Knuse and Robert DeWorra can get it wrong, especially when it comes to these very low level details, repeat to possible runtime errors, and especially when it comes to overflows. And regarding this specific computation, in fact, the bug had been already fixed in an ereta of volume two in 1995. So that's this part here, this test, which needs to be done to prevent the possible overflow. But that's not the end of it. So 10 years later, it was this test was fixed again. So it was not actually an equality that should be on here, but a greater or equal test. So hopefully after that, we have a correct description of the algorithm that can be implemented without overflows. So that's what we did. But obviously, algorithm gets implemented in many places. And that was the case in the compiler. So this algorithm was used in two other units. In this unit, you in pitch for arbitrary present computation during the combination. And in this other unit system that's are it 64 to support six point are a fake because six points are represented internally by the compiler integers with some scale. And so you need this kind of competitions. But obviously not to compete, not to implementations are alike, there are different constraints in the that has that are represented. And so on the one side, we fixed the computation in you in pitch, although we couldn't find an obvious bug. But the computation was was the one that could be fixed. In the system that's are it 64, the test was done differently. And so we didn't find a bug. So didn't apply the fix and hope that it was okay. Now fast forward to 2019. Here we were, as we usually do at the decor, doing a runtime certification for space. And one of the external reviewers looking at this unit for six point support and in particular, at algorithm D implemented in scale device made the remark that we should increase common frequency to a better implement put to better understand the working in the working of the algorithm. So that's led to a new internal review. And during this internal review, we detected the two possible silent overflows in another related function, so double divide, and the missing exception. So some case which should raise an exception, but here was not doing it in the scale device. So that's not good. That was not so bad in fact, because as I said, the overflows were were silence. So we're doing the right thing in the end. And the missing exception was just on incorrect input. Still a colleague from the specification team challenged us to start team to prove the unit. So we set set on doing that. And one week of work later, we got all the algorithm except this scale divide implementing algorithm D, which was more complex proof. So we tried to have a discussion with the specification team, but priorities to con and the while everyone moved on. Until recently, so last year, during a summer internship, a very good intern Pierre-Alexandre Bazin updated the proof that we had done two years before and finally proved this scale divide implementation. And so now it has moved. So it's in this new file s Arizu because it's a generic implementation now for 64 and 128 bits. So you have this big contracts at first, but which is quite readable. So you can look at the past condition of scale divide. Indeed, it says that if you go to big integers, that's this conversion to big for all the values involved here. The result are is really the the remnants, the result of the remnants of the multiplication of x times y divided by it. And for Q, if you ignore rounding, which is just a slightly more complex case, the quotient Q is really the quotient of x time y in mathematics divided by it. And the application is just to prevent an overflow during this competition. So great. That was proved. We were very happy to learn that finally, our implementation that had been certified was indeed the probably correct. So we say, well, let's go from there and prove everything. But the runtime is not exactly in Spark. There are a lot of uses of untyped memory for many good reasons to handle the cigarette stack for a rare comparisons for things that are not necessarily even aligned for also ports to get to the tags of objects dynamic type for binding to C string. So many reasons to use in data addresses, so type address and doing uncheck conversions between address and the pointer types. And this is something that is not at all supported by the ownership system that we have in Spark, which is a fully typed. Plus, not everything is not is provable. In these units, there are a lot of support for low level floating point operations for some language attributes in Ada, regaining floats. There are also low level support for numerics like trigonometry. There's things that do double arithmetic for double using floats. So two floats for doing it all. So all that depends on the presentation of floats. In particular, it does a lot of overlays between various types. It uses the representation of NAN, not the number and infinities, which are not in Spark. And it does complex floating point reasoning. So all these things, both at the model level for NAN and infinities and overlays, and at the level of reasoning about this floating point computation is not supported by Provers. So we cannot expect to both specify these functionalities in great detail and prove them automatically in Spark. So we settled for something less ambitious. Let's prove everything that fits the Spark subsets and can be both expressed and proved. So let's prove all the Spark things. So first example of that is the interface to C. So let's take the unit interface C. Here we had to express things in addition to what was in the unit, just to be able to specify some of the functionalities. So we add, for example, a ghost function C length ghost, which adds what it means to have the length of a C string, which ends at the null character. And then this ghost function can be used in contact. And it's self-implemented and proved. So the proof makes heavy use of advanced Spark features like loop invariance for loops to summarize the state of the current iteration of the loop or relaxed initialization for a thing that are locally uninitialized but are progressively initialized inside the loop. But all of these uses are quite simple and I'm going to show you. So here is the this C length ghost function. And you can see that it's implemented here with a simple loop to get to the point where you have the null character and you have a loop invariance as you would expect to prove in Spark when you have a loop to say that so far no character was found to be null. And this Clex function can be used then to specify other functions like this function 2, 8, r. And then you can see that this function 2, 8, r which takes this car array and returns a string. Because depending on the value of this other parameter trim null, it's going to do something different up to the null character or not. And again, in this 2, 8, r, you will see a loop invariance for loops to summarize the the work done so far. And here something else is that when we declare a variable here without initializing it in the array, we can declare it with relaxed initialization. And then inside the loop, we need to specify up to which index this array is initialized. And so proof is going to take care of approving initialization of this variable. If it holds, then it's done by Flona dc in a much more the cursor way and cannot be applied here because the array is progressively initialized. Okay, now let's move on to fixed point support. So returning to this scale divide and other functionalities. So it's implemented here in this various units, array 32, array 64, array double, so which is the generic instantiated in array 64, for example. And here we took the commands in the code which were quite detailed and translated them into Spark contracts. So you can see an example with this adds with all flow check. So we have a function here in in 64 range, which says when an argument, which is a big integer, so arbitrary integer not bounded is within the range of a sign in 64. And so this is a ghost function again, so something that's only for specification and proof. And inside the function add with all flow check. Now we can add a precondition that says for this function to operate properly, it needs to take arguments, which won't have a flow when you add them. So when you do the this summation in big integers, then it fits and the sign in integer 64, then the results will indeed be the result of the addition. And so let's look at that. So in the integer 64 bits, spec it's here, and the implementation here just renames the the generic. So let's look at the generic spec and implementation. So that's just what we describe in terms of spec. And the implementation here uses a number of what we call lemmas. So things, procedures that are ghosts, so only here for for proof, which prove a given property, the best condition from another property given in precondition. So that's a way to isolate a proof so that the automatic provers can do it much more easily. So this proof can be quite involved, as you can see here, with a number of cases being described, assertions by the provers, even some lemmas. So these lemmas are again, the same that as what I just showed, except they are marginal. So I've extracted them here in a different part of the file. And in the ends, the code is not obstructed by the use of all these codes, we're just calling the lemmas where there are needed to prove the post condition in this case. So that's a rather simple case, in fact. So now we turn to the dreaded scale divides. This is much more complex because here we're mixing in sign integer arithmetic and sign some modular integer arithmetic and arbitrary bounded integer arithmetic with these big integers. And you can see that you have quite big lemmas. And these are also proved with a more complex reasoning. And in the end, the implementation as to call this the mass and the right places in the right order for the proof to go through automatically. So we have also proved the character and string handling. So for character, it's in a data character that handling and I've example just at the bottom of the slide and for string, that the body string, the fixed string and maps plus supporting units in that that implement part of these functionalities. And here the specification comes directly from the data reference manual. So the description was translated into spot contracts. A very simple example of that is this function is controlled in characters handling. So it's specified as true if item is a control character. And the control character is defined as the character whose position is one of the ranges 0, 31 or 127, 159. And that's exactly what you have in the post condition here. The result of this function call is whether the position of the item argument is in these ranges. So specification can be a bit more complex for more involved functions. So for example, here in a last string fixed, you can see this function index, which is going to look for position of given pattern in the source string. And here, well, the there are many cases described in the specification, which turn into this large contract cases. So we're using a special form of contracts, which gives depending on various cases here before the row, the result that is expected here. And so here, this unit is in fact based on another implementation in another unit. And so this other implementation has a similar contract. And its body is verified against this contract. And here it calls other variants of index, which are themselves proved against their specification. Let's move now to explanation. So there are various implementation of explanation for sign integers, modern integers, and depending on the value of the module. So for example, here, you have the binomial modular is the simplest. So it specifies at the top here as just well, the expansion left at the exponent right. The sign version is a bit more complex, because we need to make sure that there's no overflow. So it has a precondition that uses this computation in big integers. So we doing the explanation big integers and checking that the result fits in the range. And even more complex case is a modular explanation with a non binary modulus. So when the modulus is not suitable or something, but can be 42. And here, the way to specify it is to say that the results here, X modular tick results, when considered as a beginner is really the operation done here in big integer modular. The value of the modules. So we have to do that because just doing it in modular machine integers would do a double modular and will be incorrect. So if we look now at the code. So as I said, the simplest one is this modular explanation and here it's a simple loop with as you would expect loop invariance and a few sessions. Now, if you look at the sign version, well, it's slightly more complex. So there are a number of them as really it's really thing how the operation works in big integers, especially because exponential is more difficult to reason about with the automatic tools. And so the implementation also has more ghost codes to drive the proof and calls to these lemmas to help programs. And the most complex is this exponentiation of a module type with a non binary modules, because here we have sign integers and sign integers and exponentiation with big integers. And so we have many more lemmas and we have much more effort to drive the course towards the net proof. I would like to finish with the support for a tick image and tick value. So tick image is a way to print values of various types and tick values does the converse. So it takes a string and returns the value. And the goal here is to be able to show that the image and value function in runtime are reverse functions. So give sufficiently precise post condition for value for the value function for type. So that's the post condition of the corresponding image can state value applied to the result of image of the gives back the. So what that's what we do here in this image Boolean in this code snippet, so you can see here at the bottom that indeed when we could value when we call value Boolean on the results s string from one to be because P and s are the result of this procedure. It gives back the input of the major Boolean. And we are in the process of doing that for all of the other type. So if we look now just at this, I wanted to show the specification that is needed for this value for this value for unsigned integers. So it's here. Yeah, scan and sign is one of the functions used here. And you can see that it has quite complex post condition because we need to describe what happens with the blank characters. And what happens with sign and the various ways to specify the value. And so it depends on all these other ghost functions that describe how the base and value pass the base or describe and the experience, etc. So that's all for this project. So the current status is that we managed to find a few mistakes and fix them just possible overflow and run checks. That was the good news. An example of that is the simple tests. So if you compile these codes, well, you will get an error. But not necessarily the one you expect. So here we are trying to get a Boolean value from the string which just contains a blank character. So this is incorrect and what you would expect and you will get in the next version is this last line. A constraint error is raised because it's a bad input for the attribute value here. Well, if you use the community with 20 20 version of previous, you will get the segmentation port in fact, because underneath there's a level flow in the runtime support code here. And you end up reading and writing much past the string here. And this flow happens as you would expect because the string of one character is located with the index naturalty class. So at the extreme value of possible indices here. Saisetation is slightly better with the latest version of net community 2021. Because here, instead of the segmentation port, you get the constraint error. But not the one you would expect. In fact, in this version of net community, the runtime was compiled with runtime checks on, but not overflows. So the overflow is silent. But then you get a runtime check failure when we're trying to access the array s beyond the start. So you get this index check failed. So what we are with that, we have a partial proof of the net lifetime library. So for 35 units. So that's not nothing, but that's far from the total number of units here. So as I said, using the exit to 64 version around one and run 80 units. The daily proof takes one hour and 30 minutes on the quite big server. So 63 cores Linux server. And we do all the configurations that I mentioned here. So for ARM or exit the six Linux with Vakesforks or their metal. In total, we added many specifications inside these units. So almost 400 preconditions, 500 plus conditions. The proof also requires more than just the specifications to drive the prover towards proof. So what we call ghost code, which is not executed in the end, in particular, because inside these units, we specify that ghost code should be ignored during the final compilation. So we have to add almost 150 loop invariance, almost 400 assertions, and almost 300 ghost entities, so types, variables, and many of these are actually lemas. So 150 lemas, that's what I showed you, ways to prove a given property in a smaller context. So that's automatic provers can do it automatically. And that leaves us with two questions for the future. Can this effort benefit the future specifications of the runtime by adding more guarantees to what we can do today with testing only? And also what can we do beyond what Spark supports currently? Can we do something in particular for units that use these addresses and condition to pointers that currently are not supported? Well, thank you for your attention, and I'm waiting for your questions. Then you consider that having 60 plus lines of contracts for five lines of... Okay, I'll continue since you disconnected. So the question was, do you consider that having 60 plus lines of contract for a declaration in that which is initially five lines makes the specification unreadable? And so initially, I understood this question wrong. I thought you was talking about five lines body. And indeed, there should be a relationship between the complexity of the function that you are trying to specify and the specification. And then depends how far you want to go in terms of specification. So here we went for the platinum level, wanted to fully specify functionally this function. And so the fact that the function declaration in Ada is five lines is a bit irrelevant. It doesn't say really the complexity of the function that you're trying to implement. You could have underneath the wall, the wall, a system that you're implementing or just a really small leaf function. And so that's where I think it matters. Do you learn something by specifying this larger contract like this 60 lines of contract? And so here in this case, it was pointing at the index function, which I pointed that in my talk for string manipulation. And the contract is actually quite readable. So it specify exactly what these cases are in the index function. And if you don't write this as a form of contract, well, you have English prose that you will find in the other reference manual, which is itself usually not self-contained. So you have various paragraph of the reference manual, which and end up defining the behavior of the function. So I think in the end, so there are two answers. The contract should matter to you. So it should say something interesting, otherwise, maybe don't do that. It relates also to the level at which you want to prove the code. And then in terms of use of IDEs, I hope that in the future, we have ideas which allow to hide these contractual codes like we hide the comments. And so that's something we've discussed, for example, for our future support of Spark in various IDs, whether it's the visual code or that's to you. And thank you. Another question. A previous speaker made some comments regarding Provers having to work together to prove everything. How does it work in your experience? Did you use all three? One? So yes, Spark is tailored to benefit the most from the combination of Provers, so that you have the least to do in terms of helping the Prover. If you just limit yourself to one Prover, it's just you're cutting yourself from two-thirds of the automation. And so that's just a pain. And in fact, what I did was to use the four Provers that we have now. So there's one called Colibri, which is not enabled by default because we're still working with the developers for having a better integration. But it's inside the technology, you can enable it. So there's just a switch, Prover All to have all four Provers, and here it's useful. So yes, we use constantly, as soon as you have more complex proof that go beyond basic type safety. So even the proof that the Rothschildman showed about more complex predicates and types, here you needed the three Provers, and here I needed even the four Provers that were not. Okay, thank you. Stefan asks, how do you debug, identify the issues when you write a complex contract and it fails during execution? Yeah, so here it didn't really apply because the way we use contracts for the runtime library is that we don't want these contracts to be executed. So we never execute them. We have a pragma assertion policy that we use all over the runtime to say that these contracts will never be executed. So these contracts are really here only for proof. And so if you want to make sure that the preconditions in particular are correct, you have to read them. And in general, when you develop contracts, what you should be careful about is that the contracts at the border with things that are not proofed, typically the preconditions for library, for example, when you call it from elsewhere, if the code that uses this library is not proved, the precondition could fail. So either it's a good thing because then you prevent getting into your API with the wrong context, or you don't want it to happen, and then you have to test enough. And so yeah, how do you identify that precondition, for example, is wrong? Well, here, the failure in the test, for example, would give you a scenario which you can debug. And so in contracts in Ada or Spark, or just like code, you can debug and test them. Okay, thank you. We have about a minute. Fredrik asks, did the proofs require a lot of gist functions? Yes, so there was quite a lot of gist functions, like I mentioned, but even more gist lemas, so things that you need to prove in isolation, because then the context is smaller for proof. And I also wanted to address one question, which is, is it worth it? So that was the same question as for Rod. For us here, yes, at least in terms of making sure we are sufficiently confident in this runtime to be seen if we can exploit that more generally in certification. So for here, I cannot say right now, for example, that we will benefit in certification from this proof compared to the stretching approach of specification and testing. Okay, so we have 10 seconds. There are questions that have not been answered. The room will now open and everybody is more than welcome to join. Thank you, Janik. Thank you.
 Hello, I'm going to talk about the project I've been working on for the past six months  with my colleague Pierre-Alexandre Bazin about proving the correctness of the Gnatt Light  Runtime Library. So what is this Gnatt Runtime Library? That's what we called previously at the  decor the zero footprint ZFP or Revenscar SFP or SERT Runtime. So now it's divided between the  light runtime and a more encompassing embedded runtime. And this light runtime is targeted  that's embedded platforms. So we have 77 platforms supported right now. Most of them are bare metal  with a variety of chips ARM, Leon, PowerPC, RISP5, X86 and X86 64 bits. And sometimes  with an S on top, so like PyCoS or X-Wars. And the units of that runtime are ready for  certification. So a subset of these have been already certified for use in various projects  in avionics, in space, in railway, in automotive, subject to the suitable certification  documents. So like DO178 for avionics, ECSS for space, EN51284 railway and ISO26262 for automotive.  So you can say that the units in that runtime are this subject to a high degree of scrutiny with  proper specifications put in place and test suites and reviews etc. So you can build this  runtime based on the project that you have available truly on GitHub in BB runtimes  where it takes the sources from the DCP3 and the net sources subdirector.  So just to give you a tour quickly of these units in the net light runtime, if I take the X86 64 bits  version, because of course for each version you have different number of units. And here it has  182 spec files. And I'm only counting the spec files here because some of them are just spec files,  but some of them are bodies and some of them are instantiations of generics. So they have  spec plus bodies, but declared just as a spec file. So between all of these 182 files, you have of  course support for the ADAS standard library. So that's the A-iPhone something files and the  I-iPhone something files for interfaces. So you have here a carton string handling, you have some  Nurex library, you have support for assertions and exceptions, but in this runtime there's no  propagation of exceptions, it's only local or calling the last-hand handler. And there's interfaces  with C. You have also a little bit of the Gnats user library, so we have a few G-something files,  it's mostly for I-O. And you have many files that deal with the support for  features of the language, so the Gnat runtime library, so you have 104 T as dash something files.  And so here you have support for various attributes like tick image, tick value, tick width,  attributes of floating point numbers. You have support for I-fed collaborations, especially  on fixed points and floats and explanations, including contagious and some Nurex,  and support for tasking. So all of that. Now I'm going to talk about proof. So proof using the  Spark tool. It's a formal verification tool doing two kinds of analysis, one called flow analysis  and one called proof. And proof is the most involved whether it asks provers about the  validity of some formulas which entail the correction of the code. And so here you can  see very briefly a depiction of the architecture of the Spark tool, where it starts from the  complete left inside an editor, where you can see the codes. And at the bottom you can see here  some Spark codes say assigning a value 42 in index one of array A. And through some codes,  part of it which is shared with the compiler, what I called the Gnat here, we transform that code into  a YML from intermediate form. So that's this code in the middle which represents the assignment on  the left. And which is represented by this question mark in the middle, which is the  symbol of the Y3 platform. And this platform dedicated to proof programs then generates formulas. So  you can see an example of a bit of a formula in this SMT lip syntax on the bottom right. And these  formulas are dispatched to various provers, in particular automatic provers like AlphaGo, CVC4  and D3, which are all included in the Spark technology. Okay. So in Spark, we emphasize the  fact that proof is not an all or nothing endeavor. So you can start at some bottom level, which we  call the stone level, where you have only the guarantees of having a better, safer subset of  the language. And then you can go up the scale here with the bronze level for checking constraints  of data and information flow and making sure that everything is initialized. Silver level is about  making sure that there are no runtime errors, particularly no CW in the codes. At the goal  level, you can start proving key integrity properties, whether it's there really to safety or  security. And at the platinum level, you can prove fully functionally the code. And so typically,  the platinum level is applied to a much smaller subset of the codes than what's, than where you  can apply lower levels. And the main target, usually the silver level, so absence of contenders.  But here in this project, we're going to target this platinum level, so fully functionally  describing the behavior and proving that the code complies with this specification.  So first, a little motivating example for this project. And so we're going back to 2012, when  we were adding support for big integers in that, so mathematical integers inside the compiler,  was motivated by a feature in Spark to allow intermediate computations without overflows.  So we do them using full mathematical possibilities to ignore the possibility of overflows in  some proof. And implementation was done by the late great developer, Robert DeWor,  so founder of Hedycorp, and used to always be for this multi precision division.  So we have integers in a number of machine integers. So you have array of machine integers to  represent large integers. And this algorithm is described in the art of computer programming,  volume two. So we use the second edition from 1981. And this will have an port Slater,  that's why I'm mentioning it here. At the time, so the reviewer told him that in the code that  he had written, there was a possible overflow in this large piece of code, this large expression.  But Robert, knowing that he had implemented the code from Knuse's book correctly,  and assuming that the book was correct, was not convinced by this possibility of an overflow,  and asked for an actual issue. So the reviewer went back to the codes and finally came up with  this example. So try this long multiplication division, which corresponds to activating  this expression leading to an overflow. And indeed, Robert recognized that the true results  was different from the computation in the codes given by Knuse. So what happened? Well, even the  best like Knuse and Robert DeWorra can get it wrong, especially when it comes to these very low level  details, repeat to possible runtime errors, and especially when it comes to overflows.  And regarding this specific computation, in fact, the bug had been already fixed in an  ereta of volume two in 1995. So that's this part here, this test, which needs to be done to prevent  the possible overflow. But that's not the end of it. So 10 years later, it was this test was fixed  again. So it was not actually an equality that should be on here, but a greater or equal test.  So hopefully after that, we have a correct description of the algorithm that can be implemented  without overflows. So that's what we did. But obviously, algorithm gets implemented in many  places. And that was the case in the compiler. So this algorithm was used in two other units.  In this unit, you in pitch for arbitrary present computation during the combination.  And in this other unit system that's are it 64 to support six point are a fake because six points  are represented internally by the compiler integers with some scale. And so you need this kind of  competitions. But obviously not to compete, not to implementations are alike, there are different  constraints in the that has that are represented. And so on the one side, we fixed the computation in  you in pitch, although we couldn't find an obvious bug. But the computation was was the one that  could be fixed. In the system that's are it 64, the test was done differently. And so we didn't  find a bug. So didn't apply the fix and hope that it was okay. Now fast forward to 2019.  Here we were, as we usually do at the decor, doing a runtime certification for space. And one of  the external reviewers looking at this unit for six point support and in particular, at algorithm  D implemented in scale device made the remark that we should increase common frequency to a better  implement put to better understand the working in the working of the algorithm. So that's led to a  new internal review. And during this internal review, we detected the two possible silent  overflows in another related function, so double divide, and the missing exception. So some case  which should raise an exception, but here was not doing it in the scale device. So that's not good.  That was not so bad in fact, because as I said, the overflows were were silence.  So we're doing the right thing in the end. And the missing exception was just on incorrect  input. Still a colleague from the specification team challenged us to start team to prove the  unit. So we set set on doing that. And one week of work later, we got all the algorithm except  this scale divide implementing algorithm D, which was more complex proof. So we tried to have a  discussion with the specification team, but priorities to con and the while everyone moved on.  Until recently, so last year, during a summer internship, a very good intern Pierre-Alexandre  Bazin updated the proof that we had done two years before and finally proved this scale divide  implementation. And so now it has moved. So it's in this new file s Arizu because it's a generic  implementation now for 64 and 128 bits. So you have this big contracts at first, but which is  quite readable. So you can look at the past condition of scale divide. Indeed, it says that  if you go to big integers, that's this conversion to big for all the values involved here.  The result are is really the the remnants, the result of the remnants of the multiplication  of x times y divided by it. And for Q, if you ignore rounding, which is just a slightly more  complex case, the quotient Q is really the quotient of x time y in mathematics divided by it.  And the application is just to prevent an overflow during this competition. So great.  That was proved. We were very happy to learn that finally, our implementation that had been  certified was indeed the probably correct. So we say, well, let's go from there and prove everything.  But the runtime is not exactly in Spark. There are a lot of uses of untyped memory for many good  reasons to handle the cigarette stack for a rare comparisons for things that are not necessarily even  aligned for also ports to get to the tags of objects dynamic type for binding to C string. So  many reasons to use in data addresses, so type address and doing uncheck conversions between  address and the pointer types. And this is something that is not at all supported by the  ownership system that we have in Spark, which is a fully typed. Plus, not everything is not  is provable. In these units, there are a lot of support for low level floating point operations  for some language attributes in Ada, regaining floats. There are also low level support for  numerics like trigonometry. There's things that do double arithmetic for double using floats.  So two floats for doing it all. So all that depends on the presentation of floats. In particular,  it does a lot of overlays between various types. It uses the representation of NAN,  not the number and infinities, which are not in Spark. And it does complex floating point reasoning.  So all these things, both at the model level for NAN and infinities and overlays, and at the level  of reasoning about this floating point computation is not supported by Provers. So we cannot expect  to both specify these functionalities in great detail and prove them automatically in Spark.  So we settled for something less ambitious. Let's prove everything that fits the Spark  subsets and can be both expressed and proved. So let's prove all the Spark things.  So first example of that is the interface to C. So let's take the unit interface C.  Here we had to express things in addition to what was in the unit, just to be able to specify  some of the functionalities. So we add, for example, a ghost function C length ghost,  which adds what it means to have the length of a C string, which ends at the null character.  And then this ghost function can be used in contact. And it's self-implemented and proved.  So the proof makes heavy use of advanced Spark features like loop invariance for loops to summarize  the state of the current iteration of the loop or relaxed initialization for a thing that are  locally uninitialized but are progressively initialized inside the loop. But all of these  uses are quite simple and I'm going to show you. So here is the this C length ghost function.  And you can see that it's implemented here with a simple loop to get to the point where you have  the null character and you have a loop invariance as you would expect to prove in Spark when you  have a loop to say that so far no character was found to be null. And this Clex function can be  used then to specify other functions like this function 2, 8, r. And then you can see that  this function 2, 8, r which takes this car array and returns a string. Because depending on the  value of this other parameter trim null, it's going to do something different up to the null  character or not. And again, in this 2, 8, r, you will see a loop invariance for loops to summarize  the the work done so far. And here something else is that when we declare a variable here without  initializing it in the array, we can declare it with relaxed initialization. And then inside the loop,  we need to specify up to which index this array is initialized. And so proof is going to take care  of approving initialization of this variable. If it holds, then it's done by Flona dc in a much more  the cursor way and cannot be applied here because the array is progressively initialized.  Okay, now let's move on to fixed point support. So returning to this scale divide and other  functionalities. So it's implemented here in this various units, array 32, array 64, array double,  so which is the generic instantiated in array 64, for example. And here we took the commands in the  code which were quite detailed and translated them into Spark contracts. So you can see an example  with this adds with all flow check. So we have a function here in in 64 range, which says when an  argument, which is a big integer, so arbitrary integer not bounded is within the range of a sign  in 64. And so this is a ghost function again, so something that's only for specification and proof.  And inside the function add with all flow check. Now we can add a precondition that says  for this function to operate properly, it needs to take arguments, which won't have a flow when  you add them. So when you do the this summation in big integers, then it fits and the sign in  integer 64, then the results will indeed be the result of the addition. And so let's look at that.  So in the integer 64 bits, spec it's here, and the implementation here just renames the  the generic. So let's look at the generic spec and implementation. So that's just what we describe  in terms of spec. And the implementation here uses a number of what we call lemmas. So things,  procedures that are ghosts, so only here for for proof, which prove a given property, the  best condition from another property given in precondition. So that's a way to isolate a proof  so that the automatic provers can do it much more easily. So this proof can be quite involved,  as you can see here, with a number of cases being described, assertions by the provers,  even some lemmas. So these lemmas are again, the same that as what I just showed, except  they are marginal. So I've extracted them here in a different part of the file. And in the ends,  the code is not obstructed by the use of all these codes, we're just calling the lemmas where  there are needed to prove the post condition in this case. So that's a rather simple case, in fact.  So now we turn to the dreaded scale divides. This is much more complex because here we're mixing  in sign integer arithmetic and sign some modular integer arithmetic and arbitrary bounded  integer arithmetic with these big integers. And you can see that you have quite big lemmas. And  these are also proved with a more complex reasoning. And in the end, the implementation  as to call this the mass and the right places in the right order for the proof to go through  automatically. So we have also proved the character and string handling. So for character, it's in  a data character that handling and I've example just at the bottom of the slide and for string,  that the body string, the fixed string and maps plus supporting units in that that  implement part of these functionalities. And here the specification comes directly from the  data reference manual. So the description was translated into spot contracts. A very simple  example of that is this function is controlled in characters handling. So it's specified as true  if item is a control character. And the control character is defined as the character whose  position is one of the ranges 0, 31 or 127, 159. And that's exactly what you have in the  post condition here. The result of this function call is whether the position of the item argument  is in these ranges. So specification can be a bit more complex for more involved functions. So  for example, here in a last string fixed, you can see this function index, which is going to look  for position of given pattern in the source string. And here, well, the there are many cases  described in the specification, which turn into this large contract cases. So we're using a special  form of contracts, which gives depending on various cases here before the row, the result that is  expected here. And so here, this unit is in fact based on another implementation in another unit.  And so this other implementation has a similar contract. And its body is verified  against this contract. And here it calls other variants of index, which are themselves  proved against their specification. Let's move now to explanation. So there are various  implementation of explanation for sign integers, modern integers, and depending on the value of  the module. So for example, here, you have the binomial modular is the simplest. So it specifies  at the top here as just well, the expansion left at the exponent right. The sign version is a bit  more complex, because we need to make sure that there's no overflow. So it has a precondition  that uses this computation in big integers. So we doing the explanation big integers and  checking that the result fits in the range. And even more complex case is a modular explanation  with a non binary modulus. So when the modulus is not suitable or something, but can be 42.  And here, the way to specify it is to say that the results here, X modular tick results,  when considered as a beginner is really the operation done here in big integer modular.  The value of the modules. So we have to do that because just doing it in modular machine integers  would do a double modular and will be incorrect. So if we look now at the code.  So as I said, the simplest one is this modular explanation and here it's a simple loop with  as you would expect loop invariance and a few sessions. Now, if you look at the sign version,  well, it's slightly more complex. So there are a number of them as really  it's really thing how the operation works in big integers, especially because  exponential is more difficult to reason about with the automatic tools. And so the implementation  also has more ghost codes to drive the proof and calls to these lemmas to help programs.  And the most complex is this exponentiation of a module type with a non binary modules,  because here we have sign integers and sign integers and exponentiation with big integers.  And so we have many more lemmas and we have much more effort to drive the course towards  the net proof. I would like to finish with the support for a tick image and tick value. So  tick image is a way to print values of various types and tick values does the converse. So it  takes a string and returns the value. And the goal here is to be able to show that the image  and value function in runtime are reverse functions. So give sufficiently precise  post condition for value for the value function for type. So that's the post condition of the  corresponding image can state value applied to the result of image of the gives back the.  So what that's what we do here in this image Boolean in this code snippet, so you can see here  at the bottom that indeed when we could value when we call value Boolean on the results s string  from one to be because P and s are the result of this procedure. It gives back the input of the  major Boolean. And we are in the process of doing that for all of the other type. So if we look now  just at this, I wanted to show the specification that is needed for this  value for this value for unsigned integers. So it's here.  Yeah, scan and sign is one of the functions used here. And you can see that it has quite complex  post condition because we need to describe what happens with the blank characters.  And what happens with sign and the various ways to specify the value. And so it depends on all  these other ghost functions that describe how the base and value pass the base or describe  and the experience, etc. So that's all for this project. So the current status is that we managed  to find a few mistakes and fix them just possible overflow and run checks. That was the good news.  An example of that is the simple tests. So if you compile these codes, well, you will get an error.  But not necessarily the one you expect. So here we are trying to get a Boolean value from the  string which just contains a blank character. So this is incorrect and what you would expect and  you will get in the next version is this last line. A constraint error is raised because it's  a bad input for the attribute value here. Well, if you use the community with 20 20 version of  previous, you will get the segmentation port in fact, because underneath there's a level flow  in the runtime support code here. And you end up reading and writing much past the string here.  And this flow happens as you would expect because the string of one character is located with the  index naturalty class. So at the extreme value of possible indices here.  Saisetation is slightly better with the latest version of net community 2021.  Because here, instead of the segmentation port, you get the constraint error. But not the one you  would expect. In fact, in this version of net community, the runtime was compiled with runtime  checks on, but not overflows. So the overflow is silent. But then you get a runtime check failure  when we're trying to access the array s beyond the start. So you get this index check failed.  So what we are with that, we have a partial proof of the net lifetime library. So for 35 units.  So that's not nothing, but that's far from the total number of units here. So as I said,  using the exit to 64 version around one and run 80 units. The daily proof takes one hour and 30  minutes on the quite big server. So 63 cores Linux server. And we do all the configurations that I  mentioned here. So for ARM or exit the six Linux with Vakesforks or their metal.  In total, we added many specifications inside these units. So almost 400 preconditions, 500  plus conditions. The proof also requires more than just the specifications to drive the prover  towards proof. So what we call ghost code, which is not executed in the end, in particular, because  inside these units, we specify that ghost code should be ignored during the final compilation.  So we have to add almost 150 loop invariance, almost 400 assertions, and almost 300 ghost entities,  so types, variables, and many of these are actually lemas. So 150 lemas, that's what I showed you,  ways to prove a given property in a smaller context. So that's automatic provers can do it  automatically. And that leaves us with two questions for the future. Can this effort benefit the  future specifications of the runtime by adding more guarantees to what we can do today with testing  only? And also what can we do beyond what Spark supports currently? Can we do something in particular  for units that use these addresses and condition to pointers that currently are not supported?  Well, thank you for your attention, and I'm waiting for your questions.  Then you consider that having 60 plus lines of contracts for five lines of...  Okay, I'll continue since you disconnected. So the question was, do you consider that having  60 plus lines of contract for a declaration in that which is initially five lines  makes the specification unreadable? And so initially, I understood this question wrong.  I thought you was talking about five lines body. And indeed, there should be a relationship  between the complexity of the function that you are trying to specify and the specification.  And then depends how far you want to go in terms of specification. So here we went for the platinum  level, wanted to fully specify functionally this function. And so the fact that the function  declaration in Ada is five lines is a bit irrelevant. It doesn't say really the complexity  of the function that you're trying to implement. You could have underneath the wall,  the wall, a system that you're implementing or just a really small leaf function. And so that's  where I think it matters. Do you learn something by specifying this larger contract like this  60 lines of contract? And so here in this case, it was pointing at the index function, which I  pointed that in my talk for string manipulation. And the contract is actually quite readable.  So it specify exactly what these cases are in the index function. And if you don't write this as a  form of contract, well, you have English prose that you will find in the other reference manual,  which is itself usually not self-contained. So you have various paragraph of the reference manual,  which and end up defining the behavior of the function. So I think in the end, so there are  two answers. The contract should matter to you. So it should say something interesting,  otherwise, maybe don't do that. It relates also to the level at which you want to prove the code.  And then in terms of use of IDEs, I hope that in the future, we have ideas which allow to hide  these contractual codes like we hide the comments. And so that's something we've discussed, for example,  for our future support of Spark in various IDs, whether it's the visual code or that's to you.  And thank you. Another question. A previous speaker made some comments regarding Provers  having to work together to prove everything. How does it work in your experience? Did you use all  three? One? So yes, Spark is tailored to benefit the most from the combination of Provers,  so that you have the least to do in terms of helping the Prover. If you just limit yourself to  one Prover, it's just you're cutting yourself from two-thirds of the automation. And so that's  just a pain. And in fact, what I did was to use the four Provers that we have now. So there's one  called Colibri, which is not enabled by default because we're still working with the developers  for having a better integration. But it's inside the technology, you can enable it. So there's  just a switch, Prover All to have all four Provers, and here it's useful. So yes, we use  constantly, as soon as you have more complex proof that go beyond basic type safety. So even the  proof that the Rothschildman showed about more complex predicates and types, here you needed  the three Provers, and here I needed even the four Provers that were not.  Okay, thank you. Stefan asks, how do you debug, identify the issues when you write a complex  contract and it fails during execution? Yeah, so here it didn't really apply because the way we  use contracts for the runtime library is that we don't want these contracts to be executed.  So we never execute them. We have a pragma assertion policy that we use all over the  runtime to say that these contracts will never be executed. So these contracts are really here  only for proof. And so if you want to make sure that the preconditions in particular are correct,  you have to read them. And in general, when you develop contracts, what you should be careful  about is that the contracts at the border with things that are not proofed, typically the  preconditions for library, for example, when you call it from elsewhere, if the code that uses  this library is not proved, the precondition could fail. So either it's a good thing because then  you prevent getting into your API with the wrong context, or you don't want it to happen,  and then you have to test enough. And so yeah, how do you identify that precondition, for example,  is wrong? Well, here, the failure in the test, for example, would give you a scenario which  you can debug. And so in contracts in Ada or Spark, or just like code, you can debug and test them.  Okay, thank you. We have about a minute. Fredrik asks, did the proofs require a lot of  gist functions? Yes, so there was quite a lot of gist functions, like I mentioned, but even more  gist lemas, so things that you need to prove in isolation, because then the context is smaller  for proof. And I also wanted to address one question, which is, is it worth it? So that was  the same question as for Rod. For us here, yes, at least in terms of making sure we are sufficiently  confident in this runtime to be seen if we can exploit that more generally in certification. So  for here, I cannot say right now, for example, that we will benefit in certification from this proof  compared to the stretching approach of specification and testing. Okay, so we have 10 seconds.  There are questions that have not been answered. The room will now open and everybody is more  than welcome to join. Thank you, Janik. Thank you.
ada_proving_gnat_light_runtime_0_155.png ada_proving_gnat_light_runtime_156_347.png ada_proving_gnat_light_runtime_348_719.png ada_proving_gnat_light_runtime_720_2963.png ada_proving_gnat_light_runtime_2964_5675.png ada_proving_gnat_light_runtime_5676_7895.png ada_proving_gnat_light_runtime_7896_9683.png ada_proving_gnat_light_runtime_9684_9815.png ada_proving_gnat_light_runtime_9816_12923.png ada_proving_gnat_light_runtime_12924_13415.png ada_proving_gnat_light_runtime_13416_13883.png ada_proving_gnat_light_runtime_13884_19943.png ada_proving_gnat_light_runtime_19944_20051.png ada_proving_gnat_light_runtime_20052_22691.png ada_proving_gnat_light_runtime_22692_22739.png ada_proving_gnat_light_runtime_22740_22847.png ada_proving_gnat_light_runtime_22848_24347.png ada_proving_gnat_light_runtime_24348_24539.png ada_proving_gnat_light_runtime_24540_25607.png ada_proving_gnat_light_runtime_25608_26651.png ada_proving_gnat_light_runtime_26652_28739.png ada_proving_gnat_light_runtime_28740_31451.png ada_proving_gnat_light_runtime_31452_31607.png ada_proving_gnat_light_runtime_31608_31787.png ada_proving_gnat_light_runtime_31788_32075.png ada_proving_gnat_light_runtime_32076_33731.png ada_proving_gnat_light_runtime_33732_35411.png ada_proving_gnat_light_runtime_35412_37487.png ada_proving_gnat_light_runtime_37488_38099.png ada_proving_gnat_light_runtime_38100_38375.png ada_proving_gnat_light_runtime_38376_39143.png ada_proving_gnat_light_runtime_39144_39215.png ada_proving_gnat_light_runtime_39216_39335.png ada_proving_gnat_light_runtime_39336_40967.png ada_proving_gnat_light_runtime_40968_42239.png ada_proving_gnat_light_runtime_42240_42299.png ada_proving_gnat_light_runtime_42300_42347.png ada_proving_gnat_light_runtime_42348_48227.png ada_proving_gnat_light_runtime_48228_48275.png ada_proving_gnat_light_runtime_48276_48851.png ada_proving_gnat_light_runtime_48852_52307.png ada_proving_gnat_light_runtime_52308_52655.png ada_proving_gnat_light_runtime_52656_54215.png ada_proving_gnat_light_runtime_54216_54455.png ada_proving_gnat_light_runtime_54456_56495.png ada_proving_gnat_light_runtime_56496_56711.png ada_proving_gnat_light_runtime_56712_57695.png ada_proving_gnat_light_runtime_57696_58080.png