DARPA软件自动快速认证（ARCOS）项目 |《DesCert：认证设计》142页技术报告，2022年

DARPA软件自动快速认证（ARCOS）项目的目标是 "自动评估软件保证证据，使认证者能够迅速确定系统风险是可接受的"。作为该计划的一部分，DesCert项目专注于新软件的保证驱动的开发。DesCert团队由SRI国际公司、霍尼韦尔研究院和华盛顿大学组成。我们采用了一种正式的、基于工具的方法来构建由严格的证据支持的软件工件。DesCert的工作流程将证据生成整合到设计过程中，从需求采集和分析到将高级软件需求分解为具有断言契约的架构属性和软件组件，再到可以动态和静态分析的软件。生成的证据通过保证本体论来组织，并集成到RACK的知识库中。

软件已经成为许多安全关键系统的核心组成部分。软件正在慢慢接管以前由机电设备处理的功能。在汽车中，防抱死制动系统使用软件巧妙而迅速地 "踩下刹车"，以避免因车轮锁死而打滑。车辆的许多计时、控制、安全、气候控制和信息娱乐子系统现在主要由软件处理。在系统的设计和维护方面，软件的使用支持更大的灵活性、复原力和多功能性。虽然软件不受磨损，但由于错误和安全漏洞，它可能成为系统故障的一个重要来源，因为即使是一个小的设计或编码错误也会产生很大的后果。

软件保证是一种在部署前确保包含软件组件的系统安全的方式。在系统安全方面，危险是由故障引起的潜在的危险事件。失败是对预期行为的偏离。失败可能是由一个组件的功能错误引起的。这个错误本身可能是由一个故障造成的，例如软件中的一个缺失的检查。在系统设计、操作概念和任务需求的背景下，保证案例捕捉到了软件安全的基本原理。保证案例确保所有的危险，即软件可能导致系统失败的后果，都在设计中得到了缓解。软件的保证案例包括由论据和证据支持的主张。这些要求必须涵盖软件的要求、设计、结构、代码和平台（包括硬件、通信网络、系统软件和其他库），以证明软件的行为适合其预期的目的，不会损害系统的安全。

在最高层次上，软件的理想品质被记录在跨越功能需求和性能特征的需求中。众所周知，许多软件项目的失败是由于错误的或不明确的需求。需求过程从列举危险开始，并论证这个列举是详尽的。然后构建软件需求，以指定预期的行为，同时减轻这些危险。需求捕捉软件行为的属性，包括对环境的假设、软件对输入必须采取的行动，以及软件必须避免的状态。有些属性是通用的，因为它们是由一类普通的系统来满足的。例如，软件必须避免死锁、类型违规和运行时错误。其他属性是针对系统的意图的，如确保导航数据的准确性。这些需求必须被证明是一致的、完整的和可验证的。软件设计正确地提供了这些需求，并分解为结构，即软件功能被分解为相互作用的模块的通用方式，以及低级需求（LLRs），这是强加给软件模块的契约。模型在软件设计的设计和保证中起着关键作用，它捕捉环境假设、平台假设、操作者行为，以及物理组件的行为，包括工厂（被控制的物理系统）、传感器和执行器。这些模型必须是这些组件和子系统的真实行为的足够精确的近似值，因为它是介于软件和物理世界之间的交互结构。硬件平台连同操作系统、库和胶水代码必须被证明能够正确地实现该架构。 软件组件的源代码必须满足合同的要求，并被正确地编译成可执行代码，在架构内正确地组成。因此，将所有这些要求和证据整合成一个无懈可击的系统保证案例是一个重大挑战。

保证案例的目的是什么？保证案例中提出的主张、论据和证据可以被单独检查、探测和攻击，以确保它们确实为系统安全提供了令人信服的部署前案例。论证中的这些步骤可能会因为各种原因而失败：缺失、不正确或模糊的要求或假设；不可信的工具；不精确或不匹配的语义；无效的理由；不正确的设计；以及错误的代码。保证案例的强度或效率是指持怀疑态度的评审员通过检查案例中的各个步骤，而不需要测试或分析完全集成的系统，就能轻易地找出案例中的缺陷。效率是通过使用具有精确语义的语言和符号、与语义兼容的可信工具以及可重用的工件来实现的，如测试理论、代码生成器、证明助手、类型检查器、静态分析器和编译器。如果尽管保证案例的效率很高，但没有发现任何缺陷，那么软件连同其保证案例就可以自信地被认证部署。

如果我们的目标是降低软件认证的成本，同时提高其严谨性，那么上述保证论证的步骤必须在上述意义上是有效的。评估人员必须很容易识别任何差距或缺陷。如果论证失败，失败的根源必须是令人震惊的。这意味着我们必须依赖由可重用的工具和设计概念建立的精确的主张，如健全的测试理论、需求分析器、模型检查器、类型检查器、架构框架、代码生成器和编译器。这种可重复使用的工具和概念的部署扩大了伪造的空间，因为与这些工具相关的通用声明，例如类型检查器的健全性，可以被任何工具失败的实例所伪造，甚至在保证系统内使用之外。显然，建立诸如模型检查器、类型检查器和静态分析器的健全性等高层次要求的成本较高，但这种成本可以在工具的多次使用中摊销。效率不仅仅是保证论证的一个特征，也是一种设计启发式，它有利于设计上的选择，比如严格的架构框架和语义上精确的符号，这些都放大了任何设计缺陷的突出性。

