SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 15:40 - 16:00 at OOPSLA/ECOOP - R-5
Fri 20 Nov 2020 03:40 - 04:00 at OOPSLA/ECOOP - R-5

Callbacks are an effective programming discipline for implementing event-driven programming, especially in environments like Ethereum which forbid shared global state and concurrency. Callbacks allow a callee to delegate the execution back to the caller. Though effective, they can lead to subtle mistakes principally in open environments where callbacks can be added in a new code. Indeed, several high profile bugs in smart contracts exploit callbacks. We present the first static technique ensuring \emph{modularity} in the presence of callbacks and apply it to verify prominent smart contracts. Modularity ensures that external calls to other contracts cannot affect the behavior of the contract. Importantly, modularity is guaranteed without restricting programming.

In general, checking modularity is undecidable—even for programs without loops. This paper describes an effective technique for soundly ensuring modularity harnessing SMT solvers. The main idea is to define a constructive version of modularity using \emph{commutativity} and \emph{projection} operations on program segments. We believe that this approach is also accessible to programmers, since counterexamples to modularity can be generated automatically by the SMT solvers, allowing programmers to understand and fix the error.

We implemented our approach in order to demonstrate the precision of the modularity analysis and applied it to real smart contracts, including a subset of the 150 most active contracts in Ethereum. Our implementation decompiles bytecode programs into an intermediate representation and then implements the modularity checking using SMT queries. Overall, we argue that our experimental results indicate that the method can be applied to many realistic contracts, and that it is able to prove modularity where other methods fail.

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

15:00 - 16:20: R-5OOPSLA at OOPSLA/ECOOP +12h
15:00 - 15:20
Talk
OOPSLA
Sifis LagouvardosUniversity of Athens, Greece, Neville GrechUniversity of Athens, Greece, Ilias TsatirisUniversity of Athens, Yannis SmaragdakisUniversity of Athens, Greece
15:20 - 15:40
Talk
OOPSLA
Caterina UrbanINRIA & École Normale Supérieure, Maria ChristakisMPI-SWS, Germany, Valentin WüstholzConsenSys, Germany, Fuyuan ZhangMPI-SWS
15:40 - 16:00
Talk
OOPSLA
Elvira AlbertComplutense University of Madrid, Shelly GrossmanTel Aviv University, Noam RinetzkyTel Aviv University, Israel, Clara RodríguezComplutense University of Madrid, Albert RubioComplutense University of Madrid, Mooly SagivTel Aviv University
16:00 - 16:20
Talk
OOPSLA
Shengjian GuoBaidu X-Lab, Yueqi ChenThe Pennsylvania State University, Jiyong YuUniversity of Illinois at Urbana-Champaign, Meng WuAnt Financial, Zhiqiang ZuoNanjing University, China, Peng LiBaidu X-Lab, Yueqiang ChengBaidu Security

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

03:00 - 04:20: R-5OOPSLA at OOPSLA/ECOOP
03:00 - 03:20
Talk
OOPSLA
Sifis LagouvardosUniversity of Athens, Greece, Neville GrechUniversity of Athens, Greece, Ilias TsatirisUniversity of Athens, Yannis SmaragdakisUniversity of Athens, Greece
03:20 - 03:40
Talk
OOPSLA
Caterina UrbanINRIA & École Normale Supérieure, Maria ChristakisMPI-SWS, Germany, Valentin WüstholzConsenSys, Germany, Fuyuan ZhangMPI-SWS
03:40 - 04:00
Talk
OOPSLA
Elvira AlbertComplutense University of Madrid, Shelly GrossmanTel Aviv University, Noam RinetzkyTel Aviv University, Israel, Clara RodríguezComplutense University of Madrid, Albert RubioComplutense University of Madrid, Mooly SagivTel Aviv University
04:00 - 04:20
Talk
OOPSLA
Shengjian GuoBaidu X-Lab, Yueqi ChenThe Pennsylvania State University, Jiyong YuUniversity of Illinois at Urbana-Champaign, Meng WuAnt Financial, Zhiqiang ZuoNanjing University, China, Peng LiBaidu X-Lab, Yueqiang ChengBaidu Security