Michelson 智能合约的抽象解释

智能合约的静态分析在区块链平台上正变得越来越普遍。分析器依赖于符号执行或模型检测等技术，但鲜少有分析器能同时提供强健全性保证并保证分析终止。由于智能合约通常涉及经济资产，证明除无运行时错误之外的数值性质也是可取的。智能合约执行模型与主流编程语言差异很大，且在不同区块链间存在差异，这使得最先进的分析难以适配。例如，智能合约调用可能会修改持久存储，从而影响后续调用。这使得工具难以推断出为形式化确保不存在可利用漏洞所需的循环不变式。用于 Tezos 区块链的 Michelson 智能合约语言是强类型、基于栈的，且具有严格的执行模型，几乎没有隐式运行时错误的机会。我们提出了一项正在进行中的工作，即基于抽象解释并在模块化静态分析器 MOPSA 中实现的 Michelson 静态分析器。我们的工具支持 Michelson 语义特性，包括对外部合约的内部调用。它可以证明无运行时错误，并在无限次调用上推断持久存储的循环不变式。它也正在被扩展以证明高层数值与安全性质。CCS 概念：$\bullet$ 安全与隐私 $\rightarrow$ 逻辑与验证；$\bullet$ 软件及其工程 $\rightarrow$ 自动化静态分析。