使用Echidna进行状态机测试
基于属性的测试是一种强大的技术，通过对大量随机生成的输入执行程序来验证其任意属性。Echidna是一个我一直在开发的库和可执行文件，用于将基于属性的测试应用于EVM代码（特别是用Solidity编写的代码）。
Echidna是一个针对给定智能合约ABI生成随机调用序列并确保其执行保持某些用户定义不变式（例如：这个钱包的余额绝不能减少）的库。如果你来自更传统的安全背景，可以将其视为一个模糊测试器，但需要注意的是它寻找的是用户指定的逻辑错误而不是崩溃（因为为EVM编写的程序不会以任何传统方式"崩溃"）。
Echidna中的基于属性测试功能是通过Hedgehog实现的，这是Jacob Stanley开发的一个基于属性的测试库。可以将Hedgehog视为QuickCheck的更好版本。它是一个极其强大的库，提供自动最小化测试用例生成（“收缩”）、为范围等事物精心设计的抽象，以及最重要的是，本文关注的抽象状态机测试工具。
在阅读了Tim Humphries的一篇特别优秀的博客文章（“使用Hedgehog进行状态机测试”，我将其称为"Hedgehog文章"）关于使用此功能测试简单状态机的内容后，我很好奇是否可以将相同的技术扩展到EVM。我在实际中看到的许多合约只是某些教科书状态机的实现，能够针对这种富含不变式的表示编写测试将是非常宝贵的。
本文的其余部分假设至少对Hedgehog的状态机测试功能有一定了解。如果你不熟悉该软件，我建议先阅读Humphries的博客文章。还值得注意的是，下面的代码展示了Echidna API的高级用法，你也可以使用它来测试代码而无需编写一行Haskell。
首先，我们将描述状态机的状态，然后是它的转换，完成这些后，我们将使用它来实际发现在实现它的合约中的一些错误。如果你想自己跟随操作，所有Haskell代码都在examples/state-machine中，所有Solidity代码都在solidity/turnstile中。
步骤0：构建模型
图1：一个旋转门状态机
Hedgehog文章中的状态机是一个具有两个状态（锁定和解锁）和两个动作（投入硬币和推动旋转门）的旋转门，初始状态为"锁定"。我们可以逐字复制这段代码。
1
2
3
4
5
6
|
data ModelState (v :: * -> *) = TLocked
| TUnlocked
deriving (Eq, Ord, Show)
initialState :: ModelState v
initialState = TLocked
|
然而，在Hedgehog文章中，这个抽象模型的有效实现是一个需要I/O访问的可变变量。我们可以改用简单的Solidity程序。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
contract Turnstile {
bool private locked = true; // 初始状态为锁定
function coin() {
locked = false;
}
function push() returns (bool) {
if (locked) {
return(false);
} else {
locked = true;
return(true);
}
}
}
|
此时，我们有一个只描述状态而不描述转换的抽象模型，以及一些我们声称实现状态机的Solidity代码。为了测试它，我们仍然需要描述这个机器的转换和不变式。
步骤1：编写一些命令
要编写这些测试，我们需要明确如何执行我们模型的实现。Hedgehog文章中给出的示例在任何MonadIO中工作，因为它们处理IORefs。然而，由于EVM执行是确定性的，我们可以在任何MonadState VM中工作。
最简单的命令是投入硬币。这应该总是导致旋转门解锁。
1
2
3
4
5
6
7
8
9
10
11
|
s_coin :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState
s_coin = Command (\_ -> Just $ pure Coin)
-- 无论初始状态如何，我们总是可以投入硬币
(\Coin -> cleanUp >> execCall ("coin", []))
-- 投入硬币只是调用合约中的coin()
-- 我们需要cleanUp来将多个调用链接在一起
[ Update $ \_ Coin _ -> TUnlocked
-- 投入硬币将状态设置为解锁
, Ensure $ \_ s Coin _ -> s === TUnlocked
-- 投入硬币后，状态应该是解锁的
]
|
由于我们实现中的push函数返回一个我们关心的布尔值（推动是否"成功"），我们需要一种解析EVM输出的方法。execCall的类型是MonadState VM => SolCall -> m VMResult，所以我们需要一种检查给定VMResult是true、false还是完全其他的方法。这实际上非常简单。
1
2
3
|
match :: VMResult -> Bool -> Bool
match (VMSuccess (B s)) b = s == encodeAbiValue (AbiBool b)
match _ _ = False
|
现在我们可以检查推动的结果了，我们拥有编写模型其余部分所需的一切。和之前一样，我们将编写两个命令；分别模拟旋转门锁定时和解锁时的推动。锁定时推动应该失败，并导致旋转门保持锁定。解锁时推动应该成功，并使旋转门锁定。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
s_push_locked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState
s_push_locked = Command (\s -> if s == TLocked then Just $ pure Push else Nothing)
-- 我们只能在旋转门锁定时运行此命令
(\Push -> cleanUp >> execCall ("push", []))
-- 推动只是调用push()
[ Require $ \s Push -> s == TLocked
-- 在我们推动之前，旋转门应该是锁定的
, Update $ \_ Push _ -> TLocked
-- 在我们推动之后，旋转门应该是锁定的
, Ensure $ \before after Push b -> do before === TLocked
-- 和之前一样
assert (match b False)
-- 推动应该失败
after === TLocked
-- 和之前一样
]
s_push_unlocked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState
s_push_unlocked = Command (\s -> if s == TUnlocked then Just $ pure Push else Nothing)
-- 我们只能在旋转门解锁时运行此命令
(\Push -> cleanUp >> execCall ("push", []))
-- 推动只是调用push()
[ Require $ \s Push -> s == TUnlocked
-- 在我们推动之前，旋转门应该是解锁的
, Update $ \_ Push _ -> TLocked
-- 在我们推动之后，旋转门应该是锁定的
, Ensure $ \before after Push b -> do before === TUnlocked
-- 和之前一样
assert (match b True)
-- 推动应该成功
after === TLocked
-- 和之前一样
]
|
如果你能回忆起步骤0中的图像，可以将我们在那里枚举的状态视为形状，将我们在这里编写的转换视为箭头。我们的箭头还配备了一些关于必须满足的条件才能进行每个状态转换的严格不变式（这就是我们上面的Ensure）。现在我们有了一个完全描述我们状态机的语言，我们可以简单地描述它的语句如何组合来获得一个属性！
步骤2：编写一个属性
这种组合实际上相当简单，我们只是告诉Echidna顺序执行我们的动作，由于不变式被捕获在动作本身中，这就是测试所需的全部！现在我们唯一需要的是实际的测试对象，由于我们在任何MonadState VM中工作，它只是一个VM，我们可以将属性参数化。
1
2
3
4
5
6
7
|
prop_turnstile :: VM -> property
prop_turnstile v = property $ do
actions <- forAll $ Gen.sequential (Range.linear 1 100) initialState
[s_coin, s_push_locked, s_push_unlocked
-- 生成1到100个动作，从锁定（模型）旋转门开始
evalStateT (executeSequential initialState actions) v
-- 在给定的VM上顺序执行它们。
|
你可以将上面的代码视为一个函数，它接受一个EVM状态并返回一个hedgehog可检查的断言，即它实现了我们的（haskell）状态机定义。
步骤3：测试
有了这个编写的属性，我们准备好测试一些Solidity了！让我们启动ghci来用Echidna检查这个属性。
1
2
3
4
5
|
λ> (v,_,_) <- loadSolidity "solidity/turnstile/turnstile.sol" -- 设置一个加载了我们合约的VM
λ> check $ prop_turnstile v -- 检查我们刚刚定义的属性是否成立
✓ passed 10000 tests.
True
λ>
|
它工作了！我们编写的Solidity实现了我们的旋转门状态机模型。Echidna评估了10,000个随机调用序列，没有发现任何问题。
现在，让我们找一些失败。假设我们如下所示用解锁的旋转门初始化合约。这应该是一个相当容易检测的失败，因为现在有可能在不先投入硬币的情况下成功推动。
我们可以稍微修改我们的初始合约如下：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
contract Turnstile {
bool private locked = false; // 初始状态为解锁
function coin() {
locked = false;
}
function push() returns (bool) {
if (locked) {
return(false);
} else {
locked = true;
return(true);
}
}
}
|
现在我们可以使用与之前完全相同的ghci命令：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
λ> (v,_,_) <- loadSolidity "solidity/turnstile/turnstile_badinit.sol"
λ> check $ prop_turnstile v
✗ failed after 1 test.
┏━━ examples/state-machine/StateMachine.hs ━━━
49 ┃ s_push_locked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState
50 ┃ s_push_locked = Command (\s -> if s == TLocked then Just $ pure Push else Nothing)
51 ┃ (\Push -> cleanUp >> execCall ("push", []))
52 ┃ [ Require $ \s Push -> s == TLocked
53 ┃ , Update $ \_ Push _ -> TLocked
54 ┃ , Ensure $ \before after Push b -> do before === TLocked
55 ┃ assert (match b False)
┃ ^^^^^^^^^^^^^^^^^^^^^^
56 ┃ after === TLocked
57 ┃ ]
┏━━ examples/state-machine/StateMachine.hs ━━━
69 ┃ prop_turnstile :: VM -> property
70 ┃ prop_turnstile v = property $ do
71 ┃ actions <- forAll $ Gen.sequential (Range.linear 1 100) initialState 72 ┃ [s_coin, s_push_locked, s_push_unlocked] ┃ │ Var 0 = Push 73 ┃ evalStateT (executeSequential initialState actions) v This failure can be reproduced by running: > recheck (Size 0) (Seed 3606927596287211471 (-1511786221238791673))
False
λ>
|
正如我们所料，我们的属性不满足。第一次推动时应该失败，因为模型认为旋转门是锁定的，但它实际上成功了。这正是我们上面预期的结果！
我们也可以用其他有错误的合约尝试同样的事情。考虑下面的Turnstile，它在成功推动后不会锁定。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
contract Turnstile {
bool private locked = true; // 初始状态为锁定
function coin() {
locked = false;
}
function push() returns (bool) {
if (locked) {
return(false);
} else {
return(true);
}
}
}
|
让我们再次使用那些相同的ghci命令
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
λ> (v,_,_) <- loadSolidity "solidity/turnstile/turnstile_nolock.sol"
λ> check $ prop_turnstile v
✗ failed after 4 tests and 1 shrink.
┏━━ examples/state-machine/StateMachine.hs ━━━
49 ┃ s_push_locked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState
50 ┃ s_push_locked = Command (\s -> if s == TLocked then Just $ pure Push else Nothing)
51 ┃ (\Push -> cleanUp >> execCall ("push", []))
52 ┃ [ Require $ \s Push -> s == TLocked
53 ┃ , Update $ \_ Push _ -> TLocked
54 ┃ , Ensure $ \before after Push b -> do before === TLocked
55 ┃ assert (match b False)
┃ ^^^^^^^^^^^^^^^^^^^^^^
56 ┃ after === TLocked
57 ┃ ]
┏━━ examples/state-machine/StateMachine.hs ━━━
69 ┃ prop_turnstile :: VM -> property
70 ┃ prop_turnstile v = property $ do
72 ┃ [s_coin, s_push_locked, s_push_unlocked]
┃ │ Var 0 = Coin
┃ │ Var 1 = Push
┃ │ Var 3 = Push
73 ┃ evalStateT (executeSequential initialState actions) v
This failure can be reproduced by running:
> recheck (Size 3) (Seed 133816964769084861 (-8105329698605641335))
False
λ>
|
当我们投入硬币然后推动两次时，第二次应该失败。相反，它成功了。注意，在所有这些失败中，Echidna找到了展示失败行为的最小动作序列。这是因为Hedgehog的收缩功能，默认提供此行为。
更广泛地说，我们现在有一个工具，它将接受任意合约（实现push/coin ABI），检查它们是否正确实现了我们指定的状态机，如果没有，则返回一个最小化的 falsifying 反例。作为一个从事旋转门合约工作的Solidity开发者，我可以在每次提交时运行此程序，并获得发生的任何回归的简单解释。
concluding Notes
希望以上内容提供了一个使用Echidna进行测试的激励性示例。我们编写了一个状态机的简单描述，然后测试了四个不同的合约；每种情况要么产生了合约未实现该机器的最小化证明，要么提供了它确实实现的保证声明。
如果你想尝试自己对船闸实现这种测试，请使用我们为研讨会编写的这个练习。