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
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
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
] On
Behalf Of Gunnar Peterson
Sent: Friday, October 02, 2009 3:21 PM
To: Cassidy, Colin (GE Infra, Energy)
Cc: Secure Code Mailing List
Subject: Re: [SC-L] Provably correct microkernel (seL4)
design flaws. So we have only removed 50% of the problem.
for my part there have been many, many days when I
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 kevin.w...@qwest.com wrote:
Steve Christy wrote...
I wonder what would happen if somebody
I have a few concerns with formal proofs particularly applying them in a
non-academic environment (some of which may be my own naïve lack of
understanding and my feeble memory of my university years studying formal
methods).
Firstly whilst the code provably does what you said that it would do,
At 4:33 PM -0500 10/1/09, Wall, Kevin wrote:
Professor Gernot Heiser, the John Lions Chair in Computer Science in
the School of Computer Science and Engineering and a senior principal
researcher with NICTA, said for the first time a team had been able to
prove with
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
-Original Message-
From: sc-l-boun...@securecoding.org [mailto:sc-l-boun...@securecoding.org] On
Behalf Of Jeremy Epstein
Sent: Friday, October 02, 2009 6:38 AM
To: Wall, Kevin
Cc: Secure Code Mailing List
Subject: Re: [SC-L] Provably correct microkernel (seL4)
This was discussed a few months
...@securecoding.org] On
Behalf Of Jeremy Epstein
Sent: Friday, October 02, 2009 6:38 AM
To: Wall, Kevin
Cc: Secure Code Mailing List
Subject: Re: [SC-L] Provably correct microkernel (seL4)
This was discussed a few months ago on several other lists I read.
The consensus is that it's interesting
design flaws. So we have only removed 50% of the problem.
for my part there have been many, many days when I would settle for
solving 50% of a problem
-gunnar
___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information,
11 matches
Mail list logo
