大家早上好。我来自澳大利亚国家信息与通讯技术研究机构（NICTA），主要从事软件研究。此次，我为大家介绍一下可信赖的软件系统。大家知道软件在生活当中无处不在，我们想象一下每天的日常生活，手机、汽车、电梯，工作时用的电脑，要用到的这一切都是离不开其中的软件。
　　我们每年编写以亿行计的代码，代码是人编写的，难免犯错，软件也会就会存在一些BUG，在商业软件测试里面每1000行里面就有5个BUG，BUG会让电脑死机，也可能被一些黑客利用。黑客的入侵不但会造成经济损失，甚至可能威胁生命安全。例如说使用很广泛的心脏起搏器，要通过无线的方式进行更新，有研究人员发现可以在几米之外黑掉心脏起搏器，发出超强的电脉冲致人死命。
　　所以我们需要的是可信赖的软件，这就是NICAT现在研究的一个课题。在介绍我们的技术前，我首先讲一下目前减少软件BUG的方法。首先就是测试，输入数据进去以后看输出的结果是什么，结果不符合预计就修改错误。如果经过很多次测试都没有出现问题就算合格了。但这不能够排除BUG存在的可能性。
　　现在另外一个提高软件可靠性的方式就是流程的认证。有一系列的标准规则，基于这些标准来评价软件的开发、整合等等。如果说每一项标准都符合，软件就是合格的，同样不能排除BUG的存在。
　　第三个就是形式验证。用数学方法彻底的分析每一个系统里面可能存在的行为，通过数学计算的结果，证明这个系统具备了所需的一系列功能和性能。这种方法要把真实的系统抽象为简化模型，对模型进行验证。形式验证虽然很全很彻底，但是模型不能百分之百的复制现实系统。
　　所以我们所做的就是在真实环境当中，去验证一个大系统的性能和功能是符合我们要求的。我们首先把系统组件化。在任何一个系统中，各种代码和组件并非每个都是关键的。所以我们要做的就是，找出哪些重要的，哪些不重要。分析这些组件如何沟通和相互影响，注意控制不关键的代码所获得的权力。
　　然后我们用形式验证的流程验证这一点，验证不同的组件满足了对于组件功能的要求。对于核心组件我们需要按最严格的要求进行检测，我们使用叫做seL4的技术来验证内核是符合安全要求的。
　　之后我们去验证各种各样的功能，代码的阻截、缓冲的流量等等。我们还要确保seL4和其他组件是区分开来的，其他组件没有权力控制内核的。我们首先验证内核关键功能，确保有效安全的，然后将内核组件和非关键组件实现隔离，其他非关键组件的代码没有权力控制内核，这就可以确保系统的安全性。