針對 Solidity 智能合約的抽象語法樹差異分析工具：SoliDiffy

แนวคิดหลัก

SOLIDIFFY 是一種針對 Solidity 智能合約設計的新型抽象語法樹 (AST) 差異分析工具，透過產生精確且簡潔的編輯腳本，實現對智能合約修改的精細分析，有助於漏洞偵測、自動程式碼修復和程式碼審查等下游任務。

บทคัดย่อ

SOLIDIFFY：針對 Solidity 智能合約的抽象語法樹差異分析工具

本文介紹了 SOLIDIFFY，這是一款專為 Solidity 智能合約量身打造的新型抽象語法樹 (AST) 差異分析工具。SOLIDIFFY 透過產生準確且簡潔的智能合約編輯腳本，實現精細的分析，使其成為漏洞偵測、自動程式碼修復和程式碼審查等下游任務的理想選擇。透過對大型真實 Solidity 合約數據集進行的全面評估表明，與最先進的工具相比，SOLIDIFFY 能夠提供更短、更精確的編輯腳本，同時在處理複雜的合約修改方面表現一致。SOLIDIFFY 已公開發布於 https://github.com/mojtaba-eshghie/SoliDiffy。

智能合約是透過將合約條款直接編碼到程式碼中來實現真實世界合約的自我執行程式。這些程式部署在區塊鏈平台（如以太坊）上，允許自動化且去信任化的交易。Solidity 作為一種靜態類型的程式語言，已成為開發這些智能合約的最熱門選擇。
開發人員在使用 Solidity 時，可以在多種情況下從精細的原始碼差異分析中受益匪淺。例如，當更新智能合約以修補安全漏洞時，基於抽象語法樹 (AST) 的差異分析允許開發人員精確定位程式碼結構中的特定變化，而不是逐行檢查文本變化，因為逐行檢查可能會遺漏細微但至關重要的修改。在將更新部署到不可變的區塊鏈上之前，這種精確性對於審查更新的正確性和安全含義至關重要。其他例子包括自動化除錯和程式修復，這些工具需要偵測錯誤和漏洞，並在語法層面上建議更改；精細的差異分析使這些工具能夠產生與程式碼語義意圖一致的精確編輯腳本，從而幫助實現自動化和上下文感知的修復。此外，在程式碼克隆偵測中，需要識別語法相似但不完全相同的程式碼塊，AST 差異分析可以準確捕捉基於行的工具所忽略的變化，從而增強對潛在程式碼重用或重複問題的偵測。
傳統的文本和結構差異分析工具不足以用於智能合約，因為它們無法捕捉智能合約的語義和結構細節，或者缺乏對 Solidity 的支援。針對 Solidity 智能合約的 AST 差異分析提供了一種在語法層面上偵測變化的更精細方法。

ข้อมูลเชิงลึกที่สำคัญจาก

SoliDiffy: AST Differencing for Solidity Smart Contracts

by Mojt... ที่ arxiv.org 11-13-2024

https://arxiv.org/pdf/2411.07718.pdf

สอบถามเพิ่มเติม

SOLIDIFFY 如何與其他程式分析技術（如符號執行或模糊測試）整合，以進一步加強智能合約的安全性？

SOLIDIFFY 可以作為其他程式分析技術的強大前置或補充工具，特別是針對智能合約安全性的符號執行和模糊測試：
與符號執行的整合：

縮小分析範圍： SOLIDIFFY 可以精確識別智能合約版本之間的差異，讓符號執行工具集中分析修改過的部分，而非整個合約，從而提高效率並降低分析的複雜性。
生成目標約束： SOLIDIFFY 的編輯腳本可以轉換為針對特定修改部分的約束條件，引導符號執行工具更有效地探索潛在的漏洞路徑。例如，針對新增或修改的狀態變數，可以生成約束條件，檢查其在不同交易順序和輸入下的行為。
增量式分析： SOLIDIFFY 可以支持智能合約的增量式符號執行。當合約更新時，只需分析差異部分，而無需重新分析整個合約，從而節省時間和資源。
與模糊測試的整合：

生成變異輸入： SOLIDIFFY 可以識別修改過的函數和參數，幫助模糊測試工具生成更有針對性的測試用例，重點測試修改部分的邏輯和潛在漏洞。
提高漏洞覆蓋率： 通過分析 SOLIDIFFY 識別的修改，模糊測試工具可以調整變異策略，生成更可能觸發新漏洞的輸入，提高漏洞檢測的覆蓋率。
減少測試用例數量： SOLIDIFFY 可以幫助模糊測試工具排除與未修改部分相關的測試用例，減少測試用例的數量，同時保持較高的漏洞檢測能力。
總之，SOLIDIFFY 與符號執行和模糊測試的整合可以實現更精確、高效和全面的智能合約安全分析，降低開發成本，並提高智能合約的整體安全性。

