Paper accepted for ICTAC24 | Diego Marmsoler

Our paper Verifying Type Safety for Isabelle/Solidity was accepted for publication for the 21st International Colloquium on Theoretical Aspects of Computing. A prepring is available here

Abstract. Smart contracts are programs stored on the blockchain that are often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions; thus, bugs can lead to large financial losses. In previous works, we developed a formalization of Solidity in Isabelle/HOL, which can be used to verify the properties of Solidity smart contracts. This formalization features untyped stores, where the types are inferred using a type environment. It is currently unclear whether our semantics can cause type inconsistencies between stores and their environments. With this work we address this problem by formalizing the notion of type safety for untyped stores and verifying that our semantics preserve this property. The formalization and proofs were verified using Isabelle/HOL. Our results guarantee that our semantics are type safe and the proofs can be used to simplify the verification process for the properties of Solidity smart contracts.