Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT
This program is tentative and subject to change.
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%.
This program is tentative and subject to change.
Thu 19 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 14:50 | |||
13:30 20mTalk | Precise Compositional Buffer Overflow Detection via Heap Disjointness Technical Papers Yiyuan Guo The Hong Kong University of Science and Technology, Peisen Yao Zhejiang University, Charles Zhang The Hong Kong University of Science and Technology DOI Pre-print | ||
13:50 20mTalk | Finding Cuts in Static Analysis Graphs to Debloat Software Technical Papers Christoph Blumschein Hasso Plattner Institute, University of Potsdam, Germany, Fabio Niephaus Oracle Labs, Potsdam, Codrut Stancu Oracle Labs, Christian Wimmer Oracle Labs, Jens Lincke University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute DOI Pre-print | ||
14:10 20mTalk | Scalable, Sound and Accurate Jump Table Analysis Technical Papers Huan Nguyen Stony Brook University, Soumyakant Priyadarshan Stony Brook University, R. Sekar Stony Brook University | ||
14:30 20mTalk | Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT Technical Papers Elvira Albert Complutense University of Madrid, Jesús Correas Complutense University of Madrid, Pablo Gordillo Universidad Complutense de Madrid, Guillermo Román-Díez Universidad Politécnica de Madrid, Albert Rubio Complutense University of Madrid |