NICTA宣布开发出世界第一个形式证明通用操作系统

L4是一组基于微内核构架的操作系统内核，澳大利亚研究组织NICTA创造了一个新的L4版本，称为Secure Embedded L4（简写seL4），宣布在世界上率先开发出第一个正规机器检测证明（formal machine-checked proof）通用操作系统。

seL4微内核设计针对实时应用，可潜在应用于强调安全和关键性任务的领域内，如军用和医疗行业。形式证明在较小的内核中已经实现，但这次是首次在执行复杂任务的操作系统内核中实现。研究发现常用的攻击方法对seL4无效，如恶意程序经常采用的缓存溢出漏洞。Open Kernel Labs首席科学家和NICTA的ERTOS Group负责人Gernot Heiser教授表示实现许多人认为不可能实现的任务是令人兴奋的。他表示暂时还没有产品开发计划。  

来源：solidot