【摘要】 实现基于Horn子句的检查引擎 能提高SMTChecker的证明能力
SMTChecker当前模型检查引擎是安全但还不是很完整的。这意味着报告为安全的断言和其他验证目标应该是安全的 - 除非SMTChecker或后端解算器中存在bug-但是误报可能是虚假的抽象。
当前引擎给出的反例中的两个主要误报源是：
· 循环以有界的方式处理(只考虑一次迭代)。
· 函数在各自的环境中单独分析。
因此在SMTChecker分析时，依赖于程序逻辑循环或在不同函数中使用状态变量的智能合约可能会导致误报。
为了提高SMTChecker的证明能力并减少误报，我们最近实现了一个基于Horn子句系统的新模型检查引擎，能够推理循环和状态变量之间的关系。请注意，智能合约的生命周期也可以建模为以下循环，其中每个循环迭代都是一个事务：
constructor(...);
while(true)
random_public_function(...);
新引擎的目标是自动推断循环和状态不变量，同时尝试证明安全属性，消除了前面写的额外假设的需要。
我们可以通过分析前一篇文章中的相同合同立即看到结果，而无需额外的假设：
pragma experimental SMTChecker;
contract C {
uint sum;
uint count;
function () external payable {
require(msg.value > 0);
// Avoid overflow.
require(sum + msg.value >= sum);
require(count + 1 > count);
sum += msg.value;
++count;
}
function average() public returns (uint) {
require(count > 0);
uint avg = sum / count;
assert(avg > 0);
return avg;
}
}
SMTChecker现在试图证明断言考虑整个合同和无限数量的交易，而不是仅执行一次函数平均。它自动学习合约不变量(count> 0)=>((sum / count)> 0)，它保存在每个函数的开头和结尾，并且能够证明所需的属性。我的笔记本电脑上的支票需要0.16秒。
如果我们用uint avg = count / sum替换除法，这显然打破了断言，我们得到以下反例：
(and
(function_average_68_0 2 1 0 0)
(interface_C_69_0 2 1)
(fallback_42_0 0 0 2)
(interface_C_69_0 0 0)
)
这是多事务自下而上路径的内部表示，导致断言失败的地方
(interface_C_69
(function_average_60_8
在合约构造之后，sum和count都是0.第一个事务使用msg.value = 2调用回退函数，这导致sum = 2和count = 1.第二个事务调用函数average，其中(count / sum)= 0。检查需要0.14秒。
除了合约不变量之外，引擎还尝试总结while和for循环内部的函数。它可以很快证明关于循环行为的简单属性，但问题也很容易变得太难。记住，这是一个不可判定的问题:)
function f(uint x) public pure {
uint y;
require(x > 0);
while (y < x)
++y;
assert(y == x);
}
上述断言在0.05s内得到证实。
function f() public pure {
uint x = 10;
uint y;
while (y < x)
{
++y;
x = 0;
while (x < 10)
++x;
assert(x == 10);
}
assert(y == x);
}
上面的断言涉及一个更复杂的结构和嵌套的循环，并在0.375中得到证明。
uint[] a;
function f(uint n) public {
uint i;
while (i < n)
{
a[i] = i;
++i;
}
require(n > 1);
assert(a[n-1] > a[n-2]);
}
即使上面的代码也使用数组，断言只涉及数组的两个元素，检查只需0.16秒。
function max(uint n, uint[] memory _a) public pure returns (uint) {
require(n > 0);
uint i;
uint m;
while (i < n) {
if (_a[i] > m)
m = _a[i];
++i;
}
i = 0;
while (i < n) {
assert(m >= _a[i]);
++i;
}
return m;
}
上面的函数计算并返回数组的最大值。数组的长度作为参数给出，因为.length尚不支持。这种检查要复杂得多，因为它检查计算出的最大值是否确实大于或等于无界数组的所有元素。
编辑：在写这篇文章时，这个断言序列在1小时超时后无法证明。调整一些量化求解器参数后，检查在0.13秒后成功!
如果我们将断言更改为断言(m> _a [i])，则给定的反例是数组[0,0]。
另一个与状态机更相似的例子是以下Crowdsale架构：
pragma experimental SMTChecker;
contract SimpleCrowdsale {
enum State { INIT, STARTED, FINISHED }
State state = State.INIT;
uint weiRaised;
uint cap;
function setCap(uint _cap) public {
require(state == State.INIT);
require(_cap > 0);
cap = _cap;
state = State.STARTED;
}
function () external payable {
require(state == State.STARTED);
require(msg.value > 0);
uint newWeiRaised = weiRaised + msg.value;
// Avoid overflow.
require(newWeiRaised > weiRaised);
// Would need to return the difference to the sender or revert.
if (newWeiRaised > cap)
newWeiRaised = cap;
weiRaised = newWeiRaised;
}
function finalize() public {
require(state == State.STARTED);
assert(weiRaised <= cap);
state = State.FINISHED;
}
}
当state为INIT时，函数setCap只能调用一次。 当state为STARTED时，后备函数接受多个存款(在此模拟中不发出令牌)。 Crowdsale可以在函数finalize中最终确定，它确保不会破坏cap。
分析自动学习不变的weiRaised <= cap，证明了断言。 检查需要0.09秒。
如果我们将正确的断言更改为断言(weiRaised
(and
(function_finalize_107_0 1 1 1)
(interface_SimpleCrowdsale_108_0 1 1 1)
(fallback_85_0 1 0 1 0)
(interface_SimpleCrowdsale_108_0 1 0 1)
(function_setCap_42_0 0 0 0 1)
(interface_SimpleCrowdsale_108_0 0 0 0)
)
这种自下而上的内部表示遵循与第一个示例中所示格式相同的格式。 所有状态变量都从0开始。第一个tx调用setCap(1)，它导致state = State.START和cap = 1.第二个tx用msg.value = 1调用回退函数，它将weiRaised修改为1.最后， 第三个tx调用finalize并且断言失败。 检查需要0.08秒。
这些初步实验表明新引擎可能能够合理地快速地自动证明涉及多tx行为的复杂属性。（链三丰）