Boosting SMT solver performance on mixed-bitwise-arithmetic expressions
Boosting SMT solver performance on mixed-bitwise-arithmetic expressions
复制标题
DOI：
10.1145/3453483.3454068
复制
发表时间：
2021-06
期刊：
影响因子：
--
通讯作者：
Dongpeng Xu;Binbin Liu;Weijie Feng;Jiang Ming;Qilong Zheng;Jing Li;Qiaoyan Yu
中科院分区：
文献类型：
--
作者：
Dongpeng Xu;Binbin Liu;Weijie Feng;Jiang Ming;Qilong Zheng;Jing Li;Qiaoyan Yu
可满足性模理论（SMT）求解器已被广泛应用于自动软件分析中，以推理编码程序语义本质的查询，减轻人工分析的沉重负担。许多SMT求解技术依赖于求解布尔可满足性问题（SAT），而SAT是一个NP完全问题，因此它们使用启发式搜索策略来寻求可能的解，特别是当没有已知定理可以有效地减少问题时。一个新出现的挑战，称为混合位算术（MBA）混淆，阻碍SMT解决通过构建单位方程与位操作（与，或，否定）和算术计算（加，减，乘）。常见的位或算术计算的数学定理不适用于简化MBA方程，导致SMT求解的性能瓶颈。在本文中，我们首先仔细检查求解器的性能解决不同类别的MBA表达式：线性，多项式和非多项式。我们观察到，求解器可以处理简单的线性MBA表达式，但在解决复杂的线性和非线性MBA表达式时，面临着严重的性能放缓。根本原因是复杂的MBA表达式违反了纯算术或按位计算的归约定律。为了提高求解器的性能，我们提出了一个语义保持的转换，以减少混合程度的位和算术运算。我们首先计算一个签名向量的基础上提取的MBA表达式，它捕捉完整的MBA语义的真值表。接下来，我们从签名向量生成更简单的MBA表达式。我们对3000个复杂MBA方程的大规模评估表明，我们的技术显着提高了现代SMT求解器求解MBA公式的性能。
Satisfiability Modulo Theories (SMT) solvers have been widely applied in automated software analysis to reason about the queries that encode the essence of program semantics, relieving the heavy burden of manual analysis. Many SMT solving techniques rely on solving Boolean satisfiability problem (SAT), which is an NP-complete problem, so they use heuristic search strategies to seek possible solutions, especially when no known theorem can efficiently reduce the problem. An emerging challenge, named Mixed-Bitwise-Arithmetic (MBA) obfuscation, impedes SMT solving by constructing identity equations with both bitwise operations (and, or, negate) and arithmetic computation (add, minus, multiply). Common math theorems for bitwise or arithmetic computation are inapplicable to simplifying MBA equations, leading to performance bottlenecks in SMT solving. In this paper, we first scrutinize solvers' performance on solving different categories of MBA expressions: linear, polynomial, and non-polynomial. We observe that solvers can handle simple linear MBA expressions, but facing a severe performance slowdown when solving complex linear and non-linear MBA expressions. The root cause is that complex MBA expressions break the reduction laws for pure arithmetic or bitwise computation. To boost solvers' performance, we propose a semantic-preserving transformation to reduce the mixing degree of bitwise and arithmetic operations. We first calculate a signature vector based on the truth table extracted from an MBA expression, which captures the complete MBA semantics. Next, we generate a simpler MBA expression from the signature vector. Our large-scale evaluation on 3000 complex MBA equations shows that our technique significantly boost modern SMT solvers' performance on solving MBA formulas.