每日十亿次SMT查询：云规模下的自动推理实践

在今年的计算机辅助验证（CAV）会议上，某机构的Neha Rungta发表了主题演讲，她认为某机构的创新“开启了自动推理的黄金时代”。某机构的科学家和工程师正在使用自动推理来证明关键内部系统的正确性，并帮助客户证明其云基础设施的安全性。这些创新中的许多都是由称为SMT求解器的强大推理引擎驱动的。

Zelkova

在某机构，使用自动推理来证明内部系统的正确性，并提供服务，让客户能够证明其云系统的正确性。本文将重点介绍这项工作中一个关键部分，展示如何通过一个名为Zelkova的自动推理引擎，帮助客户正确配置其访问控制。

Zelkova将一个访问控制策略和一个关于访问控制的问题作为输入，并返回问题的正确答案。答案的正确性取决于是否提出了正确的问题。这里的关键创新在于，并非要求客户提出正确的问题，而是由某云服务代表客户向Zelkova提问。

例如，S3的“阻止公共访问”功能会问Zelkova：“这个S3存储桶策略是否授予公共访问权限？”身份与访问管理（IAM）访问分析器会问Zelkova：“这个KMS密钥是否授予跨账户访问权限？”通过查看答案，客户可以轻松确定云资源的安全性。这种让云服务代为提问的模式，使得自动推理得以普及，并为所有某云客户所用。

在底层，Zelkova将策略和问题转换为SMT查询，并调用一个组合求解器来获得答案。组合求解器在后端调用多个求解器——包括Z3、CVC4、cvc5和一个自定义自动机求解器，并采用赢家通吃的策略，返回最先得出答案的求解器的结果。利用SMT求解器的多样性，Zelkova能够在几百毫秒到几十秒内快速解决查询问题。

云规模下的SMT求解

SMT求解器使用巧妙的算法和启发式方法来解决计算难题。解决查询所需的时间取决于多种因素，包括求解器配置、分析过程中选取的随机种子以及所使用的启发式方法。结果是，两个语法差异很小的查询可能会有截然不同的运行时间。同样，求解器中看似微小的实现更改也可能导致巨大的运行时间差异。

为了消除SMT求解器性能上的不可预测性和不稳定性，工程上采用了最佳实践。在部署新版Zelkova求解器之前，会进行广泛的离线测试和基准测试。

在尝试将CVC4升级到其新版本cvc5（0.0.4版本）时遇到了一些意外。通过对比两个求解器的图表，可以看到大约有15,000个由Zelkova生成的SMT查询。选择了一个查询分布，其解决时间从0.01秒到30秒不等；30秒后，求解进程会被终止并报告超时。图表右侧垂直对齐的点显示，一些在时限内未被CVC4解决的查询现在被cvc5解决了。然而，图表顶部水平对齐的点显示，cvc5对一些CVC4能解决的查询却超时了。

SMT查询运行时间的变化可能会影响客户体验。例如，在S3“阻止公共访问”功能中，分析存储桶策略时，如果求解器超时，它会将该存储桶归类为“公共”访问。假设使用之前的求解器版本，基于查询结果，有一个存储桶被标记为“非公共”。再假设使用当前求解器版本，如果同一个查询超时，则该存储桶被标记为“公共”。这将锁定该存储桶，导致预期用户无法访问。这对于未做任何配置更改的用户来说是出乎意料的。因此，需要确保所有以前能在最大时限内解决的查询，现在仍然能够被解决。

深入研究了造成这种差异的根本原因，结果发现cvc5中禁用了某个重写规则。与cvc5的开发者合作，使其重新启用（在0.0.7版本中），但故事并未就此结束。事实证明，即使修复了这个问题，在许多较简单的问题上，CVC4的速度仍然是cvc5的两倍，能在1秒内解决，而cvc5需要2秒。

这种性能下降至关重要，因为Zelkova是在诸如S3“阻止公共访问”等安全控制的请求路径中被调用的。当用户尝试将新的访问控制策略附加到S3存储桶或更新现有策略时，会同步调用Zelkova及其对应的组合求解器，以确定该策略是否授予无限制的公共访问权限。分析时间的大部分都花在了SMT求解器上，因此查询分析时间的加倍可能会严重影响用户体验。这就是为什么决定将cvc5添加到Zelkova的组合求解器中，而不是直接用它替换CVC4。

自动推理的普及

这对客户意味着什么？他们可以将注意力从技术本身转移到其价值上。告知客户，他们可以对其云基础设施的安全性做出通用性声明。这种声明涵盖了所有可能情况，而不仅仅是经过测试、模糊测试、观察或考虑过的情况。诸如S3“阻止公共访问”、IAM访问分析器、VPC网络访问分析器和Amazon Inspector等服务，让客户能够做出诸如“我的S3存储桶没有公共访问权限”这样的通用性声明。自动推理正在改变云安全的格局，而某云客户只需点击几下鼠标，即可获得这项强大的技术。FINISHED