如果 SOLIDIFFY 產生的編輯腳本仍然過於冗長或難以人類開發人員理解，那麼如何進一步優化 SOLIDIFFY 的剪枝規則和差異分析演算法？

如果 SOLIDIFFY 產生的編輯腳本過於冗長或難以理解，可以通過以下方式優化其剪枝規則和差異分析演算法：
優化剪枝規則：

語義化剪枝： 當前 SOLIDIFFY 主要進行語法層面的剪枝。可以引入語義分析，識別並移除對合約邏輯無實際影響的語法差異，例如僅僅是變數名或註釋的修改。
可配置化剪枝： 允許開發者根據需求配置剪枝規則，例如設定忽略特定類型節點的差異，或設置差異的粒度级别，控制編輯腳本的詳細程度。
基於模式的剪枝： 分析常見的 Solidity 代码修改模式，設計專門的剪枝規則，例如針對常見的重構操作（如提取函數、變更變數聲明位置等）進行優化，生成更簡潔易懂的編輯腳本。
優化差異分析演算法：

語義感知的差異分析： 將語義信息融入差異分析過程，例如識別循環不變式、函數的副作用等，更準確地判斷代码修改的意圖，避免產生冗余的編輯操作。
基於抽象語義樹（ASG）的差異分析： 與抽象語法樹相比，ASG 更能體現代码的語義信息，例如變數的定義和使用、函數調用關係等。基於 ASG 的差異分析可以生成更精確、更易理解的編輯腳本。
結合機器學習的差異分析： 利用機器學習技術，學習 Solidity 代码的修改模式和最佳編輯腳本表示方法，自動生成更簡潔、更易理解的編輯腳本。
其他優化方向：

編輯腳本可視化： 開發更直觀的編輯腳本可視化工具，例如以圖形化方式展示代码修改前後的差異，幫助開發者更輕鬆地理解編輯腳本。
編輯腳本摘要： 自動生成編輯腳本摘要，提煉出代码修改的核心信息，方便開發者快速了解修改的內容和影響。
通過以上優化，可以使 SOLIDIFFY 產生的編輯腳本更加簡潔、易懂，更方便開發者理解和使用，從而更好地服務於智能合約的安全性分析和維護。

除了程式碼差異分析之外，還有哪些其他方法可以利用 AST 來分析和理解智能合約的行為和安全性？

除了程式碼差異分析，AST 還可以應用於以下方面，以分析和理解智能合約的行為和安全性：
1. 漏洞模式檢測:

構建漏洞模式的 AST 表示: 將已知的智能合約漏洞抽象成 AST 模式，例如重入漏洞、整數溢出漏洞等。
基於 AST 匹配的漏洞檢測: 利用 AST 匹配算法，在智能合約的 AST 中搜索是否存在與漏洞模式匹配的子樹，快速識別潛在的漏洞。
2. 合約功能提取和分析:

識別關鍵 AST 節點: 提取合約中的關鍵信息，例如狀態變數、函數定義、事件定義等，構建合約的功能模型。
分析函數控制流程和數據流: 基於 AST 分析函數的控制流程圖和數據流圖，理解函數的邏輯和數據處理過程，識別潛在的安全風險。
3. 合約形式化驗證:

將 Solidity AST 轉換為形式化規範語言: 例如 F*、Coq 等，將智能合約轉換為形式化模型。
利用定理證明器驗證合約屬性: 證明合約滿足預期安全性和功能性需求，例如資金安全、狀態一致性等。
4. 合約自動生成和優化:

基於 AST 的合約模板: 設計安全可靠的合約模板，開發者可以通過修改 AST 模板快速生成滿足特定需求的智能合約。
基於 AST 的合約自動優化: 例如，自動識別並移除冗余代码、優化 gas 消耗等，提高合約的效率和安全性。
5. 合約相似性分析:

計算 AST 相似度: 利用樹編輯距離等算法，計算不同智能合約的 AST 相似度，識別潛在的代码抄襲和安全風險。
基於 AST 的合約聚類: 根據 AST 相似度對智能合約進行聚類分析，了解不同類型合約的功能和安全特性。
總之，AST 作為智能合約的結構化表示，為深入分析和理解智能合約提供了豐富的信息。除了程式碼差異分析，還可以利用 AST 進行漏洞模式檢測、功能提取、形式化驗證、自動生成和優化、相似性分析等，多角度提升智能合約的安全性。