（請注意，此行為特定於EVM。在可以識別不存在的帳戶並禁止其收取資金的其他VM中，該錯誤可能並不存在。）
形式驗證可以幫助嗎？
現在讓我們解釋一下如何透過正式驗證，尤其是在EVM位元組碼級別的驗證來發現Gridlock錯誤。
形式驗證的基本過程之一是透過符號執行來探索給定程式的所有可能行為（在這種情況下為Lockdrop合同的EVM位元組碼）。在這裡，我們使用KEVM驗證程式來象徵性地執行位元組碼。長話短說，上述lock函式位元組碼的符號執行將產生以下行為（例如由於用盡gas而導致的功能故障）。
1. 如果在新帳戶地址上已經存在一個帳戶，且現有帳戶的程式碼為非空或其現時值為非零，則還原（由於第3行的新合同建立失敗）。
2. 還原（由於第5行斷言失敗），如果新帳戶地址上已經存在一個帳戶，現有帳戶的程式碼為空，其現時值為0，餘額為非零。
3. 成功終止後，如果在新帳戶地址上已經存在一個帳戶，該帳戶的現有程式碼為空，其現時數為零，其餘額為零。 （如果現有帳戶為非空，則清除其儲存。）
4. 如果新帳戶地址沒有帳戶，則成功終止。
（注意，第三個和第四個行為需要更多的條件，例如沒有用完gas，或者正確地給出了列舉型別引數，但是為了簡單起見，我們在這裡省略了它們。）
一旦研究了合同的所有可能行為，下一個重要步驟便是仔細檢查每種行為，以確保它是有意或無意的，否則就很難被利用。確實在上述四種可能的行為中，只希望有第四種，並且我們需要分析其他行為以檢查它們是否可利用。
如果可以利用第一行為和第二行為，則可以將其用於DoS攻擊。但是，據我們所知，第一個行為幾乎是無法利用的，因為在密碼上很難在給定的特定地址建立合約帳戶（即具有非空程式碼的帳戶）。 （為此，需要使用CREATE2操作碼來查詢對應於特定地址的鹽，這與查詢SHA3雜湊的原像一樣困難。）但是第二種行為是可利用的，因為可以輕鬆地啟動一個如前所述，只需向其傳送一些以太幣即可在任何特定地址的非合同賬戶（即無程式碼的賬戶）。
另一方面，第三種行為（如果可以利用）可以用來耗盡其他人的“locked”以太幣，這確實是致命的。然而據我們所知，由於與第一種情況相似的原因，它幾乎無法被利用。 （一個人可以很容易地在一個特定的地址“啟動”一個帳戶，但是很難“擁有”該帳戶，因為這需要找到金鑰。）
綜上所述，對lock函式節碼的符號執行可能揭示了這三種不良行為，並且仔細檢查它們可能發現其中一種可被DoS攻擊利用，從而在部署之前修復了Gridlock錯誤。
吸取教訓
EVM通常是不直觀的。
Gridlock錯誤源自對EVM設計中某些非顯而易見部分的錯誤理解。如果不考慮EVM級別的智慧合約，就很容易錯過這種EVM問題，並且可能會再次引入類似的bug。
形式驗證可以提供幫助。
如果不採用有原則的方法，那麼探索所有可能的行為（尤其是在EVM級別）並非易事。形式驗證，尤其是它的符號執行過程，可以系統地探索給定智慧合約的所有可能行為，這比僅手工檢查程式碼要嚴格得多。
具體來說，我們的KEVM驗證程式使用的是EVM的確切規範（又稱KEVM），不會讓您擺脫錯誤的假設。如上所示，它甚至會發現執行路徑非常不可能，例如攻擊者找到雜湊的預映像並將其合同部署到下一個地址的情況。
形式驗證不是萬靈丹。
雖然形式驗證引導我們系統地探索和嚴格地推理給定程式的所有可能行為，實際上，它是找到程式的關鍵問題的最終途徑，如果有的話，它仍然需要大量的人工努力，有時在智力上具有挑戰性。例如即使我們自動找到了lock函式的三個不良行為，我們仍然需要手動地對它們的可利用性進行推理，這是非常重要的，並且需要安全專業知識。必須確保在手動推理過程中不遺漏任何關鍵細節。
