您的位置:首頁 > 區(qū)塊鏈 >

實現(xiàn)基于Horn子句的檢查引擎 能提高SMTChecker的證明能力

2019-08-07 14:12:40 來源: 區(qū)塊網(wǎng)

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 )是合約的空閑狀態(tài),以下數(shù)字分別是狀態(tài)變量sum和count的當(dāng)前值。(fallback_42_0 )是對回退函數(shù)的調(diào)用。

(function_average_60_8 )是對函數(shù)平均值的調(diào)用。

在合約構(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

精選 導(dǎo)讀

募資55億港元萬物云啟動招股 預(yù)計9月29日登陸港交所主板

萬科9月19日早間公告,萬物云當(dāng)日啟動招股,預(yù)計發(fā)行價介乎每股47 1港元至52 7港元,預(yù)計9月29日登陸港交所主板。按發(fā)行1 167億股計算,萬

發(fā)布時間: 2022-09-20 10:39
管理   2022-09-20

公募基金二季度持股情況曝光 隱形重倉股多為高端制造業(yè)

隨著半年報披露收官,公募基金二季度持股情況曝光。截至今年二季度末,公募基金全市場基金總數(shù)為9794只,資產(chǎn)凈值為269454 75億元,同比上

發(fā)布時間: 2022-09-02 10:45
資訊   2022-09-02

又有上市公司宣布變賣房產(chǎn) 上市公司粉飾財報動作不斷

再有上市公司宣布變賣房產(chǎn)。四川長虹25日稱,擬以1 66億元的轉(zhuǎn)讓底價掛牌出售31套房產(chǎn)。今年以來,A股公司出售房產(chǎn)不斷。根據(jù)記者不完全統(tǒng)

發(fā)布時間: 2022-08-26 09:44
資訊   2022-08-26

16天12連板大港股份回復(fù)深交所關(guān)注函 股份繼續(xù)沖高

回復(fù)交易所關(guān)注函后,大港股份繼續(xù)沖高。8月11日大港股份高開,隨后震蕩走高,接近收盤時觸及漲停,報20 2元 股。值得一提的是,在7月21日

發(fā)布時間: 2022-08-12 09:56
資訊   2022-08-12

萬家基金再添第二大股東 中泰證券擬受讓11%基金股權(quán)

7月13日,中泰證券發(fā)布公告,擬受讓齊河眾鑫投資有限公司(以下簡稱齊河眾鑫)所持有的萬家基金11%的股權(quán),交易雙方共同確定本次交易的標(biāo)的資

發(fā)布時間: 2022-07-14 09:39
管理   2022-07-14

央行連續(xù)7日每天30億元逆回購 對債市影響如何?

央行12日再次開展了30億元逆回購操作,中標(biāo)利率2 10%。這已是央行連續(xù)7日每天僅進行30億元的逆回購縮量投放,創(chuàng)下去年1月以來的最低操作規(guī)

發(fā)布時間: 2022-07-13 09:38
資訊   2022-07-13

美元指數(shù)創(chuàng)近20年新高 黃金期貨創(chuàng)出逾9個月新低

由于對美聯(lián)儲激進加息的擔(dān)憂,美元指數(shù)11日大漲近1%創(chuàng)出近20年新高。受此影響,歐美股市、大宗商品均走弱,而黃金期貨創(chuàng)出逾9個月新低。美

發(fā)布時間: 2022-07-13 09:36
資訊   2022-07-13

美股三大股指全線下跌 納斯達(dá)克跌幅創(chuàng)下記錄以來最大跌幅

今年上半年,美股持續(xù)回落。數(shù)據(jù)顯示,道瓊斯指數(shù)上半年下跌15 3%,納斯達(dá)克綜合指數(shù)下跌29 5%,標(biāo)普500指數(shù)下跌20 6%。其中,納斯達(dá)克連續(xù)

發(fā)布時間: 2022-07-04 09:51
推薦   2022-07-04

融資客熱情回升 兩市融資余額月內(nèi)增加超344億元

近期A股走強,滬指6月以來上漲4%,融資客熱情明顯回升。數(shù)據(jù)顯示,截至6月16日,兩市融資余額1 479萬億元,月內(nèi)增加344 67億元,最近一個半

發(fā)布時間: 2022-06-20 09:41
資訊   2022-06-20

4個交易日凈買入超百億元 北向資金持續(xù)流入A股市場

北向資金凈流入態(tài)勢延續(xù)。繼6月15日凈買入133 59億元后,北向資金6月16日凈買入44 52億元。自5月27日至今,除6月13日以外,北向資金累計凈

發(fā)布時間: 2022-06-17 09:37
推薦   2022-06-17