Document Open Access Logo

Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts

Authors Stian Lybech , Daniele Gorla , Luca Aceto

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2026.19.pdf
  • Filesize: 1.02 MB
  • 29 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Security and privacy → Information flow control
Keywords
  • semantic typing
  • smart contracts
  • information flow control
  • non-interference

Metrics

Abstract

This paper develops semantic typing in a smart-contract setting to ensure type safety of code that uses statically untypable language constructs, such as the fallback function. The idea is that the creator of a contract on the blockchain equips code containing such constructs with a formal proof of its type safety, given in terms of the semantics of types. Then, a user of the contract only needs to check the validity of the provided "proof certificate" of type safety. This is a form of proof-carrying code, which naturally fits with the immutable nature of the blockchain environment. As a concrete application of our approach, we focus on ensuring information flow control and non-interference for TinySol, a distilled version of the Solidity language, through security types. We provide the semantics of types in terms of a typed operational semantics of TinySol and we express the proofs of safety as coinductively-defined typing interpretations, which can be represented compactly via up-to techniques, similar to those used for bisimilarity. We also show how our machinery can be used to type the typical pointer-to-implementation pattern based on the fallback function and to reject a distilled version of the infamous Parity Multisig Wallet Attack.

Cite As Get BibTex

Stian Lybech, Daniele Gorla, and Luca Aceto. Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 19:1-19:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ECOOP.2026.19

Author Details

Stian Lybech
  • Reykjavík University, Iceland
  • University of Southern Denmark (SDU), Odense, Denmark
Daniele Gorla
  • Sapienza, Università di Roma, Italy
Luca Aceto
  • Reykjavík University, Iceland
  • Gran Sasso Science Institute, L'Aquila, Italy

Funding

  • Lybech, Stian: Supported by the Icelandic Research Fund Grant No. 218202-05(1-3), the Department of Computer Science at Reykjavik University, and by the Software Engineering section at University of Southern Denmark.
  • Aceto, Luca: Supported by the Icelandic Research Fund Grant No. 218202-05(1-3).

