SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 15:40 - 16:00 at SPLASH-I - R-5 Chair(s): Anitha Gollamudi, Alex Potanin
Fri 20 Nov 2020 03:40 - 04:00 at SPLASH-I - R-5 Chair(s): Jan Vitek

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

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

15:00 - 16:20
R-5OOPSLA at SPLASH-I +12h
Chair(s): Anitha Gollamudi Harvard University, Alex Potanin Victoria University of Wellington
15:00
20m
Talk
Precise Static Modeling of Ethereum “Memory”
OOPSLA
Sifis Lagouvardos University of Athens, Neville Grech University of Malta, Ilias Tsatiris University of Athens, Yannis Smaragdakis University of Athens
Link to publication DOI Media Attached
15:20
20m
Talk
Perfectly Parallel Fairness Certification of Neural Networks
OOPSLA
Caterina Urban INRIA & École Normale Supérieure | Université PSL, Maria Christakis MPI-SWS, Valentin Wüstholz ConsenSys, Fuyuan Zhang MPI-SWS
Link to publication DOI Media Attached
15:40
20m
Talk
Taming Callbacks for Smart Contract Modularity
OOPSLA
Elvira Albert Complutense University of Madrid, Shelly Grossman Tel Aviv University, Noam Rinetzky Tel Aviv University, Clara Rodríguez-Núñez Complutense University of Madrid, Albert Rubio Complutense University of Madrid, Mooly Sagiv Tel Aviv University
Link to publication DOI Media Attached
16:00
20m
Talk
Exposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution
OOPSLA
Shengjian Guo Baidu Security, Yueqi Chen Pennsylvania State University, Jiyong Yu University of Illinois at Urbana-Champaign, Meng Wu Ant Group, Zhiqiang Zuo Nanjing University, Peng Li Baidu Security, Yueqiang Cheng Baidu Security, Huibo Wang Baidu Security
Link to publication DOI Media Attached

Fri 20 Nov

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

03:00 - 04:20
R-5OOPSLA at SPLASH-I
Chair(s): Jan Vitek Northeastern University / Czech Technical University
03:00
20m
Talk
Precise Static Modeling of Ethereum “Memory”
OOPSLA
Sifis Lagouvardos University of Athens, Neville Grech University of Malta, Ilias Tsatiris University of Athens, Yannis Smaragdakis University of Athens
Link to publication DOI Media Attached
03:20
20m
Talk
Perfectly Parallel Fairness Certification of Neural Networks
OOPSLA
Caterina Urban INRIA & École Normale Supérieure | Université PSL, Maria Christakis MPI-SWS, Valentin Wüstholz ConsenSys, Fuyuan Zhang MPI-SWS
Link to publication DOI Media Attached
03:40
20m
Talk
Taming Callbacks for Smart Contract Modularity
OOPSLA
Elvira Albert Complutense University of Madrid, Shelly Grossman Tel Aviv University, Noam Rinetzky Tel Aviv University, Clara Rodríguez-Núñez Complutense University of Madrid, Albert Rubio Complutense University of Madrid, Mooly Sagiv Tel Aviv University
Link to publication DOI Media Attached
04:00
20m
Talk
Exposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution
OOPSLA
Shengjian Guo Baidu Security, Yueqi Chen Pennsylvania State University, Jiyong Yu University of Illinois at Urbana-Champaign, Meng Wu Ant Group, Zhiqiang Zuo Nanjing University, Peng Li Baidu Security, Yueqiang Cheng Baidu Security, Huibo Wang Baidu Security
Link to publication DOI Media Attached