Formal Verification Keystore

Dr. Jaap Boender, Formal Verification Engineer at HENSOLDT Cyber

In a previous blog post, we talked about formal verification and how we can convince ourselves (and others!) that a piece of software really works as intended. Now that we have managed to complete formal verification of our first component, the keystore, I would like to talk about it in more detail.

First of all, it is important to note that formal verification is not at all like the standard method of ensuring that software works – testing. Rather than running a program with all possible inputs and checking that the output is what we expect, formal verification is more like printing out the source code and going through it with a fine-tooth comb to make sure it does what it is supposed to and does notcontain any bugs.

If we really did it that way, the process would be pretty error prone, but we have a piece of software called an interactive theorem prover that checks our reasoning for us to make sure it is valid and we have not forgotten anything. We still must write the proof ourselves, but the theorem prover makes sure the proof is correct. (For this to work, the theorem prover must have some idea of our programming language – it has to know exactly what each statement in the source code does!)

This makes the process very labor intensive because we have to check everything: For example, whenever an array is accessed, we have to prove that it is within bounds; whenever there is a loop, we have to prove that it terminates; and so on. The advantage of this level of detail is that afterwards we really know that we have covered all the possible things that can happen.
 
After we have checked that there are no bugs, we can check that the software does what we want it to do. Here we use a specification; basically, an implementation of the program that leaves out a lot of the dirty details so we can focus on what it does. This simple specification is much easier to understand, and it is also much easier to convince ourselves that it has the properties we want (in the case of key storage, for example, that applications cannot access each other’s keys).
 
We can then verify that the implementation is a reflection of the specification, so it behaves the same way. And with that, we have verified our software: We know that our specification is valid, and we have proven that our implementation behaves exactly like the specification – so the implementation must also be valid.
READ MORE

Be the first to hear about our products and innovations!

Share on facebook
Share on linkedin
Share on email

Leave a Reply

Your email address will not be published. Required fields are marked *