Model-Based Static and Runtime Verification for Ethereum Smart Contracts. Azzopardi, S., Colombo, C., & Pace, G. In Hammoudi, S., Pires, L., & Selić, B., editors, Model-Driven Engineering and Software Development, pages 323–348, Cham, 2021. Springer International Publishing. abstract bibtex 1 download Distributed ledger technologies, e.g. blockchains, are an innovative solution to the problem of trust between different parties. Smart contracts, programs executing on these ledgers present new challenges given their non-traditional execution context – blockchains. The immutability of smart contracts once they are deployed makes their pre-deployment correctness essential. This can be achieved through verification methods, which attempt to answer conclusively whether the code respects some specification. Another approach is model-driven development, where the specification is used directly to create a correct-by-const-ruction implementation. A specification may however still need to be verified to ensure it satisfies some properties. Verifying properties pre-deployment is ideal, however it may not always be possible to do completely, depending on the complexity of the smart contract. Traditionally upon failure of a verification attempt the only option is to attempt a different verification method. Recent approaches instead enable the transformation of the verification problem into a smaller problem, reducing the load of subsequent verification attempts. We have previously proposed an automata-theoretic approach to reason systematically about this kind of residual analysis for (co-)safety properties, while we have implemented an intraprocedural data-flow approach for Java programs. In this paper we extend our approach for Solidity smart contracts, present a corresponding tool, evaluate the approach with several new case studies, and compare it with existing approaches.
@InProceedings{10.1007/978-3-030-67445-8_14,
author="Azzopardi, Shaun
and Colombo, Christian
and Pace, Gordon",
editor="Hammoudi, Slimane
and Pires, Lu{\'i}s Ferreira
and Seli{\'{c}}, Bran",
title="Model-Based Static and Runtime Verification for Ethereum Smart Contracts",
booktitle="Model-Driven Engineering and Software Development",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="323--348",
abstract="Distributed ledger technologies, e.g. blockchains, are an innovative solution to the problem of trust between different parties. Smart contracts, programs executing on these ledgers present new challenges given their non-traditional execution context -- blockchains. The immutability of smart contracts once they are deployed makes their pre-deployment correctness essential. This can be achieved through verification methods, which attempt to answer conclusively whether the code respects some specification. Another approach is model-driven development, where the specification is used directly to create a correct-by-const-ruction implementation. A specification may however still need to be verified to ensure it satisfies some properties. Verifying properties pre-deployment is ideal, however it may not always be possible to do completely, depending on the complexity of the smart contract. Traditionally upon failure of a verification attempt the only option is to attempt a different verification method. Recent approaches instead enable the transformation of the verification problem into a smaller problem, reducing the load of subsequent verification attempts. We have previously proposed an automata-theoretic approach to reason systematically about this kind of residual analysis for (co-)safety properties, while we have implemented an intraprocedural data-flow approach for Java programs. In this paper we extend our approach for Solidity smart contracts, present a corresponding tool, evaluate the approach with several new case studies, and compare it with existing approaches.",
isbn="978-3-030-67445-8"
}
Downloads: 1
{"_id":"LReqAZywWP2zhkZwR","bibbaseid":"azzopardi-colombo-pace-modelbasedstaticandruntimeverificationforethereumsmartcontracts-2021","authorIDs":["8sEvMX4Nga4Xz4o3t"],"author_short":["Azzopardi, S.","Colombo, C.","Pace, G."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Azzopardi"],"firstnames":["Shaun"],"suffixes":[]},{"propositions":[],"lastnames":["Colombo"],"firstnames":["Christian"],"suffixes":[]},{"propositions":[],"lastnames":["Pace"],"firstnames":["Gordon"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Hammoudi"],"firstnames":["Slimane"],"suffixes":[]},{"propositions":[],"lastnames":["Pires"],"firstnames":["Luís Ferreira"],"suffixes":[]},{"propositions":[],"lastnames":["Selić"],"firstnames":["Bran"],"suffixes":[]}],"title":"Model-Based Static and Runtime Verification for Ethereum Smart Contracts","booktitle":"Model-Driven Engineering and Software Development","year":"2021","publisher":"Springer International Publishing","address":"Cham","pages":"323–348","abstract":"Distributed ledger technologies, e.g. blockchains, are an innovative solution to the problem of trust between different parties. Smart contracts, programs executing on these ledgers present new challenges given their non-traditional execution context – blockchains. The immutability of smart contracts once they are deployed makes their pre-deployment correctness essential. This can be achieved through verification methods, which attempt to answer conclusively whether the code respects some specification. Another approach is model-driven development, where the specification is used directly to create a correct-by-const-ruction implementation. A specification may however still need to be verified to ensure it satisfies some properties. Verifying properties pre-deployment is ideal, however it may not always be possible to do completely, depending on the complexity of the smart contract. Traditionally upon failure of a verification attempt the only option is to attempt a different verification method. Recent approaches instead enable the transformation of the verification problem into a smaller problem, reducing the load of subsequent verification attempts. We have previously proposed an automata-theoretic approach to reason systematically about this kind of residual analysis for (co-)safety properties, while we have implemented an intraprocedural data-flow approach for Java programs. In this paper we extend our approach for Solidity smart contracts, present a corresponding tool, evaluate the approach with several new case studies, and compare it with existing approaches.","isbn":"978-3-030-67445-8","bibtex":"@InProceedings{10.1007/978-3-030-67445-8_14,\n\tauthor=\"Azzopardi, Shaun\n\tand Colombo, Christian\n\tand Pace, Gordon\",\n\teditor=\"Hammoudi, Slimane\n\tand Pires, Lu{\\'i}s Ferreira\n\tand Seli{\\'{c}}, Bran\",\n\ttitle=\"Model-Based Static and Runtime Verification for Ethereum Smart Contracts\",\n\tbooktitle=\"Model-Driven Engineering and Software Development\",\n\tyear=\"2021\",\n\tpublisher=\"Springer International Publishing\",\n\taddress=\"Cham\",\n\tpages=\"323--348\",\n\tabstract=\"Distributed ledger technologies, e.g. blockchains, are an innovative solution to the problem of trust between different parties. Smart contracts, programs executing on these ledgers present new challenges given their non-traditional execution context -- blockchains. The immutability of smart contracts once they are deployed makes their pre-deployment correctness essential. This can be achieved through verification methods, which attempt to answer conclusively whether the code respects some specification. Another approach is model-driven development, where the specification is used directly to create a correct-by-const-ruction implementation. A specification may however still need to be verified to ensure it satisfies some properties. Verifying properties pre-deployment is ideal, however it may not always be possible to do completely, depending on the complexity of the smart contract. Traditionally upon failure of a verification attempt the only option is to attempt a different verification method. Recent approaches instead enable the transformation of the verification problem into a smaller problem, reducing the load of subsequent verification attempts. We have previously proposed an automata-theoretic approach to reason systematically about this kind of residual analysis for (co-)safety properties, while we have implemented an intraprocedural data-flow approach for Java programs. In this paper we extend our approach for Solidity smart contracts, present a corresponding tool, evaluate the approach with several new case studies, and compare it with existing approaches.\",\n\tisbn=\"978-3-030-67445-8\"\n}\n\n\n","author_short":["Azzopardi, S.","Colombo, C.","Pace, G."],"editor_short":["Hammoudi, S.","Pires, L.","Selić, B."],"key":"10.1007/978-3-030-67445-8_14","id":"10.1007/978-3-030-67445-8_14","bibbaseid":"azzopardi-colombo-pace-modelbasedstaticandruntimeverificationforethereumsmartcontracts-2021","role":"author","urls":{},"metadata":{"authorlinks":{"azzopardi, s":"https://shaunazzopardi.github.io/"}},"downloads":1},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/shaunazzopardi/shaunazzopardi.github.io/master/pubs.bib","creationDate":"2021-02-04T13:26:21.992Z","downloads":1,"keywords":[],"search_terms":["model","based","static","runtime","verification","ethereum","smart","contracts","azzopardi","colombo","pace"],"title":"Model-Based Static and Runtime Verification for Ethereum Smart Contracts","year":2021,"dataSources":["mtLriRvYqkiErXwmg"]}