知识卡片
不变量是全称命题不是抽样保证
内容
系统安全属性通常表达为”不变量”——在所有可能运行状态下都必须成立的性质，而不只是在正常输入或预期负载下成立。测试天然只能覆盖典型的一小部分行为，证明不了”对所有可能的恶意或异常输入都成立”这种全称命题；形式化证明能做到，但成本极高（某微内核的完整正确性证明耗费约20年）。这提示安全断言和普通功能验证要求不同的证据强度：能通过测试用例不等于不变量真的成立，只是还没找到反例而已。
参考来源
- 位置：《Google系统架构解密：构建安全可靠的系统》第6章《面向易理解性的设计》6.1.1—6.1.2节（源文件：`../OREILY动物书合辑 图灵新版/_epub-src/text/part0014_split_056.html`）
- 结论依据：原文定义不变量为"确保的期望属性实际上……即便系统环境出现任何意想不到或恶意行为"，并说明测试和代码审阅这类方法不能带来特别强的信心，形式化证明虽更强但某微内核项目耗费约20年，证明测试通过与不变量成立之间存在证据强度差距。
- 原始内容：确保的期望属性实际上就是不变量，即便系统的环境出现任何意想不到或者恶意的行为导致运行不正常……迄今为止最大的软件验证项目之一，在机器码级别构建了由微内核实现的全面正确性和安全属性的证明。这个项目花费了大约20年的努力。