www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - First machine-checked OS kernel

reply Kagamin <spam here.lot> writes:
http://www.nicta.com.au/news/home_page_content_listing/world-first_research_breakthrough_promises_safety-critical_software_of_unprecedented_reliability

NICTA announced the completion of the world抯 first formal machine-checked
proof of a general-purpose operating system kernel, promising safety-critical
software of unprecedented levels of reliability.
Aug 20 2009
next sibling parent reply davidl <davidl nospam.org> writes:
在 Thu, 20 Aug 2009 16:56:24 +0800,Kagamin <spam here.lot> 写道:

 http://www.nicta.com.au/news/home_page_content_listing/world-first_research_breakthrough_promises_safety-critical_software_of_unprecedented_reliability

 NICTA announced the completion of the world’s first formal  
 machine-checked proof of a general-purpose operating system kernel,  
 promising safety-critical software of unprecedented levels of  
 reliability.

I'm not sure how the Singularity can be categorized. Is it proof-free or something? The proof I would imagine may make some sort of assumption of compiler correctness. If so, they may need to further proof the compiler always generate correct binaries. Otherwise kernel can be exploited if the compiler doesn't translate the code correctly. -- 使用 Opera 革命性的电子邮件客户程序: http://www.opera.com/mail/
Aug 20 2009
parent Kagamin <spam here.lot> writes:
davidl Wrote:

 If so, they may need to further proof the compiler always  
 generate correct binaries.

And that the processor doesn't have flaws either. This is what's called an unprecedented level of reliability, I believe.
Aug 20 2009
prev sibling parent Mattias Holm <mattias.holm openorbit.REMOVE.THIS.org> writes:
Kagamin wrote:
 NICTA announced the completion of the world抯 first formal machine-checked
proof of a general-purpose operating system kernel, promising safety-critical
software of unprecedented levels of reliability.

Yes, sort of what they proved was that the implementation was inline with the specification. The spec may still have bugs though. Also, they proved this for a very limited microkernel (not a general purpose OS), so they now know only that the message passing, task handling and some other minor parts work as specified, they still have no idea about the disk drivers or anything outside the micro kernel. For the amount of work they put into it, you would have been able to write tests for everything and conducted code reviews to reach a 99.9% confidence in the system for a small fraction of the cost. I still find that their work is incredibly impressive, and will be very appreciated with many software communities, especially the defense community. /Matt
Aug 20 2009