有许多标准用于评估认证的保证案例。IEC 62304是医疗设备软件认证的标准，规定了设备被宣布为安全所需的证据工件，这些设备在危险等级下运行，不可能有伤害（A级），不可能有严重伤害（B级），以及可能有死亡或严重伤害（C级）。汽车行业的功能安全标准ISO 26262横跨系统设计生命周期，涵盖需求、软件和硬件[ISO11]。MILSTD-882E规定了军用航空系统的系统安全认证的过程和程序[DoD12]。在民用航空领域，SAE ARP4754描述了开发民用飞机和系统的准则[SAE96a]，SAE ARP 4761概述了用于系统安全评估的技术[SAE96b]。这些都是与RTCA的标准一起使用的，如硬件设计保证的DO-254[RTC00]和软件安全标准的DO-178C[Inc11]。DO178-C规定了大约71个保证目标，这些目标必须完全或部分地满足，以便对软件进行从灾难性（A）到轻微（D）的危险等级认证。

许多安全标准在开发过程、保证目标和评估程序方面都有规定性。这些活动只是间接地影响系统安全。总体属性（OPs）在三个大目标方面对安全评估采取了更直接的看法[Hol18]。第一，系统的意图已经被准确地捕捉到。第二，设计的系统对于意图来说是正确的。三，系统中任何无法追踪到意图的额外功能必须是无害的或可接受的，也就是说，必须证明不会影响系统安全。OPs的方法可以与其他标准结合使用，只要论据能够与意图、正确性和无害性目标一致。

符合上述标准的软件认证是一个艰巨的劳动密集型过程，需要收集证据并构建一个能够通过评估者认可的保证案例。在安全关键环境下，认证是软件开发中时间和金钱方面最昂贵的环节。ARCOS计划旨在降低开发和认证安全关键型软件的成本并提高其效率。该计划将保证案例的构建分解为三个阶段：证据生成、证据整理和保证案例开发。DesCert项目解决了证据生成阶段的问题，重点是新软件开发。如图1.1所示，该项目旨在实现高安全性软件开发的所有阶段在三个具体方面的重大改进：与软件工件相关的主张和证据的形式严谨性，在不同抽象层次上产生的证据的可组合性，以及将证据整合到保证论证中并由评估者评估的效率。为了实现这一目标，DesCert方法强调：

1.产生严格的、语义连贯的证据的自动化工具

2.捕捉设计意图的语言和类型系统，如本体类型化。

3.复杂系统的组合式认证

4.捕捉软件和系统安全性的高效、易验证的论据

5.可重用的、值得信赖的自动化工具和技术，具有较低的摊销认证成本

6.在整个设计生命周期中持续的证据生成和验证。

DesCert团队由SRI国际公司、霍尼韦尔研究院和华盛顿大学组成。DesCert持续认证工作流程集成了许多需求建模、设计和代码分析工具，包括CLEAR需求描述语言[BMH+18, HBM+18]、用于从需求中生成测试用例和模型的Text2Test、PVS交互式证明助手、Sally模型检查器、Radler架构定义语言、用于可插拔类型检查的检查器框架、用于生成单元测试的Randoop系统、用于学习软件假定断言属性的Daikon系统，以及SeaHorn静态分析器。为了持续保证，我们开发了Baseline DesCert工作流程工具，用于监控和维护保证工件的状态。该工具还与RACK工具互动，以根据保证本体论来策划和摄取保证工件。

DesCert为新软件生成证据的方法松散地遵循DO-178C的目标。我们采用CLEAR语言，以软件组件的输入/输出状态--机器行为来捕捉软件高级要求（HLR）。HLR用于生成测试输入，驱动需求中使用的操作的输入空间和可能的状态变化，以及用于判断软件组件在测试输入上是否表现出正确行为的测试口令。符合HLR的软件设计包括软件架构及其计算和交互模型，以及组件的底层需求。我们使用Sally模型检查器[DJN18a]来分析CLEAR HLRs在组件层面和架构假设背景下的集成行为。软件架构是在Radler[LS14, LGS15]使用的多速率、准周期计算模型中捕获的。Radler的使用允许从架构属性和组件代码契约中建立HLRs。我们采用静态和动态分析工具来分析代码的通用属性，如类型良好和不存在某些类别的运行时错误，以及由前/后条件契约表达的特定属性。本体类型系统被用来将数据值与它们所代表的现象量联系起来，例如，地面速度与空气速度，地形高度与气压高度，私有数据与可发布数据，加密信息与未加密信息，以及过滤与未过滤的传感器输入。这些本体标签以一致的方式用于需求、设计和代码层面，以检测普通类型系统无法检测到的大量数据滥用错误。保证工作流程在一个叫做Baseline DesCert的框架中实现和监控，该框架随着设计的发展而维护索赔和证据。

在第二章中，我们介绍了DesCert在安全关键软件开发的保证驱动方法中生成证据的方法概要。我们的方法的细节将在随后的章节中详细阐述。在第三章中，我们描述了保证系统的案例研究，即ArduCopter平台的高级故障安全（AFS）模块，该模块用于检测和恢复特定类别的故障。第四章概述了我们的证据本体论。第5章给出了保证工具及其整合的细节。第6章描述了基线DesCert连续保证流程管理器。第七章阐述了在AFS案例研究中使用DesCert方法生成证据的细节。第8章给出了结论性意见。