使用访问控制的最弱前提验证Agda中的比特币Script
Verification of Bitcoin Script in Agda using Weakest Preconditions for Access Control
摘要：
本文有助于在交互式定理证明器Agda中验证用比特币智能合约语言BNT编写的程序。它关注的是管理比特币分发的PICOT程序的访问控制的安全属性。它主张Hoare三元组上下文中最弱的先决条件是验证访问控制的适当概念。它旨在获得对最弱前提条件的人类可读描述，以缩小用户需求与智能合约正式规范之间的验证差距。作为所提出的方法的例子，本文重点介绍了两个标准的比特币发行管理程序，支付给公钥哈希（P2PKH）和支付给Multisig（P2 MS）。本文介绍了P2PKH和P2 MS中使用的P2 T命令的操作语义，并在Agda证明助手中进行了形式化，并对使用Hoare三元组进行了推理。两种方法获得人类可读的描述最弱的先决条件进行了讨论：（1）一步一步的方法，它通过一个脚本，有时分组几个指令一起向后指令;（2）符号执行的代码和翻译成一个嵌套的情况下的区别，它允许读取最弱的先决条件作为沿接受路径的条件的合取的析取。公式推理与霍尔三元组的语法定义，以形式化这些方法在Agda。关键词和短语：区块链;加密货币;比特币;阿格达;核查;霍尔逻辑比特币脚本; P2PKH; P2MS;访问控制;最弱前提条件;谓词Transformer语义;可证明的正确性;象征性处决;智能合约
英文摘要：
This paper contributes to the verification of programs written in Bitcoin's smart contract language SCRIPT in the interactive theorem prover Agda. It focuses on the security property of access control for SCRIPT programs that govern the distribution of Bitcoins. It advocates that weakest preconditions in the context of Hoare triples are the appropriate notion for verifying access control. It aims at obtaining human-readable descriptions of weakest preconditions in order to close the validation gap between user requirements and formal specification of smart contracts. As examples for the proposed approach, the paper focuses on two standard SCRIPT programs that govern the distribution of Bitcoins, Pay to Public Key Hash (P2PKH) and Pay to Multisig (P2MS). The paper introduces an operational semantics of the SCRIPT commands used in P2PKH and P2MS, which is formalised in the Agda proof assistant and reasoned about using Hoare triples. Two methodologies for obtaining human-readable descriptions of weakest preconditions are discussed: (1) a step-by-step approach, which works backwards instruction by instruction through a script, sometimes grouping several instructions together; (2) symbolic execution of the code and translation into a nested case distinction, which allows to read off weakest preconditions as the disjunction of conjunctions of conditions along accepting paths. A syntax for equational reasoning with Hoare Triples is defined in order to formalise those approaches in Agda. Keywords and phrases: Blockchain; Cryptocurrency; Bitcoin; Agda; Verification; Hoare logic; Bitcoin script; P2PKH; P2MS; Access control; Weakest precondition; Predicate transformer semantics; Provable correctness; Symbolic execution; Smart contracts
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
