arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2109.15212cs.CRcs.CLcs.LO
收藏

基于合约与时态逻辑的账本管理系统形式化模型

A formal model for ledger management systems based on contracts and temporal logic

Sapienza University of Rome(罗马第一大学);University of Molise(莫利塞大学)

Paolo Bottoni, Anna Labella, Remo Pareschi

AI总结:

针对当前智能合约易有漏洞、语义偏离法律合约的问题,提出基于有限状态自动机的合约形式化模型,并以时态逻辑构建适配账本历史属性的抽象查询语言,提升账本系统可靠性。

摘要:

区块链技术的核心组件是账本,即一种数据库,与标准数据库不同,它会将过往交易的完整历史保存在内存中,就像公证档案一样,可供未来任何核查使用。在以太坊等第二代区块链中,账本与智能合约相结合,能够自动执行与金融或商业性质的各方协议相关的交易。智能合约与账本的结合为诸多极具创新性的应用领域提供了技术基础,例如去中心化自治组织(Decentralized Autonomous Organizations, DAOs)、首次代币发行(Initial Coin Offerings, ICOs)以及去中心化金融(Decentralized Finance, DeFi),这些应用推动区块链超越了比特币等第一代区块链仅聚焦加密货币的范畴。然而,当前智能合约以任意编程结构实现的方式,使其易受可被恶意利用的危险漏洞影响,且其语义已偏离法律合约的语义。本文提出要弥合这一分歧并恢复数据库的可靠性,为此将合约概念形式化为有限状态自动机,该自动机具有明确的计算特性,这些特性源自基于参与者资源分配的编码,以此作为基于编程的方法的替代方案。作为研究的补充,我们将时态逻辑作为抽象查询语言的基础,该语言能够有效适配账本中所存储信息的历史属性。

英文摘要:

A key component of blockchain technology is the ledger, viz., a database that, unlike standard databases, keeps in memory the complete history of past transactions as in a notarial archive for the benefit of any future test. In second-generation blockchains such as Ethereum the ledger is coupled with smart contracts, which enable the automation of transactions associated with agreements between the parties of a financial or commercial nature. The coupling of smart contracts and ledgers provides the technological background for very innovative application areas, such as Decentralized Autonomous Organizations (DAOs), Initial Coin Offerings (ICOs) and Decentralized Finance (DeFi), which propelled blockchains beyond cryptocurrencies that were the only focus of first generation blockchains such as the Bitcoin. However, the currently used implementation of smart contracts as arbitrary programming constructs has made them susceptible to dangerous bugs that can be exploited maliciously and has moved their semantics away from that of legal contracts. We propose here to recompose the split and recover the reliability of databases by formalizing a notion of contract modelled as a finite-state automaton with well-defined computational characteristics derived from an encoding in terms of allocations of resources to actors, as an alternative to the approach based on programming. To complete the work, we use temporal logic as the basis for an abstract query language that is effectively suited to the historical nature of the information kept in the ledger.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