Abstract
In this paper, we use a formal tool that performs deductive verification on industrial smart contracts, which are self-executing digital programs. Because smart contracts manipulate cryptocurrency and transaction information, if a bug occurs in such programs, serious consequences can happen, such as a loss of money. This paper aims to show that a language dedicated to deductive verification, called WhyML, can be a suitable language to write correct and proven contracts. We first encode existing contracts, using the Why3 tool, into WhyML program; next, we formulate specifications to be proven as the absence of RunTime Error and functional properties, then we verify the behaviour of the program using the Why3 system. Finally, we compile the WhyML contracts to the Ethereum Virtual Machine (EVM). Moreover, our approach estimates the cost of gas, which is a unit that measures the amount of computational effort during a transaction.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
Ethereum foundation: Solidity, the contract-oriented programming language. https://github.com/ethereum/solidity.
- 3.
- 4.
- 5.
The implementation can be found at http://francois.bobot.eu/fmbc2019/.
- 6.
References
Ethereum foundation: Ethereum and oracles. https://blog.ethereum.org/2014/07/22/ethereum-and-oracles/
Formal verification for solidity contracts. https://forum.ethereum.org/discussion/3779/formal-verification-for-solidity-contracts
Solidity hacks and vulnerabilities. https://hackernoon.com/hackpedia-16-solidity-hacks-vulnerabilities-their-fixes-and-real-world-examples-f3210eba5148
Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M.: Deductive software verification-the key book, vol. 10001. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49812-6
Ahrendt, W., et al.: Verification of smart contract business logic. In: Hojjat, H., Massink, M. (eds.) FSEN 2019. LNCS, vol. 11761, pp. 228–243. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31517-7_16
Amadio, R.M., et al.: Certified complexity (CerCo). In: Dal Lago, U., Peña, R. (eds.) FOPARA 2013. LNCS, vol. 8552, pp. 1–18. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12466-7_1
Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164–186. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54455-6_8
Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14
Bhargavan, K., et al.: Short paper: formal verification of smart contracts (2016)
Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Lescuyer, S., Mebsout, A.: The alt-ergo automated theorem prover (2008). http://alt-ergo.lri.fr/
Domowitz, I.: A taxonomy of automated trade execution systems. J. Int. Money Finance 12, 607–631 (1993)
Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8
Goodman, L.: Tezos: a self-amending crypto-ledger position paper (2014)
Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 254–269. ACM (2016)
de Moura, L., Bjørner, N.: Z3, an efficient SMT solver. http://research.microsoft.com/projects/z3/
Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008)
Nehaï, Z., Bobot, F.: Deductive Proof of Ethereum Smart Contracts Using Why3. Research report, CEA DILS, April 2019. https://hal.archives-ouvertes.fr/hal-02108987
Nehaï, Z., Piriou, P.Y., Daumas, F.: Model-checking of smart contracts. In: The 2018 IEEE International Conference on Blockchain. IEEE (2018)
Sánchez, D.C.: Raziel: Private and verifiable smart contracts on blockchains. Cryptology ePrint Archive, Report 2017/878 (2017). http://eprint.iacr.org/2017/878.pdf. Accessed 26 Sept 2017
Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. Ethereum Proj. Yellow Pap. 151, 1–32 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Nehaï, Z., Bobot, F. (2020). Deductive Proof of Industrial Smart Contracts Using Why3. In: Sekerinski, E., et al. Formal Methods. FM 2019 International Workshops. FM 2019. Lecture Notes in Computer Science(), vol 12232. Springer, Cham. https://doi.org/10.1007/978-3-030-54994-7_22
Download citation
DOI: https://doi.org/10.1007/978-3-030-54994-7_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-54993-0
Online ISBN: 978-3-030-54994-7
eBook Packages: Computer ScienceComputer Science (R0)