Obsidian：Typestate和Assets用于更安全的区块链编程
Obsidian: Typestate and Assets for Safer Blockchain Programming
摘要：
区块链平台正在广泛用于处理尚未建立相互信任的参与者之间的关键交易。许多区块链都是可编程的，支持智能合约，智能合约维护持久状态并支持转换状态的交易。不幸的是，许多智能合约中的漏洞已经被黑客利用。Obsidian是一种新颖的程序设计语言，它的类型系统可以静态检测当今智能合约中常见的错误。黑曜石是基于一个核心演算，二氧化硅，我们证明了类型的可靠性。Obsidian使用typestate来检测不适当的状态操纵，使用线性类型来检测资产滥用。我们描述了两个案例研究，评估黑曜石的适用性的领域的参数保险和供应链管理，发现黑曜石的类型系统有利于推理高层次的国家和所有权的资源。我们将我们的Obsidian实现与Solidity实现进行了比较，观察到Solidity实现需要大量的样板检查和状态跟踪，而Obsidian静态地完成这项工作。
英文摘要：
Blockchain platforms are coming into broad 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 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
