每日十亿次SMT查询的技术实践

基于SMT求解器的云端自动化推理实践

在计算机辅助验证（CAV）会议上，某机构的应用科学总监提出技术创新已"引领自动化推理的黄金时代"。研究人员通过自动化推理技术证明关键内部系统的正确性，并帮助用户验证云基础设施安全性。这些创新主要由称为SMT求解器的强大推理引擎驱动。

技术核心：从SAT到SMT

可满足性问题（SAT）要求判断变量赋值是否能满足约束条件。而可满足性模理论（SMT）将SAT推广至整数、实数、字符串或函数领域，成为形式化方法的核心——通过自动化推理证明计算机程序按预期运行。

Zelkova引擎架构

Zelkova接收访问控制策略和权限问题输入，返回准确答案。关键创新在于：不再要求用户提出正确问题，而是由云服务代表用户向Zelkova发起查询。例如：

• 对象存储服务会询问"该存储桶策略是否允许公开访问？"
• 身份访问管理分析器询问"该密钥是否允许跨账户访问？"

底层实现中，Zelkova将策略和问题转换为SMT查询，调用组合求解器（portfolio solver）获取答案。该求解器采用胜者通吃策略，并行调用Z3、CVC4、cvc5及自定义自动机求解器，返回最先响应结果。通过利用SMT求解器多样性，Zelkova能在数百毫秒至数十秒内完成查询。

规模化工程挑战

SMT求解器使用复杂算法和启发式方法解决计算难题，查询耗时受求解器配置、随机种子和启发策略等因素影响，导致语法差异微小的查询可能出现数量级的时间差异。

版本升级性能波动

在将CVC4升级至cvc5（0.0.4版）时，通过对15,000个SMT查询的测试发现：

• cvc5解决了部分CVC4超时的问题（图表右侧垂直分布点）
• 但cvc5在部分CVC4已解决的问题上超时（图表顶部水平分布点）

用户体验影响

在对象存储服务中，若求解器超时，系统会将存储桶标记为"公开"。如果用户未修改配置却因求解器版本变更导致访问权限变化，将造成意外访问阻断。经分析发现cvc5中某重写规则被禁用，在0.0.7版本重新启用后，CVC4在简单问题上仍保持两倍速度优势（1秒对比2秒）。

生产环境优化

由于Zelkova被应用于安全控制的请求链路中（如用户附加新访问策略时的同步调用），查询时间翻倍可能直接影响用户体验。因此最终采用将cvc5添加至组合求解器而非替换CVC4的方案。

技术民主化实践

通过封装复杂技术细节，使用户能直接关注价值层面：对云基础设施安全性做出全局声明（global statements）。这些声明覆盖所有可能性空间，而非仅基于测试、模糊测试或观察结果。现有服务已支持用户声明"我的存储桶不存在公开访问"等全域安全断言。

自动化推理正在重塑云安全格局，其能力通过数次点击即可为所有云用户所用。如需了解具体应用方式，可参考某机构安全会议上关于可证明安全性的专题演讲。