Smart contracts are computer code that runs in blockchain and expresses the rules of an agreement among parties. A bug in their code has major consequences, such as rule violations and security attacks. Smart contracts are immutable and cannot be easily replaced to patch a bug. To overcome these problems, there exist automatic static analyzers that find bugs before smart contracts are installed in blockchain. However, this off-chain verification is optional: programmers are not forced to use it. This paper defines on-chain verification instead, that occurs inside the same blockchain nodes, when the code of smart contracts is installed. It acts as a mandatory entry filter that bans code that does not abide to the verification rules, that are consequently part of the consensus rules of the blockchain. Thus, an improvement in on-chain verification entails a consensus update of the network. This paper provides an implementation of on-chain verification for smart contracts written in the Takamaka subset of Java, running as a Tendermint application. It shows that on-chain verification works, reporting actual experiments.

On-Chain Smart Contract Verification over Tendermint

Olivieri, Luca;Spoto, Fausto;Tagliaferro, Fabio
2021-01-01

Abstract

Smart contracts are computer code that runs in blockchain and expresses the rules of an agreement among parties. A bug in their code has major consequences, such as rule violations and security attacks. Smart contracts are immutable and cannot be easily replaced to patch a bug. To overcome these problems, there exist automatic static analyzers that find bugs before smart contracts are installed in blockchain. However, this off-chain verification is optional: programmers are not forced to use it. This paper defines on-chain verification instead, that occurs inside the same blockchain nodes, when the code of smart contracts is installed. It acts as a mandatory entry filter that bans code that does not abide to the verification rules, that are consequently part of the consensus rules of the blockchain. Thus, an improvement in on-chain verification entails a consensus update of the network. This paper provides an implementation of on-chain verification for smart contracts written in the Takamaka subset of Java, running as a Tendermint application. It shows that on-chain verification works, reporting actual experiments.
2021
978-3-662-63957-3
smart contract, software verification, program analysis, blockchain, tendermint
File in questo prodotto:
File Dimensione Formato  
on-chain_verification_smart_contracts.pdf

accesso aperto

Descrizione: Post-print article - On-Chain Smart Contract Verification over Tendermint
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 518.05 kB
Formato Adobe PDF
518.05 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/1049103
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact