[SC-L] OWASP Summit / Elections

2009-10-03 Thread Tom Brennan - OWASP
The next global summit for OWASP Foundation Inc (www.owasp.org) will be held on November 11th 2009 (Veterans Day in the USA) in Washington, DC., USA As is customary at our summits we will govern by rough consensus and collaborate face to face town hall style for our professional associations direc

Re: [SC-L] Provably correct microkernel (seL4)

2009-10-03 Thread Johan Peeters
It is my understanding that only the micro-kernel runs in kernel mode, but not having read the nitty-gritty either, I'll stand to be corrected. kr, Yo On Fri, Oct 2, 2009 at 11:20 PM, Wall, Kevin wrote: > Steve Christy wrote... > >> I wonder what would happen if somebody offered $1 to the f

Re: [SC-L] Provably correct microkernel (seL4)

2009-10-03 Thread Chris Wysopal
And presumably before they spent many man years proving implementation correctness they could have spent a fraction of that on design review and subsequent design corrections. -Chris -Original Message- From: sc-l-boun...@securecoding.org [mailto:sc-l-boun...@securecoding.org] On Behal

Re: [SC-L] Provably correct microkernel (seL4)

2009-10-03 Thread Wall, Kevin
Steve Christy wrote... > I wonder what would happen if somebody offered $1 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 p

Re: [SC-L] Provably correct microkernel (seL4)

2009-10-03 Thread Bobby Miller
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

Re: [SC-L] Provably correct microkernel (seL4)

2009-10-03 Thread Steven M. Christey
I wonder what would happen if somebody offered $1 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