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.
Tue 17 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:30 - 17:00 | |||
15:30 15mTalk | InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference Technical Papers Senxi Li The University of Tokyo, Tetsuro Yamazaki University of Tokyo, Shigeru Chiba University of Tokyo | ||
15:45 15mTalk | A Sound Type System for Secure Currency Flow Technical Papers Luca Aceto Reykjavik University, Daniele Gorla Department of Computer Science, Sapienza University of Rome, Stian Lybech Reykjavik University | ||
16:00 15mTalk | Type Tailoring Technical Papers Ashton Wiersdorf University of Utah, Stephen Chang University of Massachusetts Boston, Matthias Felleisen Northeastern University, Ben Greenman University of Utah | ||
16:15 15mTalk | Learning Gradual Typing Performance Technical Papers Mohammad Wahiduzzaman Khan UL Lafayette, Sheng Chen University of Louisiana at Lafayette, Yi He Old Dominion University | ||
16:30 15mTalk | Generalizing Shape Analysis with Gradual Types Technical Papers Zeina Migeed University of California, Los Angeles, James Reed Fireworks AI, Jason Ansel Meta, Jens Palsberg University of California, Los Angeles (UCLA) |