模理论模型计数

本论文关注软件安全性的定量评估。具体而言，它解决了信道容量的有效计算问题，即以香农熵或 R\'{e}nyi 最小熵衡量的软件泄露机密信息的最大量。大多数计算信道容量的方法要么高效但仅返回（可能非常宽松的）上界，要么精确但低效；很少有方法针对现实程序。在本论文中，我们提出了一种新颖的方法，将该问题归约为关于一阶逻辑的模型计数问题，我们将其命名为模理论模型计数（Model Counting Modulo Theories）或简称为#SMT。对于定量安全性，我们的贡献有两方面。首先，在理论层面，我们建立了衡量机密泄露与基本验证算法（如符号执行、SMT 求解器和 DPLL）之间的联系。其次，利用这些联系，我们开发了基于#SMT 的新技术来计算信道容量，同时实现了准确性和效率。这些技术可扩展至现实世界程序， illustrative 案例研究包括来自 Linux 内核的 C 程序、来自欧洲项目的 Java 程序以及匿名协议。对于形式化验证，我们的贡献也有两方面。首先，我们引入并研究了一个新的研究问题，即#SMT，它在计算信道容量之外具有其他潜在应用，例如为有界模型检查返回多个反例或自动化测试生成。其次，我们提出了一种使用经典符号执行进行有界模型检查的替代方法，该方法可并行化以利用现代多核和分布式架构。