适用于未来700种内存模型的组合符号执行技术

《Proceedings of the ACM on Programming Languages》：Compositional Symbolic Execution for the Next 700 Memory Models

本文提出基于Rocq定理证明器的内存模型可参数化CSE工具的正式基础，支持SL和ISL分析，验证了C和CHERI内存模型，确保与标准定义兼容，提升灵活性和性能。

　　

摘要

多种成功的组合符号执行（CSE）工具和平台利用分离逻辑（SL）进行组合验证，或利用不正确性分离逻辑（ISL）进行组合错误查找，其中包括VeriFast、Viper、Gillian、CN和Infer-Pulse。之前针对Gillian平台的研究表明，该平台是唯一一个在内存模型上具有参数化的CSE平台，这意味着它可以被实例化为不同的内存模型。这种参数化特性使得该平台在支持多种编程语言的分析、实现自定义自动化以及提升性能方面具有更大的灵活性。然而，目前关于内存模型参数化CSE平台的正式理论基础尚不完善。

受Gillian的启发，我们在本文中为内存模型参数化CSE平台提供了新的正式理论基础。我们的理论基础在四个方面实现了技术突破：首先，我们将这一基础实现了自动化（通过交互式定理证明器Rocq）；其次，我们通过将其应用于多种内存模型（包括C语言和CHERI语言的内存模型）来验证其有效性；第三，以往的内存模型参数化研究仅涵盖了SL分析，而我们的研究同时涵盖了SL和ISL分析；第四，我们的理论基础基于SL和ISL的标准定义（包括函数规范有效性的定义），从而确保了与其他基于标准定义的工具和平台的良好互操作性。