论文标题
使用最弱的前提条件来验证AGDA中的比特币脚本
Verification of Bitcoin Script in Agda using Weakest Preconditions for Access Control
论文作者
论文摘要
本文有助于验证在交互式定理称者AGDA中用比特币的智能合同语言脚本编写的程序的验证。它着重于控制比特币分布的脚本程序的访问控制的安全属性。它提倡在Hoare三元组中最弱的前提是验证访问控制的合适概念。它旨在获得最弱的先决条件的人类可读描述，以缩小用户需求和智能合约正式规范之间的验证差距。 作为拟议方法的示例，该论文着重于两个标准脚本程序，这些程序管理比特币的分布，支付公共密钥哈希（P2PKH）并向Multisig付款（P2MS）。本文介绍了P2PKH和P2MS中使用的脚本命令的操作语义，该命令在AGDA Proof Assistant中正式化，并有关使用Hoare Triples的理由。讨论了两种获得最弱的先决条件的人类可读描述的方法： （1）逐步的方法，该方法通过脚本通过指令向后指令，有时将几个说明分组在一起； （2）符号执行代码并将其转换为嵌套的情况区别，它允许将最弱的先决条件读取为沿接受路径的条件结合的脱节。 为了将AGDA中的这些方法形式化，定义了用于使用Hoare三元组的方程推理的语法。 关键字和短语：区块链；加密货币；比特币； agda;确认; Hoare逻辑；比特币脚本； p2pkh; P2M；访问控制；最弱的先决条件；谓词变压器语义；可证明的正确性；符号执行；智能合约
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
