NASA十大安全关键代码编程规则：从控制流到静态分析
NASA喷气推进实验室（JPL）首席科学家Gerard J. Holzmann制定C语言安全关键代码十大铁律，聚焦可验证性、确定性与工程纪律，广泛适用于航空航天、核能、医疗等生命攸关系统。
十大核心规则
- 简单控制流：禁goto/setjmp/longjmp/递归，消除循环调用图，保证执行有界。
- 循环固定上界：静态可证明迭代次数上限，防失控代码（非终止任务反向证明）。
- 禁动态内存分配：初始化后禁malloc/GC，栈内存替代，消除泄漏/越界/双重释放风险。
- 函数限60行：单页纸可打印完，强逻辑内聚，利于审阅验证。
- 断言密度≥2/函数：布尔前后置条件/循环不变量，统计显示缺陷拦截率随断言密度升高。
- 最小作用域声明：数据隐藏原则，防变量复用混淆故障诊断。
- 检查参数与返回值：非void函数返回值必检，参数入口必验，显式转void表示有意忽略。
- 限制预处理器：仅允许头文件包含/简单宏，禁递归/拼接/可变参数，条件编译指令需工具标记justify，防指数级版本爆炸。
- 限制指针：单级解引用，禁隐藏在typedef/宏中，禁函数指针，便于静态分析追踪数据流。
- 全编译零警告：首日开启最高警告级，日跑顶级静态分析器零通过，困惑代码重写而非抑制警告。
工程哲学
规则虽严苛，实为“以约束换确定性”。工具链成熟（C语言静态分析器/模型提取器/编译器）使强制执行成为可能。核心思想：在人类认知极限内，用机械可验证的约束构建不可动摇的可信基座。
工业技术