Document Open Access Logo

A Sound Type System for Secure Currency Flow

Authors Luca Aceto , Daniele Gorla , Stian Lybech

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.1.pdf
  • Filesize: 0.97 MB
  • 27 pages

Document Identifiers

Author Details

Luca Aceto
  • Reykjavík University, Iceland
Daniele Gorla
  • Sapienza, Università di Roma, Italy
Stian Lybech
  • Reykjavík University, Iceland

Funding

  • Aceto, Luca: Supported by the Icelandic Research Fund Grant No. 218202-05(1-3).
  • Lybech, Stian: Supported by the Icelandic Research Fund Grant No. 218202-05(1-3).

Acknowledgements

We thank the anonymous reviewers for their constructive attitude and for the fruitful comments that helped us improve our paper. Luca Aceto and Stian Lybech thank Mohammad Hamdaqa for sharing his expertise with them during extensive discussions on safety properties for smart contracts, which helped shape the research agenda for the work reported in this paper.

Cite AsGet BibTex

Luca Aceto, Daniele Gorla, and Stian Lybech. A Sound Type System for Secure Currency Flow. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 1:1-1:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.1

Abstract

In this paper we focus on TinySol, a minimal calculus for Solidity smart contracts, introduced by Bartoletti et al. We start by rephrasing its syntax (to emphasise its object-oriented flavour) and give a new big-step operational semantics. We then use it to define two security properties, namely call integrity and noninterference. These two properties have some similarities in their definition, in that they both require that some part of a program is not influenced by the other part. However, we show that the two properties are actually incomparable. Nevertheless, we provide a type system for noninterference and show that well-typed programs satisfy call integrity as well; hence, programs that are accepted by our type system satisfy both properties. We finally discuss the practical usability of the type system and its limitations by means of some simple examples.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program analysis
  • Theory of computation → Type structures
