Debugging Smart Contract’s Business Logic Using Symbolic Model Checking

使用符號邏輯檢查為智慧合約的商業邏輯debug

(InfoTeCS, Russia)

智慧合約是一種在區塊鏈上執行的特殊程式。它不可更改、透明，為實現容錯性、審查容忍性服務提供了一種可能的實現方式。不幸的是，它的不可更改性導致智慧合約必須在釋出到區塊鏈上之前做好商業邏輯正確性的檢測，而這是很困難的。幾宗大型的事故已表明，智慧合約的使用者有必要使用專門的工具來驗證智慧合約的正確性。現有的自動檢測工具只能發現已知的實現bug，但是不能檢查商業邏輯是否正確。本文提出了一個符號邏輯檢查技術，可用於一類solidity程式，以展示程式的狀態資訊和跡資訊，後者其實是某種弱“時空”資訊。我們對所提出的技術在MiniDAO智慧合約上做了評測。我們的方法能在幾秒鐘內檢測到這個合約中存在的非平凡的商業邏輯錯誤。