
在现代飞机等系统中,软件失效可能导致灾难性后果,此时,信任并非一种选择,而是一种建立在确凿证据之上的要求。当生命受到威胁时,随意的软件开发方法是不足够的,这迫切需要一个规范、可验证的框架。本文深入探讨了 DO-178C,这一为航空电子软件安全提供框架的开创性标准。它不仅是一套规则,更是一种构建安全逻辑论证的哲学。本次探索始于第一章 原则与机制,我们将在此剖析 DO-178C 的核心宗旨,包括通过可追溯性实现的“证据大链条”、基于风险的设计保证等级 (DAL) 阶梯,以及像 MC/DC 这样严格的验证技术。随后,在 应用与跨学科联系 一章中,将展示这些原则的普适力量,说明它们如何被应用于汽车、医疗和工业系统,并为认证复杂工具乃至人工智能提供了前进的道路。
我们如何能信任一台数字手中掌握着数百条生命的计算机?当一台机器以超音速飞行、在风暴中导航、并降落在一条狭窄的沥青跑道上时,我们不能仅仅希望其软件是正确的。我们需要确知。我们需要构建一个如此令人信服、如此严谨的论证,使其能够经受住世界上最苛刻专家的审视。这就是航空电子软件的世界,其指导哲学被收录在一份名为 DO-178C 的文档中。
但 DO-178C 并非神奇的公式或官僚的清单。它是一个用于推理的框架,是将科学方法应用于构建我们赖以生存的软件的艺术。其核心在于构建一条完整的证据链,一个能够排除合理怀疑、证明软件将完成其预定功能——并且仅此而已的故事。让我们来探讨构成这一宏大论证的美妙而环环相扣的原则。
想象一下,你是一名侦探,你的嫌疑对象是一个百万行代码的计算机程序。你不能仅仅宣布它是“安全的”。你必须立案。每一份证据都必须被记录,每一项声明都必须被证实,推理链中的每一个环节都必须牢不可破。这就是可追溯性的精髓。它是整个安全论证的逻辑支柱。
这个链条始于系统级危险分析,该分析识别出所有可能出错的可怕情况。针对每一种危险,都会创建安全需求来预防或减轻它。这些需求是第一个环节。从那里开始,链条向下延伸:
这就创建了一个完整的、双向的连接网络。你可以选择任何一个高层安全需求,并沿着链条一直追溯到一行代码以及证明其有效的测试结果。反之,你也可以选择一行代码,并沿着链条向上追溯,以理解它为什么存在——它服务于哪个需求,以及它有助于减轻哪个危险。
但仅仅有链接是不够的;可追溯性的质量至关重要。链条完整吗?它有薄弱环节吗?我们甚至可以定义指标来衡量证据链的质量:
这个“证据大链条”不是一份静态文档。它是一个活的、有生命的逻辑结构,经过精心管理和审计,构成了信任的基础。
现在,一个自然的问题出现了:这个证据链需要有多强?当然,控制乘客机上娱乐屏幕的软件,不需要与实际驾驶飞机的软件受到同等级别的审查。
这就是分级方法原则的用武之地。我们验证工作的强度应与风险成正比。该过程始于系统安全评估,该评估对软件失效的潜在后果进行分类。这些分类很直观:
DO-178C 将这些失效分类转化为设计保证等级 (DALs),我们可以将其视为信任阶梯上的梯级。风险越高,我们必须攀登得越高。
例如,计算主飞行控制律的软件,其错误可能是灾难性的,必须按照 DAL A 进行开发。相比之下,仅仅是格式化非关键维护日志的软件可以是 DAL E,对此 DO-178C 不要求任何与安全相关的任务。
这个信任阶梯是一项极其务实的原则。它让开发人员能够将最密集、最昂贵和最耗时的精力集中在最重要的地方,确保将最高级别的严谨性应用于可能造成最大危害的功能上。
那么,攀登这个阶梯到底意味着什么?是什么让 DAL A 比 DAL C 严格得多?答案在于必须满足的特定验证目标。其中最重要、也最优雅的一个是结构覆盖率分析。
所有针对安全关键系统的测试都是基于需求的,这意味着每个测试的存在都必须是为了验证一个特定的需求。但我们如何知道我们的测试是否彻底?我们可能为每个需求都设置了测试,但这些测试可能只执行了“正常路径”,而代码中一些隐蔽的角落则完全未被触及。
结构覆盖率就是我们的手电筒。它是一种对代码进行插桩的方法,用以观察我们的测试套件执行了代码的哪些部分。随着我们攀登 DAL 阶梯,我们手电筒的光束变得更加聚焦和强大。
DAL C:语句覆盖率。这是第一个严格等级。它要求:代码中每一个可执行语句(或行)是否都至少运行过一次?这就像确保你至少走遍了一个城市的每一条街道。
DAL B:判定覆盖率。这更为严格。它要求:对于代码中的每一个判定(例如,一个 if 或 while 语句),我们是否测试了 true 和 false 两种结果?在每一个岔路口,我们是否都尝试过向左和向右转?
DAL A:修正条件/判定覆盖 (MC/DC)。这是结构覆盖率的顶峰,也是一种美妙的逻辑。对于任何复杂的判定,仅仅让整个表达式为真或为假是不够的。我们必须证明,判定中的每一个独立的原子条件本身都能独立地影响最终结果。
让我们以一个假设的飞行控制模块为例。假设一个判定基于三个条件:。为了实现 MC/DC,我们需要为每个条件找到“独立对”测试。对于条件 ,我们需要找到两个测试用例,其中:
例如,测试对 (c1=0, c2=1, c3=0) -> D=0 和 (c1=1, c2=1, c3=0) -> D=1 展示了 的独立性。我们必须为 、 和 都找到这样的配对。这证明我们的测试足够敏感,能够捕捉到与每个独立条件相关的错误,而不仅仅是它们的组合效应。这是揭示细微逻辑错误的强大审查工具。
另一个随 DAL 等级提高而加强的关键原则是独立性。对于 DAL A 和 B,验证活动(如代码审查和运行测试)必须由创建该产物的开发人员以外的人员执行。这是“双人规则”在工程上的体现,是一种内置的交叉检查,以防范个人错误和偏见。
让我们提出一个深刻的问题。假设我们做到了。我们的 DAL A 代码实现了 100% 的 MC/DC。我们拥有完美的可追溯性。现在我们的软件就完全安全了吗?
令人惊讶而又警醒的答案是:并非如此。我们所有的测试只证明了代码正确地实现了设计。但如果设计本身就是错误的呢?如果一个需求缺失或有缺陷呢?这些被称为系统性故障,它们就像机器中的幽灵。它们是人类思维中的错误,再多的代码测试也无法找到一个只存在于工程师头脑中或需求文档中的缺陷。
那么我们如何与这些幽灵作斗争?这就是系统性能力或过程成熟度概念发挥作用的地方。这个理念认为,一个成熟、规范的开发过程——充满严格的评审、危险分析、形式化建模和严格的配置管理——是我们对抗设计层面缺陷的主要武器。
考虑一个思想实验。想象两种缺陷:简单的“代码缺陷”和更深层次的“设计缺陷”。我们严格的测试(如 MC/DC)在消除代码缺陷方面非常有效,但它并非为发现设计缺陷而设计。设计缺陷最初被引入的数量取决于我们工程过程的质量。一个风险模型表明,要达到灾难性事件所要求的极低失效率(例如,每小时低于十亿分之一,即 ),你需要两种机制协同工作:
两者单独都不足以胜任。这揭示了一个美妙的统一体:我们最关键系统的安全建立在两大支柱之上——验证的严谨性和过程的规范性。
当这些基本原则被应用于当今的前沿技术时,它们比以往任何时候都更具现实意义。
数字孪生或在环处理器 (PIL) 仿真是软件本身的一个完美飞行模拟器。它允许工程师创建飞机及其环境的虚拟副本,然后在这个虚拟世界中,在目标处理器上运行实际的飞行软件。这是一个极其强大的工具。我们可以运行数百万次自动化测试,安全地探索危险的边缘情况(如发动机故障或传感器失灵),注入故障,并精确地收集满足我们覆盖率目标(如 MC/DC)所需的数据。然而,这些强大的工具是符合性方法,而不是捷径。它们帮助我们更高效、更彻底地为我们的安全论证生成证据,但它们不允许我们跳过目标本身。事实上,要使用一个工具来生成认证证据,该工具本身必须经过鉴定,证明其是可信的。
此外,安全不仅关乎软件计算什么,还关乎它何时计算。一个安全的系统必须是确定性和可预测的。软件架构的选择在这里至关重要。时间触发 (TT) 架构就像一场精心编排的芭蕾舞,每个软件任务都被安排在预定的精确时刻运行。这消除了时间抖动,并使系统的最坏情况行为易于分析。相比之下,事件触发 (ET) 架构更像是即兴爵士乐,任务响应事件而运行。虽然更灵活,但这会引入诸如阻塞和抖动等复杂性,这些复杂性更难分析和界定,从而使得构建一个令人信服的安全论证更加困难。
最后,现代系统通常需要在同一台计算机上执行重要性迥异的任务。一个飞行控制器可能需要运行其 DAL A 级别的稳定回路,同时还要管理 DAL C 级别的遥测数据。将所有东西都按 DAL A 标准构建将是极其昂贵的。这就是混合关键性系统所要解决的挑战。其巧妙的解决方案是为关键任务提供两个执行时间预算:一个乐观预算 ,以及一个悲观的、经认证的预算 ,其中 。系统在标称的“低”模式下运行,假设所有任务都将满足其乐观预算。如果某个高关键性任务超出了其乐观预算,系统会立即切换到“高”模式,在该模式下,它会放弃或降级所有低关键性工作,以确保高关键性功能拥有满足其截止时间所需的所有资源。这是一个优雅的解决方案,它将通常情况下的效率与最坏情况下的保证安全相结合。
DO-178C 及其姊妹标准并非为了扼杀创新。它们提供了一个理性、灵活且深刻的框架,用于应用现代工程技术来构建值得我们最终信任的软件。这是一种从宇宙的物理定律到最高的安全原则,一砖一瓦地构建一个无懈可击的论证的哲学。
为航空界严格定义的系统性安全工程原则,其应用并不仅限于驾驶舱。就像物理学的基本定律一样,它们具有普适性,描述了一个共同的难题:如何构建我们赖以生存的复杂系统。虽然其最初的语言是在飞行的背景下形成的,但其核心思想——可追溯性、可验证性以及对风险管理的深刻尊重——现在已在众多高风险领域以多种“方言”被广泛应用。
人们可能会在工业厂房中听到安全完整性等级 (SILs),在自动驾驶汽车中听到汽车安全完整性等级 (ASILs),或在飞机上听到设计保证等级 (DALs)。这些都代表了针对其特定领域量身定制的不同风险校准。例如,化工厂中的一个工业安全功能可能以其按需失效的平均概率为特征,对于一个 SIL 2 系统,其目标可能为 。相比之下,客机飞行控制软件的失效可能是灾难性的,因此被要求达到最高标准 DAL A。但在这些不同标记的背后,是一种共同的哲学:潜在危害越大,所需的安全证明就越强。正是这种共同的哲学,使得在 30,000 英尺高空学到的经验能够以同样的力量应用于手术室或高速公路上。
一个基本原则的真正力量在于它能照亮一个新的领域。航空电子安全技术如今在其发源地之外的许多领域已变得不可或缺。
以医疗设备领域为例。从输液泵到诊断成像,软件现已成为一切的核心。医疗器械软件 (SaMD) 代码中的一个逻辑缺陷可能带来与飞行控制器缺陷同样可怕的后果。我们如何确保其逻辑的健全性?在这里,一项来自航空电子安全手册的强大技术——修正条件/判定覆盖 (MC/DC)——找到了新的用武之地。MC/DC 是一种严格的测试形式,它远不止是简单地运行代码;它要求提供证据,证明一个复杂逻辑判定中的每个条件都已被证明能独立影响结果。将这种最初为灾难性飞行场景设计的审查级别应用于医疗设备的判定逻辑,有助于消除那些可能伤害患者的细微但关键的缺陷。这是保证技术从一个安全关键领域到另一个领域的直接转移。
一个更引人注目的融合正在汽车领域发生,安全与信息安全领域在此交汇。现代汽车是一个带轮子的网络,一个关键的安全需求是“免于干扰”——保证非关键组件(如信息娱乐系统)的故障不会导致关键组件(如刹车系统)的故障。在航空电子领域,这种隔离通常通过物理分区来实现。但现代硬件提供了一种更优雅的解决方案。像可信执行环境 (TEEs)(如 Arm TrustZone)这样的安全特性可用于在处理器中创建隔离的、防篡改的“安全区”。这些安全区最初旨在保护加密密钥等机密,但它们恰好提供了确保免于干扰所需的强大空间和时间隔离。可以构建一个保证论证,说明 TEE 的硬件强制隔离如何直接满足像 ISO 26262(汽车)和 DO-178C(航空电子)等标准的软件隔离目标,从而创造出一种美妙的协同效应,即安全机制成为安全论证的基石。
当我们认证一个软件时,我们真正信任的是什么?我们不仅信任软件本身,还信任用于创建它的整个工具链。这是一个“层层堆叠,无穷无尽”的问题,安全工程必须解决协议栈的每一层。
大多数程序员将编译器视为一个不会出错的翻译器,一个能将人类可读的源代码转换成机器可执行指令的魔法盒子。对于安全关键系统,这种随意的信任是我们无法承受的奢侈。编译器并非魔法;它是一个复杂的软件,可能并且有时确实含有缺陷。更微妙的是,它的优化程序可能会以难以预测的方式改变程序的行为,尤其是其时序行为。对于最关键的系统,我们必须问:编译器是否保留了代码的语义?它对资源使用(如最坏情况执行时间 WCET)的影响是否有界且已知?因此,一个用于 DAL A 软件的可认证编译流程看起来与标准流程非常不同。它通常使用语言的一个受限的、“安全的”子集来消除未定义行为,并且每个优化遍都可能需要为其正确性及其对执行时间的有界影响生成形式化证明或“证书”。本质上,我们必须拥有一个经过验证的编译器来构建经过验证的软件。
这一原则远远超出了编译器的范畴。现代系统如此复杂,以至于无法仅通过物理测试来验证。我们依赖于高保真模拟器(现在时髦地称为“数字孪生”)来运行数百万虚拟英里或飞行小时的测试。但这提出了一个深刻的问题:如果我们用数字孪生来获得对真实系统的信心,我们又如何获得对数字孪生本身的信心呢?
答案在于,不应将数字孪生视为一个简单的测试平台,而应将其视为一个必须经过正式鉴定的“验证工具”。根据 DO-330(软件工具鉴定考量)等标准,如果一个工具的输出被用来消除或减少其他验证活动,那么该工具必须被鉴定到与其所受信任程度相称的级别。这意味着要为数字孪生的可信度构建一个严谨的论证。这个论证并非要证明数字孪生是现实的完美复制品——没有模型能做到这一点。相反,它是一个由证据支持的量化论证。我们建立一个“可信度计划”,用一组精心挑选的物理实验来验证数字孪生的预测,最重要的是,我们*量化不确定性*。最终的声明不是“系统是安全的,因为数字孪生是这么说的”,而是“我们已经量化了数字孪生的预测不确定性,即使考虑到这个不确定性并使用一个保守的统计边界,系统的估计失效率仍然低于所需的安全目标。”这种成熟的、基于风险的方法使我们能够利用仿真的力量,而不会陷入其完美无缺的幻想之中。
现代安全论证很少是单一的、整体性的证明。相反,它是一个精心结构化的安全案例,一幅由不同证据线索编织而成的织锦,共同描绘出一幅令人信服的安全图景。
想象一个制造单元中的机器人系统,其架构是一组相互通信的服务。我们如何论证危险故障(如碰撞)的概率是可接受的低水平?我们可以构建一个复合论证。首先,我们可以使用*形式化方法——一种数学证明形式——来表明控制逻辑的设计是正确的,但需要假设*两件事:(1) 感知系统不会漏掉任何障碍物,以及 (2) 服务之间的消息能准时到达。这个证明有力地约束了问题:设计本身不是风险来源,因此残余风险必然来自对我们假设的违背。
然后,安全论证通过用不同种类的证据来解除这些假设。为了解决时序假设,我们使用最坏情况时序分析来证明系统架构能保证截止时间得到满足。为了解决感知假设,我们查阅硬件数据手册以获取传感器的随机失效率,并利用数字孪生进行广泛的统计测试,以估计由软件引起的感知失效的概率。通过运行数十亿个虚拟场景,我们可以为这个失效率设定一个统计学上的上限。最后,我们将这些残余的失效概率组合起来——保守地将它们相加,以防它们并非独立——从而得出总的系统失效率,然后我们再将其与需求进行核对。这种结合了形式化证明、分析结果和统计证据的多管齐下的论证,是现代安全工程的一个标志。
最大的挑战——也是机遇——是将这些永恒的安全原则应用于人工智能和机器学习的新世界。人工智能不是传统意义上被编程的;它从数据中学习。这要求我们在验证方法上进行深刻的转变。
“测试”一个神经网络控制器意味着什么?仅仅测量“代码覆盖率”几乎毫无意义。我们需要新的指标,这些指标能反映系统的行为,而非其结构。一个强大的想法是“需求鲁棒性覆盖率”。使用像信号时序逻辑 (STL) 这样的形式化语言,我们可以指定一个安全需求——例如,无人机必须在阵风后 5 秒内稳定下来。对于任何给定的测试,我们都可以计算出一个“鲁棒性”得分,这个数字不仅告诉我们系统是通过了还是失败了,还告诉我们它距离失败的边缘有多近。一个导致“险些失败”的测试远比一个以巨大余量通过的测试更有价值。通过搜索最小化这个鲁棒性得分的测试,我们可以将测试引向最具挑战性和启发性的场景,从而获得比结构覆盖率所能提供的更深刻的见解。
最终,机器学习的出现迫使我们面对系统最根本的输入:数据本身。在经典系统中,设计产物是源代码和需求文档。在一个基于机器学习的系统中,训练好的模型 是代码 、训练数据 和训练参数 的函数:。数据不再仅仅是“测试输入”;它是一个塑造最终系统逻辑的主要设计产物。
这对认证具有重大影响。“配置管理”的概念必须扩展以包含数据。我们需要严格的数据集溯源:完整记录数据来自何处,以及如何被收集、标记和整理。我们需要数据治理:一套控制措施,以确保数据在其整个生命周期中的质量、完整性和适用性。训练数据的变更与源代码的变更同等重要,其对安全性的影响必须经过同样严格的评估。为一个支持机器学习的系统进行安全论证,如果没有一个完整、可追溯且受治理的数据管道,就好比在不控制铝材质量的情况下制造飞机。这是对未知的赌博。DO-178C 的原则——严谨性、可追溯性和控制——仍然是我们坚定的指南,但我们必须应用这些原则的领域已经从代码世界扩展到了广阔而复杂的数据世界。