联手形式化方法专委会“可满足性模理论”术语发布 | CCF术语快线

InfoBox：

中文名：可满足性模理论

外文名：Satisfiability modulo theories

简写：SMT

学科：计算机软件与理论

基本简介：

可满足性模理论的基本思想是针对多种数据类型和相应的谓词逻辑理论，提出一个一般的框架，使得可以求解特定背景理论下的谓词逻辑公式的可满足性判定问题，进一步，可以求解涵盖多种理论的混合逻辑公式的可满足性判定问题。可满足性模理论与交互式定理证明相比，能够处理的逻辑公式要少一些，一般考虑无量词或者量词嵌套较少的谓词逻辑公式，但其优势在于能够实现逻辑推理的完全自动化。

可满足性模理论考虑的谓词逻辑理论主要包括含有等于符号的未解释函数(EUF)、位向量(BV)、数组(Array)、整数线性算术(LIA)、实数线性算术(LRA)、整数非线性算术(NIA)、字符串(String)等。求解SMT公式可满足性问题的工具被称为SMT求解器。目前，比较有代表性的SMT求解器有微软开发的Z3求解器、美国斯坦福大学和爱荷华大学开发的CVC4/CVC5求解器、美国斯坦福国际研究院开发的Yices求解器等。对SMT求解的研究不但是自动推理、约束求解领域主流国际会议IJCAR/CADE、CP和SAT的主题，同时也是形式验证和编程语言领域的重要国际会议CAV、POPL、FM、TACAS上非常活跃的议题。SMT同时也受到产业界的高度关注，微软、英特尔、亚马逊、Cadence等公司的研究院或实验室都在开展与SMT相关的研究项目。

发展历程：

实现逻辑推理自动化是人类社会的终极梦想之一，贯穿人类文明的发展历程。20世纪50-60年代，人工智能的符号学派对于逻辑推理自动化进行了探讨，开发了一些逻辑推理系统[1,2,3,4]，但这些系统的推理能力普遍较弱。2000年左右，命题逻辑的可满足性问题（SAT）求解取得突破，普林斯顿大学的Sharad Malik团队开发了SAT求解器Chaff[5]，首次实现了对大规模命题逻辑公式的求解，并且开始应用于工业界解决实际问题。几乎同时，各种特殊逻辑理论的判定算法的研究开始复兴，出现了一批早期的求解器，比如斯坦福大学的SVC[6]和SteP[7]、SRI的ICS[8]等。研究人员随后考虑了SAT和特殊理论判定算法的融合，由此提出了可满足性模理论问题(SMT)[9]。SMT发展的里程碑包括：2003年开始组织每年一度的SMT研讨会(SMT Workshop)[10]、2004年提出了 SMT-LIB作为SMT问题求解的输入格式标准[11]、2005年创建了SMT竞赛(SMT-COMP)[12]。迄今为止，SMT竞赛收集了超过100,000个测试用例。2010年之后出现了一批比较成熟的SMT求解器，比如美国微软的Z3[13]、美国斯坦福大学和爱荷华大学的CVC4/ CVC5[14,15]、美国斯坦福国际研究院的Yices[16]等。

应用领域：

SMT求解器已经成为软件工程、编程语言、以及信息安全领域的基础引擎，其应用场景多种多样，下面对这些应用场景进行具体阐述。

软件分析与验证：

软件演绎验证归结为两个逻辑公式的蕴涵问题，然后可以编码为SMT的可满足性问题进行求解。微软基于Z3求解器开发了程序演绎验证工具Dafny[17]与Boogie[18]。

软件的符号执行将路径约束编码为SMT公式，从而将路径可行性问题编码为SMT问题，如果SMT公式有解，则可以生成测试用例。斯坦福大学基于SMT求解器开发了符号执行工具Klee[19]，微软基于Z3求解器开发了测试用例生成工具Pex[20]。

语法制导的程序合成问题基于程序模版生成程序，其基本思想是将程序合成问题编码为SMT公式，利用SMT求解器来搜索符合要求的程序[21]。

软件模糊测试是近十年以来的一种非常流行的发现软件系统漏洞的技术，基于动态执行的黑盒模糊测试存在覆盖率较低的问题，因此研究人员已经提出了白盒模糊测试，即将符号执行和动态执行相结合来寻找更多的漏洞，而SMT求解器是符号执行的核心，因此白盒模糊测试技术广泛使用SMT求解器。微软基于Z3求解器开发了模糊测试工具SAGE[22]，发现了Windows应用的很多漏洞。

定理证明：SMT求解器已经集成到了很多交互式定理证明器比如Coq和Isabelle中用于提升其自动化程度[23,24]。

云计算安全性：亚马逊Web服务建立了自动推理组, 基于SMT求解器开发了Zelkova工具和sideTrail工具，其中前者用于验证AMS身份和密钥管理策略以及简单存储服务配置策略的安全性，后者用于验证密码算法实现关于侧信道攻击的安全性[25]。

参考文献：