Analysis of “Effectively Callback Freeness” for Smart Contracts

Abstract

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. This work presents the first static technique ensuring 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 work describes an effective technique for soundly ensuring modularity harnessing SMT solvers. The main idea is to define a constructive version of modularity using commutativity and projection operations on program segments. 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 queried contracts in Ethereum). Our implementation decompiles bytecode programs into an intermediate representation and then implements the modularity checking using SMT queries. 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. The main results in this project have been submitted to the ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity (OOPSLA 2020).

Los callbacks son esenciales en muchos entornos de programación, especialmente en los que como Ethereum no permiten estados globales compartidos ni concurrencia. A través de ellos un programa llamado puede llevar de nuevo la ejecución al llamante. A pesar de su efectividad, su uso puede dar lugar a errores. De hecho, muchos de los principales ataques realizados sobre smart contracts explotan su uso. Este trabajo presenta el primer método estático para asegurar modularidad en presencia de callbacks y su aplicación sobre algunos de los principales smart contracts. La modularidad de un contrato asegura que llamadas a contratos externos no pueden afectar a su comportamiento. Cabe destacar que se garantiza modularidad sin establecer restricciones sobre la programación. En general, estudiar la modularidad de un programa es indecidible, incluso cuando no incluye bucles. Este trabajo describe un método efectivo para demostrarla de manera sólida utilizando SMT solvers. La idea clave es el desarrollo de una noción de modularidad basada en la conmutación y proyección de segmentos del programa. De cara a estudiar la precisión del análisis hemos implementado y aplicado nuestra técnica sobre smart contracts reales (incluyendo un subconjunto de los 150 contratos más llamados en Ethereum). Nuestra implementación decompila el bytecode de los programas a una representación intermedia y después estudia su modularidad a través de consultas a SMT solvers. Los resultados experimentales obtenidos indican que el método puede aplicarse sobre multitud de contratos, y que es capaz de demostrar modularidad en casos donde otros métodos fallan. Los principales resultados de este trabajo se han presentado a la conferencia internacional ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity (OOPSLA 2020).