Keywords
  • smart contracts
  • call integrity
  • noninterference
  • type system

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Luca Aceto, Daniele Gorla, and Stian Lybech. A sound type system for secure currency flow. CoRR, abs/2405.12976, 2024. URL: https://doi.org/10.48550/arXiv.2405.12976.
  2. Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. A survey of attacks on ethereum smart contracts (sok). In Proc. of POST, volume 10204 of LNCS, pages 164-186. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54455-6_8.
  3. Massimo Bartoletti, Letterio Galletta, and Maurizio Murgia. A minimal core calculus for solidity contracts. In Cristina Pérez-Solà, Guillermo Navarro-Arribas, Alex Biryukov, and Joaquin Garcia-Alfaro, editors, Data Privacy Management, Cryptocurrencies and Blockchain Technology, pages 233-243, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-31500-9_15.
  4. Christian Bräm, Marco Eilers, Peter Müller, Robin Sierra, and Alexander J. Summers. Rich specifications for Ethereum smart contract verification. Proc. ACM Program. Lang., 5(OOPSLA):1-30, 2021. URL: https://doi.org/10.1145/3485523.
  5. Franck Cassez, Joanne Fuller, and Aditya Asgaonkar. Formal verification of the Ethereum 2.0 Beacon Chain. In 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 13243 of LNCS, pages 167-182. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_9.
  6. Franck Cassez, Joanne Fuller, and Horacio Mijail Anton Quiles. Deductive verification of smart contracts with Dafny. In 27th International Conference on Formal Methods for Industrial Critical Systems, volume 13487 of LNCS, pages 50-66. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15008-1_5.
  7. Silvia Crafa, Matteo Di Pirro, and Elena Zucca. Is solidity solid enough? In Financial Cryptography Workshops, 2019. Google Scholar
  8. The dao smart contract. http://etherscan.io/address/0xbb9bc244d798123fde783fcc1c72d3bb8c189413#code, 2016.
  9. Josselin Feist, Gustavo Grieco, and Alex Groce. Slither: a static analysis framework for smart contracts. In Proceedings of the 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain, pages 8-15. IEEE / ACM, 2019. URL: https://doi.org/10.1109/WETSEB.2019.00008.
  10. Ethereum Foundation. Solidity documentation. https://docs.soliditylang.org/, 2022. Accessed: 2024-01-15.
  11. Thomas Genet, Thomas P. Jensen, and Justine Sauvage. Termination of Ethereum’s smart contracts. In Proc. of the 17th International Joint Conference on e-Business and Telecommunications - Volume 2: SECRYPT, pages 39-51. ScitePress, 2020. URL: https://doi.org/10.5220/0009564100390051.
  12. J. A. Goguen and J. Meseguer. Security policies and security models. In 1982 IEEE Symposium on Security and Privacy, pages 11-11, 1982. URL: https://doi.org/10.1109/SP.1982.10014.
  13. Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. A semantic framework for the security analysis of ethereum smart contracts. In Lujo Bauer and Ralf Küsters, editors, Principles of Security and Trust, pages 243-269, Cham, 2018. Springer International Publishing. Google Scholar
  14. Xinwen Hu, Yi Zhuang, Shangwei Lin, Fuyuan Zhang, Shuanglong Kan, and Zining Cao. A security type verifier for smart contracts. Comput. Secur., 108:102343, 2021. URL: https://doi.org/10.1016/j.cose.2021.102343.
  15. Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. ZEUS: analyzing safety of smart contracts. In 25th Annual Network and Distributed System Security Symposium. The Internet Society, 2018. URL: https://www.ndss-symposium.org/wp-content/uploads/2018/02/ndss2018_09-1_Kalra_paper.pdf.
  16. Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. Making smart contracts smarter. In Proc. SIGSAC Conf. on Computer and Communications Security, pages 254-269. ACM, 2016. URL: https://doi.org/10.1145/2976749.2978309.
  17. Anastasia Mavridou and Aron Laszka. Designing secure Ethereum smart contracts: A finite state machine based approach. In 22nd Conference on Financial Cryptography and Data Security, volume 10957 of LNCS, pages 523-540. Springer, 2018. URL: https://doi.org/10.1007/978-3-662-58387-6_28.
  18. Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: An Appetizer. Springer-Verlag London, 2007. URL: https://doi.org/10.1007/978-1-84628-692-6.
  19. The parity wallet breach. https://www.coindesk.com/30-million-ether-reported-stolen-parity-wallet-breach/, 2017.
  20. The parity wallet vulnerability. https://paritytech.io/blog/security-alert.html, 2017.
  21. Daejun Park, Yi Zhang, and Grigore Rosu. End-to-end formal verification of Ethereum 2.0 Deposit Smart Contract. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV Proceedings, Part I, volume 12224 of Lecture Notes in Computer Science, pages 151-164. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53288-8_8.
  22. Grigore Rosu and Traian-Florin Serbanuta. An overview of the K semantic framework. J. Log. Algebraic Methods Program., 79(6):397-434, 2010. URL: https://doi.org/10.1016/j.jlap.2010.03.012.
  23. Clara Schneidewind, Ilya Grishchenko, Markus Scherer, and Matteo Maffei. ethor: Practical and provably sound static analysis of ethereum smart contracts. In Proc. of SIGSAC Conf. on Computer and Communications Security, pages 621-640. ACM, 2020. URL: https://doi.org/10.1145/3372297.3417250.
  24. Pablo Lamela Seijas, Simon J. Thompson, and Darryl McAdams. Scripting smart contracts for distributed ledger technology. IACR Cryptol. ePrint Arch., 2016:1156, 2016. Google Scholar
  25. Geoffrey Smith and Dennis M. Volpano. Secure information flow in a multi-threaded imperative language. In Proc. of 25th POPL, pages 355-364. ACM, 1998. Google Scholar
  26. Palina Tolmach, Yi Li, Shang-Wei Lin, Yang Liu, and Zengxiang Li. A survey of smart contract formal specification and verification. ACM Computing Surveys (CSUR), 54(7):148:1-148:38, 2020. URL: https://doi.org/10.1145/3464421.
  27. Petar Tsankov, Andrei Marian Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin T. Vechev. Securify: Practical security analysis of smart contracts. In Proc. of SIGSAC Conference on Computer and Communications Security, pages 67-82. ACM, 2018. URL: https://doi.org/10.1145/3243734.3243780.
  28. Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4, August 2000. URL: https://doi.org/10.3233/JCS-1996-42-304.
  29. Renlord Yang, Toby Murray, Paul Rimba, and Udaya Parampalli. Empirically analyzing Ethereum’s gas mechanism. In Proc. of IEEE European Symposium on Security and Privacy Workshops, pages 310-319. IEEE, 2019. URL: https://doi.org/10.1109/EuroSPW.2019.00041.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact