solidity static analysis

靜態分析與殘留/商分析

基於https://github.com/shaunazzopardi/solity-cfg-builder和https://github.com/gordonpace/gordonpace/contractlarva，基於固體智能合約驗證的靜態分析。

概述

該工具試圖證明固體智能合約的特性，並且部分成功返回了殘留財產，尚待證明固體智能合約。

我們使用堅固智能合約的控制流圖表示，以試圖通過過度x型固定合同（基於固體cfg builder及其可變狀態）來證明智能合約的屬性。

這部分基於EPCTS系列Prepost 2017會議記錄中介紹的工作，並在ARXIV上獲得。

分析的詳細描述

1. 每個智能合約功能都表示為控制流動機（CFA），其過渡標記為三重包含：（i）程序變量狀態上的條件； （ii）一種轉換程序變量狀態的語句； （iii）在說明執行時激活的屬性事件。

2. 每個這樣的自動機都通過抽象過渡（僅由屬性事件標記）增強，該過渡允許在程序的初始，呼叫或結束狀態時發生任何事件。這被用作手術室內分析的基礎。每個這樣的自動機對調用相應函數的智能合約的所有執行都過度估計。該自動機稱為抽象控制流動自動機（ACFA）。

3. 一個簡單的斷言傳播算法通過CFA的明確狀態傳播了關於程序變量狀態（由條件和語句暗示的）的主張，直到遇到可能影響主張的語句為止。這是聲音。

4. 屬性表示為動態事件自動機（DEA），該屬性使用標記為以下三倍的過渡：（i）事件； （ii）屬性變量狀態的警衛； （iii）對屬性變量狀態的訴訟。

5. 具有可變抽象的ACFA由DEA組成，產生一個帶有CFA成對和DEA過渡對的過渡的抽象監視系統（AMS），或者俱有包含＃符號的位置之一。當使用＃而不是CFA過渡時，它標誌著抽象過渡的匹配，而當DEA過渡而不是DEA Trunce時，則表示沒有DEA過渡匹配。

6. 然後，針對程序的每個功能創建一個AMS，以給定的DEA。

7. 在AMS構建過程中，SMT求解器Z3被稱為即時稱為，以確定在實際運行中，給定的過渡是否有可能激活。給定CFA-DEA過渡對，我們檢查DEA Guard是否可以在CFA過渡的條件和說明的源狀態的可變抽像上保持真實。雖然給出了CFA-＃對，但我們檢查是否與CFA過渡的狀態和說明的源狀態的可變抽象與否定了此時可能激活的DEA過渡後衛的分離的否定不一致（請確保從相同的DEA狀態進行DEA轉變以使其具有相互限制的Guelards）。

8. 分析每個AM以識別CFA-DEA過渡對，提取以這種方式使用的DEA轉換，忽略DEA過渡與＃佔位符的匹配。這些DEA過渡的結合產生了原始DEA的殘差。有時可以通過對殘留DEA的語法​​分析進一步降低這。

9. 此外，從AMS中，我們可以確定何時可以刪除DEA過渡的後衛（即更改為true ），即何時可以在AMS中使用它。

10. 如果產生的殘留物沒有過渡，則已證明該財產。

限制

1. 我們沒有處理函數修改器和智能合約的繼承（內聯合所有內容以啟用分析）；
2. DEA腳本不完全支持：
   • DEA可變狀態被忽略（分析中僅考慮程序狀態的條件）；
   • 僅支持腳本的“ DEA {...}”部分；
3. 到達呼叫狀態刪除了有關該計劃狀態的所有已知斷言；
4. V0.4。 *堅固代碼。

要求

1. （必需）Z3可在路徑中執行（以證明有關智能合約的斷言）；
2. （可選）GraphViz（可視化CFA，ACFA和AMS），或使用http://webgraphviz.com/。

構建工具

要求：Cabal v2.4。 *（例如安裝完整的Haskell平台）

彙編：按照此處的說明

使用工具：

為了正確的結果，請務必確保使用堅固的編譯器編譯實體代碼。

要使用該工具，請通過智能合約固體文件，DEA屬性文件的位置以及輸出的首選位置，例如執行：

./main“ ./examples/courierservice.sol”。

執照

該項目是根據Apache 2.0許可證的條款獲得許可的。