SMTChecker當(dāng)前模型檢查引擎是安全但還不是很完整的。這意味著報告為安全的斷言和其他驗證目標(biāo)應(yīng)該是安全的 - 除非SMTChecker或后端解算器中
SMTChecker當(dāng)前模型檢查引擎是安全但還不是很完整的。這意味著報告為安全的斷言和其他驗證目標(biāo)應(yīng)該是安全的 - 除非SMTChecker或后端解算器中存在bug-但是誤報可能是虛假的抽象。
當(dāng)前引擎給出的反例中的兩個主要誤報源是：
· 循環(huán)以有界的方式處理(只考慮一次迭代)。
· 函數(shù)在各自的環(huán)境中單獨分析。
因此在SMTChecker分析時，依賴于程序邏輯循環(huán)或在不同函數(shù)中使用狀態(tài)變量的智能合約可能會導(dǎo)致誤報。
為了提高SMTChecker的證明能力并減少誤報，我們最近實現(xiàn)了一個基于Horn子句系統(tǒng)的新模型檢查引擎，能夠推理循環(huán)和狀態(tài)變量之間的關(guān)系。請注意，智能合約的生命周期也可以建模為以下循環(huán)，其中每個循環(huán)迭代都是一個事務(wù)：
constructor(...);
while(true)
random_public_function(...);
新引擎的目標(biāo)是自動推斷循環(huán)和狀態(tài)不變量，同時嘗試證明安全屬性，消除了前面寫的額外假設(shè)的需要。
我們可以通過分析前一篇文章中的相同合同立即看到結(jié)果，而無需額外的假設(shè)：
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現(xiàn)在試圖證明斷言考慮整個合同和無限數(shù)量的交易，而不是僅執(zhí)行一次函數(shù)平均。它自動學(xué)習(xí)合約不變量(count> 0)=>((sum / count)> 0)，它保存在每個函數(shù)的開頭和結(jié)尾，并且能夠證明所需的屬性。我的筆記本電腦上的支票需要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)
)
這是多事務(wù)自下而上路徑的內(nèi)部表示，導(dǎo)致斷言失敗的地方
(interface_C_69
(function_average_60_8
在合約構(gòu)造之后，sum和count都是0.第一個事務(wù)使用msg.value = 2調(diào)用回退函數(shù)，這導(dǎo)致sum = 2和count = 1.第二個事務(wù)調(diào)用函數(shù)average，其中(count / sum)= 0。檢查需要0.14秒。
除了合約不變量之外，引擎還嘗試總結(jié)while和for循環(huán)內(nèi)部的函數(shù)。它可以很快證明關(guān)于循環(huán)行為的簡單屬性，但問題也很容易變得太難。記住，這是一個不可判定的問題:)
function f(uint x) public pure {
uint y;
require(x > 0);
while (y < x)
++y;
assert(y == x);
}
上述斷言在0.05s內(nèi)得到證實。
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);
}
上面的斷言涉及一個更復(fù)雜的結(jié)構(gòu)和嵌套的循環(huán)，并在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]);
}
即使上面的代碼也使用數(shù)組，斷言只涉及數(shù)組的兩個元素，檢查只需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;
}
上面的函數(shù)計算并返回數(shù)組的最大值。數(shù)組的長度作為參數(shù)給出，因為.length尚不支持。這種檢查要復(fù)雜得多，因為它檢查計算出的最大值是否確實大于或等于無界數(shù)組的所有元素。
編輯：在寫這篇文章時，這個斷言序列在1小時超時后無法證明。調(diào)整一些量化求解器參數(shù)后，檢查在0.13秒后成功!
如果我們將斷言更改為斷言(m> _a [i])，則給定的反例是數(shù)組[0,0]。
另一個與狀態(tài)機更相似的例子是以下Crowdsale架構(gòu)：
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;
}
}
當(dāng)state為INIT時，函數(shù)setCap只能調(diào)用一次。 當(dāng)state為STARTED時，后備函數(shù)接受多個存款(在此模擬中不發(fā)出令牌)。 Crowdsale可以在函數(shù)finalize中最終確定，它確保不會破壞cap。
分析自動學(xué)習(xí)不變的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)
)
這種自下而上的內(nèi)部表示遵循與第一個示例中所示格式相同的格式。 所有狀態(tài)變量都從0開始。第一個tx調(diào)用setCap(1)，它導(dǎo)致state = State.START和cap = 1.第二個tx用msg.value = 1調(diào)用回退函數(shù)，它將weiRaised修改為1.最后， 第三個tx調(diào)用finalize并且斷言失敗。 檢查需要0.08秒。
這些初步實驗表明新引擎可能能夠合理地快速地自動證明涉及多tx行為的復(fù)雜屬性。（鏈三豐）
關(guān)鍵詞： Horn子句 檢查引擎 SMTChecker
