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

15:00 - 16:20: R-5OOPSLA at SPLASH-I +12h
Chair(s): Alex PotaninVictoria University of Wellington, Anitha GollamudiHarvard University
15:00 - 15:20
Talk
Precise Static Modeling of Ethereum “Memory”
OOPSLA
Sifis LagouvardosUniversity of Athens, Neville GrechUniversity of Malta, Ilias TsatirisUniversity of Athens, Yannis SmaragdakisUniversity of Athens
Link to publication DOI Media Attached
15:20 - 15:40
Talk
Perfectly Parallel Fairness Certification of Neural Networks
OOPSLA
Caterina UrbanINRIA & École Normale Supérieure | Université PSL, Maria ChristakisMPI-SWS, Valentin WüstholzConsenSys, Fuyuan ZhangMPI-SWS
Link to publication DOI Media Attached
15:40 - 16:00
Talk
Taming Callbacks for Smart Contract Modularity
OOPSLA
Elvira AlbertComplutense University of Madrid, Shelly GrossmanTel Aviv University, Noam RinetzkyTel Aviv University, Clara Rodríguez-NúñezComplutense University of Madrid, Albert RubioComplutense University of Madrid, Mooly SagivTel Aviv University
Link to publication DOI Media Attached
16:00 - 16:20
Talk
Exposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution
OOPSLA
Shengjian GuoBaidu Security, Yueqi ChenPennsylvania State University, Jiyong YuUniversity of Illinois at Urbana-Champaign, Meng WuAnt Group, Zhiqiang ZuoNanjing University, Peng LiBaidu Security, Yueqiang ChengBaidu Security, Huibo WangBaidu Security
Link to publication DOI Media Attached

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

03:00 - 04:20: R-5OOPSLA at SPLASH-I
Chair(s): Jan VitekNortheastern University / Czech Technical University
03:00 - 03:20
Talk
Precise Static Modeling of Ethereum “Memory”
OOPSLA
Sifis LagouvardosUniversity of Athens, Neville GrechUniversity of Malta, Ilias TsatirisUniversity of Athens, Yannis SmaragdakisUniversity of Athens
Link to publication DOI Media Attached
03:20 - 03:40
Talk
Perfectly Parallel Fairness Certification of Neural Networks
OOPSLA
Caterina UrbanINRIA & École Normale Supérieure | Université PSL, Maria ChristakisMPI-SWS, Valentin WüstholzConsenSys, Fuyuan ZhangMPI-SWS
Link to publication DOI Media Attached
03:40 - 04:00
Talk
Taming Callbacks for Smart Contract Modularity
OOPSLA
Elvira AlbertComplutense University of Madrid, Shelly GrossmanTel Aviv University, Noam RinetzkyTel Aviv University, Clara Rodríguez-NúñezComplutense University of Madrid, Albert RubioComplutense University of Madrid, Mooly SagivTel Aviv University
Link to publication DOI Media Attached
04:00 - 04:20
Talk
Exposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution
OOPSLA
Shengjian GuoBaidu Security, Yueqi ChenPennsylvania State University, Jiyong YuUniversity of Illinois at Urbana-Champaign, Meng WuAnt Group, Zhiqiang ZuoNanjing University, Peng LiBaidu Security, Yueqiang ChengBaidu Security, Huibo WangBaidu Security
Link to publication DOI Media Attached