隨著區塊鏈技術迅速的發展，乙太坊的應用越來越接近我們的生活，乙太坊提供平台給使用者開發屬於自己的應用(智能合約)，使用者可以利用智能合約來實現不同領域的應用，包括保險理賠、樂透彩券領獎…等，由於現今大部分乙太坊的應用皆跟資金的交易有相關，所以如果應用中的程式碼存在著重大的安全性漏洞，並遭到駭客攻擊，往往會造成重大的損失，因此現今有許多的論文在研究要如何驗證智能合約的安全性，研究何種驗證方式能夠確實的捕獲合約中的安全性漏洞。
當驗證完後的智能合約會交由乙太坊虛擬機(EVM)來執行合約程式碼，此時如果虛擬機內部實現有錯誤的話，合約執行出來的結果仍然是錯的，因此確保負責執行智能合約的虛擬機之正確性就顯得非常重要。本論文將依照乙太坊虛擬機的規範(乙太坊黃皮書)來驗證EVM的指令實現是否正確，同時我們設計一組用於驗證EVM的驗證接口，並且我們所編寫的驗證 指令之property皆以該接口的命名方式來編寫，藉此方法可以達到不同的EVM設計可以重複使用我們的property在我們的驗證平台上進行指令的驗證，提高驗證環境的重複使用性(reusability)。
透過本篇論文提出的正規驗證流程，我們在一個開源的EVM上進行指令驗證，並且該EVM指令的驗證結果皆為正確(指令集當中的92個指令)。最後藉由在EVM的指令實現中植入錯誤，並且該錯誤是過去虛擬機指令驗證方式(Ethereum Testsuite)所檢測不到的，但是使用本篇論文所提出的正規方法來驗證則能夠捕獲設計中的錯誤，有此可知，本篇論文提出的EVM指令驗證方法能夠補足testsuite在其他EVM實現中會有corner case驗證不到的可能性。

In recent years, many smart contracts on the ethereum platform are increasingly closer to our life. The existence of smart contract enables us to complete complicated transactions without depending on the third party. It should be not only fast, but also secure guaranteed. When the smart contract is requested to execute, the action is performed by ethereum virtual machine (EVM). If EVM occurs errors in the process of implementation, the contract execution result will also have mistaken. Therefore, ensuring the correctness of the EVM is very important. In this work, we propose a framework to formally verify EVM instruction implementations by model checking to check whether the instruction operation behaviors working on EVM is the same as the expected definitions in the ethereum yellow paper. In addition, we also define a set of interfaces specifically for EVM instruction verification to achieve the reusability of our proposed verification environment. The experimental results indicate that the formal verification method used in this work is more trustworthy than the conventional testing method. It can exactly capture the errors in the design which may be undetected by testing/simulation methods. The defined instructions are divided into 11 categories, and our work has completed to verify 7 categories, including 92 instructions of total 134.

[1] L. Alt and C. Reitwiessner, "Smt-based verification of solidity smart contracts," in International Symposium on Leveraging Applications of Formal Methods, 2018: Springer, pp. 376-388.
[2] Y. Hirai, "Defining the ethereum virtual machine for interactive theorem provers," in International Conference on Financial Cryptography and Data Security, 2017: Springer, pp. 520-535.
[3] A. Reid et al., "End-to-end verification of processors with ISA-formal," in International Conference on Computer Aided Verification, 2016: Springer, pp. 42-58.
[4] Ethereum Yellow Paper [Online]. Available:
https://ethereum.github.io/yellowpaper/paper.pdf.
[5] Ethereum Consensus Tests [Online]. Available:
https://github.com/ethereum/tests.
[6] CBMC [Online]. Available: https://www.cprover.org/cbmc/.
[7] R. Metta, "Verifying code and its optimizations: An experience report," in 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops, 2011: IEEE, pp. 578-583.
[8] A. Miller, Z. Cai, and S. Jha, "Smart contracts and opportunities for formal methods," in International Symposium on Leveraging Applications of Formal Methods, 2018: Springer, pp. 280-299.
[9] blockchain introduced [Online]. Available: https://www.mile.cloud/zh-hant/whatis-blockchain/.
[10] smart contract introduction [Online]. Available:
https://blog.gasolin.idv.tw/2017/09/02/what-is-smart-contract/.
[11] Ethereum Virtual Machine introduction [Online]. Available:
https://blog.csdn.net/TurkeyCock/article/details/83786471.
[12] Aleth – Ethereum C++ client, tools and libraries [Online]. Available:
https://github.com/ethereum/aleth.
[13] pyethapp : pyethapp is the python based client implementing the Ethereum cryptoeconomic state machine. [Online]. Available:
https://github.com/ethereum/pyethapp.
[14] Go Ethereum : Official Golang implementation of the Ethereum protocol [Online]. Available: https://github.com/ethereum/go-ethereum.
[15] Testsuite of Ethereumj : Comparison & Bitwise Logic Operations Part [Online]. Available: https://github.com/ethereum/ethereumj/blob/develop/ethereumjcore/src/test/java/org/ethereum/vm/VMBitOpTest.java.
[16] Testsuite of Cpp-Ethereum : Comparison & Bitwise Logic Operations Part [Online]. Available:
https://github.com/ethereum/tests/tree/a0c430053817ff5cf1023d1bf4b70e5538073490/VMTests/vmBitwiseLogicOperation.