【译文】美国航天局(NASA)编写安全关键程序的 10 条编码规则
大型软件项目使用各种编码标准和准则。这些准则规定了编写软件时必须遵守的基本规则。通常,它们确定
- 代码应该如何构建?
- 应该或不应该使用哪种语言功能?
这些规则要想行之有效,就必须简洁明了,便于理解和记忆。美国国家航空航天局(NASA)作为世界顶级的航天机构,也遵循类似的规则。
从引导航天器轨迹到管理生命支持系统,软件程序在确保每次任务的安全和成功方面发挥着至关重要的作用。美国国家航空航天局制定并完善了一套编码指南,作为其任务软件开发的支柱。
这些规则随着时间的推移而演变,其中包含了从过去的任务和技术进步中吸取的经验教训。了解这些规则的历史有助于我们了解 NASA 如何不断努力确保太空任务软件的可靠性和安全性。
下面,我们列出了由 JPL 首席科学家杰拉德-J-霍尔兹曼(Gerard J. Holzmann)制定的 NASA 10 条编码规则。这些规则主要集中在安全参数方面,也可适用于其他编程语言。
您知道吗?
美国国家航空航天局(NASA)成功登陆火星的 “好奇号 “漫游车依靠近 250 万行代码运行。这凸显了星际任务所需软件的复杂性和大规模性。
规则 1 – 简单的控制流
使用非常简单的控制流结构编写程序 – 不要使用 setjmp 或 longjmp 结构、goto 语句以及直接或间接递归。
理由:简单的控制流可提高代码的清晰度和验证能力。没有递归,就不会有循环函数调用图。因此,所有本应受约束的执行实际上仍然是受约束的。
规则 2–循环的固定上限
每个循环都必须有一个预先确定的上限。验证工具应能静态证明循环迭代的设定上限不会被超过。
如果无法静态证明循环上限,则视为违反规则。
理由:设置循环界限和避免递归有助于防止代码执行失控。不过,这条规则不适用于设计为非终止的迭代,如进程调度程序。在这种情况下,应采用相反的规则–必须能静态证明迭代不会终止。
规则 3 – 禁止动态内存分配
初始化后不要使用动态内存分配。
原因是内存分配器(如 malloc)和垃圾回收器经常会出现不可预测的行为,从而对性能造成极大影响。此外,程序员的错误也可能导致内存错误,其中包括
- 试图分配比实际可用内存更多的内存
- 忘记释放内存
- 释放内存后继续使用内存
- 超越已分配内存的边界
强制所有模块在固定的、预先分配的存储区域内运行,可以消除这些问题,并更容易验证内存使用情况。
要在不使用堆内存分配的情况下动态分配内存,一种方法是利用堆栈内存。
规则 4 – 不使用大篇幅函数
任何函数的长度都不得超过标准参考格式打印在一张纸上的长度。这条准则要求将函数的代码行数控制在 60 行以内,确保每条声明一行,每条语句一行。
原因:过长的函数通常是结构不良的表现。每个函数都应是一个可理解和可验证的逻辑单元。要理解一个跨越计算机显示屏多个屏幕的逻辑单元是相当困难的。
规则 5 – 低断言密度
程序的断言密度应为平均每个函数至少两个断言。断言用于检查在实际执行中绝对不会出现的异常情况。断言应定义为布尔测试。当断言失败时,应采取明确的恢复措施。
如果静态检查工具证明断言永远不会失败或永远不成立,则认为违反了规则。
原因:根据业界的编码工作量统计,单元测试每 10 到 100 行代码至少能截获一个缺陷。截获缺陷的机会随着断言密度的增加而增加。
断言的使用也很重要,因为它们是强大的防御性编码策略的一部分。断言用于验证函数的前置和后置条件、函数的参数和返回值以及循环变量。在测试完性能关键代码后,可以有选择地禁用断言。
规则 6 – 在最小范围内声明数据对象
这一条支持数据隐藏的基本原则。所有数据对象都必须在尽可能小的范围内声明。
原因:如果对象不在作用域内,其值就不能被引用或破坏。这条规则不鼓励为多个不兼容的目的重复使用变量,因为这会使故障诊断复杂化。
规则 7 – 检查参数和返回值
每个调用函数都应检查非虚函数的返回值,每个函数内部都应检查参数的有效性。
在最严格的形式下,这条规则意味着甚至 printf 语句和文件关闭语句的返回值也应进行检查。
理由:如果对错误的响应与对成功的响应没有什么不同,那么就应该明确检查返回值。对 close 和 printf 的调用通常就是这种情况。明确地将函数返回值赋值为 void 是可以接受的,这表明编码者明确地(而不是意外地)决定忽略返回值。
规则 8 – 预处理器的有限使用
预处理器的使用应仅限于包含头文件和宏定义。不允许使用递归宏调用、标记粘贴和变量参数列表。
即使在大型应用程序开发工作中,也应该有理由使用一个或两个以上的条件编译指令,而不是使用标准的模板,以避免多次包含相同的头文件。每次使用都必须由基于工具的检查程序标记出来,并在代码中说明理由。
理由:C 预处理器是一个功能强大而又含糊不清的工具,它可能会破坏代码的清晰度,并使许多基于文本的检查程序感到困惑。即使掌握了正式的语言定义,也很难解读无约束预处理器代码中构造的效果。
对条件编译的警惕同样重要–仅 10 个条件编译指令,就可能有 1024 个可能的代码版本(2^10),大大增加了所需的测试工作量。
规则 9-有限制地使用指针
必须限制使用指针。不允许超过一级的引用。指针的取消引用操作不应隐藏在类型定义声明或宏定义中。
也不允许使用函数指针。
原因:即使是专家也很容易滥用指针。使用指针很难跟踪或分析程序中的数据流,尤其是基于工具的静态分析器。
函数指针还限制了静态分析器的检查类型。因此,只有在有充分理由的情况下才能使用函数指针。如果使用函数指针,工具几乎不可能证明没有递归,因此应提供其他方法来弥补分析能力上的损失。
规则 10 – 编译所有代码
从开发的第一天起,所有代码都必须编译。编译器警告必须在编译器最严谨的设置下启用。代码必须在无任何警告的情况下编译。
所有代码都应每天使用至少一种(最好不止一种)最先进的静态源代码分析器进行检查,并应在零警告的情况下通过分析过程。
原因:市场上有很多有效的源代码分析器,其中一些还是免费工具。任何程序员都没有理由不使用这种现成的技术。
如果编译器或静态分析器遇到混乱或错误,则应重写导致问题的代码,使其更加直接有效。
NASA 是如何看待这些规则的呢?
“这些规则就像汽车上的安全带一样:一开始可能会有点不舒服,但一段时间后,使用它们就会成为第二天性,不使用它们就会变得难以想象”。
NASA 使用什么编程语言?
NASA 使用多种编程语言,用于不同的项目和任务。虽然语言的选择取决于每个项目的具体要求,但最常用的语言有
- C 和 C++ 用于开发航天器上的控制系统和嵌入式系统
- Python 用于数据分析、模拟和脚本任务
- Java 用于开发独立于平台的应用程序和软件模块
- Fortran 支持传统代码和数值模拟
- Matlab 用于工程和科学应用中的数学建模、模拟和分析
- Ada 经常用于安全关键型系统
- 汇编语言用于某些对底层控制和优化至关重要的场合
- JavaScript 可促进与任务数据的实时交互
- 高阶汇编语言/Shuttle(HAL/S)是一种实时航空编程语言编译器,专为航空电子应用而设计
错误率和可靠性
美国国家航空航天局(NASA)对软件工具的错误率要求极低。他们通常以每 10,000 行代码中错误少于一个为目标,以确保航天器系统的可靠性。
他们还非常重视冗余和容错。例如,航天器上的软件程序通常包括备份系统,即使主系统出现故障,也能保证功能正常。
此外,NASA 的软件测试阶段非常全面,包括模拟测试、硬件在环测试和实际测试。例如,火星探测器在开始星际旅行之前,在地球上进行了多年的测试。
本文文字及图片出自 NASA’s 10 Coding Rules for Writing Safety Critical Program