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

[Gunnar Peterson]

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, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

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

[Jeremy Epstein]

Caveats on the proofs, as I recall.  I'll try to dig up the details.
It's been pretty extensively discussed elsewhere...

On Fri, Oct 2, 2009 at 12:54 PM, Dimitri DeFigueiredo
 wrote:
> There is a proof for a whole kernel I can use today. How's that not 
> practically useful? Is it not practically useful because there are caveats on 
> the proof? I don't we can just dismiss this one without further reasoning or 
> because we don't know how to apply it to our own problems.
>
> 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 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 documented on their web site) that make
> it clear it's not really as useful as it might sound.
>
> --Jeremy
>
> On Thu, Oct 1, 2009 at 5:33 PM, Wall, Kevin  wrote:
>> 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,
>>
>>    "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 mathematical rigour that an operating-system kernel -- the
>>    code at the heart of any computer or microprocessor -- was 100 per cent
>>    bug-free and therefore immune to crashes and failures."
>>
>> In a new item at NICTA
>> 
>>
>> it mentions this proof was the effort of 6 people over 5 years (not quite
>> sure if it was full-time) and that "They have successfully verified 7,500
>> lines of C code [there's the problem! -kww] and proved over 10,000
>> intermediate theorems in over 200,000 lines of formal proof". The proof is
>> "machine-checked using the interactive theorem-proving program Isabelle".
>>
>> Also the same site mentions:
>>    The scientific paper describing this research will appear in the 22nd
>>    ACM Symposium on Operating Systems Principles (SOSP)
>>        http://www.sigops.org/sosp/sosp09/.
>>    Further details about NICTA's L4.verified research project can be found
>>    at http://ertos.nicta.com.au/research/l4.verified/.
>>
>> 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.
>>
>> -kevin
>> ---
>> Kevin W. Wall           Qwest Information Technology, Inc.
>> kevin.w...@qwest.com    Phone: 614.215.4788
>> "It is practically impossible to teach good programming to students
>>  that have had a prior exposure to BASIC: as potential programmers
>>  they are mentally mutilated beyond hope of regeneration"
>>    - Edsger Dijkstra, How do we tell truths that matter?
>>      http://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD498.html
>>
>> ___
>> Secure Coding mailing list (SC-L) SC-L@securecoding.org
>> List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
>> List charter available at - http://www.securecoding.org/list/charter.php
>> SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
>> as a free, non-commercial service to the software security community.
>> ___
>>
>
> ___
> Secure Coding mailing list (SC-L) SC-L@securecoding.org
> List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
> List charter available at - http://www.securecoding.org/list/charter.php
> SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
> as a free, non-commercial service to the software security community.
> ___
>

___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
_

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

[Dimitri DeFigueiredo]

There is a proof for a whole kernel I can use today. How's that not practically 
useful? Is it not practically useful because there are caveats on the proof? I 
don't we can just dismiss this one without further reasoning or because we 
don't know how to apply it to our own problems.

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 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 documented on their web site) that make
it clear it's not really as useful as it might sound.

--Jeremy

