Blockchain

以太坊虚拟机执行模型

以太坊 Yellow Paper 学习笔记（五）

Posted by Nicodechal on 2020-10-26

执行模型说明了在特定的字节码指令和环境数据下系统状态如何被修改。这部分使用以太坊虚拟机 EVM 描述。该虚拟机是一个准图灵完备的虚拟机，因为其能进行的计算受限于 gas。

执行环境

执行模型使用 Ξ\Xi 函数描述：

(σ′,g′,A,o)≡Ξ(σ,g,I)(\mathbf{\sigma}',g',A,\mathbf{o})\equiv\Xi(\mathbf{\sigma}, g, I)

即对于输入的状态 σ\mathbf{\sigma} 和可用的 gas 量 gg，以及执行时的环境变量 II(包含执行代码、变量等) 执行相关代码，得到执行后的状态、执行后剩余的 gas，执行后的子状态 ( 包含区块中一个交易执行后的一些信息，例如日志等 ) 和代码输出。

下面给出其具体的定义。

Ξ(σ,g,I,T)≡(σ′,μg′,A,o)(σ′,μ′,A,...,o)≡X((σ,μ,A0,I))μg≡gμpc≡0μm≡(0,0,...)μi≡0μs≡()μo≡()\begin{aligned} \Xi(\mathbf{\sigma},g,I,T) &\equiv(\mathbf{\sigma}',\mathbf{\mu}_g', A,\mathbf{}o) \\\\ (\mathbf{\sigma}',\mathbf{\mu}', A,...,\mathbf{}o) &\equiv X((\mathbf{\sigma},\mathbf{\mu}, A^0,I)) \\\\ \mathbf{\mu}_g &\equiv g \\\\ \mathbf{\mu}_{pc} &\equiv 0 \\\\ \mathbf{\mu}_\mathbf{m} &\equiv (0,0,...) \\\\ \mathbf{\mu}_i &\equiv 0 \\\\ \mathbf{\mu}_\mathbf{s} &\equiv () \\\\ \mathbf{\mu}_\mathbf{o} &\equiv () \end{aligned}

其中 μ\mathbf{\mu} 表示的是机器状态，包括下面字段：

  1. μg\mathbf{\mu}_g 当前可用的 gas。
  2. μpc\mathbf{\mu}_{pc} 当前的程序计数器。
  3. μm\mathbf{\mu}_\mathbf{m} 当前的内存是一个字节数组用来模拟内存。
  4. μi\mathbf{\mu}_i 内存中可用的字 ( 一个字是 256 位 ) 数。
  5. μs\mathbf{\mu}_\mathbf{s} 栈中的内容。

这里基于 Ξ\Xi 中的参数构造 XX 函数的输入，XX 输入包括需要改变的状态、机器状态、初始的子状态和环境变量。

得到的结果提取需要的字段得到 Ξ\Xi 函数的输出。

执行过程

其中 XX 代表整个执行过程，它是递归定义的，使用 OO 表示一个指令的执行过程，XX 定义如下：

