Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Stian Lybech, Daniele Gorla, Luca Aceto

TL;DR

The paper tackles type-safety for smart contracts that use untypable constructs like the fallback function by adopting a semantic typing approach. It develops a TinySol-based framework with security types, a typed operational semantics, and coinductive typing interpretations, augmented by up-to techniques to keep proofs finite and storable on the blockchain. The key contributions include formalizing non-interference within a smart-contract setting, enabling proof-carrying-code certificates for untypable fragments, and demonstrating how pointer-to-implementation patterns can be typed safely. This approach offers a principled path to certifying runtime safety of complex contract interactions while preserving expressiveness for upgradable and reflection-like features on-chain.

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 the language 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 a way for expressing the proofs of safety as coinductively-defined typing interpretations and for representing them 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. However, our main contribution is not the safety theorem per se (and so security properties different from non-interference can be considered as well), but rather the presentation of the theoretical developments necessary to make this approach work in a blockchain/smart-contract setting.

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

TL;DR

The paper tackles type-safety for smart contracts that use untypable constructs like the fallback function by adopting a semantic typing approach. It develops a TinySol-based framework with security types, a typed operational semantics, and coinductive typing interpretations, augmented by up-to techniques to keep proofs finite and storable on the blockchain. The key contributions include formalizing non-interference within a smart-contract setting, enabling proof-carrying-code certificates for untypable fragments, and demonstrating how pointer-to-implementation patterns can be typed safely. This approach offers a principled path to certifying runtime safety of complex contract interactions while preserving expressiveness for upgradable and reflection-like features on-chain.

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 the language 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 a way for expressing the proofs of safety as coinductively-defined typing interpretations and for representing them 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. However, our main contribution is not the safety theorem per se (and so security properties different from non-interference can be considered as well), but rather the presentation of the theoretical developments necessary to make this approach work in a blockchain/smart-contract setting.

Paper Structure

This paper contains 27 sections, 47 theorems, 63 equations, 28 figures.

Table of Contents

  1. Introduction
  2. The TinySol language and its security types
  3. Typed Syntax
  4. Types and Type Environments for Information Flow Control and Non-Interference
  5. Semantic Typing for TinySol
  6. Typed operational semantics
  7. Properties of typed transitions
  8. Typing interpretations and semantic type rules for stacks and commands
  9. Safe and unsafe fallback calls
  10. Variadic arguments
  11. Up-to techniques for semantic typing
  12. A motivating example
  13. Typing interpretations up-to union
  14. Concluding remarks
  15. Data-Availability Statement
  16. ...and 12 more sections

Key Result

proposition 1

Assume $Q$ satisfies that all security levels in $Q$ occur in descending order. For all type environments $\Sigma$, $\Gamma$ and $\Delta$, security levels $s_1 \sqsupseteq s_2 \sqsupseteq \text{\normalfontfst}(Q)$, and environments $\text{\normalfont\sffamily env}_{TSV}$, it holds that, for every $s

Figures (28)

  • Figure 1: The syntax of TinySol.
  • Figure 2: Typed operational semantics of stacks (1).
  • Figure 3: Typed operational semantics of stacks (2): method calls
  • Figure 4: The semantic type rule for fallback function calls.
  • Figure 5: An example of the pointer-to-implementation pattern.
  • ...and 23 more figures

Theorems & Definitions (64)

  • definition 1: Types and environments
  • definition 2: Interface definition language
  • definition 3: Well-formedness of $\Gamma$
  • definition 4: TypeOf
  • proposition 1: Coercion property for stacks
  • definition 5: Construction of $\text{\normalfont\sffamily env}_{SV}$
  • lemma 1: Correctness of the construction
  • corollary 1: Safe state abstraction
  • theorem 1: Runtime preservation
  • theorem 2: Runtime non-interference for stacks
  • ...and 54 more