2019/07/05 by Silvia Crafà, Crafa, Silvia, Matteo Di Pirro +1
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Logic, programming, and type systems #Programming Languages (cs.PL) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.1907.02952
openalex publication_date 2019/07/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The recent release of Solidity 0.5 introduced a new type to prevent Ether transfers to smart contracts that are not supposed to receive money. Unfortunately, the compiler fails in enforcing the guarantees this type intended to convey, hence the type soundness of Solidity 0.5 is no better than that of Solidity 0.4. In this paper we discuss a paradigmatic example showing that vulnerable Solidity patterns based on potentially unsafe callback expressions are still unchecked. We also point out a solution that strongly relies on formal methods to support a type-safer smart contracts programming discipline, while being retro-compatible with legacy Solidity code.