Obsidian: Typestate and Assets for Safer Blockchain Programming
Obsidian: Typestate and Assets for Safer Blockchain Programming
复制标题
Obsidian：用于更安全的区块链编程的类型状态和资产
DOI：
10.1145/3417516
复制
发表时间：
2020
影响因子：
1.3
通讯作者：
Aldrich, Jonathan
中科院分区：
文献类型：
--
作者：
Coblenz, Michael;Oei, Reed;Etzel, Tyler;Koronkevich, Paulette;Baker, Miles;Bloem, Yannick;Myers, Brad A.;Sunshine, Joshua;Aldrich, Jonathan
区块链平台正在用于处理尚未建立相互信任的参与者之间的关键交易。许多区块链都是可编程的，支持智能合约，智能合约维护持久状态并支持转换状态的交易。不幸的是，许多智能合约中的错误已被黑客利用。 Obsidian 是一种新颖的编程语言，具有类型系统，可以静态检测当今智能合约中常见的错误。 Obsidian 基于核心微积分 Silica，我们证明了其类型的可靠性。 Obsidian 使用类型状态来检测不当的状态操作，并使用线性类型来检测资产滥用。我们集成了一个权限系统，该系统对所有权概念进行编码，以允许安全、灵活的别名。我们描述了两个评估 Obsidian 在参数保险和供应链管理领域的适用性的案例研究，发现 Obsidian 的类型系统有助于对高级状态和资源所有权进行推理。我们将 Obsidian 实现与 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, supportingsmart 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 usestypestateto detect improper state manipulation and useslinear typesto detect abuse of assets. We integrated a permissions system that encodes a notion ofownershipto 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：
10.1109/icse.2007.92
发表时间：
2007-05
期刊：
29th International Conference on Software Engineering (ICSE'07)
影响因子：
--
作者：
Jeffrey Stylos;S. Clarke
通讯作者：
Jeffrey Stylos;S. Clarke
IELE：严格设计的区块链语言和工具生态系统
DOI：
--
发表时间：
2019
期刊：
World Congress on Formal Methods
影响因子：
--
作者：
T. Kasampalis;Dwight Guth;Brandon M. Moore;Traian;Y. Zhang;Daniele Filaretti;V. Serbanuta;Ralph E. Johnson;Grigore Roşu
通讯作者：
Grigore Roşu
DOI：
--
发表时间：
2011
期刊：
影响因子：
--
作者：
K. Bierhoff;Nels E. Beckman;Jonathan Aldrich
通讯作者：
Jonathan Aldrich
DOI：
10.1007/978-3-662-44202-9_7
发表时间：
2014-08
期刊：
--
影响因子：
--
作者：
Joshua Sunshine;J. Herbsleb;Jonathan Aldrich
通讯作者：
Joshua Sunshine;J. Herbsleb;Jonathan Aldrich
DOI：
10.1145/2534973
发表时间：
2013-11
期刊：
ACM Trans. Comput. Educ.
影响因子：
--
作者：
A. Stefik;Susanna Siebert
通讯作者：
A. Stefik;Susanna Siebert