Join us for a PhD thesis defence of Stian Lybech on his thesis A Type Theoretic Approach to Smart Contract Safety.

Defence committee:

Supervision:

• Main Supervisor: Luca Aceto, Supervisor Professor, Reykjavík University, Iceland
• Co-Supervisor: Mohammad Hamdaqa, Assistant Professor, Polytechnique Montreal, Canada
• External Supervisor: Daniele Gorla,  Associate Professor, Sapienza University of Rome, Italy,

Committee members:

• Ettore Merlo, Professor, Polytechnique Montreal, Canada
• Silvia Crafa, Associate Professor, University of Padova, Italy

Examiners:

• Laura Bocchi, Examiner Reader, University of Kent, UK
• Maurizio Murgia, Assistant Professor, Gran Sasso Science Institute, Italy

Master of ceremony: 

• Henning Arnór Úlfarsson

Abstract:
Type systems are routinely employed in many modern programming languages to statically ensure various notions of runtime safety. We explore issues of typability and notions of safety in two different fields: Firstly, we focus on process calculi with composite channel names, where the type of a channel must somehow be derived from the types of its constituents. This collection of results includes a simple type system for the 𝜌-calculus, along with some results of expressivity w.r.t. the 𝜋-calculus; a generic type system for the Higher-Order Ψ-calculus, extending a similar type system for the ‘first-order’ Ψ-calculus; and a simple type system for 𝑒𝜋, which aims to highlight a connexion to type structures from class-based/object-oriented languages.

Secondly, we focus on the language TinySol, which models core features of the smart-contract language Solidity. Smart contracts are immutable programs with publicly visible code, that run atop a blockchain and are used to manage financial assets of users. Guided by insights from our work in process calculi, we develop type systems for ensuring three different properties: non-interference, call-integrity, and absence of out-of-gas exceptions. 

Lastly, we seek to tackle some of the shortcomings of the conventional, syntactic approach to type soundness, which had become evident in our previous developments. In particular, we study a peculiar construct in Solidity, known as the fallback function, which is untypable by syntactic type rules. Hence, we turn to a semantic approach to type soundness which allows type safety to be shown, even in cases where welltypedness cannot be proved by ordinary syntactic type rules. We use this approach to propose a method by which type safety may be recovered, even for contracts containing fallback functions, by allowing the programmer to supply a manual proof of type-safety for untypable pieces of code. This method does not depend on specific features of the fallback function, or even of TinySol or Solidity, and it may therefore also be developed for other smart-contract languages.