Secure Coding mailing list archives
Provably correct microkernel (seL4)
From: b.g.miller at gmail.com (Bobby Miller)
Date: Fri, 2 Oct 2009 13:59:48 -0700
I might argue that it may fix problems that aren't fixable otherwise. My experience in this area is very old, but I found that the biggest benefit of formal methods was not so much the proof but the flaws discovered and fixed on the way to the proof.
In conclusion, it seems an awful effort to fix half the problem, I'd expect, though cant prove, that a combination of other secure development processes working together will get better results with less overall effort. CJC
-------------- next part -------------- An HTML attachment was scrubbed... URL: <http://krvw.com/pipermail/sc-l/attachments/20091002/4627e9c6/attachment.htm>
Current thread:
- Provably correct microkernel (seL4), (continued)
- Provably correct microkernel (seL4) Dimitri DeFigueiredo (Oct 02)
- Provably correct microkernel (seL4) Jeremy Epstein (Oct 02)
- Provably correct microkernel (seL4) Dimitri DeFigueiredo (Oct 02)
- Provably correct microkernel (seL4) ljknews (Oct 02)
- Provably correct microkernel (seL4) Cassidy, Colin (GE Infra, Energy) (Oct 02)
- Provably correct microkernel (seL4) Gunnar Peterson (Oct 02)
- Provably correct microkernel (seL4) Chris Wysopal (Oct 02)
- Provably correct microkernel (seL4) Gunnar Peterson (Oct 02)
- Provably correct microkernel (seL4) Johan Peeters (Oct 02)
- Provably correct microkernel (seL4) Steven M. Christey (Oct 02)
- Provably correct microkernel (seL4) Wall, Kevin (Oct 02)
- Provably correct microkernel (seL4) Johan Peeters (Oct 03)
- Provably correct microkernel (seL4) Wall, Kevin (Oct 02)
- Provably correct microkernel (seL4) Bobby Miller (Oct 02)