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

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
Times are displayed in time zone: Central Time (US & Canada) change

13:00 - 14:20: 3SAS / DLS at SPLASH-III +12h
Chair(s): Patrick CousotNew York University, Michael HomerVictoria University of Wellington
13:00 - 13:20
Research paper
SAS
Ankush DasCarnegie Mellon University, Shaz QadeerNovi, USA
Pre-print
13:20 - 13:40
Talk
DLS
Ingkarat Rak-amnouykitRensselaer Polytechnic Institute, Daniel McCrevanRensselaer Polytechnic Institute, Ana MilanovaRensselaer Polytechnic Institute, Martin HirzelIBM Research, Julian DolbyIBM Research, USA
Link to publication DOI Pre-print Media Attached
13:40 - 14:00
Research paper
SAS
Samuele BuroUniversità degli Studi di Verona, Roy CroleUniversity of Leicester, Isabella MastroeniUniversity of Verona, Italy
File Attached
14:00 - 14:20
Talk
DLS
Donald PinckneyNortheastern University, Arjun GuhaUniversity of Massachusetts at Amherst, Yuriy BrunUniversity of Massachusetts Amherst
Link to publication DOI Pre-print Media Attached

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

01:00 - 02:20: 3SAS / DLS at SPLASH-III
Chair(s): Francesco RanzatoUniversity of Padova, Michael HomerVictoria University of Wellington
01:00 - 01:20
Research paper
SAS
Ankush DasCarnegie Mellon University, Shaz QadeerNovi, USA
Pre-print
01:20 - 01:40
Talk
DLS
Ingkarat Rak-amnouykitRensselaer Polytechnic Institute, Daniel McCrevanRensselaer Polytechnic Institute, Ana MilanovaRensselaer Polytechnic Institute, Martin HirzelIBM Research, Julian DolbyIBM Research, USA
Link to publication DOI Pre-print Media Attached
01:40 - 02:00
Research paper
SAS
Samuele BuroUniversità degli Studi di Verona, Roy CroleUniversity of Leicester, Isabella MastroeniUniversity of Verona, Italy
File Attached
02:00 - 02:20
Talk
DLS
Donald PinckneyNortheastern University, Arjun GuhaUniversity of Massachusetts at Amherst, Yuriy BrunUniversity of Massachusetts Amherst
Link to publication DOI Pre-print Media Attached