Secure Coding mailing list archives

Provably correct microkernel (seL4)

From: yo at secappdev.org (Johan Peeters)
Date: Fri, 2 Oct 2009 18:50:55 +0200

My $.02... I don't think this approach is going to catch on anytime soon.
Spending 30 or so staff years verifying a 7500 line C program is not going
to be seen as cost effective by most real-world managers. But interesting
research nonetheless.


maybe not as crazy as it sounds: this is a micro kernel and hence a
security chokepoint. The other stuff running on top do not need the
same level of assurance.

kr,

Yo
-- 
Johan Peeters
http://johanpeeters.com

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) 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) 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)
- <Possible follow-ups>
- Provably correct microkernel (seL4) Bobby Miller (Oct 02)