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.

翻译：本文在智能合约场景中发展了语义类型化方法，以确保使用静态不可类型化语言构造（如回退函数）的代码的类型安全性。核心思想是：区块链上的合约创建者为包含此类构造的代码配备基于类型语义的形式化类型安全证明。随后，合约用户仅需验证所提供类型安全"证明证书"的有效性。这是一种证明携带代码（proof-carrying code）形式，天然契合区块链环境的不可变性。作为本方法的具体应用，我们专注于通过安全类型确保Solidity语言精简版本TinySol的信息流控制与非干扰性。我们基于TinySol的类型化操作语义给出了类型的语义，并将安全证明表示为余归纳定义的类型解释，这些解释可通过与双模拟类似的up-to技术进行紧凑表示。我们还展示了如何利用该机制对基于回退函数的典型指针到实现模式进行类型化，并拒绝著名Parity多签名钱包攻击的精简版本。