New SoCP paper

Created in January 28, 2025

2025

Our paper Deductive verification of Solidity smart contracts with SSCalc is finally published in Science of Computer Programming.

In the paper:

  • We provide a novel calculus to support the verification of Solidity smart contracts.
  • The calculus is formalized in Isabelle and its soundness is mechanically verified.
  • We demonstrate the approach by verifying an invariant for an implementation of a token in Solidity.

Abstract. Smart contracts are programs stored on the blockchain, often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions and thus bugs can lead to large financial losses. With this paper, we address this problem by describing a verification environment for Solidity in Isabelle/HOL. To this end, we first describe a calculus to reason about Solidity smart contracts. The calculus is formalized in Isabelle/HOL and its soundness is mechanically verified. Then, we verify a theorem which guarantees that all instances of an arbitrary contract type satisfy a corresponding invariant. The theorem can be used to verify invariants for Solidity smart contracts. This is demonstrated by a case study in which we use our approach to verify a simple token implemented in Solidity. Our results show that the framework has the potential to significantly reduce the verification effort compared to verifying directly from the semantics.

Link: https://www.sciencedirect.com/science/article/pii/S0167642325000061