安全关键系统验证：保障软件可靠性与安全性

### 安全关键系统验证：保障软件可靠性与安全性 #### 1. 引言 不可靠的软件产品发布可能会导致财产损失或对第三方造成伤害（包括生命损失）。因此，公司在发布软件产品之前，需要确保其产品符合预期用途。广泛使用的软件必须具备可靠性，即软件在需要时可用，并且能够安全、可靠地运行，无任何不良副作用。 如今，数十亿设备和计算机连接到互联网，这导致计算机攻击事件增多。因此，必须仔细考虑计算机安全问题，开发者需要了解系统面临的威胁以及消除这些威胁的技术。软件开发者需要开发安全可靠的系统，使其能够应对并从外部攻击中恢复。 安全关键系统是指一旦发生故障可能会导致重大经济损失或人员伤亡的系统。例如，飞机飞行控制系统、核电站和导弹系统等。在设计和开发这些系统时，必须采用严格的流程，仅靠软件测试通常不足以验证此类系统的正确性。 安全关键行业认为，对安全关键软件的任何更改都会产生一个新程序。因此，新程序需要向公众证明其可靠性和安全性，这就需要进行广泛的测试。此外，还可以采用形式验证和模型检查等技术，为系统的正确性提供额外的保证。 安全关键系统需要可靠、可用，并且在需要时能够正常运行。软件必须正确、可靠地运行，无任何不良副作用。一旦发生故障（如武器系统故障），可能会导致巨大的破坏，甚至危及生命或公众安全。 开发安全关键系统需要严格的流程，并进行严格的质量保证，以确保系统安全可用，不会对公众造成危险。这包括严格的设计和开发流程，以减少软件中的缺陷数量，以及全面的测试，以验证其正确性。在某些情况下，可能无法在实际环境中测试安全关键系统，此时通常会采用其他技术来增强对其正确性的信心。形式化方法就是一种有助于开发和验证安全关键系统的方法。 形式化方法是一组数学技术，用于严格陈述拟议系统的要求。它们可用于从数学规范推导程序，并提供严格的证明，以确保实现的程序满足其规范。形式化方法还可以证明规范中的某些属性为真，这在安全关键和安全敏感应用中尤为有价值。数学规范不会像自然语言描述那样存在歧义，并且可以进行严格的分析，以证明关键属性的存在或不存在。 安全关键系统通常设计为具有容错能力，即系统能够处理并从执行过程中发生的故障中恢复。容错能力通过预测异常事件并设计系统来处理这些事件来实现。容错系统设计为在发生故障时能够安全地失效，程序设计为在发生错误或异常时继续工作（可能性能会有所降低），而不是崩溃。许多容错系统会对所有操作进行镜像处理，即每个操作在两个或多个重复系统上执行，这样如果一个系统发生故障，另一个系统可以接管。 #### 2. 软件可靠性 软件可靠性是指程序在一段时间内无故障运行的概率，通常用平均故障时间来表示。它与硬件可靠性不同，硬件的特点是组件会随着时间的推移而物理磨损，而软件是无形的，软件故障是由于设计和实现错误导致的。换句话说，软件在设计和开发时要么正确，要么错误，不会随着时间的推移而物理损坏。 硬件领域在开发可靠的可靠性模型方面非常成功，这些模型可以有效地预测硬件组件（或产品）的使用寿命。这引发了软件领域对开发科学的软件可靠性模型的兴趣。这样的模型将为在客户现场部署软件之前预测其可靠性提供可靠的机制，并增强对软件符合预期用途和安全使用的信心。 软件可靠性的定义为：软件在指定时间内无故障运行的概率，它是对软件未来行为的一种陈述，通常用平均故障时间（MTTF）或平均故障间隔时间（MTBF）来表示。 统计抽样技术常用于预测硬件的可靠性，因为在生产环境中测试所有产品是不可行的。通过样本的质量来推断整个产品群体的质量，这种方法在制造环境中非常有效，因为制造过程中的变化通常会导致物理产品出现缺陷。 硬件故障通常是由于组件磨损引起的，通常需要更换组件。硬件组件预计能够使用一定的时间，其故障率的变化通常是由于制造过程的变化或组件的运行环境导致的。目前已经开发出了良好的硬件可靠性预测器，每个硬件组件都有预期的平均故障时间。产品的可靠性可以通过其各个组件的可靠性来确定。 软件是一项需要设计师和程序员团队共同参与的智力活动。它本身不会物理磨损，软件故障通常是由特定的用户输入引起的。每个软件代码副本都是相同的，软件代码要么正确，要么错误。也就是说，软件故障是由于设计和实现错误导致的，而不是软件随着时间的推移而物理磨损。虽然已经开发了许多软件可靠性模型（如软件可靠性增长模型），但软件工程界尚未开发出一种值得信赖的、健全的软件可靠性预测模型。 要抽样的软件群体包括软件的所有可能执行路径，由于这可能是无限的，因此通常不可能进行全面测试。软件的使用方式（即用户输入）会影响其可靠性。设 If 表示导致故障的输入集合（即当且仅当用户输入 if 导致故障时，if 属于 If）。软件故障时间的随机性是由于选择 If 中的输入时的不可预测性。可能 If 中的元素是很少使用的输入，因此软件可能会被认为是可靠的。 Harlan Mills 等人表明，在提高平均故障时间（MTTF）方面，覆盖测试不如使用测试成本效益高。统计使用测试可用于预测软件的未来性能和可靠性。它需要了解系统的预期使用情况和软件的所有可能使用方式。抽样按照预期使用情况进行，并计算软件可靠性指标。 Harlan Mills 等人在 IBM 开发了净室软件开发方法。这种正式的软件开发方法涉及应用统计技术，根据软件的预期使用情况计算其可靠性指标。这包括根据预期使用概率从软件的所有可能使用方式中选择测试用例进行执行。统计使用测试在发现导致故障的缺陷方面比覆盖测试更有效。 软件可靠性模型试图预测软件的未来可靠性，并决定软件是否可以发布。一个缺陷并不总是会导致故障，因为它可能发生在很少使用的执行路径上。研究表明，许多观察到的故障是由少数现有缺陷引起的。 缺陷数量和缺陷密度可能不是运行可靠性的良好预测指标，仅仅强调消除软件中的大量缺陷可能不足以实现高可靠性。修复软件中的缺陷会产生一个新版本的软件，可靠性模型假设可靠性会增