L4是一组基于微内核构架的操作系统内核，澳大利亚研究组织NICTA创造了一个新的L4版本，称为Secure Embedded L4（简写seL4），宣布在世界上率先开发出第一个正规机器检测证明（formal machine-checked proof）通用操作系统。
seL4微内核设计针对实时应用，可潜在应用于强调安全和关键性任务的领域内，如军用和医疗行业。形式证明在较小的内核中已经实现，但这次是首次在执行复杂任务的操作系统内核中实现。研究发现常用的攻击方法对seL4无效，如恶意程序经常采用的缓存溢出漏洞。Open Kernel Labs首席科学家和NICTA的ERTOS Group负责人Gernot Heiser教授表示实现许多人认为不可能实现的任务是令人兴奋的。他表示暂时还没有产品开发计划。
来源：solidot
aanchun1989 于 2009-08-29 22:18:57发表:
不懂
35749810 于 2009-08-29 19:23:11发表:
不懂
wangyu 于 2009-08-17 16:55:10发表:
不懂
ailove 于 2009-08-17 14:56:15发表:
期待
xzj4167 于 2009-08-17 13:34:24发表:
顶一个，chome又有对手了