Abstract
A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them.
This tool paper describes our type-based static verification tool Helmholtz for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. Helmholtz is designed on top of our extension of Michelson’s type system with refinement types. Helmholtz takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. Helmholtz successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.
A. Kawata—Current affiliation: Preferred Networks, Inc.
Chapter PDF
Similar content being viewed by others
References
Michelson: the language of smart contracts in Tezos. https://tezos.gitlab.io/whitedoc/michelson.html, retrieved Oct. 14, 2020.
Benton, N.: A Typed, Compositional Logic for a Stack-Based Abstract Machine. In: Proceedings of Asian Sympoisum on Programming Languages and Systems (APLAS). pp. 364–380. Springer Berlin Heidelberg (2005). https://doi.org/10.1007/11575467_24
Bernardo, B., Cauderlier, R., Hu, Z., Pesin, B., Tesson, J.: Mi-Cho-Coq, a framework for certifying Tezos smart contracts. In: Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I. Lecture Notes in Computer Science, vol. 12232, pp. 368–379. Springer (2019). https://doi.org/10.1007/978-3-030-54994-7_28
Goodman, L.: Tezos — a self-amending crypto-ledger. white paper. https://tezos.com/static/white_paper-2dc8c02267a8fb86bd67a108199441bf.pdf (2014), retrieved Oct. 14, 2020.
Grossman, S., Abraham, I., Golan-Gueta, G., Michalevsky, Y., Rinetzky, N., Sagiv, M., Zohar, Y.: Online detection of effectively callback free objects with applications to smart contracts. Proc. ACM Program. Lang. 2(POPL) (Dec 2017). https://doi.org/10.1145/3158136
Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B., Park, D., Zhang, Y., Stefanescu, A., Rosu, G.: KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF). pp. 204–217 (Jul 2018). https://doi.org/10.1109/CSF.2018.00022
Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: Financial Cryptography and Data Security. pp. 520–535. Springer International Publishing (2017)
Honda, K., Yoshida, N.: A compositional logic for polymorphic higher-order functions. In: Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 24-26 August 2004, Verona, Italy. pp. 191–202. ACM (2004). https://doi.org/10.1145/1013963.1013985
Kawaguchi, M., Rondon, P.M., Jhala, R.: Type-based data structure verification. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15-21, 2009. pp. 304–315. ACM (2009). https://doi.org/10.1145/1542476.1542510
Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011,San Jose, CA, USA, June 4-8, 2011. pp. 222–233 (2011). https://doi.org/10.1145/1993498.1993525
de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. pp. 337–340 (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system. https://bitcoin.org/bitcoin.pdf (2008), retrieved Oct. 12, 2020.
Owens, S., Böhm, P., Zappa Nardelli, F., Sewell, P.: Lem: A lightweight tool for heavyweight semantics. In: Interactive Theorem Proving. pp. 363–369. Springer Berlin Heidelberg (2011)
Park, D., Zhang, Y., Saxena, M., Daian, P., Roşu, G.: A formal verification tool for Ethereum VM bytecode. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. pp. 912–915. ACM (Oct 2018). https://doi.org/10.1145/3236024.3264591
Pierce, B.C.: Types and Programming Languages. MIT Press (2002)
Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008. pp. 159–169 (2008). https://doi.org/10.1145/1375581.1375602
Roşu, G., Şerbănută, T.F.: An overview of the K semantic framework. The Journal of Logic and Algebraic Programming 79(6), 397–434 ( 2010). https://doi.org/10.1016/j.jlap.2010.03.012
Siegel, D.: Understanding the DAO attack. CoinDesk (2016), https://www.coindesk.com/understanding-dao-hack-journalists, retrieved Oct. 13, 2020.
Szabo, N.: Formalizing and securing relationships on public networks. First Monday 2(9) (Sep 1997). https://doi.org/10.5210/fm.v2i9.548
Terauchi, T.: Dependent types from counterexamples. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. pp. 119–130 (2010). https://doi.org/10.1145/1706299.1706315
The Coq development team: The coq proof assistant reference manual (2020), http://coq.inria.fr, version 8.12.0
Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal. pp. 277–288 (2009). https://doi.org/10.1145/1599410.1599445
Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Jones, S.L.P.: Refinement types for Haskell. In: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014. pp. 269–282. ACM (2014). https://doi.org/10.1145/2628136.2628161
Xi, H.: Dependent ML an approach to practical programming with dependent types. J. Funct. Program. 17(2), 215–286 (2007). https://doi.org/10.1017/S0956796806006216
Xi, H., Harper, R.: A dependently typed assembly language. In: Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP ’01), Firenze (Florence), Italy, September 3-5, 2001. pp. 169–180. ACM (2001). https://doi.org/10.1145/507635.507657
Zhu, H., Jagannathan, S.: Compositional and lightweight dependent type inference for ML. In: Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings. pp. 295–314 (2013). https://doi.org/10.1007/978-3-642-35873-9_19
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Nishida, Y. et al. (2021). Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types. In: Groote, J.F., Larsen, K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science(), vol 12652. Springer, Cham. https://doi.org/10.1007/978-3-030-72013-1_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-72013-1_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72012-4
Online ISBN: 978-3-030-72013-1
eBook Packages: Computer ScienceComputer Science (R0)