递归比特币合约的流动性验证

智能合约——在免信任环境中规范加密资产交换的计算机协议——已随着区块链技术的普及而流行。智能合约的一个标志性安全属性是流动性：在非流动性合约中，可能发生某些资产被冻结，即任何人都无法赎回的情况。近期针对以太坊的流动性攻击已冻结了数亿美元，印证了该问题的相关性。我们研究在 BitML 上验证流动性的问题，BitML 是一种面向智能合约的 DSL，带有到 Bitcoin 的安全编译器，具备货币转移、合约重协商与共识递归等原语。我们的主要成果是一种流动性验证技术。我们首先将 BitML 的无限状态语义转换为有限状态语义，后者聚焦于选定合约集合的行为，并抽象掉上下文的动作。相对于所选合约，该抽象是可靠的，即若抽象后的合约是流动的，则具体合约亦是如此。随后我们通过模型检测有限状态抽象来验证流动性。我们实现了一个自动验证 BitML 合约流动性并将其编译至 Bitcoin 的工具链，并通过一组代表性合约的基准测试对其进行了评估。