Hi Adam,
This is not just an issue of using some tools…
You need a formalisation in mathematical logic of (a) a specification of the functionality of your code and (b) the code itself. You then need to prove a lot of theorems that in the end show that (b) is a refinement of (a), meaning all possible behaviours of (b) are allowed by (a). In our case (b) is obtained by using our C parser to convert the C code into statements in higher-order logic. That C parser itself is written in that logic, defines an operational semantics of our C subset and thus gives the C program a formal meaning. This is described in this paper: https://ts.data61.csiro.au/publications/nictaabstracts/Klein_AEMSKH_14.abstr...
Additional things to note:
1) Our C parser does not support all of C, but the subset that seL4 is written in. Most of the things omitted you shouldn’t use anyway (such as goto), the biggest restriction is that it doesn’t allow you to pass references to automatic variables. If your program isn’t in our C subset, the parser won’t grog it.
2) To our knowledge, no-one has done an operational semantics of C++ (some people have tried but seem to have got nowhere). So C++ is way out for now.
3) In our experience, verifying non-trivial code that hasn’t been written with verification in mind is still infeasible. So functionally verifying an existing code-base isn’t likely to work.
4) Specifying the functional properties (a) generally requires a strong formal-methods background
5) Doing the refinement proof is a lot of hard work even for experts. For seL4, there are about 20 lines of proof script per line of C code.
Gernot
On 30 May 2017, at 9:24 , Adam Badura mailto:adam.f.badura@gmail.com> wrote:
I expect this might be (or even probably is) a bad place to ask this but at the same time I didn’t find any better coming from the Contact Information page (http://sel4.systems/contact/).
I’m working on a conference paper (not sure if I will make it but still trying to – code::divehttp://codedive.pl/ if anyone would be interested) about proving program correctness. Considering my own knowledge in the field and expected knowledge of the audience there would be nothing new in that paper – more like an update on what is the current state of the field. Yet I wanted to supply also some examples.
As main example I would like to show proof (or at least parts of it) of correctness (adherence to specification) of C++ code, possibly reduced to C code if need be. After research in this topic and finding this project some time ago it felt natural to reuse its tools. But I fail to do so. Could you possibly guide me? Using your tools and techniques what should I do to prove correctness of some piece of code. I think source code level would be more than enough – for this task no need to verify binary in any form.
As a side example I would like to show how your proves look like. I’m not sure what you are generating / writing as a proof (that gets later verified automatically). I imagine a sequence of something. Some formulas in natural deduction perhaps? Or something else? Whatever that would be I guess it must be pretty long so it is not like I would show and analyze it all but instead would like to somehow let the audience “feel the size”.
If – as I expect – this is not the right place to ask and you cannot help me with above questions, could you at least point me to where to ask them?
Adam Badura
_______________________________________________
Devel mailing list
Devel@sel4.systemsmailto:Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
