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
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
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
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
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
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, subscript
curecoding.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 ago on sev
blems.
Dimitri
-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 discuss
> 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 mi
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 mathema
vin
> Sent: 01 October 2009 22:34
> To: Secure Code Mailing List
> Subject: [SC-L] Provably correct microkernel (seL4)
>
> Thought there might be several on this list who might appreciate
> this, at least from a theoretical perspective but had not seen
> it. (Especially Larr
This was discussed a few months ago on several other lists I read.
The consensus is that it's interesting, and is further than anyone
else has gone in recent years to do proofs, but not practically
useful. Additionally, there are a lot of caveats on the proof (which
I don't recall, but are well do
Thought there might be several on this list who might appreciate
this, at least from a theoretical perspective but had not seen
it. (Especially Larry Kilgallen, although he's probably already seen it. :)
In
http://www.unsw.edu.au/news/pad/articles/2009/sep/microkernel_breakthrough.html,
"Pro
13 matches
Mail list logo
