使用集成的高保障软件堆栈加快上市时间

作者：Paul Pazandak，Fabrizio Bertocci

通用计算、操作系统 （OS）、固有的语言功能（如 C 内存分配）和软件质量问题导致整个行业的系统缺乏固有的安全性和弹性。这导致了许多安全漏洞，对国家安全产生了可怕的后果。有必要通过应用合理的安全和工程原则，基于适当的技术和工具设计有保证的系统。

一般来说，构建一个有保证的系统需要对问题领域有透彻的了解，对特定于领域的工作流程和要求进行深入分析，仔细的架构考虑和设计权衡，经过审查的开发，正确的配置以及最终产品的托管部署。在整个产品生命周期中也需要这种程度的护理。

具体而言，与系统体系结构相关，利用硬件和软件技术及工具增强安全性归结为将合理的安全原则应用于合适的目标，例如内存访问（例如，开放设计原则、最小特权原则、特权分离原则和完全中介原则）。其他研究和开发工作可能会将这些原则的不同应用应用于其特定环境和设计目标。

构建可信赖和高保证系统的过程是复杂、昂贵的，并且需要大量的专业知识。最终目标是创建一个完整的软件 - 硬件解决方案，其组件（单独或集体）满足客户对安全和安保所需的保证级别。这将根据所需的标准而有所不同。

例如，用于飞行安全适航性的RTCA DO-178C和用于自动驾驶汽车的ISO 26262都包含与组件的关键级别（角色）相对应的多个级别的认证。例如，在DO-178C中，有五个级别：

A级（灾难性）：阻止持续安全飞行或降落，许多致命伤害

B级（危险/严重）：对少数乘员造成潜在致命伤害

C 级（主要）：影响机组人员的工作效率、不适或可能对乘员造成伤害

D级（次要）：飞机安全裕度降低，但完全在机组人员能力范围内

E级（无影响）：完全不影响飞机安全

就资金和时间而言，从上到下建立一个高保证的系统的成本太高了。相反，目标应该是开发尽可能少的代码。人们可以获取或许可的经过验证的/可认证代码越多，设计，开发，维护和认证所需的代码就越少。这将加快开发工作并显著降低成本。高确定性软件堆栈提供了此功能。

此堆栈的作用是提供经过验证的基础。它由经过验证或认证的实时操作系统（RTOS）和分布式通信中间件组成。

高确定性软件堆栈的基础

在过去的六年中，在DARPA研究资助下，RTI一直在为嵌入式系统开发经过验证的堆栈，以加速安全/安保认证。在此堆栈中，我们使用 RTI 的可认证连接软件框架。RTI 支持对象管理组数据分发服务标准 （OMG DDS）。如今，Connext 正在近 2，000 个关键系统中运行，涵盖航空电子/国防、自主系统、医疗机器人、能源和工业系统。利用OMG DDS开放标准，能够快速将松散耦合（分布式）的软件组件组装到工作系统中。

对于安全实时操作系统，我们选择了开源 seL4 分离内核（sel4.系统）。它是一个数学上可证明的正确微内核，它将在运行过程之间提供时间和空间分离。它保证进程之间不会出现意外的数据泄漏，并且一个进程不会影响另一个进程的操作。这提供了更高的系统弹性和安全性，这也是多独立安全级别 （MILS） 解决方案的属性。

如今，seL4的衍生产品正被几家大型科技公司使用。

对安全微内核的需求

要了解对像 seL4 这样的安全微内核的需求，从仔细研究内核设计原则开始是很有帮助的。

如图 2 所示，有两种主要的内核设计方法 - 单片内核和微内核。在前者中，提供典型操作系统服务所需的所有代码都直接在内核本身中实现。内核以硬件的特权模式执行，这意味着所有代码都被授予对所有系统资源的无限制访问和控制。

［图2 |如果设计正确，微内核操作系统（OS）包含的代码远远少于整体架构，从而减少了攻击面，简化了合规性等等。

这种类型的实现可能有益于整体系统性能，但如果任何内核组件具有某种类型的故障（攻击者可以利用这种状态），则可能导致危险情况。Linux内核提供了一个突出的例子，它包含超过2000万行代码，预计包含一定数量的错误，提供潜在的攻击渠道。

相比之下，微内核设计通过大幅减少可信计算库（TCB）来应对这一缺点，TCB意味着整个系统中必须可信才能正常运行的代码子集。微内核遵循内核仅包含最基本机制（例如，进程间通信和调度）的设计原则。所有剩余的操作系统功能必须转移到非特权用户模式，从而在隔离的沙箱中封装运行。

这种方法可以保护内核进程免受来自外部的任何干扰，只允许明确需要的通信。对于像 seL4 这样设计良好的微内核，这意味着代码库可以减少到一万行代码的数量级。这大大缩小了攻击面。

seL4 和 DDS：可靠的组合

seL4 的目的是为需要它的应用程序提供可靠、安全和可靠的基础。例如，这包括军事系统、医疗设备、机器人、自动驾驶汽车和能源系统。无一例外，这些高保证的应用程序需要可靠和强大的分布式通信功能，这是 seL4 无法提供的。

OMG DDS用于实时系统是一个实时，安全，松散耦合，发布/订阅软件连接框架，适用于分布式系统，非常适合作为高保证系统的通信层，包括任何安全RTOS，如seL4。虽然还有其他开源和商业现成的通信框架技术，但这些框架缺乏高保证认证，充其量只能提供基本的全有或全无的安全性。

对于DDS，seL4创建了一个丰富，低成本，更小的占地面积，高保证的基础。对于 seL4，DDS 提供了一个基于开放标准的通信协议。

DDS 大大简化了 seL4 组件间/应用程序开发，降低了相关成本，并促进了 seL4 开发社区中的组件互操作性。DDS 是一种解决方案，它将以更一致、更安全、更高效的方式标准化数据分发。它提供了一个发布-订阅模型，使分布式系统开发更简单、更快速、更安全。应用程序开发人员可以减轻创建自己的零碎的，也许是专有的，一次性解决方案的负担，用于基于消息的通信和破译消息序列，使他们能够专注于特定于域的组件，并依靠DDS提供与系统中其他（本地和远程）实体的标准化，安全的交互。

降低高保障软件的进入壁垒

DDS 将显著降低决定使用 seL4/CAmkES 的公司和开发人员的进入门槛，因为它提供了一个抽象层，隐藏了与在 seL4 之上开发应用程序相关的大部分复杂性。DDS将大大减少内部开发时间和对seL4主题专业知识的需求。

审核编辑：郭婷