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