弦理论可满足性求解的计算复杂性
On the Computational Complexity of Satisfiability Solving for String Theories
摘要：
可满足性求解器在软件验证中发挥着越来越重要的作用，特别是在安全漏洞分析中的有效使用。字符串处理是许多软件应用程序（如浏览器和Web服务器）的关键部分。这些应用程序容易受到通过网络接收的恶意数据的攻击。因此，用于分析此类应用程序安全性的自动化工具需要对字符串进行推理。出于效率的原因，最好有一个将字符串视为第一类类型的求解器。在本文中，我们提出了一些理论的字符串，是有用的软件安全的背景下，并分析了计算复杂性的理论。我们使用这种复杂性分析，激发字节爆炸的方法，采用布尔编码的字符串约束相应的布尔可满足性问题。
英文摘要：
Satisfiability solvers are increasingly playing a key role in software verification, with particularly effective use in the analysis of security vulnerabilities. String processing is a key part of many software applications, such as browsers and web servers. These applications are susceptible to attacks through malicious data received over network. Automated tools for analyzing the security of such applications, thus need to reason about strings. For efficiency reasons, it is desirable to have a solver that treats strings as first-class types. In this paper, we present some theories of strings that are useful in a software security context and analyze the computational complexity of the presented theories. We use this complexity analysis to motivate a byte-blast approach which employs a Boolean encoding of the string constraints to a corresponding Boolean satisfiability problem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
