我们人类在编写企业操作系统上是可以信赖的吗？或者说我们的努力只是过于繁琐了？

　　在过去的数十年间我们一直在为此而努力，但是结果却并不理想：可以肯定的说人类编写的任何代码都布满了漏洞，我们编写的软件如此复杂以致这些漏洞经常是时隔多年都没有被发现。

　　举例来说，上周谷歌公司的两位研究专家Tavis Ormandy和Julien Tinnes发现一个漏洞潜伏在Linux系统核心中将近1年的时间。Tinnes在他的博客中表示“自从2001年以来，这个漏洞对所有体系架构上的所有2.4和2.6核心造成了影响”。

　　从理想状态来说，我们人类需要的是一组永远正确的机器人来检查我们的工作，来保证我们在编写企业操作系统软件时不会犯下任何代码编译的错误。

　　我们没有这种机器人，但是我们有“伊莎贝拉”，一种由剑桥大学和Technische University共同开发的校验辅助应用软件，可在在BSD授权下免费下载伊莎贝拉可以让精确的数学公式以形式语言表现出来，为证明逻辑微积分学上的这些公式提供工具。

　　上周，澳大利亚的研究专家宣布他们使用伊莎贝拉来完成了首个常规用途操作系统核心的形式机器检验证法。正在论证的核心是安全的内置L4（SEL4）微核心，这个核心的设计是专门用来监管航空和交通领域的重要安全系统。

　　根据指导SEL4研发工作的澳大利亚研究专家团队负责人Gerwin Klein博士的说法，他们实现的是常规功能的正确校验。同时还显示出核心对许多常规的攻击反应并不敏感，诸如缓冲区溢出等，如果是涉及航空领域安全的操作系统，这种结果无疑是令人期待的。

　　好消息是Klein的工作可能会帮助未来的企业级操作系统更加安全和可靠。剑桥大学计算机实验室的计算机逻辑学教授兼负责伊莎贝拉计划的科学家Larry Paulson强调说，证明操作系统核心中7500行C代码的正确性是一项独一无二的成就，应该最终能实现满足目前不可思议的可靠性标准的软件。他还补充说“这项计划实现的不仅是经过识别的微核心，而其是能够作为用来研发其他识别软件的技术母体来使用”。

　　不过还有个坏消息是在SEL4中验证的7500行C代码花费了12个专家4年的时间才完成，在超过20万行的形式证法中涉及了超过1万个中间定理--才得出伊莎贝拉的验证结果。鉴于Linux和Windows核心有超过500万行代码，他们当然不可能为了证明中间定理再冷冻多年，因此对于时下的企业级操作系统，来自于缓冲区溢出漏洞的可靠性和灵活性不是很快就能实现的。

　　当然除非有人制造出代码检验的机器人。