每日十亿次查询：自动推理如何保障云安全
在某中心，科学家和工程师们正在利用自动推理技术来证明关键内部系统的正确性，并帮助客户验证其云基础设施的安全性[citation:1]。这项工作的核心是强大的SMT求解器，它们每天处理的查询量高达十亿次[citation:1]。
SMT（可满足性模理论）是SAT（布尔可满足性问题）的泛化，它能够处理整数、实数、字符串或函数等理论，是形式化方法——即使用自动推理来证明计算机程序将按预期运行——的主要工具。
Zelkova：自动化的安全策略分析引擎
为了将自动推理的力量带给所有客户，某中心开发了名为Zelkova的自动推理引擎[citation:1]。它的工作原理是：
- 输入：一个访问控制策略和一个关于访问控制的问题。
- 输出：该问题的正确答案。
Zelkova的创新之处在于，它改变了用户与复杂验证工具的交互方式。与其要求客户（可能并不熟悉形式化方法）提出正确的问题，不如让某中心的服务代表客户向Zelkova提问[citation:1]。例如：
- “某对象存储服务的‘阻止公开访问’功能会询问：‘此存储桶策略是否授予了公开访问权限？’”
- “身份与访问管理服务的‘访问分析器’会询问：‘此密钥是否授予了跨账户访问权限？’”
这使得客户只需查看清晰的是/否答案，即可轻松确定云资源的安全性，从而民主化了自动推理技术，让所有用户都能使用[citation:1]。
背后的技术栈：SMT与投资组合求解器
在底层，Zelkova将策略和问题转化为SMT查询，然后调用一个投资组合求解器来获取答案[citation:1]。
- 翻译：将用高级策略语言编写的安全声明转换为形式化的SMT逻辑公式。
- 求解：投资组合求解器同时调用多个后端求解器（如Z3、CVC4、cvc5以及自定义的自动机求解器）。
- 返回：采用“赢家通吃”策略，返回最先给出答案的求解器的结果[citation:1]。
利用不同SMT求解器的多样性，Zelkova能够快速解决查询——通常在几百毫秒到数十秒之内[citation:1]。
工程化挑战：在云规模下保持稳定与性能
SMT求解器使用巧妙的算法和启发式方法来解决计算难题，其查询解决时间取决于多种因素，包括求解器配置、分析期间选取的随机种子以及所使用的启发式方法[citation:1]。这导致两个语法差异很小的查询可能具有完全不同的运行时间，求解器中的微小实现更改也可能导致较大的运行时差异。
为了平衡SMT求解器性能的不可预测性和非单调性，团队采用了严格的工程最佳实践。在部署Zelkova的新版求解器之前，会进行广泛的离线测试和基准测试[citation:1]。
案例：从CVC4升级到cvc5
在计划将CVC4升级到其新版本cvc5（0.0.4版）时，团队遇到了挑战[citation:1]。在对比图中，对于约15，000个由Zelkova生成的SMT查询：
- 一些之前CVC4在时间限制内未能解决的查询，cvc5能够解决（图中右侧垂直排列的点）。
- 但cvc5也对一些CVC4能解决的查询超时（图顶部水平排列的点）[citation:1]。
这种变化直接影响客户体验。例如，在分析存储桶策略时，如果求解器超时，系统会将存储桶归类为“公开”。如果用户未更改配置，却因求解器版本不同而得到不同的结果，这将是不可接受的[citation:1]。
团队与cvc5开发人员合作，定位并修复了问题根源（一个重写规则被禁用），并在0.0.7版本中重新启用[citation:1]。然而，即使在修复之后，Cvc5在许多简单问题上仍然比CVC4慢一倍（例如，1秒对比2秒）[citation:1]。
由于Zelkova在安全控制（如阻止公开访问）的请求路径中被同步调用，分析时间的加倍可能直接降低用户体验。因此，团队决定将cvc5添加到Zelkova的投资组合求解器中，而不是用它替换CVC4，以此平衡性能与能力，确保稳定和高效[citation:1]。
结论：迈向可证明的安全
通过这项技术，客户可以对其云基础设施的安全性做出全称陈述——即该陈述在全部可能性范围内都成立，而不仅仅基于测试、模糊测试或观察到的有限情况[citation:1]。例如，“我的存储桶没有任何公开访问权限”。
某中心的服务使得自动推理技术正在改变云安全格局，其能力通过几次点击即可提供给所有客户，实现了从学术研究到大规模工业实践的成功转化[citation:1]。
更多精彩内容 请关注我的个人公众号 公众号（办公AI智能小助手）或者 我的个人博客 https://blog.qife122.com/
对网络安全、黑客技术感兴趣的朋友可以关注我的安全公众号（网络安全技术点滴分享）
