使用集成的高保证软件堆栈加快上市时间
作者：Paul Pazandak，Fabrizio Bertocci
通用计算、操作系统 （OS）、固有语言功能（如 C 内存分配）和软件质量问题导致整个行业的系统缺乏固有的安全性和弹性。这导致了许多安全漏洞，对国家安全造成了可怕的后果。有必要通过应用健全的安全和工程原则，根据适当的技术和工具设计有保证的系统。
一般来说，构建有保证的系统需要对问题域有透彻的了解，深入分析特定于域的工作流和要求，仔细的架构考虑和设计权衡，审查开发，正确配置和最终产品的托管部署。在整个产品生命周期中也需要这种级别的护理。
具体而言，与系统架构相关，利用硬件和软件技术和工具增强安全性归结为将合理的安全原则应用于合适的目标，例如内存访问（例如，开放设计、最小特权、特权分离和完全中介原则）。其他研究和开发工作可能会将这些原则应用于其特定的环境和设计目标。
构建可信赖和高保证系统的过程复杂、昂贵，并且需要大量专业知识。最终目标是创建一个完整的软件-硬件解决方案，其组件（单独和集体）满足客户所需的安全和安保保证级别。这将因所需的标准而异。
例如，用于飞行安全适航性的RTCA DO-178C和用于自动驾驶汽车的ISO 26262都包含与组件具有的关键级别（角色）相对应的多个级别的认证。例如，在DO-178C中，有五个级别：
A级（灾难性）：防止持续安全飞行或着陆，许多致命伤害
B级（危险/严重）：对少数乘员造成潜在致命伤害
C级（主要）：损害乘员效率、不适或可能对乘员造成伤害
D级（次要）：飞机安全裕度降低，但完全在机组人员的能力范围内
E级（无影响）：完全不影响飞机的安全
从上到下建立一个高保证系统在资金和时间方面都太昂贵了。相反，目标应该是开发尽可能少的代码。人们可以获得或许可的经过验证/可认证的代码越多，设计、开发、维护和认证所需的代码就越少。这将加快开发工作并大大降低成本。高保证软件堆栈提供了这一点。
此堆栈的作用是提供一个经过验证的基础。它由经过验证或认证的实时操作系统（RTOS）（安全RTOS）和分布式通信中间件组成。
高保证软件堆栈的基础
在过去的六年里，在DARPA的研究资助下，RTI一直致力于嵌入式系统的经过验证的堆栈，以加速安全/安保认证。在这个堆栈中，我们使用RTI的可认证Connext软件框架。RTI Connext 支持对象管理组数据分发服务标准（OMG DDS）。Connext目前在近2，000个关键系统中运行，涵盖航空电子/国防，自主系统，医疗机器人，能源和工业系统。利用OMG DDS开放标准，能够将松散耦合（分布式）的软件组件快速组装到工作系统中。
对于安全实时操作系统，我们选择了开源的seL4分离内核（sel4.systems）。它是一个数学上可证明正确的微内核，它将在正在运行的进程之间提供时间和空间分离。它保证进程之间不会有意外的数据泄漏，并且一个进程不会影响另一个进程的操作。这提供了更大的系统弹性和安全性，这也是多个独立安全级别（MILS） 解决方案的属性。
如今，seL4的衍生物正被几家大型科技公司使用。
对安全微内核的需求
要了解对像seL4这样的安全微内核的需求，首先仔细研究内核设计原则是有帮助的。
如图 2 所示，有两种主要的内核设计方法 – 单片内核和微内核。在前者中，提供典型操作系统服务所需的所有代码都直接在内核本身中实现。内核以硬件的特权模式执行，这意味着所有代码都被授予对所有系统资源的无限制访问和控制。
图2 如果设计得当，微内核操作系统（OS）包含的代码比单片架构少得多，从而减少了攻击面、简化了合规性等。
这种类型的实现可能对整体系统性能有益，但如果任何内核组件具有某种类型的故障（攻击者可以利用这种状态），则可能导致危险情况。一个突出的例子是Linux内核，它包含超过2000万行代码，可以预期包含一定数量的错误，提供潜在的攻击渠道。
相比之下，微内核设计通过大幅减少可信计算基础（TCB）来应对这一缺点，这意味着整个系统中必须信任的代码子集才能正常运行。微内核遵循的设计原则是让内核仅包含最基本的机制（例如，进程间通信和调度）。所有剩余的操作系统功能必须转移到非特权用户模式，从而在隔离的沙箱中封装运行。
此方法可保护内核进程免受来自外部的任何干扰，只允许明确需要的通信。对于像seL4这样设计良好的微内核，这意味着代码库可以减少到一万行代码的数量级。这大大缩小了攻击面。
seL4 和 DDS：可靠的组合
seL4 的目的是为需要它的应用程序提供可靠、安全和可靠的基础。例如，这包括军事系统、医疗设备、机器人、自动驾驶汽车和能源系统。无一例外，这些高保证应用需要可靠而强大的分布式通信功能，而 seL4 不提供此功能。
OMG DDS for Real-Time Systems是一个实时、安全、松散耦合的分布式系统发布/订阅软件连接框架，非常适合作为高保证系统的通信层，包括任何安全RTOS，如seL4。虽然还有其他开源和商业现成的通信框架技术，但这些框架缺乏高保证认证，充其量只能提供基本的全有或全无安全性。
对于 DDS，seL4 创造了一个丰富、成本更低、占用空间更小、高保证的基础。对于seL4，DDS提供了一个基于开放标准的通信协议。
DDS 极大地简化了 seL4 组件间/应用程序开发，降低了相关成本，并促进了 seL4 开发社区中的组件互操作性。DDS 是一种解决方案，它将以更一致、安全和高效的方式标准化数据分发。它提供了一个发布-订阅模型，可实现更轻松、更快速、更安全的分布式系统开发。应用程序开发人员可以减轻为基于消息的通信和解密消息序列创建自己的零碎（可能是专有的）一次性解决方案的负担，使他们能够专注于特定于域的组件，并依靠DDS与系统中的其他（本地和远程）实体提供标准化的安全交互。
降低高保证软件的进入门槛
DDS将大大降低决定使用seL4 / CAmkES的公司和开发人员的进入门槛，因为它提供了一个抽象层，隐藏了与在seL4之上开发应用程序相关的大部分复杂性。DDS将显著缩短开发时间，减少对内部seL4主题专业知识的需求。
