SAS 2020
Wed 18 - Fri 20 November 2020 Online Conference
co-located with SPLASH 2020
Wed 18 Nov 2020 13:00 - 13:20 at SPLASH-III - 3 Chair(s): Patrick Cousot, Michael Homer
Thu 19 Nov 2020 01:00 - 01:20 at SPLASH-III - 3 Chair(s): Michael Homer, Francesco Ranzato

Blockchains support execution of smart contracts: programs encoding complex transactions between distrusting parties. Due to their distributed nature, blockchains rely on third-party miners to execute and validate transactions. Miners are compensated by charging users with gas based on the execution cost of the transaction. To compute the exact gas cost, blockchains track gas cost dynamically creating its own overhead. This paper presents a static exact gas-cost analysis technique that can be employed to eliminate dynamic gas tracking. This approach presents further benefits such as providing miners with a trusted gas bound that can be verified in linear time, and eliminating out-of-gas exceptions. To handle recursion and unbounded computation, we propose a novel amortization technique that stores gas inside data structures. We have implemented our analysis technique in a tool called GasBoX that takes a contract as input and infers the gas cost of its functions automatically. We have evaluated GasBoX on 13 standard smart contracts borrowed from real-world blockchain projects. Our soundness theorem proves that the gas bound inferred by GasBoX exactly matches the gas cost at runtime and no dynamic gas tracking is necessary.

Wed 18 Nov

Displayed time zone: Central Time (US & Canada) change

13:00 - 14:20
3SAS / DLS at SPLASH-III +12h
Chair(s): Patrick Cousot New York University, Michael Homer Victoria University of Wellington
13:00
20m
Research paper
Exact and Linear-Time Gas-Cost Analysis
SAS
Ankush Das Carnegie Mellon University, Shaz Qadeer Novi, USA
Pre-print
13:20
20m
Talk
Python 3 Types in the Wild: A Tale of Two Type Systems
DLS
Ingkarat Rak-amnouykit Rensselaer Polytechnic Institute, Daniel McCrevan Rensselaer Polytechnic Institute, Ana Milanova Rensselaer Polytechnic Institute, Martin Hirzel IBM Research, Julian Dolby IBM Research, USA
Link to publication DOI Pre-print Media Attached
13:40
20m
Research paper
On Multi-Language Abstraction: Towards a Static Analysis of Multi-Language Programs
SAS
Samuele Buro Università degli Studi di Verona, Roy Crole University of Leicester, Isabella Mastroeni University of Verona, Italy
File Attached
14:00
20m
Talk
Wasm/k: Delimited Continuations for WebAssembly
DLS
Donald Pinckney Northeastern University, Arjun Guha University of Massachusetts at Amherst, Yuriy Brun University of Massachusetts Amherst
Link to publication DOI Pre-print Media Attached

Thu 19 Nov

Displayed time zone: Central Time (US & Canada) change

01:00 - 02:20
3DLS / SAS at SPLASH-III
Chair(s): Michael Homer Victoria University of Wellington, Francesco Ranzato University of Padova
01:00
20m
Research paper
Exact and Linear-Time Gas-Cost Analysis
SAS
Ankush Das Carnegie Mellon University, Shaz Qadeer Novi, USA
Pre-print
01:20
20m
Talk
Python 3 Types in the Wild: A Tale of Two Type Systems
DLS
Ingkarat Rak-amnouykit Rensselaer Polytechnic Institute, Daniel McCrevan Rensselaer Polytechnic Institute, Ana Milanova Rensselaer Polytechnic Institute, Martin Hirzel IBM Research, Julian Dolby IBM Research, USA
Link to publication DOI Pre-print Media Attached
01:40
20m
Research paper
On Multi-Language Abstraction: Towards a Static Analysis of Multi-Language Programs
SAS
Samuele Buro Università degli Studi di Verona, Roy Crole University of Leicester, Isabella Mastroeni University of Verona, Italy
File Attached
02:00
20m
Talk
Wasm/k: Delimited Continuations for WebAssembly
DLS
Donald Pinckney Northeastern University, Arjun Guha University of Massachusetts at Amherst, Yuriy Brun University of Massachusetts Amherst
Link to publication DOI Pre-print Media Attached