學術產出-學位論文
文章檢視/開啟
書目匯出
-
題名 智能合約堆疊溢位偵測與靜態分析
Static Stack Overflow Detection on Smart Contracts作者 黃仲瑀
Huang, Chung Yu貢獻者 郁方
黃仲瑀
Huang, Chung Yu關鍵詞 區塊鏈
以太坊
智能合約
靜態分析
符號執行日期 2018 上傳時間 3-九月-2018 15:48:18 (UTC+8) 摘要 近期，不只是在資訊領域，區塊鏈技術的應用正在如火如荼的快速成長中。各種新興虛擬貨幣如雨後春筍般大量出現，新創產業也陸續利用發行ICO的方式募資。有賴於智能合約，區塊鏈能夠運用的領域越來越廣泛。智能合約的功能就像一支在區塊鏈上的程式，使用者可以對智能合約發起交易，交易的過程所執行的內容，則是由智能合約中的程式邏輯決定，比方說一個點數交換的智能合約，其中可能包含了點數的轉換或是儲值的功能。各式各樣的智能合約已經存在目前的區塊鏈環境中，但就像是一般的程式一樣，智能合約也是有可能成為惡意行為的攻擊對象。此次研究的目的，是希望能夠透過靜態分析，針對尚未執行前的智能合約進行惡意行為檢查。我們希望能夠讓使用者在尚未執行智能合約之前，就能夠先針對智能合約進行檢測。在部份的研究中，已經有些實用的工具能夠檢查出潛在的風險。而我們希望能夠針對智能合約執行時的錯誤例外進行分析，這些錯誤例外包含了堆疊溢位以及gas值超過區塊上限的情況。透過我們的分析，能夠知道智能合約中有沒有包含循環，從這些循環來找出錯誤例外的發生。
Decentralized cryptocurrencies are based on a distributed ledger (a publicly- readable record) of a sequence of transactions. Recently, applications based on blockchain technologies have grown fast in many fields in our life, not only in technical industries but also in others such as financial industries. Smart contracts are programs that can be triggered by blockchain transactions. The transaction logic is coding inside the smart contract and can be executed automatically. Transactions will be kept on blockchain and cannot be modified by others. However, just like other programs, there exist some dangerous actions that can make the smart contract vulnerable. It is essential for having a rigorous approach to checking the correctness of smart contracts. In this work, we investigate static analysis techniques to detect vulnerabilities that could be exploited by malicious executions at runtime. Mainly, we focus on unexpected exceptions that occur inside a smart contract, such as EVM stack overflow or massive consumption of gas, which may lead to abnormal termination or abortion of contract execution. We target on contract opcodes and build instruction level symbolic execution for gas consumption and stack simulation. The analysis process consists of control flow graph construction with gas and stack status associated blocks. We then apply depth-first search to detect cycles that may raise stack size and generate their path constraints for execution accordingly. By solving the path constraints, we identify the inputs to trigger the execution and detect potential vulnerabilities or massive gas consumption. Our model checking approach benefits from soundness from formal reasoning, as well as automation from systematic symbolic execution. We report our analysis results against various contracts on Etherscan.參考文獻 References [1] P. Dai, N. Mahi, J. Earls, and A. Norta, “Smart-contract value-transfer protocols on a distributed mobile application platform,” URL: https://qtum. org/uploads/- files/cf6d69348ca50dd985b60425ccf282f3. pdf, 2017. [2] “Solidity-solidity 0.4.21 documentation.” https://solidity.readthedocs.io/en/ develop/. [3] “Counterparty.” https://counterparty.io/. [4] “Stellar - develop the world’s new financial system.” https://www.stellar.org/. [5] “Home — lisk.” https://lisk.io/. [6] “The dao (organization) - wikipedia.” https://en.wikipedia.org/wiki/The_DAO_ (organization). [7] N. Atzei, M. Bartoletti, and T. Cimoli, “A survey of attacks on ethereum smart contracts (sok),” in International Conference on Principles of Security and Trust, pp. 164–186, Springer, 2017. [8] “coloredcoins.org.” http://coloredcoins.org/. [9] “Create a democracy contract in ethereum.” https://www.ethereum.org/dao. [10] “Monegraph.” https://monegraph.com/. [11] K. Delmolino, M. Arnett, A. Kosba, A. Miller, and E. Shi, “Step by step towards creating a safe smart contract: Lessons and insights from a cryptocurrency lab,” in International Conference on Financial Cryptography and Data Security, pp. 79–94, Springer, 2016. [12] T. Dickerson, P. Gazzillo, M. Herlihy, and E. Koskinen, “Adding concurrency to smart contracts,” in Proceedings of the ACM Symposium on Principles of Distributed Computing, pp. 303–312, ACM, 2017. [13] M. Herlihy, V. Luchangco, M. Moir, and W. N. Scherer III, “Software transactional memory for dynamic-sized data structures,” in Proceedings of the twenty-second annual symposium on Principles of distributed computing, pp. 92–101, ACM, 2003. [14] L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, “Making smart contracts smarter,” in Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 254–269, ACM, 2016. [15] “Oyente by oyente.” https://oyente.github.io/benchmarks/. [16] K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote, N. Swamy, et al., “Formal verification of smart contracts: Short paper,” in Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, pp. 91–96, ACM, 2016. [17] N. Swamy, C. Hrit¸cu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, et al., “Dependent types and multimonadic effects in f,” in ACM SIGPLAN Notices, vol. 51, pp. 256–270, ACM, 2016. [18] A. Dika, “Ethereum smart contracts: Security vulnerabilities and security tools,” Master’s thesis, NTNU, 2017. [19] “Securify - formal verification of ethereum smart contracts.” https://securify.ch/. [20] “Smartdec — smart contracts security audit.” http://smartcontracts.smartdec. net/. [21] M. Suiche, “Porosity: A decompiler for blockchain-based smart contracts bytecode,” DEF CON, vol. 25, 2017. [22] E. Hildenbrandt, M. Saxena, X. Zhu, N. Rodrigues, P. Daian, D. Guth, and G. Rosu, “Kevm: A complete semantics of the ethereum virtual machine,” tech. rep., 2017. [23] S. Amani, M. B´egel, M. Bortin, and M. Staples, “Towards verifying ethereum smart contract bytecode in isabelle/hol,” CPP. ACM. To appear, 2018. [24] A. Mavridou and A. Laszka, “Tool demonstration: Fsolidm for designing secure ethereum smart contracts,” [25] “Finite-state machine - wikipedia.” https://en.wikipedia.org/wiki/ Finite-state_machine. [26] “Nxt - the blockchain application platform.” https://nxtplatform.org/. [27] P. L. Seijas, S. J. Thompson, and D. McAdams, “Scripting smart contracts for distributed ledger technology.,” IACR Cryptology ePrint Archive, vol. 2016, p. 1156, 2016. [28] “Zero-knowledge proof - wikipedia.” https://en.wikipedia.org/wiki/ Zero-knowledge_proof. [29] “Proof-carrying code - wikipedia.” https://en.wikipedia.org/wiki/ Proof-carrying_code. [30] J. Rubin, M. Naik, and N. Subramanian, “Merkelized abstract syntax trees.” [31] “Ethereum network status.” https://ethstats.net/. [32] “Ethereum blockchain explorer and search.” https://etherscan.io/. [33] “Installing the solidity compiler — solidity 0.4.21 documentation.” http:// solidity.readthedocs.io/en/v0.4.21/installing-solidity.html. [34] “Remix - solidity ide.” https://remix.ethereum.org/#optimize=false&version= builtin. [35] “Graphviz - graph visualization software.” https://www.graphviz.org/ 描述 碩士
國立政治大學
資訊管理學系
105356037資料來源 http://thesis.lib.nccu.edu.tw/record/#G0105356037 資料類型 thesis dc.contributor.advisor 郁方 zh_TW dc.contributor.author (作者) 黃仲瑀 zh_TW dc.contributor.author (作者) Huang, Chung Yu en_US dc.creator (作者) 黃仲瑀 zh_TW dc.creator (作者) Huang, Chung Yu en_US dc.date (日期) 2018 en_US dc.date.accessioned 3-九月-2018 15:48:18 (UTC+8) - dc.date.available 3-九月-2018 15:48:18 (UTC+8) - dc.date.issued (上傳時間) 3-九月-2018 15:48:18 (UTC+8) - dc.identifier (其他 識別碼) G0105356037 en_US dc.identifier.uri (URI) http://nccur.lib.nccu.edu.tw/handle/140.119/119883 - dc.description (描述) 碩士 zh_TW dc.description (描述) 國立政治大學 zh_TW dc.description (描述) 資訊管理學系 zh_TW dc.description (描述) 105356037 zh_TW dc.description.abstract (摘要) 近期，不只是在資訊領域，區塊鏈技術的應用正在如火如荼的快速成長中。各種新興虛擬貨幣如雨後春筍般大量出現，新創產業也陸續利用發行ICO的方式募資。有賴於智能合約，區塊鏈能夠運用的領域越來越廣泛。智能合約的功能就像一支在區塊鏈上的程式，使用者可以對智能合約發起交易，交易的過程所執行的內容，則是由智能合約中的程式邏輯決定，比方說一個點數交換的智能合約，其中可能包含了點數的轉換或是儲值的功能。各式各樣的智能合約已經存在目前的區塊鏈環境中，但就像是一般的程式一樣，智能合約也是有可能成為惡意行為的攻擊對象。此次研究的目的，是希望能夠透過靜態分析，針對尚未執行前的智能合約進行惡意行為檢查。我們希望能夠讓使用者在尚未執行智能合約之前，就能夠先針對智能合約進行檢測。在部份的研究中，已經有些實用的工具能夠檢查出潛在的風險。而我們希望能夠針對智能合約執行時的錯誤例外進行分析，這些錯誤例外包含了堆疊溢位以及gas值超過區塊上限的情況。透過我們的分析，能夠知道智能合約中有沒有包含循環，從這些循環來找出錯誤例外的發生。 zh_TW dc.description.abstract (摘要) Decentralized cryptocurrencies are based on a distributed ledger (a publicly- readable record) of a sequence of transactions. Recently, applications based on blockchain technologies have grown fast in many fields in our life, not only in technical industries but also in others such as financial industries. Smart contracts are programs that can be triggered by blockchain transactions. The transaction logic is coding inside the smart contract and can be executed automatically. Transactions will be kept on blockchain and cannot be modified by others. However, just like other programs, there exist some dangerous actions that can make the smart contract vulnerable. It is essential for having a rigorous approach to checking the correctness of smart contracts. In this work, we investigate static analysis techniques to detect vulnerabilities that could be exploited by malicious executions at runtime. Mainly, we focus on unexpected exceptions that occur inside a smart contract, such as EVM stack overflow or massive consumption of gas, which may lead to abnormal termination or abortion of contract execution. We target on contract opcodes and build instruction level symbolic execution for gas consumption and stack simulation. The analysis process consists of control flow graph construction with gas and stack status associated blocks. We then apply depth-first search to detect cycles that may raise stack size and generate their path constraints for execution accordingly. By solving the path constraints, we identify the inputs to trigger the execution and detect potential vulnerabilities or massive gas consumption. Our model checking approach benefits from soundness from formal reasoning, as well as automation from systematic symbolic execution. We report our analysis results against various contracts on Etherscan. en_US dc.description.tableofcontents Contents Abstract 1 Introduction 1 2 Related works 3 2.1 Blockchain and Smart Contract Applications 3 2.2 Smart Contract Security 3 2.3 Security Issue Detection 5 3 Motivating Example 7 3.1 Cycle Detection 9 3.2 Stack Simulation 9 3.3 Results 11 4 Methodology 13 4.1 Contract opcode extraction 13 4.2 Control flow graph construction 16 4.3 Stack overflow detection 18 4.4 Gas Estimation 22 4.5 Stack-based Symbolic Simulation 23 5 Experiment 30 5.1 Source Code Fetching 30 5.2 Source Code Comparison 30 5.3 Compile Result 31 6 Conclusions and Future Work 33 References 35 zh_TW dc.source.uri (資料來源) http://thesis.lib.nccu.edu.tw/record/#G0105356037 en_US dc.subject (關鍵詞) 區塊鏈 zh_TW dc.subject (關鍵詞) 以太坊 zh_TW dc.subject (關鍵詞) 智能合約 zh_TW dc.subject (關鍵詞) 靜態分析 zh_TW dc.subject (關鍵詞) 符號執行 zh_TW dc.title (題名) 智能合約堆疊溢位偵測與靜態分析 zh_TW dc.title (題名) Static Stack Overflow Detection on Smart Contracts en_US dc.type (資料類型) thesis en_US dc.relation.reference (參考文獻) References [1] P. Dai, N. Mahi, J. Earls, and A. Norta, “Smart-contract value-transfer protocols on a distributed mobile application platform,” URL: https://qtum. org/uploads/- files/cf6d69348ca50dd985b60425ccf282f3. pdf, 2017. [2] “Solidity-solidity 0.4.21 documentation.” https://solidity.readthedocs.io/en/ develop/. [3] “Counterparty.” https://counterparty.io/. [4] “Stellar - develop the world’s new financial system.” https://www.stellar.org/. [5] “Home — lisk.” https://lisk.io/. [6] “The dao (organization) - wikipedia.” https://en.wikipedia.org/wiki/The_DAO_ (organization). [7] N. Atzei, M. Bartoletti, and T. Cimoli, “A survey of attacks on ethereum smart contracts (sok),” in International Conference on Principles of Security and Trust, pp. 164–186, Springer, 2017. [8] “coloredcoins.org.” http://coloredcoins.org/. [9] “Create a democracy contract in ethereum.” https://www.ethereum.org/dao. [10] “Monegraph.” https://monegraph.com/. [11] K. Delmolino, M. Arnett, A. Kosba, A. Miller, and E. Shi, “Step by step towards creating a safe smart contract: Lessons and insights from a cryptocurrency lab,” in International Conference on Financial Cryptography and Data Security, pp. 79–94, Springer, 2016. [12] T. Dickerson, P. Gazzillo, M. Herlihy, and E. Koskinen, “Adding concurrency to smart contracts,” in Proceedings of the ACM Symposium on Principles of Distributed Computing, pp. 303–312, ACM, 2017. [13] M. Herlihy, V. Luchangco, M. Moir, and W. N. Scherer III, “Software transactional memory for dynamic-sized data structures,” in Proceedings of the twenty-second annual symposium on Principles of distributed computing, pp. 92–101, ACM, 2003. [14] L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, “Making smart contracts smarter,” in Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 254–269, ACM, 2016. [15] “Oyente by oyente.” https://oyente.github.io/benchmarks/. [16] K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote, N. Swamy, et al., “Formal verification of smart contracts: Short paper,” in Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, pp. 91–96, ACM, 2016. [17] N. Swamy, C. Hrit¸cu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, et al., “Dependent types and multimonadic effects in f,” in ACM SIGPLAN Notices, vol. 51, pp. 256–270, ACM, 2016. [18] A. Dika, “Ethereum smart contracts: Security vulnerabilities and security tools,” Master’s thesis, NTNU, 2017. [19] “Securify - formal verification of ethereum smart contracts.” https://securify.ch/. [20] “Smartdec — smart contracts security audit.” http://smartcontracts.smartdec. net/. [21] M. Suiche, “Porosity: A decompiler for blockchain-based smart contracts bytecode,” DEF CON, vol. 25, 2017. [22] E. Hildenbrandt, M. Saxena, X. Zhu, N. Rodrigues, P. Daian, D. Guth, and G. Rosu, “Kevm: A complete semantics of the ethereum virtual machine,” tech. rep., 2017. [23] S. Amani, M. B´egel, M. Bortin, and M. Staples, “Towards verifying ethereum smart contract bytecode in isabelle/hol,” CPP. ACM. To appear, 2018. [24] A. Mavridou and A. Laszka, “Tool demonstration: Fsolidm for designing secure ethereum smart contracts,” [25] “Finite-state machine - wikipedia.” https://en.wikipedia.org/wiki/ Finite-state_machine. [26] “Nxt - the blockchain application platform.” https://nxtplatform.org/. [27] P. L. Seijas, S. J. Thompson, and D. McAdams, “Scripting smart contracts for distributed ledger technology.,” IACR Cryptology ePrint Archive, vol. 2016, p. 1156, 2016. [28] “Zero-knowledge proof - wikipedia.” https://en.wikipedia.org/wiki/ Zero-knowledge_proof. [29] “Proof-carrying code - wikipedia.” https://en.wikipedia.org/wiki/ Proof-carrying_code. [30] J. Rubin, M. Naik, and N. Subramanian, “Merkelized abstract syntax trees.” [31] “Ethereum network status.” https://ethstats.net/. [32] “Ethereum blockchain explorer and search.” https://etherscan.io/. [33] “Installing the solidity compiler — solidity 0.4.21 documentation.” http:// solidity.readthedocs.io/en/v0.4.21/installing-solidity.html. [34] “Remix - solidity ide.” https://remix.ethereum.org/#optimize=false&version= builtin. [35] “Graphviz - graph visualization software.” https://www.graphviz.org/ zh_TW dc.identifier.doi (DOI) 10.6814/THE.NCCU.MIS.024.2018.A05 -
