SMTChecker當前模型檢查引擎是安全但還不是很完整的。這意味著報告為安全的斷言和其他驗證目標應該是安全的 - 除非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行為的復雜屬性。（鏈三豐）
關鍵詞： Horn子句 檢查引擎 SMTChecker
