形式化验证入门(part1)

初心
智能合约的安全性至关重要:DAO 事件仍历历在目,parity 黑客攻击以及最近推迟的硬分叉,不仅是开发人员,包括普通用户在内都希望能出现更安全的代码来保障他们的资产安全。

那么如果每个优质的代码背后都有坚实的数学理论作为支撑,而不仅仅只是开发人员的个人素养呢?

值得庆幸的是,随着以太坊的形式化验证工具的逐渐成熟完备,它现在不仅可行而且实用~

本文旨在对 K-framework 进行逐步深入的探讨,以期能够对 EVM 的智能合约进行形式化验证。

核心
形式化验证的整个核心是 【K 语言】,它用于定义计算机程序的行为,例如针对类型为 uint 的变量 x 定义行为 x++ , 它的 solidity 执行程序总是会将 x 里的值加 1 ,直到它的上限$x=2^{256}-1$

  1. 若要对智能合约是否符合要求进行形式化验证,则需要提供以下几类信息:
    所使用编程语言的低级语义形式;
    上述例子中的低级语义形式为:
    如果$x=2^{256}-1$,那么 x++ 会将 x 的值归零;
    否则 x++ 会将 x 的值加一;
  2. 程序对应的EVM字节码
  3. 程序对应的高级语义形式;
    上述例子中的高级语义形式为:
    Function uint addOne(int x)returns x+1 only if x<=$2^256-1$,else returns 0;

其中程序的高级语义形式是最富有挑战性的部分,必须制定希望程序执行的方式。

**见证奇迹的时刻**(高光时刻到来了⭐BlingBling)
验证程序用于证明当前程序及其所使用编程语言的低等语义形式与所提供的高等语义形式所对应的表现形式是相同的。

虽然 K-framework 生态系统非常复杂,但是包罗万象,应有尽有:

  1. K 语言允许用户编写任何类型的程序语义
  2. 支持使用 Z3 来证明语义,z3 是由 Micorosoft Research 研发的自动证明工具。
  3. 以太坊虚拟机的语义,由 Everett Hildenbrandt 编写。
  4. 两种领域特定语言(DSL) 来创建高等语义:
    act(由 dapphub 创建的 KLAB )和 eDSL(由 runtimeverification 创建)

在实际开发过程中唯一待做的工作就是编写高等语义并使其一同运转,高等语义可以直接在 K 中完成,也可以用其中一种 DSL,特别是 Solidity .

第二部分见咯~

Leave a Reply

Your email address will not be published.

当前无网络链接