科技 澳大利亚研发出无法被入侵的系统内核

操作系统是计算机安全的核心，而操作系统的核心是内核。澳大利亚国家研究机构开发出了第一个形式证明黑客无法入侵的内核seL4。seL4具有多个高度安全的特性：它设计只能做它允许做的事情，未获授权代码无法修改，未获许可不能读取它的内存和传输的数据。


seL4的一个早期版本OKL4已被数百万智能手机使用。该机构的Gernot Heiser说，seL4采用了新方法孤立内核中的数据，但最关键的安全特性是代码能被在数学上检查。