On Thu, Oct 1, 2009 at 5:33 PM, Wall, Kevin  wrote:
> 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,
>
>    "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 mathematical rigour that an operating-system kernel -- the
>    code at the heart of any computer or microprocessor -- was 100 per cent
>    bug-free and therefore immune to crashes and failures."
>
> In a new item at NICTA
> 
>
> it mentions this proof was the effort of 6 people over 5 years (not quite
> sure if it was full-time) and that "They have successfully verified 7,500
> lines of C code [there's the problem! -kww] and proved over 10,000
> intermediate theorems in over 200,000 lines of formal proof". The proof is
> "machine-checked using the interactive theorem-proving program Isabelle".
>
> Also the same site mentions:
>    The scientific paper describing this research will appear in the 22nd
>    ACM Symposium on Operating Systems Principles (SOSP)
>        http://www.sigops.org/sosp/sosp09/.
>    Further details about NICTA's L4.verified research project can be found
>    at http://ertos.nicta.com.au/research/l4.verified/.
>
> 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.
>
> -kevin
> ---
> Kevin W. Wall           Qwest Information Technology, Inc.
> kevin.w...@qwest.com    Phone: 614.215.4788
> "It is practically impossible to teach good programming to students
>  that have had a prior exposure to BASIC: as potential programmers
>  they are mentally mutilated beyond hope of regeneration"
>    - Edsger Dijkstra, How do we tell truths that matter?
>      http://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD498.html
>
> ___
> Secure Coding mailing list (SC-L) SC-L@securecoding.org
> List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
> List charter available at - http://www.securecoding.org/list/charter.php
> SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
> as a free, non-commercial service to the software security community.
> ___
>

___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

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

[Johan Peeters]

> 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
___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

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

[ljknews]

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 mathematical rigour that an operating-system kernel -- the
> code at the heart of any computer or microprocessor -- was 100 per cent
> bug-free and therefore immune to crashes and failures."

Reading nothing beyond what was posted, the problem I see is
to provide a complete specification against which to prove
correctness.
-- 
Larry Kilgallen
___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

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

[Cassidy, Colin (GE Infra, Energy)]

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, that
does not mean that what you said the code should do is necessarily correct.
As Gary McGraw has pointed out 50% of security issues are bugs, 50% are
design flaws.  So we have only removed 50% of the problem.

Secondly, as you pointed out, that is an awful lot of effort in terms of man
years for what is essentially a small program and I don’t think it will
scale well

Thirdly, I suspect this is one of those processes that is easier to apply to
greenfield development, I don’t think many developers will have that luxury.

In conclusion, it seems an awful effort to fix half the problem, I'd expect,
though cant prove, that a combination of other secure development processes
working together will get better results with less overall effort.

CJC

> -Original Message-
> From: sc-l-boun...@securecoding.org 
> [mailto:sc-l-boun...@securecoding.org] On Behalf Of Wall, Kevin
> 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 Larry Kilgallen, although he's probably 
> already seen it. :)
> 
> In 
> http://www.unsw.edu.au/news/pad/articles/2009/sep/microkernel_
> breakthrough.html,
> 
> "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 mathematical rigour that an operating-system 
> kernel -- the
> code at the heart of any computer or microprocessor -- 
> was 100 per cent
> bug-free and therefore immune to crashes and failures."
> 
> In a new item at NICTA
> 
> 
> it mentions this proof was the effort of 6 people over 5 
> years (not quite
> sure if it was full-time) and that "They have successfully 
> verified 7,500
> lines of C code [there's the problem! -kww] and proved over 10,000
> intermediate theorems in over 200,000 lines of formal proof". 
> The proof is
> "machine-checked using the interactive theorem-proving 
> program Isabelle".
> 
> Also the same site mentions:
> The scientific paper describing this research will appear 
> in the 22nd
> ACM Symposium on Operating Systems Principles (SOSP)
> http://www.sigops.org/sosp/sosp09/.
> Further details about NICTA's L4.verified research 
> project can be found
> at http://ertos.nicta.com.au/research/l4.verified/.
> 
> 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.
> 
> -kevin
> ---
> Kevin W. Wall   Qwest Information Technology, Inc.
> kevin.w...@qwest.comPhone: 614.215.4788
> "It is practically impossible to teach good programming to students
>  that have had a prior exposure to BASIC: as potential programmers
>  they are mentally mutilated beyond hope of regeneration"
> - Edsger Dijkstra, How do we tell truths that matter?
>   http://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD498.html
> 
> ___
> Secure Coding mailing list (SC-L) SC-L@securecoding.org
> List information, subscriptions, etc - 
> http://krvw.com/mailman/listinfo/sc-l
> List charter available at - 
> http://www.securecoding.org/list/charter.php
> SC-L is hosted and moderated by KRvW Associates, LLC 
> (http://www.KRvW.com)
> as a free, non-commercial service to the software security community.
> ___
> 


smime.p7s
Description: S/MIME cryptographic signature
___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

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

[Jeremy Epstein]

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 documented on their web site) that make
it clear it's not really as useful as it might sound.

--Jeremy

On Thu, Oct 1, 2009 at 5:33 PM, Wall, Kevin  wrote:
> 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,
>
>    "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 mathematical rigour that an operating-system kernel -- the
>    code at the heart of any computer or microprocessor -- was 100 per cent
>    bug-free and therefore immune to crashes and failures."
>
> In a new item at NICTA
> 
>
> it mentions this proof was the effort of 6 people over 5 years (not quite
> sure if it was full-time) and that "They have successfully verified 7,500
> lines of C code [there's the problem! -kww] and proved over 10,000
> intermediate theorems in over 200,000 lines of formal proof". The proof is
> "machine-checked using the interactive theorem-proving program Isabelle".
>
> Also the same site mentions:
>    The scientific paper describing this research will appear in the 22nd
>    ACM Symposium on Operating Systems Principles (SOSP)
>        http://www.sigops.org/sosp/sosp09/.
>    Further details about NICTA's L4.verified research project can be found
>    at http://ertos.nicta.com.au/research/l4.verified/.
>
> 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.
>
> -kevin
> ---
> Kevin W. Wall           Qwest Information Technology, Inc.
> kevin.w...@qwest.com    Phone: 614.215.4788
> "It is practically impossible to teach good programming to students
>  that have had a prior exposure to BASIC: as potential programmers
>  they are mentally mutilated beyond hope of regeneration"
>    - Edsger Dijkstra, How do we tell truths that matter?
>      http://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD498.html
>
> ___
> Secure Coding mailing list (SC-L) SC-L@securecoding.org
> List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
> List charter available at - http://www.securecoding.org/list/charter.php
> SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
> as a free, non-commercial service to the software security community.
> ___
>

___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

[SC-L] Provably correct microkernel (seL4)

[Wall, Kevin]

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,

"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 mathematical rigour that an operating-system kernel -- the
code at the heart of any computer or microprocessor -- was 100 per cent
bug-free and therefore immune to crashes and failures."

In a new item at NICTA


it mentions this proof was the effort of 6 people over 5 years (not quite
sure if it was full-time) and that "They have successfully verified 7,500
lines of C code [there's the problem! -kww] and proved over 10,000
intermediate theorems in over 200,000 lines of formal proof". The proof is
"machine-checked using the interactive theorem-proving program Isabelle".

Also the same site mentions:
The scientific paper describing this research will appear in the 22nd
ACM Symposium on Operating Systems Principles (SOSP)
http://www.sigops.org/sosp/sosp09/.
Further details about NICTA's L4.verified research project can be found
at http://ertos.nicta.com.au/research/l4.verified/.

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.

-kevin
---
Kevin W. Wall   Qwest Information Technology, Inc.
kevin.w...@qwest.comPhone: 614.215.4788
"It is practically impossible to teach good programming to students
 that have had a prior exposure to BASIC: as potential programmers
 they are mentally mutilated beyond hope of regeneration"
- Edsger Dijkstra, How do we tell truths that matter?
  http://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD498.html

___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___