
原标题:他们写的代码能上天!NASA的10条安全编码准则大公开
美国国家航空航天局(National Aeronautics and Space Administration,缩写为NASA)是美国联邦政府的一个独立机构。负责制定、实施美国的太空计划,开展航空科学暨太空科学的研究。
作为一家厉害到分分钟“上天”的国字头机构,这里自然聚集了全球顶尖的科学家、工程师、设计师,以及码农。
他们写的代码能上天
在凶险的太空环境里,人类的足迹十分有限,为了不断向更远处进发,NASA的许多工作都离不开计算机的辅助。而且,因为需求的特殊性和重要性,他们所使用的很多计算机软件都是内部自行开发的,码农地位之高,不言自喻。

著名的喷气推进实验室 (Jet Propulsion Laboratory ,缩写JPL)为 NASA 做了大量此方面的研究和开发。比如著名的“好奇号”火星探测器、“旅行者号”探测器,后者在飞行25年后离开了太阳系,至今仍为地球提供着科学信息。

“地面上”的码农出现bug可能会导致黑屏,这里的码农如果出现bug那很可能会引发一场牵连性命的事故,这样高水平自动化的长时间任务,对软件质量提出了更高的要求。
当代码的正确性会对人的生命产生决定性影响的时候,例如飞机、将宇航员送上同步轨道的航天器、以及距离居住地仅几英里远的核电站等设施运行的控制代码,编码的标准自然也就提高了许多许多倍。
编程界的“航天标准”
在美国加州理工学院喷气推进实验室与美国国家航空航天局的共同研究下,NASA 喷气推进实验室首席科学家 Gerard J. Holzmann 提出了侧重于安全参数的10条代码编写准则,指导着为 NASA 工作的全球顶尖程序员编写高度安全的软件代码。

这些指南奠定了软件开发过程中必须遵守的基本原则:
1、代码的结构如何安排?
2、应当或不应当使用哪些语言特性?
出于效果的角度考虑,这些原则必须尽可能精简并且足够具体,这样才能更好地被人理解、记忆。

10条安全编码准则
1、简化控制流程
使用尽可能精简的控制流程构造编写程序,不要使用 setjmp、 longjmp 构造和 goto 语句,以及直接或间接的 recursion。
┇原因:简化控制流程有助于提高代码清晰度,增强代码可验证能力。不使用递归,便不会产生循环的函数调用图,这样也可证明所有本应有界的执行实际上都是有界的。
━━━━━
2、为循环使用固定次数上限

所有循环必须有固定次数的上限,我们可以通过验证工具静态地证明,为循环中迭代数量所设立的上限次数未被超越。
如果无法以静态方式对循环的次数界限加以证明,则可认为未遵守该原则。
┇原因:为循环设置次数界限,避免使用递归,这些做法有助于预防代码失控。然而该原则无法适用于本就不应终止的迭代(例如进程调度器)。此时将沿用该原则的逆向原则:必须能够静态地证明迭代不能终止。
━━━━━
3、不使用动态内存分配
不要在初始化完成后进行动态内存分配。
┇原因:为诸如 malloc 等内存分配机制,以及垃圾回收器通常会产生无法预知的行为,进而可能会对性能产生影响。更重要的是,还有可能因为程序员的失误造成内存错误,例如:
l 试图分配超过可用物理内存数的内存
l 忘记释放内存
l 继续使用已被释放的内存
l 对已分配内存进行越界使用
应强制所有模块位于固定大小、预先分配的存储区域中,借此可避免此类问题,并简化内存使用情况的验证工作。未分配内存的情况下,动态请求内存的唯一方式是使用栈内存。
━━━━━
4、不使用冗长的函数
┇原因:过长的函数通常意味着结构并非最优,每个函数都应是可理解、可验证的单一逻辑单位。如果在计算机显示器上需要多屏界面才能完整显示,这样的逻辑单位通常会极难理解。递归 2次调用
本文来自电脑杂谈,转载请注明本文网址:
http://www.pc-fly.com/a/jisuanjixue/article-55664-1.html
那巴萨尔就活过来