FOLLOW US ON:
HEADQUARTER POSTAL ADDRESS:
OUR OFFICE IS LOCATED HERE:
By Dr. Jacob Boender, Formal Verification Engineer at HENSOLDT Cyber GmbH
One of the specialties of HENSOLDT Cyber is *formal verification*. This may sound very sophisticated, but what is it exactly? In this blog, we will endeavor to explain. In general, whenever we write a computer program, we would like it to behave exactly the way we want it to. But how to be sure? Generally, the way software developers do this is by *testing*; running a program under specific circumstances and checking that it then does the right thing.
However, testing is not entirely foolproof. The main drawback is that it is only run on a limited number of test cases: if you do not include a particular test case, any bugs that test case might reveal will only show up when your program is actually in use (with dire consequences ensuing…)
The approach of formal verification is different: we use mathematical methods (either automatic, such as model checking, or manual, like interactive theorem proving) to *prove* properties of the program, for example that its output is what we expect it to be, or that it doesn’t keep running forever. Since we’re checking properties of the program as a whole, we’re not dependent on whether we’ve covered everything with test cases.
Of course, formal verification is not perfect either: since we are reasoning about the program, we must have some sort of idea of how it behaves—in other words, we need to have a mathematical model of the programming language our program is written in. And if this model is different from how the program behaves on a real machine, errors might still occur.
So, while formal verification cannot replace testing, it does offer another way of checking a program for errors that is highly complementary to testing. And therefore, it allows you to be more confident about the correctness of your program – and that’s what it’s all about in the end!
Thanks for the insight, I would appreciate a follow up blog post describing your approach to formal verification. Are you using Cogent for instance or some other methods, and what is your experience with the different methods. Are any particular components of TRENTOS-M easier to verify?. If so, which and why?
Spark/Ada is another approach to formal verification that could be of interest for user applications as Spark/Ada is a very well integrated solution. Maybe they have complementary uses?
Hey – sorry I’m only now replying to this, I don’t seem to receive notifications when there are comments…As to your question, I have written a post about the result of our first big formal verification project, which may answer some of your questions; but in general our approach is post-facto verification with Isabelle and AutoCorres. We haven’t verified a lot of components yet (it takes a lot of time!) so I can only say in general that the more complicated a component is, the more difficult it is to verify (it won’t amaze you to learn this, I imagine…)
We know of Cogent, and have been experimenting with it here and there – I think it’s an interesting solution that has a lot of potential, but we haven’t used it for anything big yet. Hopefully that will change soon.
Spark/Ada we know of as well – it’s a different approach, since it is more towards the model checking end of the spectrum. A truly killer solution would be something that combines the flexibility of deductive verification methods with the automation of model checking, but there’s still a lot of research to be done before we get there (in a way that’s applicable for industrial-scale software developments)…
Do you use Coq and/or Agda to formally verify the correctness of programs at Hensoldt?
Hi Daniel – we use Isabelle, mostly because there’s a lot of available libraries for C verification, such as the C parser and AutoCorres. (My background before joining Hensoldt Cyber was almost entirely in Coq, so I know it well; it’s a very elegant system and I do miss working with it sometimes…)