以太坊以區塊鍊技術為基礎，並在區塊鍊平台上發展智能合約(Solidity 編寫的程
式)。由於任何一個人皆可以編寫智能合約，而這些人可能不一定擅長於智能合約編
寫，所以一旦將合約發佈到鍊上，合約的錯誤將永存於區塊鍊上，且永久無法撤回，
例如最有名的TheDAO 事件，駭客利用智能合約的漏洞，將該公司的大筆資金移轉
到指定的帳戶，盜領將近五千萬美金。
所以也越來越多學者致力於研究如何驗證智能合約，盡可能將捕獲智能合約的漏洞，
由於智能合約是由程式語言(Solidity) 所編寫再經由編譯器將其編譯為Bytecode 並交
由以太坊虛擬機(EVM) 來執行，因此各個環節都必須要嚴格掌控，只要有任何一個
環節出錯，將會導致智能合約無法正確執行，甚至造成巨額的損失。
而在以太坊階層中最底層的以太坊虛擬機(EVM) 是負責執行智能合約編譯後的
Bytcode，而以太坊虛擬機必需依照以太坊黃皮書裡定義的指令規範，將指令實現正
確，否則就算正確的智能合約而執行過後的結果也會不如預期。
本篇論文是採用正規驗證的方式驗證以太訪虛擬機，並根據黃皮書裡的指令規範編
寫驗證Property，將黃皮書中定義的140 個指令全數驗證完畢，以及設計一組以太坊
虛擬機驗證皆口，使用者只要正確的將以太坊虛擬的訊號接上我們所設計的接口，
便能重複使用我們編寫的驗證Property 在我們的驗證平台進行驗證。最後我們透過
在以太坊虛擬機中植入錯誤程式碼，這些錯誤程式碼卻未能被官方釋出的測試套件
所偵測，然而透過我們的驗證方式能夠成功捕獲以太坊虛擬機指令實現上的錯誤，
以彌補測試套件在驗證方面的不足，達到更全面性的驗證。

Ethereum is based on blockchain technology and develops smart contracts (programs written by Solidity) on the blockchain platform. Once the smart contract is uploaded on the chain, the smart contract errors will remain on the blockchain forever and cannot be withdrawn forever, such as the most famous The DAO event. Therefore, more and more reserchers are committed to studying how to verify smart contracts and try to capture the vulnerabilities of smart contracts. Because smart contracts are written by a programming language (Solidity) and then compiled into bytecode by a compiler and sent to Ethereum Virtual machine (EVM) to execute, so all parts must be strictly controlled. As long as there is an error in any part, the smart contract will not be executed correctly and even cause huge losses. In this paper we formal method to verify the instruction of Ethereum virtual machine and verifies all the 140 instructions defined in the yellow paper. As well as designing a set of interface, users only need to correctly connect the EVM signal to the interface we designed, Then they can reuse the verification property we wrote for verification on our verification platform. Finally, we inject some error codes in EVM, but these error codes were not detected by the official testsuite. However, through our verification method, we can successfully capture errors in the implementation of the Ethereum virtual machine instructions to make up for the lack of verification in the testsuite and achieve a more comprehensive verification.

[1] Aleth ethereum c++ client, tools and libraries. [Online]. Available:https://github.com/ethereum/aleth. Accessed: 2020-08-20.
[2] Ethereum consensus tests. [Online]. Available:https://github.com/ethereum/tests. Accessed: 2020-09-20.
[3] Ethereum virtual machine introduction. [Online]. Available:https://blog.csdn.net/TurkeyCock/article/details/83786471. Accessed: 2020-08-20.
[4] Ethereumj. [Online]. Available:https://github.com/ethereum/ethereumj. Accessed:2020-08-20.
[5] Go ethereum. [Online]. Available:https://geth.ethereum.org/. Accessed: 2020-08-20.
[6] Smart contract. [Online]. Available:https://en.wikipedia.org/wiki/Smart_contract. Accessed: 2020-10-30.
[7] Trinity. [Online]. Available:https://trinity.ethereum.org/. Accessed: 2020-08-20.
[8] What is smart contract. [Online]. Available:https://blog.gasolin.idv.tw/2017/09/02/what-is-smart-contract/. Accessed: 2021-06-30.
[9] Mouhamad Almakhour, Layth Sliman, Abed Ellatif Samhat, and Abdelhamid Mellouk.Verification of smart contracts: A survey. Pervasive and Mobile Computing, page 101227, 2020.
[10] Leonardo Alt and Christian Reitwiessner. Smt-based verification of solidity smart contracts.In International Symposium on Leveraging Applications of Formal Methods, pages 376–388. Springer, 2018.
[11] Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples. Towards verifying ethereum smart contract bytecode in isabelle/hol. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 66–77, 2018.
[12] Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, et al. Formal verification of smart contracts: Short paper. In Proceedings of the 2016 ACM workshop on programming languages and analysis for security, pages 91–96, 2016.
[13] Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Kurt Jensen and Andreas Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), volume 2988 of Lecture Notes in Computer Science, pages 168–176. Springer, 2004.
[14] Nick Dodson. Solint: A linting utility for ethereum solidity smart-contracts, 2016.
[15] Chun-Sheng Ke and Yean-Ru Chen. Instruction verification of ethereum virtual machine by formal method. In 2020 Indo–Taiwan 2nd International Conference on Computing, Analytics and Networks (Indo-Taiwan ICAN), pages 69–74. IEEE, 2020.
[16] Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system. Decentralized Business Review, page 21260, 2008.
[17] Gavin Wood et al. Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper, 151(2014):1–32, 2014.