资金费率
资金费率热力图
多空比
大户多空比
币安/欧易/火币大户多空比
Bitfinex杠杆多空比
账号安全
资讯收藏
自选币种
智能合约的形式化验证：加密货币领域的新兴趋势
智能合约的形式化验证是加密货币领域的一个新兴趋势，旨在减少智能合约中漏洞和缺陷的发生率。这些漏洞和缺陷导致了多起备受瞩目的黑客攻击和普遍的安全问题。形式化验证在硬件和软件系统中有广泛的应用。随着系统复杂性的增加，尤其是在硬件领域，形式化验证变得尤为重要。在区块链网络中，智能合约漏洞和利用的频发，使得改进智能合约编程和审计成为必要。
形式化验证的背景
形式化验证使用形式化方法来检查硬件或软件系统的设计是否满足特定属性。形式化方法是一种特殊的数学技术，用于硬件和软件系统的规范、开发和验证。使用形式化方法来证明或反驳预期算法的正确性，被称为形式化验证。
Martin Davis 在 1954 年开发了第一个计算机生成的数学证明。这一概念在 1960 年代开始流行，用于验证 Pascal 和 Java 等早期语言编写的计算机程序的正确性。在 1994 年 Pentium FDIV 漏洞等一些备受关注的计算机漏洞之后，形式化验证需要普及的观点开始逐渐扩大。
测试软件或硬件系统可以分为两个主要阶段：
- 验证：确定产品是否符合用户的需
- 确认：测试产品是否符合规范
确认包括生成与产品设计规范（即算法、硬件芯片）相对应的抽象数学模型，而生成模型的形式化方法主要源于理论计算机科学基础。
形式化验证在硬件系统中的使用变得极为重要，几乎每个主要硬件制造商都使用它来确保产品的鲁棒性。然而，其在软件中的使用远不及在硬件中普遍，这主要归因于硬件制造的商业性质。
然而，随着区块链和加密货币的出现，这一动态开始发生变化，因为大量的价值转移在去中心化网络中自主执行。与传统系统相比，智能合约的正确性成为一个紧迫的问题。了解智能合约利用的简短历史，就足以理解合约代码中简单漏洞的后果。
为什么要在智能合约中使用形式化验证？
根据最近对近 100 万个以太坊智能合约进行的一项研究，34,200 个合约在每 10 秒内被标记为易受攻击。这一惊人的数字是通过分析智能合约的跟踪漏洞得出的，包括：
- 发现永久锁定资金的合约
- 发现资金随意泄露给任意用户的合约
- 发现可以被任何人终止的合约
与为区块链编程智能合约相关的一般逻辑复杂性和新颖性一样，一旦智能合约被提交到区块链，其不可变性质使得漏洞可能更具破坏性。
Brian Marick 和 Daejun Park 提供了对智能合约漏洞的出色分析，以及形式化验证如何帮助减少这些漏洞的发生。本质上，开发人员通常有两种方式无法从智能合约中获得他们想要的结果：
- 误解意图
- 在实现该意图时出错
许多这些标准错误可能导致巨额资金被锁定，如 Parity 钱包或 DAO 事件中以太坊的递归发送利用。形式化验证被用作一种数学确认方式，确保特定漏洞不会导致破坏性利用向量。
形式化规范被用作智能合约寻找的精确输出或结果，计算机可以检查这一点。验证随后在合约编译为字节码后进行，形式化验证证明编译后的字节码实现了规范。然而，手动执行形式化验证是一个艰巨的过程，有时会伴随自己的错误。甚至验证形式化证明结果也可能有其细微差别。
像 Coq 证明助手这样的工具已被开发出来，以帮助促进关于程序属性的机械化证明，目前被几种新兴加密货币使用，它们使用的语言嵌入在 Coq 中。
虽然智能合约审计通过代码审查提供了急需的保证层，但智能合约的形式化验证可以通过数学分析进一步减少漏洞的发生。随着智能合约变得越来越普遍，形式化验证的应用在行业中变得更加广泛似乎是自然的。
形式化验证的当前应用
几个平台要么已经集成了形式化验证，要么计划很快集成。评估这些平台内运行的智能合约的安全性和安全性，对于衡量它们在阻止关键漏洞方面的有效性至关重要。
Zilliqa
Zilliqa 是一个高吞吐量的区块链，旨在托管可扩展且安全的去中心化应用程序（dapps）。Zilliqa 背后的几位技术开发人员是早期研究的作者，该研究发现了数千个智能合约弱点。
Zilliqa 使用一种名为 Scilla 的新编程语言，由 Zilliqa 团队的成员和其他一些附属机构设计。Scilla 是一种中级语言，嵌入在 Coq 证明助手中。它旨在成为高级语言的翻译目标，以便在合约编译为字节码之前执行分析和验证。
Tezos
Tezos 是用 OCaml 编写的，其智能合约语言是基于 OCaml 的 Michelson。选择 OCaml 是因为其函数式编程提供了速度、明确的语法和语义以及实现形式化证明的能力。Tezos 还使用 Coq 证明助手来促进智能合约的形式化验证。
Tezos 联合创始人 Arthur Breitman 发布了有关在 Coq 中验证一些 Michelson 合约的详细信息，包括去年在测试网上的多签合约。Tezos 最近刚刚推出，因此其形式化验证的应用应该为使用该方法改进智能合约安全性的状态提供一个很好的衡量标准。困扰 Solidity 合约的利用是否会在 Tezos 中上演，还需要一些时间来展开，但评估 Tezos 上的智能合约的安全性可能非常能预示一个持续的趋势。
Cardano
Cardano 是用 Haskell 编写的，其智能合约语言是基于 Haskell 的 Plutus。
Cardano 设计了一个 Cardano 计算层（CCL），由两层组成：
- 一个正式指定的虚拟机和语言框架
- 促进智能合约代码验证的正式指定语言
目标是创建一个环境，简化保证合约按设计运行而不出现灾难性漏洞的过程。值得注意的是，Cardano 不像以太坊的 EVM 那样使用有界堆栈设计，因此不必担心堆栈算术流程，这使得它更容易正式验证智能合约。
Ethereum
以太坊一直在研究形式化验证的整合，已经有一段时间了，有几个项目正在调查其潜力。其中一篇名为“让智能合约更智能”的出版物，专注于智能合约漏洞，并提出了缓解这些漏洞的方法，包括改进以太坊的操作语义以促进形式化验证。
以太坊中的 gas 限制使得实施形式化验证具有挑战性。此外，了解 Solidity 程序含义的唯一方法是将其编译为字节码。编译器变化迅速，因此验证工具也需要适应变化的速率。考虑到以太坊的成熟网络和历史，如果形式化验证在以太坊网络中广泛使用，智能合约的形式化验证将显然为它们在缓解漏洞方面的有效性提供最佳衡量标准。
结论
形式化验证是一项高度复杂且艰巨的任务。尽管如此，它已成为硬件行业的通用标准，并可能在软件领域继续获得动力。区块链和加密货币网络——高价值转移普遍存在——无疑会加速这一效果。衡量智能合约形式化验证的积极影响可能需要几年时间才能展开，因为我们只看到了这一趋势的开始，它应该成为行业中更广泛的趋势。
