學術產出-Theses
Article View/Open
Publication Export
-
題名 形式化 Gas 弱點偵測及攻擊生成
Symbolic Gas Vulnerability Detection and Attack Synthesis作者 彭旻浩
Peng, Min-Hao貢獻者 郁方
Yu, Fang
彭旻浩
Peng, Min-Hao關鍵詞 區塊鏈
智能合約
控制流程圖
形式化執行
Blockchain
Smart contract
Control flow graph
Gas estimation
Gas vulnerability
Symbolic execution日期 2020 上傳時間 2-Sep-2020 11:45:22 (UTC+8) 摘要 近期，不只是在資訊領域，區塊鏈技術的應用正在如火如荼的快速成長中。各種新興虛擬貨幣如雨後春筍般大量出現，新創產業也陸續利用發行ICO的方式募資。有賴於智能合約，區塊鏈能夠運用的領域越來越廣泛。智能合約的功能就像一支在區塊鏈上的程式，使用者可以對智能合約發起交易，交易的過程所執行的內容，則是由智能合約中的程式邏輯決定，比方說一個點數交換的智能合約，其中可能包含了點數的轉換或是儲值的功能。各式各樣的智能合約已經存在目前的區塊鏈環境中，但就像是一般的程式一樣，智能合約也是有可能成為惡意行為的攻擊對象。此次研究的目的，是希望能夠透過靜態分析，針對尚未執行前的智能合約進行 Gas 弱點檢查。我們希望能夠讓使用者在尚未執行智能合約之前，就能夠先針對智能合約進行檢測。在部份的研究中，已經有些實用的工具能夠檢查出針對 Gas 潛在的風險。而我們希望能夠針對智能合約執行時的 Gas 消耗進行分析，透過我們的分析，能夠偵測智能合約中是否包含 Gas 相關的弱點。
Successful executions of smart contracts require sufficient pre-allocated transaction fees, i.e., gas, on Ethereum. A gas vulnerability is a feasible execution of smart contracts that has its gas consumption depending on external inputs, e.g., used to check loop conditions or to calculate gas formulas. Such gas vulnerabilities may be exploited to raise massive gas consumption that leads the execution to unexpected exceptions. In this work, we propose an instruction-level symbolic stack simulation approach for systematic gas vulnerability detection and attack synthesis. The analysis process consists of 1) a sound control flow graph construction with blocks that are associated with their gas formulas and stack states, 2) symbolic execution path enumeration along with path and gas constraints generation, where loops are symbolically encoded with an auxiliary index for the number of iterations, and 3) gas vulnerability detection and its attack synthesis. To synthesize an attack to exploit the vulnerability, we use the sat model returned by an SMT solver to generate the inputs to trigger the execution that exceeds the gas limit. We report our analysis results against various contracts on Etherscan and In-house development cases, revealing previously unknown vulnerabilities in these contracts.參考文獻 [1] N. Szabo, “Formalizing and securing relationships on public networks,” First Monday, vol. 2, no. 9, 1997. [Online]. Available: https://journals.uic.edu/ojs/index. php/fm/article/view/548[2] coloredcoins, “coloredcoins.org,” http://coloredcoins.org/, 2019.[3] Ethereum, “Create a democracy contract in ethereum,” https://www.ethereum.org/ dao, 2019.[4] Monegraph, “Monegraph,” https://monegraph.com/, 2019.[5] G. Wood et al., “Ethereum: A secure decentralised generalised transaction ledger,” Ethereum project yellow paper, vol. 151, no. 2014, pp. 1–32, 2014.[6] Ethereum, “Solidity,” https://solidity.readthedocs.io, 2019.[7] N. Grech, M. Kong, A. Jurisevic, L. Brent, B. Scholz, and Y. Smaragdakis, “Madmax: Surviving out-of-gas conditions in ethereum smart contracts,” Proc. ACM Program. Lang., vol. 2, no. OOPSLA, pp. 116:1–116:27, Oct. 2018. [Online]. Available: http://doi.acm.org/10.1145/3276486[8] T. Chen, X. Li, X. Luo, and X. Zhang, “Under-optimized smart contracts devour your money,” in 2017 IEEE 24th International Conference on Software Analysis, Evolution and Reengineering (SANER). Klagenfurt, Austria: IEEE, Feb 2017, pp. 442–446.[9] D. Gopinath, C. S. Pa ̆s ̆areanu, K. Wang, M. Zhang, and S. Khurshid, “Symbolic execution for attribution and attack synthesis in neural networks,” in Proceedings of the 41st International Conference on Software Engineering: Companion Proceedings, ser. ICSE ’19. Montreal, Quebec, Canada: IEEE Press, 2019, pp. 282–283. [Online]. Available: https://doi.org/10.1109/ICSE-Companion.2019.00115[10] B. Loring, D. Mitchell, and J. Kinder, “Sound regular expression semantics for dynamic symbolic execution of javascript,” CoRR, vol. abs/1810.05661, pp. 425–438, 2018. [Online]. Available: http://arxiv.org/abs/1810.05661[11] Ethereum, “Ethereum network status,” https://ethstats.net/, 2019.[12] N. Atzei, M. Bartoletti, and T. Cimoli, “A survey of attacks on ethereum smart contracts (sok),” in Principles of Security and Trust, M. Maffei and M. Ryan, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2017, pp. 164–186.[13] 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 Financial Cryptography and Data Security, J. Clark, S. Meiklejohn, P. Y. Ryan, D. Wallach, M. Brenner, and K. Rohloff, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2016, pp. 79–94.[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, ACM. New York, NY, USA: ACM, 2016, pp. 254–269.[15] I. Grishchenko, M. Maffei, and C. Schneidewind, “Foundations and tools for the staticanalysisofethereumsmartcontracts,”inComputerAidedVerification. Cham: Springer International Publishing, 2018, pp. 51–78.[16] A. Hahn, R. Singh, C. Liu, and S. Chen, “Smart contract-based campus demon- stration of decentralized transactive energy auctions,” in 2017 IEEE Power Energy Society Innovative Smart Grid Technologies Conference (ISGT). Washington, DC, USA: IEEE, 2017, pp. 1–5.[17] Y. Wang, S. Lahiri, S. Chen, R. Pan, I. Dillig, C. Born, I. Naseer, and K. Ferles, “Formal verification of workflow policies for smart contracts in azure blockchain,” in Verified Software: Theories, Tools and Experiments. Springer, September 2019.[18] K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote, N. Swamy, and S. Zanella- B ́eguelin, “Formal verification of smart contracts: Short paper,” in Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, ser. PLAS ’16. New York, NY, USA: ACM, 2016, pp. 91–96. [Online]. Available: http://doi.acm.org/10.1145/2993600.2993611[19] N. Swamy, C. Hri ̧tcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, J.-K. Zinzindohoue, and S. Zanella-B ́eguelin, “Dependent types and multi-monadic effects in f*,” in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’16. New York, NY, USA: ACM, 2016, pp. 256–270. [Online]. Available: http://doi.acm.org/10.1145/2837614.2837655[20] A. Dika, “Ethereum smart contracts: Security vulnerabilities and security tools,” Master’s thesis, NTNU, 2017.[21] P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. Bu ̈nzli, and M. Vechev, “Securify: Practical security analysis of smart contracts,” in Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, ser. CCS ’18. New York, NY, USA: ACM, 2018, pp. 67–82. [Online]. Available: http://doi.acm.org/10.1145/3243734.3243780[22] Ethereum, “Remix - solidity ide,” https://remix.ethereum.org/#optimize=false& version=builtin, 2019.[23] SmartDec, “Smartdec — smart contracts security audit,” http://smartcontracts. smartdec.net/, 2017.[24] B. Jiang, Y. Liu, and W. K. Chan, “Contractfuzzer: Fuzzing smart contracts for vulnerability detection,” in Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ser. ASE 2018. New York, NY, USA: ACM, 2018, pp. 259–269. [Online]. Available: http: //doi.acm.org/10.1145/3238147.3238177[25] Mythril, “Mythril,” https://mythx.io/, 2019.[26] S. Kalra, S. Goel, M. Dhawan, and S. Sharma, “Zeus: Analyzing safety of smart contracts,” in NDSS. San Diego, California, USA: NDSS, 2018, pp. 1–12.[27] J. Krupp and C. Rossow, “teether: Gnawing at ethereum to automatically exploit smart contracts,” in 27th USENIX Security Symposium (USENIX Security 18). Baltimore, MD: USENIX Association, Aug. 2018, pp. 1317–1333. [Online]. Available: https://www.usenix.org/conference/usenixsecurity18/presentation/krupp[28] Y. Feng, E. Torlak, and R. Bod ́ık, “Precise attack synthesis for smart contracts,” CoRR, vol. abs/1902.06067, 2019. [Online]. Available: http: //arxiv.org/abs/1902.06067[29] M. Suiche, “Porosity: A decompiler for blockchain-based smart contracts bytecode,” DEF CON, vol. 25, p. 11, 2017.[30] E. Hildenbrandt, M. Saxena, X. Zhu, N. Rodrigues, P. Daian, D. Guth, and G. Rosu, “Kevm: A complete semantics of the ethereum virtual machine,” University of Illi- nois, Tech. Rep., 2017.[31] S. Amani, M. B ́egel, M. Bortin, and M. Staples, “Towards verifying ethereum smart contract bytecode in isabelle/hol,” in Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, ser. CPP 2018. New York, NY, USA: ACM, 2018, pp. 66–77. [Online]. Available: http://doi.acm.org/10.1145/3167084[32] A. Mavridou and A. Laszka, “Tool demonstration: Fsolidm for designing secure ethereum smart contracts,” in Principles of Security and Trust. Cham: Springer International Publishing, 2018, pp. 270–277.[33] ——, “Designing secure ethereum smart contracts: A finite state machine based approach,” in Financial Cryptography and Data Security, S. Meiklejohn and K. Sako, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2018, pp. 523–540.[34] Nxt, “Nxt - the blockchain application platform,” https://nxtplatform.org/, 2019.[35] Ethereum, “Ethereum blockchain explorer and search,” https://etherscan.io/, 2019.[36] P. L. Seijas, S. J. Thompson, and D. McAdams, “Scripting smart contracts for dis- tributed ledger technology.” IACR Cryptology ePrint Archive, vol. 2016, p. 1156, 2016.[37] O. Goldreich and Y. Oren, “Definitions and properties of zero-knowledge proof sys- tems,” Journal of Cryptology, vol. 7, no. 1, pp. 1–32, 1994.[38] G. C. Necula, “Proof-carrying code,” in Proceedings of the 24th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, ser. POPL ’97. New York, NY, USA: Association for Computing Machinery, 1997, p. 106–119. [Online]. Available: https://doi.org/10.1145/263699.263712[39] J. Rubin, M. Naik, and N. Subramanian, “Merkelized abstract syntax trees,” 2019.[40] E. Albert, P. Gordillo, A. Rubio, and I. Sergey, “GASTAP: A gas analyzer for smart contracts,” CoRR, vol. abs/1811.10403, 2018. [Online]. Available: http://arxiv.org/abs/1811.10403[41] D. Kebbal and P. Sainrat, “Combining symbolic execution and path enumeration in worst-case execution time analysis,” in 6th International Workshop on Worst- Case Execution Time Analysis (WCET’06), ser. OpenAccess Series in Informatics (OASIcs), F. Mueller, Ed., vol. 4. Dagstuhl, Germany: Schloss Dagstuhl–Leibniz- Zentrum fuer Informatik, 2006, pp. 33 – 38.[42] B. Benhamamouch, B. Monsuez, and F. V ́edrine, “Computing wcet using symbolic execution,” in Second International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2008). UK: Springer International Publishing, 2008, pp. 1–12.[43] A. Biere, J. Knoop, L. Kova ́cs, and J. Zwirchmayr, “The auspicious couple: Symbolic execution and wcet analysis,” in 13th International Workshop on Worst-Case Execu- tion Time Analysis, ser. OpenAccess Series in Informatics (OASIcs), C. Maiza, Ed., vol. 30. Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2013, pp. 53–63.[44] C. S. Pa ̆s ̆areanu, R. Kersten, K. Luckow, and Q.-S. Phan, “Symbolic execution and recent applications to worst-case execution, load testing, and security analysis,” in Advances in Computers, ser. Advances in Computers, A. M. Memon, Ed. United States: Elsevier, 2019, vol. 113, pp. 289 – 314.[45] T. Liang, A. Reynolds, N. Tsiskaridze, C. Tinelli, C. Barrett, and M. Deters, “An efficient smt solver for string constraints,” Formal Methods in System Design, vol. 48, no. 3, pp. 206–234, 2016.[46] H.-E. Wang, T.-L. Tsai, C.-H. Lin, F. Yu, and J.-H. R. Jiang, “String analysis via automata manipulation with logic circuit representation,” in Computer Aided Verifi- cation, S. Chaudhuri and A. Farzan, Eds. Cham: Springer International Publishing, 2016, pp. 241–260.[47] H.-E. Wang, S.-Y. Chen, F. Yu, and J.-H. R. Jiang, “A symbolic model checking approach to the analysis of string and length constraints,” in Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ser. ASE 2018. New York, NY, USA: Association for Computing Machinery, 2018, p. 623–633. [Online]. Available: https://doi.org/10.1145/3238147.3238189[48] A. Aydin, W. Eiers, L. Bang, T. Brennan, M. Gavrilov, T. Bultan, and F. Yu, “Parameterized model counting for string and numeric constraints,” in Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ser. ESEC/FSE 2018. New York, NY, USA: Association for Computing Machinery, 2018, p. 400–410. [Online]. Available: https://doi.org/10.1145/3236024.3236064[49] Counterparty, “Counterparty,” https://counterparty.io/, 2018.[50] Stellar, “Stellar - develop the world’s new financial system,” https://www.stellar. org/, 2019.[51] Lisk, “Home — lisk,” https://lisk.io/, 2019.[52] L. de Moura and N. Bjørner, “Z3: An efficient smt solver,” in Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and J. Rehof, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 337–340.[53] Ethereum, “Installing the solidity compiler — solidity 0.4.21 documentation,” http: //solidity.readthedocs.io/en/v0.4.21/installing-solidity.html, 2017.[54] Graphviz, “Graphviz - graph visualization software,” https://www.graphviz.org/, 2019.[55] L. Gonnord, D. Monniaux, and G. Radanne, “Synthesis of ranking functions using extremal counterexamples,” in Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI ’15. New York, NY, USA: Association for Computing Machinery, 2015, p. 608–618. [Online]. Available: https://doi.org/10.1145/2737924.2737976[56] A. M. Ben-Amram, J. J. Dom ́enech, and S. Genaim, “Multiphase-linear ranking functions and their relation to recurrent sets,” in Static Analysis, B.-Y. E. Chang, Ed. Cham: Springer International Publishing, 2019, pp. 459–480.[57] M. H. Peng, “Our analysis tools,” https://github.com/hichyen1207/ SmartContractCFG, 2019. 描述 碩士
國立政治大學
資訊管理學系
107356010資料來源 http://thesis.lib.nccu.edu.tw/record/#G0107356010 資料類型 thesis dc.contributor.advisor 郁方 zh_TW dc.contributor.advisor Yu, Fang en_US dc.contributor.author (Authors) 彭旻浩 zh_TW dc.contributor.author (Authors) Peng, Min-Hao en_US dc.creator (作者) 彭旻浩 zh_TW dc.creator (作者) Peng, Min-Hao en_US dc.date (日期) 2020 en_US dc.date.accessioned 2-Sep-2020 11:45:22 (UTC+8) - dc.date.available 2-Sep-2020 11:45:22 (UTC+8) - dc.date.issued (上傳時間) 2-Sep-2020 11:45:22 (UTC+8) - dc.identifier (Other Identifiers) G0107356010 en_US dc.identifier.uri (URI) http://nccur.lib.nccu.edu.tw/handle/140.119/131489 - dc.description (描述) 碩士 zh_TW dc.description (描述) 國立政治大學 zh_TW dc.description (描述) 資訊管理學系 zh_TW dc.description (描述) 107356010 zh_TW dc.description.abstract (摘要) 近期，不只是在資訊領域，區塊鏈技術的應用正在如火如荼的快速成長中。各種新興虛擬貨幣如雨後春筍般大量出現，新創產業也陸續利用發行ICO的方式募資。有賴於智能合約，區塊鏈能夠運用的領域越來越廣泛。智能合約的功能就像一支在區塊鏈上的程式，使用者可以對智能合約發起交易，交易的過程所執行的內容，則是由智能合約中的程式邏輯決定，比方說一個點數交換的智能合約，其中可能包含了點數的轉換或是儲值的功能。各式各樣的智能合約已經存在目前的區塊鏈環境中，但就像是一般的程式一樣，智能合約也是有可能成為惡意行為的攻擊對象。此次研究的目的，是希望能夠透過靜態分析，針對尚未執行前的智能合約進行 Gas 弱點檢查。我們希望能夠讓使用者在尚未執行智能合約之前，就能夠先針對智能合約進行檢測。在部份的研究中，已經有些實用的工具能夠檢查出針對 Gas 潛在的風險。而我們希望能夠針對智能合約執行時的 Gas 消耗進行分析，透過我們的分析，能夠偵測智能合約中是否包含 Gas 相關的弱點。 zh_TW dc.description.abstract (摘要) Successful executions of smart contracts require sufficient pre-allocated transaction fees, i.e., gas, on Ethereum. A gas vulnerability is a feasible execution of smart contracts that has its gas consumption depending on external inputs, e.g., used to check loop conditions or to calculate gas formulas. Such gas vulnerabilities may be exploited to raise massive gas consumption that leads the execution to unexpected exceptions. In this work, we propose an instruction-level symbolic stack simulation approach for systematic gas vulnerability detection and attack synthesis. The analysis process consists of 1) a sound control flow graph construction with blocks that are associated with their gas formulas and stack states, 2) symbolic execution path enumeration along with path and gas constraints generation, where loops are symbolically encoded with an auxiliary index for the number of iterations, and 3) gas vulnerability detection and its attack synthesis. To synthesize an attack to exploit the vulnerability, we use the sat model returned by an SMT solver to generate the inputs to trigger the execution that exceeds the gas limit. We report our analysis results against various contracts on Etherscan and In-house development cases, revealing previously unknown vulnerabilities in these contracts. en_US dc.description.tableofcontents 1 INTRODUCTION 12 RELATED WORKS 33 Gas Vulnerabilities 73.1 Bounded Gas Vulnerability 83.2 Unbounded Gas Vulnerability 104 Methodology 124.1 Contract opcode extraction 134.2 The control flow graph construction 144.3 Symbolic Gas Estimation 184.4 Stack-based Symbolic Simulation 214.5 Memory and Storage as Uninterpreted Function 244.6 Parametric Gas Consumption of Loops 264.7 Termination with Ranking Function Derivation 294.8 Attack synthesis 335 EXPERIMENT 345.1 Analyzing In-house Contracts 345.2 In-house Contracts Comparison 385.3 Analyzing Public Contracts on Etherscan 406 Conclusion 447 References 45 zh_TW dc.format.extent 765321 bytes - dc.format.mimetype application/pdf - dc.source.uri (資料來源) http://thesis.lib.nccu.edu.tw/record/#G0107356010 en_US dc.subject (關鍵詞) 區塊鏈 zh_TW dc.subject (關鍵詞) 智能合約 zh_TW dc.subject (關鍵詞) 控制流程圖 zh_TW dc.subject (關鍵詞) 形式化執行 zh_TW dc.subject (關鍵詞) Blockchain en_US dc.subject (關鍵詞) Smart contract en_US dc.subject (關鍵詞) Control flow graph en_US dc.subject (關鍵詞) Gas estimation en_US dc.subject (關鍵詞) Gas vulnerability en_US dc.subject (關鍵詞) Symbolic execution en_US dc.title (題名) 形式化 Gas 弱點偵測及攻擊生成 zh_TW dc.title (題名) Symbolic Gas Vulnerability Detection and Attack Synthesis en_US dc.type (資料類型) thesis en_US dc.relation.reference (參考文獻) [1] N. Szabo, “Formalizing and securing relationships on public networks,” First Monday, vol. 2, no. 9, 1997. [Online]. Available: https://journals.uic.edu/ojs/index. php/fm/article/view/548[2] coloredcoins, “coloredcoins.org,” http://coloredcoins.org/, 2019.[3] Ethereum, “Create a democracy contract in ethereum,” https://www.ethereum.org/ dao, 2019.[4] Monegraph, “Monegraph,” https://monegraph.com/, 2019.[5] G. Wood et al., “Ethereum: A secure decentralised generalised transaction ledger,” Ethereum project yellow paper, vol. 151, no. 2014, pp. 1–32, 2014.[6] Ethereum, “Solidity,” https://solidity.readthedocs.io, 2019.[7] N. Grech, M. Kong, A. Jurisevic, L. Brent, B. Scholz, and Y. Smaragdakis, “Madmax: Surviving out-of-gas conditions in ethereum smart contracts,” Proc. ACM Program. Lang., vol. 2, no. OOPSLA, pp. 116:1–116:27, Oct. 2018. [Online]. Available: http://doi.acm.org/10.1145/3276486[8] T. Chen, X. Li, X. Luo, and X. Zhang, “Under-optimized smart contracts devour your money,” in 2017 IEEE 24th International Conference on Software Analysis, Evolution and Reengineering (SANER). Klagenfurt, Austria: IEEE, Feb 2017, pp. 442–446.[9] D. Gopinath, C. S. Pa ̆s ̆areanu, K. Wang, M. Zhang, and S. Khurshid, “Symbolic execution for attribution and attack synthesis in neural networks,” in Proceedings of the 41st International Conference on Software Engineering: Companion Proceedings, ser. ICSE ’19. Montreal, Quebec, Canada: IEEE Press, 2019, pp. 282–283. [Online]. Available: https://doi.org/10.1109/ICSE-Companion.2019.00115[10] B. Loring, D. Mitchell, and J. Kinder, “Sound regular expression semantics for dynamic symbolic execution of javascript,” CoRR, vol. abs/1810.05661, pp. 425–438, 2018. [Online]. Available: http://arxiv.org/abs/1810.05661[11] Ethereum, “Ethereum network status,” https://ethstats.net/, 2019.[12] N. Atzei, M. Bartoletti, and T. Cimoli, “A survey of attacks on ethereum smart contracts (sok),” in Principles of Security and Trust, M. Maffei and M. Ryan, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2017, pp. 164–186.[13] 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 Financial Cryptography and Data Security, J. Clark, S. Meiklejohn, P. Y. Ryan, D. Wallach, M. Brenner, and K. Rohloff, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2016, pp. 79–94.[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, ACM. New York, NY, USA: ACM, 2016, pp. 254–269.[15] I. Grishchenko, M. Maffei, and C. Schneidewind, “Foundations and tools for the staticanalysisofethereumsmartcontracts,”inComputerAidedVerification. Cham: Springer International Publishing, 2018, pp. 51–78.[16] A. Hahn, R. Singh, C. Liu, and S. Chen, “Smart contract-based campus demon- stration of decentralized transactive energy auctions,” in 2017 IEEE Power Energy Society Innovative Smart Grid Technologies Conference (ISGT). Washington, DC, USA: IEEE, 2017, pp. 1–5.[17] Y. Wang, S. Lahiri, S. Chen, R. Pan, I. Dillig, C. Born, I. Naseer, and K. Ferles, “Formal verification of workflow policies for smart contracts in azure blockchain,” in Verified Software: Theories, Tools and Experiments. Springer, September 2019.[18] K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote, N. Swamy, and S. Zanella- B ́eguelin, “Formal verification of smart contracts: Short paper,” in Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, ser. PLAS ’16. New York, NY, USA: ACM, 2016, pp. 91–96. [Online]. Available: http://doi.acm.org/10.1145/2993600.2993611[19] N. Swamy, C. Hri ̧tcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, J.-K. Zinzindohoue, and S. Zanella-B ́eguelin, “Dependent types and multi-monadic effects in f*,” in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’16. New York, NY, USA: ACM, 2016, pp. 256–270. [Online]. Available: http://doi.acm.org/10.1145/2837614.2837655[20] A. Dika, “Ethereum smart contracts: Security vulnerabilities and security tools,” Master’s thesis, NTNU, 2017.[21] P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. Bu ̈nzli, and M. Vechev, “Securify: Practical security analysis of smart contracts,” in Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, ser. CCS ’18. New York, NY, USA: ACM, 2018, pp. 67–82. [Online]. Available: http://doi.acm.org/10.1145/3243734.3243780[22] Ethereum, “Remix - solidity ide,” https://remix.ethereum.org/#optimize=false& version=builtin, 2019.[23] SmartDec, “Smartdec — smart contracts security audit,” http://smartcontracts. smartdec.net/, 2017.[24] B. Jiang, Y. Liu, and W. K. Chan, “Contractfuzzer: Fuzzing smart contracts for vulnerability detection,” in Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ser. ASE 2018. New York, NY, USA: ACM, 2018, pp. 259–269. [Online]. Available: http: //doi.acm.org/10.1145/3238147.3238177[25] Mythril, “Mythril,” https://mythx.io/, 2019.[26] S. Kalra, S. Goel, M. Dhawan, and S. Sharma, “Zeus: Analyzing safety of smart contracts,” in NDSS. San Diego, California, USA: NDSS, 2018, pp. 1–12.[27] J. Krupp and C. Rossow, “teether: Gnawing at ethereum to automatically exploit smart contracts,” in 27th USENIX Security Symposium (USENIX Security 18). Baltimore, MD: USENIX Association, Aug. 2018, pp. 1317–1333. [Online]. Available: https://www.usenix.org/conference/usenixsecurity18/presentation/krupp[28] Y. Feng, E. Torlak, and R. Bod ́ık, “Precise attack synthesis for smart contracts,” CoRR, vol. abs/1902.06067, 2019. [Online]. Available: http: //arxiv.org/abs/1902.06067[29] M. Suiche, “Porosity: A decompiler for blockchain-based smart contracts bytecode,” DEF CON, vol. 25, p. 11, 2017.[30] E. Hildenbrandt, M. Saxena, X. Zhu, N. Rodrigues, P. Daian, D. Guth, and G. Rosu, “Kevm: A complete semantics of the ethereum virtual machine,” University of Illi- nois, Tech. Rep., 2017.[31] S. Amani, M. B ́egel, M. Bortin, and M. Staples, “Towards verifying ethereum smart contract bytecode in isabelle/hol,” in Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, ser. CPP 2018. New York, NY, USA: ACM, 2018, pp. 66–77. [Online]. Available: http://doi.acm.org/10.1145/3167084[32] A. Mavridou and A. Laszka, “Tool demonstration: Fsolidm for designing secure ethereum smart contracts,” in Principles of Security and Trust. Cham: Springer International Publishing, 2018, pp. 270–277.[33] ——, “Designing secure ethereum smart contracts: A finite state machine based approach,” in Financial Cryptography and Data Security, S. Meiklejohn and K. Sako, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2018, pp. 523–540.[34] Nxt, “Nxt - the blockchain application platform,” https://nxtplatform.org/, 2019.[35] Ethereum, “Ethereum blockchain explorer and search,” https://etherscan.io/, 2019.[36] P. L. Seijas, S. J. Thompson, and D. McAdams, “Scripting smart contracts for dis- tributed ledger technology.” IACR Cryptology ePrint Archive, vol. 2016, p. 1156, 2016.[37] O. Goldreich and Y. Oren, “Definitions and properties of zero-knowledge proof sys- tems,” Journal of Cryptology, vol. 7, no. 1, pp. 1–32, 1994.[38] G. C. Necula, “Proof-carrying code,” in Proceedings of the 24th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, ser. POPL ’97. New York, NY, USA: Association for Computing Machinery, 1997, p. 106–119. [Online]. Available: https://doi.org/10.1145/263699.263712[39] J. Rubin, M. Naik, and N. Subramanian, “Merkelized abstract syntax trees,” 2019.[40] E. Albert, P. Gordillo, A. Rubio, and I. Sergey, “GASTAP: A gas analyzer for smart contracts,” CoRR, vol. abs/1811.10403, 2018. [Online]. Available: http://arxiv.org/abs/1811.10403[41] D. Kebbal and P. Sainrat, “Combining symbolic execution and path enumeration in worst-case execution time analysis,” in 6th International Workshop on Worst- Case Execution Time Analysis (WCET’06), ser. OpenAccess Series in Informatics (OASIcs), F. Mueller, Ed., vol. 4. Dagstuhl, Germany: Schloss Dagstuhl–Leibniz- Zentrum fuer Informatik, 2006, pp. 33 – 38.[42] B. Benhamamouch, B. Monsuez, and F. V ́edrine, “Computing wcet using symbolic execution,” in Second International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2008). UK: Springer International Publishing, 2008, pp. 1–12.[43] A. Biere, J. Knoop, L. Kova ́cs, and J. Zwirchmayr, “The auspicious couple: Symbolic execution and wcet analysis,” in 13th International Workshop on Worst-Case Execu- tion Time Analysis, ser. OpenAccess Series in Informatics (OASIcs), C. Maiza, Ed., vol. 30. Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2013, pp. 53–63.[44] C. S. Pa ̆s ̆areanu, R. Kersten, K. Luckow, and Q.-S. Phan, “Symbolic execution and recent applications to worst-case execution, load testing, and security analysis,” in Advances in Computers, ser. Advances in Computers, A. M. Memon, Ed. United States: Elsevier, 2019, vol. 113, pp. 289 – 314.[45] T. Liang, A. Reynolds, N. Tsiskaridze, C. Tinelli, C. Barrett, and M. Deters, “An efficient smt solver for string constraints,” Formal Methods in System Design, vol. 48, no. 3, pp. 206–234, 2016.[46] H.-E. Wang, T.-L. Tsai, C.-H. Lin, F. Yu, and J.-H. R. Jiang, “String analysis via automata manipulation with logic circuit representation,” in Computer Aided Verifi- cation, S. Chaudhuri and A. Farzan, Eds. Cham: Springer International Publishing, 2016, pp. 241–260.[47] H.-E. Wang, S.-Y. Chen, F. Yu, and J.-H. R. Jiang, “A symbolic model checking approach to the analysis of string and length constraints,” in Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ser. ASE 2018. New York, NY, USA: Association for Computing Machinery, 2018, p. 623–633. [Online]. Available: https://doi.org/10.1145/3238147.3238189[48] A. Aydin, W. Eiers, L. Bang, T. Brennan, M. Gavrilov, T. Bultan, and F. Yu, “Parameterized model counting for string and numeric constraints,” in Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ser. ESEC/FSE 2018. New York, NY, USA: Association for Computing Machinery, 2018, p. 400–410. [Online]. Available: https://doi.org/10.1145/3236024.3236064[49] Counterparty, “Counterparty,” https://counterparty.io/, 2018.[50] Stellar, “Stellar - develop the world’s new financial system,” https://www.stellar. org/, 2019.[51] Lisk, “Home — lisk,” https://lisk.io/, 2019.[52] L. de Moura and N. Bjørner, “Z3: An efficient smt solver,” in Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and J. Rehof, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 337–340.[53] Ethereum, “Installing the solidity compiler — solidity 0.4.21 documentation,” http: //solidity.readthedocs.io/en/v0.4.21/installing-solidity.html, 2017.[54] Graphviz, “Graphviz - graph visualization software,” https://www.graphviz.org/, 2019.[55] L. Gonnord, D. Monniaux, and G. Radanne, “Synthesis of ranking functions using extremal counterexamples,” in Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI ’15. New York, NY, USA: Association for Computing Machinery, 2015, p. 608–618. [Online]. Available: https://doi.org/10.1145/2737924.2737976[56] A. M. Ben-Amram, J. J. Dom ́enech, and S. Genaim, “Multiphase-linear ranking functions and their relation to recurrent sets,” in Static Analysis, B.-Y. E. Chang, Ed. Cham: Springer International Publishing, 2019, pp. 459–480.[57] M. H. Peng, “Our analysis tools,” https://github.com/hichyen1207/ SmartContractCFG, 2019. zh_TW dc.identifier.doi (DOI) 10.6814/NCCU202001258 en_US
