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.lhs 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 <[email protected]> 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 > [email protected] > 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. _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
