Advertisement

VeriSolid: Correct-by-Design Smart Contracts for Ethereum

  • Anastasia Mavridou
  • Aron LaszkaEmail author
  • Emmanouela Stachtiari
  • Abhishek Dubey
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11598)

Abstract

The adoption of blockchain based distributed ledgers is growing fast due to their ability to provide reliability, integrity, and auditability without trusted entities. One of the key capabilities of these emerging platforms is the ability to create self-enforcing smart contracts. However, the development of smart contracts has proven to be error-prone in practice, and as a result, contracts deployed on public platforms are often riddled with security vulnerabilities. This issue is exacerbated by the design of these platforms, which forbids updating contract code and rolling back malicious transactions. In light of this, it is crucial to ensure that a smart contract is secure before deploying it and trusting it with significant amounts of cryptocurrency. To this end, we introduce the VeriSolid framework for the formal verification of contracts that are specified using a transition-system based model with rigorous operational semantics. Our model-based approach allows developers to reason about and verify contract behavior at a high level of abstraction. VeriSolid allows the generation of Solidity code from the verified models, which enables the correct-by-design development of smart contracts.

References

  1. 1.
    Albert, E., Gordillo, P., Livshits, B., Rubio, A., Sergey, I.: EthIR: a framework for high-level analysis of Ethereum bytecode. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 513–520. Springer, Cham (2018).  https://doi.org/10.1007/978-3-030-01090-4_30CrossRefGoogle Scholar
  2. 2.
    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_8CrossRefGoogle Scholar
  3. 3.
    Atzei, N., Bartoletti, M., Lande, S., Zunino, R.: A formal model of Bitcoin transactions. In: Meiklejohn, S., Sako, K. (eds.) FC 2018. LNCS, vol. 10957. Springer, Berlin (2018).  https://doi.org/10.1007/978-3-662-58387-6_29CrossRefGoogle Scholar
  4. 4.
    Bartoletti, M., Pompianu, L.: An empirical analysis of smart contracts: platforms, applications, and design patterns. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 494–509. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-70278-0_31CrossRefGoogle Scholar
  5. 5.
    Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41–48 (2011)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Bhargavan, K., et al.: Short paper: formal verification of smart contracts. In: Proceedings of the 11th ACM Workshop on Programming Languages and Analysis for Security (PLAS), in Conjunction with ACM CCS 2016, pp. 91–96, October 2016Google Scholar
  7. 7.
    Bliudze, S., et al.: Formal verification of infinite-state BIP models. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 326–343. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-24953-7_25CrossRefGoogle Scholar
  8. 8.
    Brent, L., et al.: Vandal: a scalable security analysis framework for smart contracts. arXiv preprint arXiv:1809.03981 (2018)
  9. 9.
    Christidis, K., Devetsikiotis, M.: Blockchains and smart contracts for the Internet of Things. IEEE Access 4, 2292–2303 (2016)CrossRefGoogle Scholar
  10. 10.
    Clack, C.D., Bakshi, V.A., Braine, L.: Smart contract templates: foundations, design landscape and research directions. arXiv preprint arXiv:1608.00771 (2016)
  11. 11.
    Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)CrossRefGoogle Scholar
  12. 12.
    Colombo, C., Ellul, J., Pace, G.J.: Contracts over smart contracts: recovering from violations dynamically. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 300–315. Springer, Cham (2018).  https://doi.org/10.1007/978-3-030-03427-6_23CrossRefGoogle Scholar
  13. 13.
    Ellul, J., Pace, G.: Runtime verification of Ethereum smart contracts. In: Workshop on Blockchain Dependability (WBD), in Conjunction with 14th European Dependable Computing Conference (EDCC) (2018)Google Scholar
  14. 14.
    Finley, K.: A \$50 million hack just showed that the DAO was all too human. Wired. https://www.wired.com/2016/06/50-million-hack-just-showed-dao-human/ (2016)
  15. 15.
    Frantz, C.K., Nowostawski, M.: From institutions to code: towards automated generation of smart contracts. In: 1st IEEE International Workshops on Foundations and Applications of Self* Systems (FAS*W), pp. 210–215. IEEE (2016)Google Scholar
  16. 16.
    Fröwis, M., Böhme, R.: In code we trust? In: Garcia-Alfaro, J., Navarro-Arribas, G., Hartenstein, H., Herrera-Joancomartí, J. (eds.) ESORICS/DPM/CBT -2017. LNCS, vol. 10436, pp. 357–372. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-67816-0_20CrossRefGoogle Scholar
  17. 17.
    Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of Ethereum smart contracts. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243–269. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89722-6_10CrossRefGoogle Scholar
  18. 18.
    Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of Ethereum smart contracts. Technical report, TU Wien (2018)Google Scholar
  19. 19.
    Hildenbrandt, E., et al.: KEVM: a complete semantics of the Ethereum virtual machine. Technical report, UIUC (2017)Google Scholar
  20. 20.
    Hirai, Y.: Formal verification of deed contract in Ethereum name service, November 2016. https://yoichihirai.com/deed.pdf
  21. 21.
    Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520–535. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-70278-0_33CrossRefGoogle Scholar
  22. 22.
    Hu, J., Zhong, Y.: A method of logic-based smart contracts for blockchain system. In: Proceedings of the 4th International Conference on Data Processing and Applications (ICPDA), pp. 58–61. ACM (2018)Google Scholar
  23. 23.
    Jeffrey, D.U.: Principles of Database and Knowledge-base Systems. Computer Science Press, New york (1989)Google Scholar
  24. 24.
    Jiao, J., Kan, S., Lin, S.W., Sanan, D., Liu, Y., Sun, J.: Executable operational semantics of Solidity. arXiv preprint arXiv:1804.01295 (2018)
  25. 25.
    Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 23rd ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 254–269. ACM, October 2016Google Scholar
  26. 26.
    Maróti, M., et al.: Next generation (meta) modeling: web-and cloud-based collaborative tool infrastructure. In: Proceedings of the MPM@ MoDELS, pp. 41–60 (2014)Google Scholar
  27. 27.
    Mavridou, A., Laszka, A.: Designing secure Ethereum smart contracts: a finite state machine based approach. In: Meiklejohn, S., Sako, K. (eds.) FC 2018. LNCS, vol. 10957. Springer, Berlin (2018).  https://doi.org/10.1007/978-3-662-58387-6_28CrossRefGoogle Scholar
  28. 28.
    Mavridou, A., Laszka, A.: Tool demonstration: FSolidM for designing secure ethereum smart contracts. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 270–277. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89722-6_11CrossRefGoogle Scholar
  29. 29.
    Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: Verisolid: correct-by-design smart contracts for Ethereum. arXiv preprint arXiv:1901.01292 (2019). https://arxiv.org/pdf/1901.01292.pdf
  30. 30.
    Milner, R.: Communication and Concurrency, vol. 84. Prentice Hall, New York (1989)zbMATHGoogle Scholar
  31. 31.
    Mueller, B.: Smashing Ethereum smart contracts for fun and real profit. In: 9th Annual HITB Security Conference (HITBSecConf) (2018)Google Scholar
  32. 32.
    Newman, L.H.: Security news this week: \$280m worth of Ethereum is trapped thanks to a dumb bug. Wired, November 2017. https://www.wired.com/story/280m-worth-of-ethereum-is-trapped-for-a-pretty-dumb-reason/
  33. 33.
    Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: 34th Annual Computer Security Applications Conference (ACSAC) (2018)Google Scholar
  34. 34.
    Noureddine, M., Jaber, M., Bliudze, S., Zaraket, F.A.: Reduction and abstraction techniques for BIP. In: Lanese, I., Madelaine, E. (eds.) FACS 2014. LNCS, vol. 8997, pp. 288–305. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-15317-9_18CrossRefGoogle Scholar
  35. 35.
    O’Connor, R.: Simplicity: a new language for blockchains. In: Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, PLAS 2017, pp. 107–120. ACM, New York (2017).  https://doi.org/10.1145/3139337.3139340
  36. 36.
    Parizi, R.M., Dehghantanha, A., Choo, K.K.R., Singh, A.: Empirical vulnerability analysis of automated smart contracts security testing on blockchains. In: 28th Annual International Conference on Computer Science and Software Engineering (CASCON) (2018)Google Scholar
  37. 37.
    Plotkin, G.D.: A structural approach to operational semantics. Computer Science Department, Aarhus University, Denmark (1981)Google Scholar
  38. 38.
    Solidity by example: blind auction (2018). https://solidity.readthedocs.io/en/develop/solidity-by-example.html#blind-auction. Accessed 25 Sept 2018
  39. 39.
    Solidity documentation: common patterns (2018). http://solidity.readthedocs.io/en/develop/common-patterns.html#state-machine. Accessed 25 Sept 2018
  40. 40.
    Solidity documentation: security considerations - use the checks-effects-interactions pattern (2018). http://solidity.readthedocs.io/en/develop/security-considerations.html#use-the-checks-effects-interactions-pattern. Accessed 25 Sept 2018
  41. 41.
    Stortz, R.: Rattle - an Ethereum EVM binary analysis framework. In: REcon, Montreal (2018)Google Scholar
  42. 42.
    Tsankov, P., Dan, A., Cohen, D.D., Gervais, A., Buenzli, F., Vechev, M.: Securify: practical security analysis of smart contracts. In: 25th ACM Conference on Computer and Communications Security (CCS) (2018)Google Scholar
  43. 43.
    Underwood, S.: Blockchain beyond Bitcoin. Commun. ACM 59(11), 15–17 (2016)CrossRefGoogle Scholar
  44. 44.
    Wöhrer, M., Zdun, U.: Design patterns for smart contracts in the Ethereum ecosystem. In: Proceedings of the 2018 IEEE Conference on Blockchain, pp. 1513–1520 (2018)Google Scholar
  45. 45.
    Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. Technical report, EIP-150, Ethereum Project - Yellow Paper, April 2014Google Scholar
  46. 46.
    Yang, Z., Lei, H.: Lolisa: formal syntax and semantics for a subset of the solidity programming language. arXiv preprint arXiv:1803.09885 (2018)

Copyright information

© International Financial Cryptography Association 2019

Authors and Affiliations

  • Anastasia Mavridou
    • 1
  • Aron Laszka
    • 2
    Email author
  • Emmanouela Stachtiari
    • 3
  • Abhishek Dubey
    • 1
  1. 1.Vanderbilt UniversityNashvilleUSA
  2. 2.University of HoustonHoustonUSA
  3. 3.Aristotle University of ThessalonikiThessalonikiGreece

Personalised recommendations