arXiv subjects

Stian Lybech

Publications and source records attributed to Stian Lybech.

7 recordsLinked to original sources

arXiv2026

Information Flow Control in Off-Chain Components

This paper develops a model of a smart-contract language for a blockchain architecture with off-chain components. Off-chain components are pieces of smart contracts that execute at designated locations outside of the network of blockchain nodes, but remain synchronised with the on-chain contract state. They react to changes to the on-chain state, but may also notify the on-chain component about events in the world, e.g. stock prices, weather data etc., or even act as a bridge between different blockchains. This affords greater flexibility for the developer, but may also enable new vulnerabilities. As a concrete example, we use the model to study the problem of ensuring integrity and secrecy of data between the on-chain and off-chain components, using static information flow control techniques. This fails, even in the absence of a loop construct, because off-chain components act as separate threads and can encode a blocking construct e.g. through recursive method calls. We end the paper with a discussion of possible ways to remedy this situation.

cs.CR↗

arXiv2025

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

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.

cs.PL↗

arXiv2024

Typing Composite Subjects

Many type systems have been presented in the literature for variants of the pi-calculus, but none of them are able to handle composite subjects such as those found in the language epi, which features polyadic synchronisation. The purpose of this paper is to address the question of how to type composite subjects in a general fashion. We assess the validity of our proposal by first proving the standard correctness results for a type system (i.e., subject reduction and type safety). Then, we follow the path opened by Sangiorgi in 1998 and show an encoding in epi of a minimal OO language called WC (While with \Classes) whose ``expectable'' type system exactly corresponds to the one induced by ours via the encoding. This comparison contributes to understanding the relationship between our types and conventional types for OO languages.

cs.PL↗

arXiv2024

Preventing Out-of-Gas Exceptions by Typing

We continue the development of TinySol, a minimal object-oriented language based on Solidity, the standard smart-contract language used for the Ethereum platform. We first extend TinySol with exceptions and a gas mechanism, and equip it with a small-step operational semantics. Introducing the gas mechanism is fundamental for modelling real-life smart contracts in TinySol, since this is the way in which termination of Ethereum smart contracts is usually ensured. We then devise a type system for smart contracts guaranteeing that such programs never run out of gas at runtime. This is a desirable property for smart contracts, since a transaction that runs out of gas is aborted, but the price paid to run the code is not returned to the invoker.

cs.PL↗

arXiv2024

A Sound Type System for Secure Currency Flow

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.

cs.PL↗

arXiv2022

A Generic Type System for Higher-Order $Ψ$-calculi

The Higher-Order $Ψ$-calculus framework (HO$Ψ$) is a generalisation of many first- and higher-order extensions of the $π$-calculus. It was proposed by Parrow et al. who showed that higher-order calculi such as HO$π$ and CHOCS can be expressed as HO$Ψ$-calculi. In this paper we present a generic type system for HO$Ψ$-calculi which extends previous work by Hüttel on a generic type system for first-order $Ψ$-calculi. Our generic type system satisfies the usual property of subject reduction and can be instantiated to yield type systems for variants of HOπ, including the type system for termination due to Demangeon et al. Moreover, we derive a type system for the $ρ$-calculus, a reflective higher-order calculus proposed by Meredith and Radestock. This establishes that our generic type system is richer than its predecessor, as the $ρ$-calculus cannot be encoded in the $π$-calculus in a way that satisfies standard criteria of encodability.

cs.LO↗

arXiv2022

Encodability and Separation for a Reflective Higher-Order Calculus

The $ρ$-calculus (Reflective Higher-Order Calculus) of Meredith and Radestock is a $π$-calculus-like language with some unusual features, notably, structured names, runtime generation of free names, and the lack of an operator for scoping visibility of names. These features pose some interesting difficulties for proofs of encodability and separation results. We describe two errors in a previously published attempt to encode the $π$-calculus in the $ρ$-calculus by Meredith and Radestock. Then we give a new encoding and prove its correctness, using a set of encodability criteria close to those proposed by Gorla, and discuss the adaptations necessary to work with a calculus with runtime generation of structured names. Lastly we prove a separation result, showing that the $ρ$-calculus cannot be encoded in the $π$-calculus.

cs.LO↗