SmartML: Towards a Modeling Language for Smart Contracts
Adele Veschetti, Richard Bubel, Reiner Hähnle
TL;DR
SmartML tackles the prevalence of smart contract vulnerabilities by introducing a platform‑independent modeling language with a formal SOS semantics and a type system focused on safe reentrancy. It defines precise notions of reentrancy safety, contract locations, and a locking mechanism that staticly enforces safe interaction patterns, enabling automatic verification and reducing the risk of attacks. Through a case study, it demonstrates how aliasing and the lock set Δ prevent unsafe reentrant calls across single, cross‑function, and cross‑contract scenarios, while allowing safe tail reentrancy. The work aims to bridge the gap between practical contract development and rigorous verification, offering a foundation for automated proofs, static analysis, and future translation between SmartML and existing languages to enhance security in decentralized systems.
Abstract
Smart contracts codify real-world transactions and automatically execute the terms of the contract when predefined conditions are met. This paper proposes SmartML, a modeling language for smart contracts that is platform independent and easy to comprehend. We detail its formal semantics and type system with a focus on its role in addressing security vulnerabilities. We show along a case study, how SmartML contributes to the prevention of reentrancy attacks, illustrating its efficacy in reinforcing the reliability and security of smart contracts within decentralized systems.