X((σ,μ,A,I))≡{(∅,μ,A0,I,∅)if Z(σ,μ,I)(∅,μ′,A0,I,o)if w=REVERTO(σ,μ,A,I)⋅oif o≠∅X(O(σ,μ,A,I))otherwiseX((\mathbf{\sigma},\mathbf{\mu},A,I))\equiv \left\{ \begin{array}{} (\emptyset,\mathbf{\mu},A^0,I,\emptyset) & if\ Z(\mathbf{\sigma},\mathbf{\mu},I) \\ (\emptyset,\mathbf{\mu}',A^0,I,\mathbf{o}) & if\ w=\mathrm{REVERT} \\ O(\mathbf{\sigma},\mathbf{\mu},A,I)\cdot \mathbf{o} & if\ \mathbf{o}\neq\emptyset \\ X(O(\mathbf{\sigma},\mathbf{\mu},A,I)) & \mathrm{otherwise} \end{array} \right.

其中：

o≡H(μ,I)(a,b,c,d)⋅e≡(a,b,c,d,e)μ′≡μ expect:μg′≡μg−C(σ,μ,I)\begin{aligned} \mathbf{o} &\equiv H(\mathbf{\mu},I) \\\\ (a,b,c,d)\cdot e &\equiv (a,b,c,d,e) \\\\ \mathbf{\mu}' &\equiv \mathbf{\mu}\ \mathrm{expect:} \\\\ \mathbf{\mu_g}' &\equiv \mathbf{\mu_g}-C(\mathbf{\sigma},\mathbf{\mu},I) \end{aligned}

HH 函数表示正常停机返回，得到返回值。

H(μ,I)≡{HRETURN(μ) if w∈{RETURN,REVERT}() if w∈{STOP,SELFDESTRUCT}∅otherwiseH(\mathbf{\mu},I)\equiv \left\{ \begin{array}{} H_{\mathrm{RETURN}}(\mathbf{\mu})&\ \mathrm{if}\ w\in \{\mathrm{RETURN,REVERT}\} \\ ()&\ \mathrm{if}\ w\in\{\mathrm{STOP,SELFDESTRUCT}\} \\ \emptyset & \mathrm{otherwise} \end{array} \right.

如果最后的指令是 RETURN,REVERT\mathrm{RETURN,REVERT} 则从机器状态中取出返回值，如果是 STOP,SELFDESTRUCT\mathrm{STOP,SELFDESTRUCT} 则返回空数组，其他情况返回空集。

ZZ 则表示异常停机 ( 例如 gas 用完等等，稍后展开 )。

CC 计算当前执行消耗的 gas 数量并从剩余 gas 中减去该值。 CC 比较复杂这里不展开。

一次迭代

OO 表示一次执行，定义如下：

O((σ,μ,A,I))≡(σ′,μ′,A′,I)Δ≡αw−δw∥μs′∥≡∥μs∥+Δ∀x∈[αw,∥μs′∥):μs′[x]≡μs[x−Δ]\begin{aligned} O((\mathbf{\sigma},\mathbf{\mu},A,I)) &\equiv (\mathbf{\sigma}',\mathbf{\mu}',A',I) \\\\ \Delta &\equiv \alpha_w-\delta_w \\\\ \parallel\mathbf{\mu_\mathbf{s}'}\parallel &\equiv \parallel \mathbf{\mu_s}\parallel + \Delta \\\\ \forall x\in[\alpha_w,\parallel\mathbf{\mu_\mathbf{s}'}\parallel): \mathbf{\mu_s}'[x] &\equiv \mathbf{\mu_s}[x-\Delta] \end{aligned}

每一次调用，OO 从栈顶取出指令的参数，执行后将返回值压入栈中。Δ\Delta 表示栈的高度变化。δw\delta_w 表示指令 ww 执行时出栈元素数量，αw\alpha_w 则表示指令 ww 执行的入栈元素。后两行表示栈的运行流程，即每次从栈顶 ( index 最小一端 ) 取出或增加元素。

ww 定义为当前执行：

w≡{Ib[μpc]if μpc<∥Ib∥STOPotherwisew\equiv \left\{ \begin{array}{} I_\mathrm{b}[\mathbf{\mu}_\mathrm{pc}] & \mathrm{if}\ \mu_\mathrm{pc}<\parallel I_\mathrm{b}\parallel \\ \mathrm{STOP} & \mathrm{otherwise} \end{array} \right.

指令执行时，还会花费 gas，同时改变 pc 计数器：

μg′≡μg−C(σ,μ,I)μpc′≡{JJUMP(μ)if w=JUMPJJUMPI(μ)if w=JUMPON(μpc,w)otherwise\begin{aligned} \mathbf{\mu_g}' &\equiv \mathbf{\mu_g}-C(\mathbf{\sigma},\mathbf{\mu},I) \\\\ \mathbf{\mu}_\mathrm{pc}' &\equiv \left\{ \begin{array}{} J_\mathrm{JUMP}(\mathbf{\mu}) & \mathrm{if}\ w=\mathrm{JUMP}\\ J_\mathrm{JUMPI}(\mathbf{\mu}) & \mathrm{if}\ w=\mathrm{JUMPO}\\ N(\mathbf{\mu_{\mathrm{}pc}},w) & \mathrm{otherwise} \end{array} \right. \end{aligned}

对于跳转指令 JUMP,JUMPI\mathrm{JUMP,JUMPI} 将 pc 值改为跳转到的位置。其他情况调用 NN 函数计算下一位置。

N(i,w)≡{i+w−PUSH1+2if w∈[PUSH1,PUSH32]i+1otherwiseN(i,w)\equiv \left\{ \begin{array}{} i + w - \mathrm{PUSH1} + 2 & \mathrm{if}\ w\in[\mathrm{PUSH1},\mathrm{PUSH32}] \\ i + 1 & \mathrm{otherwise} \end{array} \right.

这里主要对于 PUSH\mathrm{PUSH} 系列指令跳过了压栈的数据，其他情况直接加一即可。

异常停机

出现以下情况会异常停机

  1. gas 不足，即 μg<C(σ,μ,I)\mathbf{\mu}_g<C(\mathbf{\sigma},\mathbf{\mu},I)。
  2. 当前指令不可用，用 δw=∅\delta_w=\emptyset 表示。
  3. 栈高度小于需要出栈的元素数，∥μs∥<δw\parallel\mathbf{\mu_s}\parallel<\delta_w。
  4. JUMP,JUMPI\mathrm{JUMP,JUMPI} 指令的跳转地址不可用。使用 D(Ib)D(I_\mathrm{b}) 表示代码 IbI_\mathrm{b} 可以跳转的地址集合，则有 w=JUMP∧μs[0]∉D(Ib)w=\mathrm{JUMP} \wedge \mathbf{\mu_s}[0]\notin D(I_\mathrm{b}) 或 w=JUMPI∧μs[1]≠0∧μs[0]∉D(Ib)w=\mathrm{JUMPI} \wedge \mathbf{\mu_s}[1]\neq 0 \wedge \mathbf{\mu_s}[0]\notin D(I_\mathrm{b})
  5. RETURNDATACOPY\mathrm{RETURNDATACOPY} 指令可以将栈中的返回值拷贝到内存，使用 μs[1]\mathbf{\mu_s}[1] 表示起始地址，μs[2]\mathbf{\mu_s}[2] 表示最大偏移，所以，他们的和如果大于输出的长度则出现异常。 w=RETURNDATACOPY∧μs[1]+μs[2]>∥μo∥w=\mathrm{RETURNDATACOPY} \wedge\mathbf{\mu_s}[1]+ \mathbf{\mu_s}[2]>\parallel \mathbf{\mu_o} \parallel
  6. 栈高度超过 1024，∥μs∥−δw+αw>1024\parallel \mathbf{\mu_s} \parallel - \delta_w+\alpha_w > 1024。
  7. 静态调用时修改状态。使用 IwI_\mathrm{w} 表示修改状态的权限。则有 Iw∧W(w,μ)I_\mathrm{w}\wedge W(w,\mathrm{\mu})

其中

W(w,μ)≡w∈{CREATE,CREATE2,SSTORE,SELFDESTRUCT}∨LOG0≤w∧w≤LOG4∨(w∈{CALL,CALLCODE}∧μs[2]≠0)\begin{aligned} W(w,\mathrm{\mu}) \equiv & w\in \{\mathrm{CREATE,CREATE2,SSTORE,SELFDESTRUCT}\}\vee \\\\ &\mathrm{LOG0 \leq w\wedge w\leq LOG4} \vee \\\\ &(w\in \{\mathrm{CALL,CALLCODE}\}\wedge \mathbf{\mu_s}[2]\neq 0) \end{aligned}

D(Ib)D(I_\mathrm{b}) 表示代码 IbI_\mathrm{b} 可以跳转的地址集合：

D(c)≡DJ(c,0)DJ(c,i)≡{{}if i≥∥c∥{i}∪DJ(c,N(i,c[i]))if c[i]=JUMPDESTDJ(c,N(i,c[i]))otherwise\begin{aligned} D(\mathbf{c}) &\equiv D_J(\mathbf{c},0) \\\\ D_J(\mathbf{c},i) &\equiv \left\{ \begin{array}{} \{\} & \mathrm{if}\ i\geq\parallel\mathbf{c} \parallel \\ \{i\}\cup D_J(\mathbf{c},N(i,\mathbf{c}[i])) & \mathrm{if}\ \mathbf{c}[i]=\mathrm{JUMPDEST} \\ D_J(\mathbf{c},N(i,\mathbf{c}[i])) & \mathrm{otherwise} \end{array} \right. \end{aligned}

这里对当前位置 ii 的指令进行判断，如果是 JUMPDEST\mathrm{JUMPDEST} 则将 i ( 也就是指向跳转地址的地址 ) 加入集合，同时从当前位置继续遍历代码。

综上，异常停止判断函数如下：

Z(σ,μ,I)≡ μg<C(σ,μ,I) ∨δw=∅ ∨∥μs∥<δw ∨w=JUMP∧μs[0]∉D(Ib) ∨w=JUMPI∧μs[1]≠0∧μs[0]∉D(Ib) ∨w=RETURNDATACOPY∧μs[1]+μs[2]>∥μo∥ ∨∥μs∥−δw+αw>1024 ∨¬Iw∧W(w,μ)\begin{aligned} Z(\mathbf{\sigma},\mathbf{\mu},I)\equiv\ &\mathbf{\mu}_g<C(\mathbf{\sigma},\mathbf{\mu},I)\ \vee \\\\ &\delta_w=\emptyset\ \vee \\\\ &\parallel\mathbf{\mu_s}\parallel<\delta_w\ \vee \\\\ &w=\mathrm{JUMP} \wedge \mathbf{\mu_s}[0]\notin D(I_\mathrm{b})\ \vee \\\\ &w=\mathrm{JUMPI} \wedge \mathbf{\mu_s}[1]\neq 0 \wedge \mathbf{\mu_s}[0]\notin D(I_\mathrm{b})\ \vee \\\\ &w=\mathrm{RETURNDATACOPY} \wedge\mathbf{\mu_s}[1]+ \mathbf{\mu_s}[2]>\parallel \mathbf{\mu_o} \parallel\ \vee \\\\ &\parallel \mathbf{\mu_s} \parallel - \delta_w+\alpha_w > 1024\ \vee \\\\ &\neg I_\mathrm{w}\wedge W(w,\mathrm{\mu}) \end{aligned}

FEATURED TAGS
Blockchain
FRIENDS