一句话：提出面向 Solidity 生成的 EVM 字节码的内存分割变换，用保守内存与指针分析加速 SMT 智能合约验证。
基于 SMT 的低层代码验证需对内存操作建模与推理，而现有通过指针分析将内存拆分为不相交区域以加速 SMT 求解的技术多针对 C/C++ 的显式分配操作。EVM 内存只是字节数组且无分配原语，使这些方法不直接适用。本文针对 Solidity 编译器生成的 EVM 字节码，提出由保守内存分析引导的内存分割变换。分析分两阶段：先恢复内存分配与内存区域，再进行指针分析；其目标是实现内存分割，从而加速验证。作者将分析与变换集成到 CertoraProver 中，在 229 个真实智能合约验证任务上评估，SMT 求解最多加速 120 倍，并消除 16 次超时。
SMT-based verification of low-level code requires modeling and reasoning about memory operations. Prior work has shown that optimizing memory representations is beneficial for scaling verification—pointer analysis, for example can be used to split memory into disjoint regions leading to faster SMT solving. However, these techniques are mostly designed for C and C++ programs with explicit operations for memory allocation which are not present in all languages. For instance, on the Ethereum virtual machine, memory is simply a monolithic array of bytes which can be freely accessed by Ethereum bytecode, and there is no allocation primitive. In this paper, we present a memory splitting transformation guided by a conservative memory analysis for Ethereum bytecode generated by the Solidity compiler. The analysis consists of two phases: recovering memory allocation and memory regions, followed by a pointer analysis. The goal of the analysis is to enable memory splitting which in turn speeds up verification. We have implemented both the analysis and the memory splitting transformation as part of a verification tool, CertoraProver, and show that the transformation speeds up SMT solving by up to 120× and additionally mitigates 16 timeouts when used on 229 real-world smart contract verification tasks.
@article{GrossmanTBASN24,
title = {Practical Verification of Smart Contracts using Memory Splitting},
author = {Shelly Grossman and John Toman and Alexander Bakst and Sameer Arora and Mooly Sagiv and Chandrakana Nandi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689796}
}