References

  1. Luca Aceto, Daniele Gorla, and Stian Lybech. A sound type system for secure currency flow, 2024. An extended abstract appeared in the Proc. of ECOOP 2024 (https://doi.org/10.4230/LIPIcs.ECOOP.2024.1). URL: https://doi.org/10.48550/arXiv.2405.12976.
  2. Luca Aceto, Daniele Gorla, Stian Lybech, and Mohammad Hamdaqa. Preventing out-of-gas exceptions by typing. In Leveraging Applications of Formal Methods, Verification and Validation, pages 409-426. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-73709-1_25.
  3. Amal Jamil Ahmed. Semantics of Types for Mutable State. PhD thesis, Princeton University, 2004. URL: http://www.ccs.neu.edu/home/amal/ahmedsthesis.pdf.
  4. Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657-683, September 2001. URL: https://doi.org/10.1145/504709.504712.
  5. Musard Balliu. Logics for Information Flow Security:From Specification to Verification. PhD thesis, Royal Institute of Technology, Stockholm, Sweden, 2014. URL: https://nbn-resolving.org/urn:nbn:se:kth:diva-150423.
  6. Massimo Bartoletti, Letterio Galletta, and Maurizio Murgia. A minimal core calculus for solidity contracts. In Data Privacy Management, Cryptocurrencies and Blockchain Technology, pages 233-243. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31500-9_15.
  7. Lennart Beringer and Martin Hofmann. Secure information flow and program logics. In 20th IEEE Computer Security Foundations Symposium, CSF 2007, pages 233-248. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/CSF.2007.30.
  8. Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, and Dusko Pavlovic. Sound up-to techniques and complete abstract domains. In Proc. of LICS, pages 175-184. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209169.
  9. Filippo Bonchi, Barbara König, and Sebastian Küpper. Up-to techniques for weighted systems. In Proc. of TACAS, volume 10205 of LNCS, pages 535-552, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_31.
  10. Luis Caires. Behavioral and spatial observations in a logic for the pi-calculus. In Foundations of Software Science and Computation Structures, pages 72-89. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24727-2_7.
  11. Luis Caires. Logical semantics of types for concurrency. In Algebra and Coalgebra in Computer Science, pages 16-35. Springer, August 2007. URL: https://doi.org/10.1007/978-3-540-73859-6_2.
  12. Luis Caires and Luca Cardelli. A spatial logic for concurrency (part I). Information and Computation, 186(2):194-235, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00137-8.
  13. Luis Caires and Luca Cardelli. A spatial logic for concurrency (part II). Theoretical Computer Science, 322(3):517-565, 2004. URL: https://doi.org/10.1016/j.tcs.2003.10.041.
  14. Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek. Gradual typing: a new perspective. Proc. ACM Program. Lang., 3(POPL):16:1-16:32, 2019. URL: https://doi.org/10.1145/3290329.
  15. Konstantinos Chatzikokolakis, Catuscia Palamidessi, and Valeria Vignudelli. Up-to techniques for generalized bisimulation metrics. In Prod. of CONCUR, volume 59 of LIPIcs, pages 35:1-35:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.35.
  16. R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Inc., USA, 1986. Google Scholar
  17. Nils Anders Danielsson. Up-to techniques using sized types. Proc. ACM Program. Lang., 2(POPL):43:1-43:28, 2018. URL: https://doi.org/10.1145/3158131.
  18. Farzaneh Derakhshan, Stephanie Balzer, and Limin Jia. Session logical relations for noninterference. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-14, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470654.
  19. Thomas Dickerson, Paul Gazzillo, Maurice Herlihy, Vikram Saraph, and Eric Koskinen. Proof-carrying smart contracts. In Financial Cryptography and Data Security: FC 2018 International Workshops, BITCOIN, VOTING, and WTSC, Nieuwpoort, Curaçao, March 2, 2018, Revised Selected Papers, pages 325-338, Berlin, Heidelberg, 2018. Springer-Verlag. URL: https://doi.org/10.1007/978-3-662-58820-8_22.
  20. Ethereum Foundation. Solidity documentation. https://docs.soliditylang.org/, 2022. Accessed: 2025-07-01.
  21. Dan Frumin, Robbert Krebbers, and Lars Birkedal. Compositional non-interference for fine-grained concurrent programs. In 42nd IEEE Symposium on Security and Privacy, SP 2021, pages 1416-1433. IEEE, 2021. URL: https://doi.org/10.1109/SP40001.2021.00003.
  22. J. A. Goguen and J. Meseguer. Security policies and security models. In 1982 IEEE Symposium on Security and Privacy, pages 11-20, 1982. URL: https://doi.org/10.1109/SP.1982.10014.
  23. Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal. Mechanized logical relations for termination-insensitive noninterference. Proc. ACM Program. Lang., 5(POPL):1-29, 2021. URL: https://doi.org/10.1145/3434291.
  24. 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. URL: https://doi.org/10.1007/978-3-319-89722-6_10.
  25. Xinwen Hu, Yi Zhuang, Shang-Wei Lin, Fuyuan Zhang, Shuanglong Kan, and Zining Cao. A security type verifier for smart contracts. Computers & Security, 108:102343, 2021. URL: https://doi.org/10.1016/j.cose.2021.102343.
  26. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. Rustbelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang., 2(POPL), 2017. URL: https://doi.org/10.1145/3158154.
  27. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28:e20, 2018. URL: https://doi.org/10.1017/S0956796818000151.
  28. Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. The essence of higher-order concurrent separation logic. In Proc. of ESOP, pages 696-723. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_26.
  29. Stian Lybech, Daniele Gorla, and Luca Aceto. Typing fallback functions: A semantic approach to type safe smart contracts, 2025. URL: https://doi.org/10.48550/arXiv.2512.04755.
  30. Adrian Manning. Solidity security: A comprehensive list of known attack vectors and common anti-patterns, 2018. URL: https://blog.sigmaprime.io/solidity-security.html.
  31. Per Martin-Löf. Constructive mathematics and computer programming. In L. Jonathan Cohen, Jerzy Łoś, Helmut Pfeiffer, and Klaus-Peter Podewski, editors, Logic, Methodology and Philosophy of Science VI, volume 104 of Studies in Logic and the Foundations of Mathematics, pages 153-175. Elsevier, 1982. URL: https://doi.org/10.1016/S0049-237X(09)70189-2.
  32. Robin Milner. Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, 1989. Google Scholar
  33. Robin Milner. The polyadic pi-calculus: a tutorial. In Logic and Algebra of Specification, pages 203-246. Springer Berlin Heidelberg, 1993. URL: https://doi.org/10.1007/978-3-642-58041-3_6.
  34. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, i. Information and Computation, 100(1):1-40, 1992. URL: https://doi.org/10.1016/0890-5401(92)90008-4.
  35. George C. Necula. Proof-carrying code. In Proc. of POPL, pages 106-119. ACM, 1997. URL: https://doi.org/10.1145/263699.263712.
  36. 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.
  37. Joachim Parrow. An introduction to the pi-calculus. In Handbook of Process Algebra, pages 479-543. Elsevier, 2001. URL: https://doi.org/10.1016/B978-044482830-9/50026-6.
  38. Gordon Plotkin. Lambda-definability and logical relations, 1973. URL: https://www.cl.cam.ac.uk/~nk480/plotkin-logical-relations.pdf.
  39. Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan Rutten, editors, Advanced Topics in Bisimulation and Coinduction, Cambridge Tracts in Theoretical Computer Science, pages 233-289. Cambridge University Press, 2011. URL: https://doi.org/10.1017/cbo9780511792588.007.
  40. Ilham Ahmed Qasse. Immutable Yet Mutable: Empirical Studies in Smart Contract Upgradeability. PhD thesis, Reykjavík University, December 2024. URL: https://iris.landsbokasafn.is/en/publications/immutable-yet-mutable-empirical-studies-in-smart-contract-upgrade.
  41. Vineet Rajani and Deepak Garg. On the expressiveness and semantics of information flow types. J. Comput. Secur., 28(1):129-156, 2020. An extended abstract appeared in IEEE CSF 2018. URL: https://doi.org/10.3233/JCS-191382.
  42. Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011. URL: https://doi.org/10.1017/CBO9780511777110.
  43. Davide Sangiorgi and Robin Milner. The problem of "weak bisimulation up to"'. In Rance Cleaveland, editor, CONCUR '92, Third International Conference on Concurrency Theory, volume 630 of Lecture Notes in Computer Science, pages 32-46. Springer, 1992. URL: https://doi.org/10.1007/BFb0084781.
  44. Davide Sangiorgi and Valeria Vignudelli. Environmental bisimulations for probabilistic higher-order languages. ACM Trans. Program. Lang. Syst., 41(4):22:1-22:64, 2019. URL: https://doi.org/10.1145/3350618.
  45. Davide Sangiorgi and David Walker. The pi-calculus: a Theory of Mobile Processes. Cambridge University Press, 2003. URL: https://doi.org/10.1017/9781316134924.
  46. Jeremy G. Siek and Walid Taha. Gradual typing for objects. In Proc. of ECOOP, volume 4609 of LNCS, pages 2-27. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73589-2_2.
  47. Matvey Soloviev, Musard Balliu, and Roberto Guanciale. Security properties through the lens of modal logic. In 37th IEEE Computer Security Foundations Symposium, CSF 2024, pages 340-355. IEEE, 2024. URL: https://doi.org/10.1109/CSF61375.2024.00009.
  48. William W. Tait. Intensional interpretations of functionals of finite type I. J. Symb. Log., 32(2):198-212, 1967. URL: https://doi.org/10.2307/2271658.
  49. Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. A logical approach to type soundness. Journal of the ACM, 71(6), 2024. URL: https://doi.org/10.1145/3676954.
  50. Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. 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.
  51. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38-94, 1994. URL: https://doi.org/10.1006/inco.1994.1093.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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