一句话：先用不健全静态资源分析获得精确存储成本界，再用 Max-SMT 修正以恢复健全性，用于以太坊 gas 分析。
存储是跨程序执行持久保留的内存；在区块链中其内容被复制并产生最高的 gas 费用。以太坊存储成本模型具有动态性：某键首次访问成本更高，写访问还依值是否改变而有不同成本。现有 gas 分析器一律按最大成本估算，过于悲观且界过松。本文提出先用现成静态资源分析但不总假设最坏成本，从而得到不健全但更精确的界；再用新的 Max-SMT 方法计算修正量以恢复健全性。作者实现了该方法，并用其改进以太坊 gas 分析器 gastap 和 asparagus；在超过 40 万个函数上实验，存储界精度最高提升 75%，最常见提升为 10–20%。
A storage is a persistent memory whose contents are kept across different program executions. In the blockchain technology, storage contents are replicated and incur the largest costs of a program’s execution (a.k.a. gas fees). Storage costs are dynamically calculated using a rather complex model which assigns a much larger cost to the first access made in an execution to a storage key, and besides assigns different costs to write accesses depending on whether they change the values w.r.t. the initial and previous contents. Safely assuming the largest cost for all situations, as done in existing gas analyzers, is an overly-pessimistic approach that might render useless bounds because of being too loose. The challenge is to soundly, and yet accurately, synthesize storage bounds which take into account the dynamicity implicit to the cost model. Our solution consists in using an off-the-shelf static resource analysis —but do not always assuming a worst-case cost— and hence yielding unsound bounds; and then, in a posterior stage, computing corrections to recover soundness in the bounds by using a new Max-SMT based approach. We have implemented our approach and used it to improve the precision of two gas analyzers for Ethereum, gastap and asparagus. Experimental results on more than 400,000 functions show that we achieve great accuracy gains, up to 75%, on the storage bounds, being the most frequent gains between 10-20%.
DOI 原文 ·
@inproceedings{paperbot8582,
title = {Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT},
author = {Elvira Albert and Jesús Correas and Pablo Gordillo and Guillermo Román-Díez and Albert Rubio},
booktitle = {ISSTA},
year = {2024},
doi = {10.1145/3650212.3680352}
}