Solidity的SMTchecker現在支援多事務檢查和無邊界迴圈
By 區塊鏈研究實驗室·
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 <sum> <count>)是合約的空閒狀態,以下數字分別是狀態變數sum和count的當前值。(fallback_42_0 <sum> <count> <msg.value>)是對回退函式的呼叫。(function_average_60_8 <sum> <count> <return_value> <avg>)是對函式平均值的呼叫。在合約構造之後,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 <cap); 我們得到以下3個交易的反例:(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行為的複雜屬性。#Solidity#SMTchecker#Github
免責聲明:
- 本文版權歸原作者所有,僅代表作者本人觀點,不代表鏈報觀點或立場。
- 如發現文章、圖片等侵權行爲,侵權責任將由作者本人承擔。
- 鏈報僅提供相關項目信息,不構成任何投資建議。
推荐阅读