![securecoding logo](/images/securecoding-logo.png)
Secure Coding mailing list archives
Provably correct microkernel (seL4)
From: coley at linus.mitre.org (Steven M. Christey)
Date: Fri, 2 Oct 2009 16:15:53 -0400 (EDT)
I wonder what would happen if somebody offered $10000 to the first applied researcher to find a fault or security error. According to http://ertos.nicta.com.au/research/l4.verified/proof.pml, buffer overflows, memory leaks, and other issues are not present. Maybe people would give up if they don't gain some quick results, but it seems like you'd want to sanity-check the claims using alternate techniques. - Steve
Current thread:
- Provably correct microkernel (seL4) Wall, Kevin (Oct 01)
- Provably correct microkernel (seL4) Jeremy Epstein (Oct 02)
- 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)
- <Possible follow-ups>
- Provably correct microkernel (seL4) Bobby Miller (Oct 02)
- Provably correct microkernel (seL4) Jeremy Epstein (Oct 02)