一句话：提出 Obsidian 语言及其核心演算 Silica，用 typestate 与线性类型静态检测智能合约常见漏洞，并证明类型可靠性。
区块链智能合约处理互不信任参与者间的关键交易，但合约漏洞常被黑客利用。Obsidian 是面向智能合约的新型编程语言，其类型系统可静态检测常见缺陷。它建立在核心演算 Silica 上，并证明了类型可靠性。语言用 typestate 检测不当状态操作，用线性类型检测资产滥用，并集成权限系统编码所有权概念，从而支持安全而灵活的别名。作者通过参数化保险与供应链管理两个案例研究评估适用性，发现其类型系统有助于推理高层状态和资源所有权。与 Solidity 实现对比表明，Solidity 需要大量样板式检查与状态跟踪，而 Obsidian 能静态完成这些工作。
Blockchain platforms are coming into use for processing critical transactions among participants who have not established mutual trust. Many blockchains are programmable, supporting smart contracts , which maintain persistent state and support transactions that transform the state. Unfortunately, bugs in many smart contracts have been exploited by hackers. Obsidian is a novel programming language with a type system that enables static detection of bugs that are common in smart contracts today. Obsidian is based on a core calculus, Silica, for which we proved type soundness. Obsidian uses typestate to detect improper state manipulation and uses linear types to detect abuse of assets. We integrated a permissions system that encodes a notion of ownership to allow for safe, flexible aliasing. We describe two case studies that evaluate Obsidian’s applicability to the domains of parametric insurance and supply chain management, finding that Obsidian’s type system facilitates reasoning about high-level states and ownership of resources. We compared our Obsidian implementation to a Solidity implementation, observing that the Solidity implementation requires much boilerplate checking and tracking of state, whereas Obsidian does this work statically.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{CoblenzOEKBBMSA20,
title = {Obsidian},
author = {Michael Coblenz and Reed Oei and Tyler Etzel and Paulette Koronkevich and Miles Baker and Yannick Bloem and Brad A. Myers and Joshua Sunshine and Jonathan Aldrich},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {42},
number = {3},
year = {2020},
doi = {10.1145/3417516}
}