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