hi,
When does seL4 get re-proven? When code gets pulled into the master branch on github? Once a year? Something in-between?
Is it clear what code is actually proven? Is everything in github under the proofs? Or are there things that fall outside the proven kernel? How would anybody see that?
:-)
Thanks!
Hi Raoul,
yes, this is a good one to add to the FAQ.
seL4 gets re-proven semi-continuously. You can see the proof updates coming through on https://github.com/seL4/l4v/commits/master and you can see the kernel revision the proof currently refers to in https://github.com/seL4/verification-manifest/blob/master/default.xml
It's usually the head of the master branch.
Your guess is right that re-proof usually happens when something gets pulled onto the seL4 master branch. The rough protocol for that is that together with the kernel team, the verification team picks the next feature(s) usually from the experimental branch, isolates them on a separate small feature branch, starts verifying that, and when done, merges both into the proof repository and seL4-master. Occasionally, something new gets directly into master, is verified there and then pulled through to experimental.
The frequency depends on what and how and who has time. Larger features take longer to write and prove, get pushed when they are done, and get selected by importance for the projects we're running. Not many of these per year. Small updates take a day to a few weeks and we often do them on the side. There's no specific schedule at the moment.
Which code is part of the proof is already in the FAQ, but maybe a bit too distributed: currently the imx31 platform, ARMv6 architecture, all other config options unset (in particular DEBUG, PROFILING, etc) -- all C code for this combination apart from machine interface and boot code.
You can see the exact verification config options in https://github.com/seL4/l4v/blob/master/spec/cspec/c/Makefile and the machine interface are the functions that correspond to the ones in this Haskell file: https://github.com/seL4/seL4/blob/master/haskell/src/SEL4/Machine/Hardware.l... These are the functions that have explicit assumptions about their behaviour instead of a proof.
You can inspect the gory details by looking at the preprocessor output in the file kernel_all.c_pp in the proof build -- this is what the prover, the proof engineer, and the compiler see after configuration is done. So a quick way of figuring out if something is in this proof input or not is checking if the contents of that file change if you make a change to the source you're wondering about. You don't need the prover for this, and only parts of the seL4 build environment.
The top-level proof makes statements about the behaviour of all of the kernel entry points, which we enumerate once manually in the proof. The prover reads in these entry points, and anything that they call must either have a proof or an assumption for it to complete its proof. If anything is missing, the proof fails.
That means all of the C code that is in this kernel_all.c_pp file either: - has a proof, - or has an explicit assumption about it, - or is not part of the kernel (i.e. is never called)
The ones with explicit assumptions are the machine interface functions mentioned above (they're usually inline asm) and the functions that are only called by the boot process (usually marked with the BOOT_CODE macro in the source so they're easy to spot).
Cheers, Gerwin
On 07.01.2015, at 8:26 am, Raoul Duke raould@gmail.com wrote:
hi,
When does seL4 get re-proven? When code gets pulled into the master branch on github? Once a year? Something in-between?
Is it clear what code is actually proven? Is everything in github under the proofs? Or are there things that fall outside the proven kernel? How would anybody see that?
:-)
Thanks!
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
hi Gerwin,
Wow, thanks! Terrific details, there.
More questions come to mind! :-) How sustainable does the team see the proving being long term? Are there ¥€$ to cover the role(s)? What is the limit on how much code can change, and have the proving keep up? Etc.?
Congratulations to you all for a terrific project.
Hi Raoul,
so far it doesn’t look like sustainability is a problem. We’ve been continually updating and extending the proofs since 2009.
The drivers for change in seL4 are mostly new cool features we’d like to implement (such as better real-time support and verified virtualisation extensions), API simplifications, or performance enhancements. There are also change drivers for just the proofs: new properties to prove, more automation, and making maintenance more efficient. In the verified code, we don’t have this otherwise frequent source of change: implementation bugs.
That said, if someone has a request for a new verified feature or verified platform port that we don’t already have on our agenda, it needs to come with sufficient funding to make it worth our while. More ¥€$ could certainly mean quicker pace and more features. It might get cheaper if it’s interesting research-wise ;-)
Predicting cost for re-proof is a bit of a black art that we’re trying to get a better handle on. (Not dissimilar to predicting cost for a software project in general). Many cases are easy to predict, but if you’re changing something centrally important in the system it might invalidate a lot of the proof. So far we haven’t seen this very often (working on one right now), but we try of course to pick our changes such that they are compatible with the way seL4 works.
I don’t want to give the impression that updating the proof is no work. It is significant work, but it’s not so bad that we don’t think we can keep it up. We also often implement and try out new experimental features without verification. The ones we think are worth it go on the experimental branch. Some of these have been sitting there for a while, because they need more work before they’re suitable for verification. Others get pulled in straight away.
Cheers, Gerwin
On 8 Jan 2015, at 5:21 am, Raoul Duke raould@gmail.com wrote:
hi Gerwin,
Wow, thanks! Terrific details, there.
More questions come to mind! :-) How sustainable does the team see the proving being long term? Are there ¥€$ to cover the role(s)? What is the limit on how much code can change, and have the proving keep up? Etc.?
Congratulations to you all for a terrific project.
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
This seems like such a terrific existence proof that we can actually use proofs for real-world systems. I wish more people would crow about it from the rooftops. Well done to you all!
-
Gerwin Klein -
Raoul Duke