DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2026.19

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

Authors: Stian Lybech, Daniele Gorla, and Luca Aceto

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{lybech_et_al:LIPIcs.ECOOP.2026.19,
  author =	{Lybech, Stian and Gorla, Daniele and Aceto, Luca},
  title =	{{Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{19:1--19:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.19},
  URN =		{urn:nbn:de:0030-drops-261159},
  doi =		{10.4230/LIPIcs.ECOOP.2026.19},
  annote =	{Keywords: semantic typing, smart contracts, information flow control, non-interference}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2024.1

A Sound Type System for Secure Currency Flow

Authors: Luca Aceto, Daniele Gorla, and Stian Lybech

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.ECOOP.2024.1,
  author =	{Aceto, Luca and Gorla, Daniele and Lybech, Stian},
  title =	{{A Sound Type System for Secure Currency Flow}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{1:1--1:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.1},
  URN =		{urn:nbn:de:0030-drops-208508},
  doi =		{10.4230/LIPIcs.ECOOP.2024.1},
  annote =	{Keywords: smart contracts, call integrity, noninterference, type system}
}

Search Results

Documents authored by Lybech, Stian

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

Abstract

Cite as

A Sound Type System for Secure Currency Flow

Abstract

Cite as

Thanks for your feedback!

Could not send message