当AI扫描器说"这个配置看起来不安全，置信度87%"时，形式化验证器说的是"这个配置确实不安全，这是具体的主体、动作和资源证明"。一个是预测，一个是证据。对于保险、审计，以及80%有确切答案的云安全问题来说，这种区别至关重要。
一位首席信息安全官走进网络安全保险续保会议。承保人只问了一个问题：你最敏感的S3存储桶是否会被未授权主体访问？
有两种回答方式。AI驱动的云安全工具给出的是："基于训练数据中的类似配置，该存储桶似乎有适当的控制措施，置信度92%。"形式化验证器给出的是否定的确切答案及见证："不——对以下17个约束条件（涵盖存储桶策略、身份联邦、IAM和账户级公共访问块）求解为UNSAT。"
承保人清楚哪种答案能在代位求偿诉讼中站得住脚。
当Z3这类求解器返回UNSAT时，它已证明模型中没有任何自由变量赋值能满足约束条件。不存在任何主体、动作、资源、角色假设、信任路径或策略条件——在模型范围内——违反该属性。答案是相对于模型数学完备的。当求解器返回SAT时，它提供见证：满足约束条件的具体赋值，明确指出构成违规的确切主体、动作和资源。
这里没有置信度分数，没有概率，没有温度参数，没有误报率，没有训练数据，没有"这可能与已知不良模式相似"。只有从事实到裁决的函数，且裁决相对于给定输入是正确的。
模型相对于现实的局限性是可枚举的：若模型不包含SCP评估，求解器就不会发现SCP问题；若不包含Cognito身份池信任，就不会发现身份联邦链问题。但操作者确切知道验证器覆盖什么、不覆盖什么。AI工具的局限性则是统计性的且不可知的——你无法枚举训练数据未覆盖的内容，不匹配任何训练模式的配置会被静默遗漏，表面类似不良模式的配置会被错误标记。
这种确定性使验证器可审计：今天运行得UNSAT，明天对相同事实库运行仍得UNSAT，三年后审计师索要证据时，对相同事实库运行还是得UNSAT。证明是可复现的证据。
热门跟贴