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.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.