TY - GEN
T1 - Modeling and Verification of Solidity Smart Contracts with the B Method
AU - Baba, Fayçal
AU - Mammar, Amel
AU - Frappier, Marc
AU - Laleau, Régine
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.
PY - 2025/1/1
Y1 - 2025/1/1
N2 - Smart contracts written using the Solidity programming language of the Ethereum platform are well-known to be subject to bugs and vulnerabilities, which already have led to the loss of millions of dollars worth of assets. Since smart contract code cannot be updated to patch security flaws, reasoning about smart contract correctness to ensure the absence of vulnerabilities before their deployment is of the utmost importance. In this paper, we present a formal approach for generating correct smart contracts from B specification that verify safety properties. Our approach consists of two phases: first a smart contract and its properties are specified and verified in B, then a set of rules we defined are applied to generate the correct smart contract code in Solidity. The approach is implemented in a tool that can generate Solidity contract from a proven B project. The whole approach is demonstrated by a case study on the ERC-20 (Ethereum Request for Comments 20) Wrapped Ether (WETH) contract, which is abstractly specified in B, with invariants stating correctness properties, modeled checked with ProB for temporal properties, implemented in B0, proven correct, and automatically translated into a Solidity contract.
AB - Smart contracts written using the Solidity programming language of the Ethereum platform are well-known to be subject to bugs and vulnerabilities, which already have led to the loss of millions of dollars worth of assets. Since smart contract code cannot be updated to patch security flaws, reasoning about smart contract correctness to ensure the absence of vulnerabilities before their deployment is of the utmost importance. In this paper, we present a formal approach for generating correct smart contracts from B specification that verify safety properties. Our approach consists of two phases: first a smart contract and its properties are specified and verified in B, then a set of rules we defined are applied to generate the correct smart contract code in Solidity. The approach is implemented in a tool that can generate Solidity contract from a proven B project. The whole approach is demonstrated by a case study on the ERC-20 (Ethereum Request for Comments 20) Wrapped Ether (WETH) contract, which is abstractly specified in B, with invariants stating correctness properties, modeled checked with ProB for temporal properties, implemented in B0, proven correct, and automatically translated into a Solidity contract.
KW - B Method
KW - Blockchain
KW - Formal modeling and verification
KW - Refinement
KW - Smart contract
KW - Solidity
UR - https://www.scopus.com/pages/publications/85206193615
U2 - 10.1007/978-3-031-66456-4_9
DO - 10.1007/978-3-031-66456-4_9
M3 - Conference contribution
AN - SCOPUS:85206193615
SN - 9783031664557
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 159
EP - 178
BT - Engineering of Complex Computer Systems - 28th International Conference, ICECCS 2024, Proceedings
A2 - Bai, Guangdong
A2 - Ishikawa, Fuyuki
A2 - Ait-Ameur, Yamine
A2 - Papadopoulos, George A.
PB - Springer Science and Business Media Deutschland GmbH
T2 - 28th International Conference on Engineering of Complex Computer Systems, ICECCS 2024
Y2 - 19 June 2024 through 21 June 2024
ER -