We introduce Featherweight Solidity, a calculus formalizing the core features of the Solidity language, thus providing a fundamental step to reason about safety properties of smart contracts’ source code. The formalization includes a static type system that represents the foundation of the Solidity compiler. We show that it prevents some errors whereas many others, such as accesses to a non existing function or state variable, are only detected at runtime and cause interruption and rolling-back of transactions. We then propose a refinement of the type system that is retro-compatible with original Solidity code, and statically captures more errors, such as unsafe casts and unsafe call-back expressions.
CITATION STYLE
Crafa, S., Di Pirro, M., & Zucca, E. (2020). Is Solidity Solid Enough? In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11599 LNCS, pp. 138–153). Springer. https://doi.org/10.1007/978-3-030-43725-1_11
Mendeley helps you to discover research relevant for your work.