First machine-checked OS kernel

[davidl]

在 Thu, 20 Aug 2009 16:56:24 +0800，Kagamin <spam at 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/