同功能重入漏洞檢測

http://pages.cpsc.ucalgary.ca/~joel.reardon/blockchain/readings/ndss2018_09-1_Kalra_paper.pdf我正在閱讀 [ ]中討論的 Zeus 工具對相同功能重入的檢測。他們已經完成了複製。我無法理解這種方法。由於我們正在修改 SC，這是測試智能合約 (SC) 的有效方法嗎？我們可以在測試期間修改 SC 嗎？

論文說：

Solidity 中的重入可以通過 call 方法發生。send 僅呼叫具有有限氣體的預設函式以用於記錄目的。ZEUS 通過首先複製正在考慮的函式，並在呼叫呼叫之前插入對複製的呼叫來處理相同函式的重入。圖 14 顯示了圖 2 中範例的修補函式。請注意，ZEUS 確保修補是在同一基本塊內完成的，以確保如果呼叫複製的函式，那麼也會呼叫 call。此外，我們還在呼叫程式碼之前斷言 false。如果驗證者找到通向此斷言的路徑，則表明存在錯誤。

有人請幫我理解

在這種情況下，他們會驗證正確性，作者將其定義為

遵守安全程式實踐

他們有效測試的是重入漏洞的根本原因：不遵守檢查 - 效果 - 互動模式。

以他們的範常式式碼為例：

function withdrawBalance() {
   uint amountToWithdraw = userBalances[msg.sender];

   // CHECK
   if (amountToWithdraw > 0) {
       // INTERACTION
       withdrawBalance’();
       msg.sender.call(userBalances[msg.sender]);
       // EFFECT
       userBalances[msg.sender] = 0;
   }
}

不尊重範式，這裡是檢查 - 互動 - 效果。這意味著惡意攻擊者可能會withdrawBalance通過實現withdrawBalance再次呼叫的回退函式來從自身呼叫。

因此，呼叫堆棧將是：

• 提款餘額
• 備份功能
• 提款餘額

執行withdrawBalance兩次，因此在應該禁止的地方撤回兩次。他們的複製方法人為地創建了一條可能允許重入攻擊的路徑。

如果驗證者找到通向此斷言的路徑，則表明存在錯誤。

確實，如果可以利用該路徑，則在我們的範例中存在諸如雙重退出之類的漏洞。如果尊重正確的程式實踐，則此路徑不應該是可利用的。

現在看這個稍微修改的例子，和以前一樣，但只是尊重 CHECK - EFFECT - INTERACTION 模式：

function withdrawBalance() {
   uint amountToWithdraw = userBalances[msg.sender];

   // CHECK
   if (amountToWithdraw > 0) {
       // EFFECT
        userBalances[msg.sender] = 0;
       // INTERACTION
       withdrawBalance’();
       msg.sender.call(userBalances[msg.sender]);
   }
}

再一次，我們包含對複製函式的呼叫，但它創建的路徑是不可利用的，因為租借攻擊不會通過檢查步驟 ( if (amountToWithdraw > 0))，因為效果 ( userBalances[msg.sender] = 0;) 是在互動步驟之前應用的。

由於我們正在修改 SC，這是測試智能合約 (SC) 的有效方法嗎？我們可以在測試期間修改 SC 嗎？

您可以親眼看到它在這些範例中是有效的。它確實略微修改了原始函式流程，並添加了少量氣體成本，但它允許顯式檢測相同的函式重入漏洞，這是預期目標。

只要您的測試不改變智能合約的邏輯或任何不變數，就可以了。這種複製方法不會改變任何這些（至少在這個例子中）。

在某些範例中，此方法不起作用並且無意中乾擾了智能合約邏輯/不變數，在您期望使用 X 氣體呼叫的地方採用類似的函式，並期望在退出您的函式或恢復之前留下 Y 氣體，他們檢測方法的 gas 成本會破壞你的合約邏輯。

然而，這將是一個不好的做法，因為您不應該假設操作碼的氣體成本在時間上是恆定的。但它表明，這種複製方法雖然大部分是正確的，但並不總是正確的。

引用自：https://ethereum.stackexchange.com/questions/116919