验证递归比特币合约的流动性
Verifying liquidity of recursive Bitcoin contracts
AI总结：
针对智能合约中资产冻结的流动性安全问题，提出基于BitML的有限状态抽象与模型检查验证技术，并实现自动验证与编译工具链。
摘要：
智能合约——在无需信任的环境中规范加密资产交换的计算机协议——随着区块链技术的普及而变得流行。智能合约的一个标志性安全属性是流动性：在非流动性合约中，可能发生某些资产被冻结，即任何人都无法赎回的情况。这一问题的重要性由最近针对以太坊的流动性攻击所证明，这些攻击冻结了数亿美元的资产。我们着手解决在BitML上验证流动性的问题，BitML是一种用于智能合约的领域特定语言，具有到比特币的安全编译器，支持货币转账、合约重新协商和共识递归等原语。我们的主要成果是一种流动性验证技术。我们首先将BitML的无限状态语义转换为有限状态语义，该语义聚焦于选定合约集合的行为，抽象掉上下文的行为。对于所选合约而言，这种抽象是可靠的，即如果抽象后的合约是流动的，那么具体合约也是流动的。然后，我们通过模型检查有限状态抽象来验证流动性。我们实现了一个工具链，能够自动验证BitML合约的流动性并将其编译为比特币，并通过一组代表性合约的基准对其进行了评估。
英文摘要：
Smart contracts - computer protocols that regulate the exchange of crypto-assets in trustless environments - have become popular with the spread of blockchain technologies. A landmark security property of smart contracts is liquidity: in a non-liquid contract, it may happen that some assets remain frozen, i.e. not redeemable by anyone. The relevance of this issue is witnessed by recent liquidity attacks to Ethereum, which have frozen hundreds of USD millions. We address the problem of verifying liquidity on BitML, a DSL for smart contracts with a secure compiler to Bitcoin, featuring primitives for currency transfers, contract renegotiation and consensual recursion. Our main result is a verification technique for liquidity. We first transform the infinite-state semantics of BitML into a finite-state one, which focusses on the behaviour of a chosen set of contracts, abstracting from the moves of the context. With respect to the chosen contracts, this abstraction is sound, i.e. if the abstracted contract is liquid, then also the concrete one is such. We then verify liquidity by model-checking the finite-state abstraction. We implement a toolchain that automatically verifies liquidity of BitML contracts and compiles them to Bitcoin, and we assess it through a benchmark of representative contracts.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
