Nothing Special   »   [go: up one dir, main page]

skip to main content
research-article
Open access

Symbolic value-flow static analysis: deep, precise, complete modeling of Ethereum smart contracts

Published: 15 October 2021 Publication History

Abstract

We present a static analysis approach that combines concrete values and symbolic expressions. This symbolic value-flow (“symvalic”) analysis models program behavior with high precision, e.g., full path sensitivity. To achieve deep modeling of program semantics, the analysis relies on a symbiotic relationship between a traditional static analysis fixpoint computation and a symbolic solver: the solver does not merely receive a complex “path condition” to solve, but is instead invoked repeatedly (often tens or hundreds of thousands of times), in close cooperation with the flow computation of the analysis.
The result of the symvalic analysis architecture is a static modeling of program behavior that is much more complete than symbolic execution, much more precise than conventional static analysis, and domain-agnostic: no special-purpose definition of anti-patterns is necessary in order to compute violations of safety conditions with high precision.
We apply the analysis to the domain of Ethereum smart contracts. This domain represents a fundamental challenge for program analysis approaches: despite numerous publications, research work has not been effective at uncovering vulnerabilities of high real-world value.
In systematic comparison of symvalic analysis with past tools, we find significantly increased completeness (shown as 83-96% statement coverage and more true error reports) combined with much higher precision, as measured by rate of true positive reports. In terms of real-world impact, since the beginning of 2021, the analysis has resulted in the discovery and disclosure of several critical vulnerabilities, over funds in the many millions of dollars. Six separate bug bounties totaling over $350K have been awarded for these disclosures.

Supplementary Material

Auxiliary Presentation Video (oopsla21main-p476-p-video.mp4)
This is a presentation video of our OOPSLA'21 talk. We present a static analysis approach that combines concrete values and symbolic expressions. This symbolic value-flow (“symvalic”) analysis models program behavior with high precision, e.g., full path sensitivity. To achieve deep modeling of program semantics, the analysis relies on a symbiotic relationship between a traditional static analysis fixpoint computation and a symbolic solver: the solver does not merely receive a complex “path condition” to solve, but is instead invoked repeatedly (often tens or hundreds of thousands of times), in close cooperation with the flow computation of the analysis.

References

[1]
Martín Abadi and Leslie Lamport. 1993. Composing Specifications. ACM Trans. Program. Lang. Syst., 15, 1 (1993), Jan., 73–132. issn:0164-0925 https://doi.org/10.1145/151646.151649
[2]
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, and Albert Rubio. 2020. GASOL: gas analysis and optimization for ethereum smart contracts. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 118–125.
[3]
Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, and Ilya Sergey. 2018. EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. In Automated Technology for Verification and Analysis (ATVA). Springer International Publishing, 513–520.
[4]
Elvira Albert, Pablo Gordillo, Albert Rubio, and Maria A. Schett. 2020. Synthesis of Super-Optimized Smart Contracts Using Max-SMT. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham. 177–200. isbn:978-3-030-53288-8
[5]
Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, and Mooly Sagiv. 2020. Taming Callbacks for Smart Contract Modularity. Proc. ACM Program. Lang., 4, OOPSLA (2020), Article 209, Nov., 30 pages. https://doi.org/10.1145/3428277
[6]
Saswat Anand, Patrice Godefroid, and Nikolai Tillmann. 2008. Demand-Driven Compositional Symbolic Execution. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 367–381. isbn:978-3-540-78800-3
[7]
Roberto Baldoni, Emilio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. 2018. A Survey of Symbolic Execution Techniques. ACM Comput. Surv., 51, 3 (2018), Article 50, May, 39 pages. issn:0360-0300 https://doi.org/10.1145/3182657
[8]
Aaron Bembenek, Michael Greenberg, and Stephen Chong. 2020. Formulog: Datalog for SMT-Based Static Analysis (Extended Version). CoRR, abs/2009.08361 (2020), arxiv:2009.08361. arxiv:2009.08361
[9]
Eric Bodden, Társis Tolêdo, Márcio Ribeiro, Claus Brabrand, Paulo Borba, and Mira Mezini. 2013. SPLLIFT: Statically Analyzing Software Product Lines in Minutes Instead of Years. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’13). Association for Computing Machinery, New York, NY, USA. 355–364. isbn:9781450320146 https://doi.org/10.1145/2491956.2491976
[10]
Marcel Böhme, Van-Thuan Pham, and Abhik Roychoudhury. 2016. Coverage-Based Greybox Fuzzing as Markov Chain. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS ’16). Association for Computing Machinery, New York, NY, USA. 1032–1043. isbn:9781450341394 https://doi.org/10.1145/2976749.2978428
[11]
Lexi Brent, Neville Grech, Sifis Lagouvardos, Bernhard Scholz, and Yannis Smaragdakis. 2020. Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020). Association for Computing Machinery, New York, NY, USA. 454–469. isbn:9781450376136 https://doi.org/10.1145/3385412.3385990
[12]
Lexi Brent, Anton Jurisevic, Michael Kong, Eric Liu, Francois Gauthier, Vincent Gramoli, Ralph Holz, and Bernhard Scholz. 2018. Vandal: A Scalable Security Analysis Framework for Smart Contracts. CoRR, abs/1802.08660 (2018), arxiv:1809.03981. arxiv:1809.03981
[13]
Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proc. 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX, 209–224.
[14]
T. Chen, Y. Feng, Z. Li, H. Zhou, X. Luo, X. Li, X. Xiao, J. Chen, and X. Zhang. 2020. GasChecker: Scalable Analysis for Discovering Gas-Inefficient Smart Contracts. IEEE Transactions on Emerging Topics in Computing, 1–1. https://doi.org/10.1109/TETC.2020.2979019
[15]
Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. 2011. S2E: A Platform for in-Vivo Multi-Path Analysis of Software Systems. In Proceedings of the Sixteenth International Conference on Architectural Support for Programming Languages and Operating Systems. 46, Association for Computing Machinery, New York, NY, USA. 265–278. issn:0362-1340 https://doi.org/10.1145/1961296.1950396
[16]
E. M. Clarke, E. A. Emerson, and A. P. Sistla. 1986. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst., 8, 2 (1986), April, 244–263. issn:0164-0925 https://doi.org/10.1145/5397.5399
[17]
Edmund M. Clarke, Orna Grumberg, and David E. Long. 1994. Model Checking and Abstraction. ACM Trans. Program. Lang. Syst., 16, 5 (1994), Sept., 1512–1542. issn:0164-0925 https://doi.org/10.1145/186025.186051
[18]
Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, Kurt Jensen and Andreas Podelski (Eds.) (Lecture Notes in Computer Science, Vol. 2988). Springer, 168–176. https://doi.org/10.1007/978-3-540-24730-2_15
[19]
Mike Czech, Marie-Christine Jakobs, and Heike Wehrheim. 2016. Just test what you cannot verify!. In Software Engineering 2016, Jens Knoop and Uwe Zdun (Eds.). Gesellschaft für Informatik e.V., Bonn. 17–18.
[20]
Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg. 337–340. isbn:3540787992
[21]
Dedaub. 2021. Ethereum Pawn Stars: ’$5.7M in hard assets? Best I can do is $2.3M’. https://medium.com/dedaub/ethereum-pawn-stars-5-7m-in-hard-assets-best-i-can-do-is-2-3m-b93604be503e
[22]
Dedaub. 2021. Killing a Bad (Arbitrage) Bot ... to Save its Owners. https://medium.com/dedaub/killing-a-bad-arbitrage-bot-f29e7e808c7d
[23]
Dedaub. 2021. Look Ma’, no source! Hacking a DeFi Service with No Source Code Available. https://medium.com/dedaub/look-ma-no-source-hacking-a-defi-service-with-no-source-code-available-c40a6583f28f
[24]
Dedaub. 2021. Yield Skimming: Forcing Bad Swaps on Yield Farming. https://medium.com/dedaub/yield-skimming-forcing-bad-swaps-on-yield-farming-397361fd7c72?source=friends_link&sk=d146b3640321f0a3ccc80540b54368ff
[25]
I. Dudina and A. Belevantsev. 2017. Using static symbolic execution to detect buffer overflows. Programming and Computer Software, 43 (2017), 277–288.
[26]
Thomas Durieux, João F. Ferreira, Rui Abreu, and Pedro Cruz. 2020. Empirical Review of Automated Analysis Tools on 47,587 Ethereum Smart Contracts. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering (ICSE ’20). Association for Computing Machinery, New York, NY, USA. 530–541. isbn:9781450371216 https://doi.org/10.1145/3377811.3380364
[27]
E. Emerson and A. Sistla. 1996. Symmetry and Model Checking. Formal Methods in System Design, 9 (1996), 08, 105–131. isbn:978-3-540-56922-0 https://doi.org/10.1007/BF00625970
[28]
Josselin Feist, Gustavo Grieco, and Alex Groce. 2019. Slither: A Static Analysis Framework for Smart Contracts. 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), May, isbn:9781728122571 https://doi.org/10.1109/wetseb.2019.00008
[29]
Cormac Flanagan and Patrice Godefroid. 2005. Dynamic Partial-Order Reduction for Model Checking Software. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’05). Association for Computing Machinery, New York, NY, USA. 110–121. isbn:158113830X https://doi.org/10.1145/1040305.1040315
[30]
Patrice Godefroid. 2007. Compositional dynamic test generation. In Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 47–54.
[31]
Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed automated random testing. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 213–223. isbn:1-59593-056-6 https://doi.org/10.1145/1065010.1065036
[32]
Patrice Godefroid, Michael Y. Levin, and David Molnar. 2008. Automated Whitebox Fuzz Testing. In NDSS. 8, 151–166. https://www.microsoft.com/en-us/research/publication/automated-whitebox-fuzz-testing/
[33]
Patrice Godefroid, Michael Y. Levin, and David Molnar. 2012. SAGE: Whitebox Fuzzing for Security Testing: SAGE Has Had a Remarkable Impact at Microsoft. Commun. ACM, 10, 1 (2012), Jan., 20–27. issn:1542-7730 https://doi.org/10.1145/2090147.2094081
[34]
Neville Grech, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. 2019. Gigahorse: Thorough, Declarative Decompilation of Smart Contracts. In Proceedings of the 41st International Conference on Software Engineering (ICSE ’19). IEEE Press, Piscataway, NJ, USA. 1176–1186. https://doi.org/10.1109/ICSE.2019.00120
[35]
Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. 2018. MadMax: Surviving Out-of-Gas Conditions in Ethereum Smart Contracts. Proc. ACM Programming Languages, 2, OOPSLA (2018), Nov., https://doi.org/10.1145/3276486
[36]
Gustavo Grieco, Will Song, Artur Cygan, Josselin Feist, and Alex Groce. 2020. Echidna: Effective, Usable, and Fast Fuzzing for Smart Contracts. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2020). Association for Computing Machinery, New York, NY, USA. 557–560. isbn:9781450380089 https://doi.org/10.1145/3395363.3404366
[37]
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. 2017. Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts. Proc. ACM Program. Lang., 2, POPL (2017), Article 48, Dec., 28 pages. https://doi.org/10.1145/3158136
[38]
Ákos Hajdu and Dejan Jovanović. 2020. solc-verify: A Modular Verifier for Solidity Smart Contracts. In Verified Software. Theories, Tools, and Experiments, Supratik Chakraborty and Jorge A. Navas (Eds.). Springer International Publishing, Cham. 161–179. isbn:978-3-030-41600-3
[39]
Jingxuan He, Mislav Balunović, Nodar Ambroladze, Petar Tsankov, and Martin Vechev. 2019. Learning to Fuzz from Symbolic Execution with Application to Smart Contracts. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS ’19). Association for Computing Machinery, New York, NY, USA. 531–548. isbn:9781450367479 https://doi.org/10.1145/3319535.3363230
[40]
E. Hildenbrandt, M. Saxena, N. Rodrigues, X. Zhu, P. Daian, D. Guth, B. Moore, D. Park, Y. Zhang, A. Stefanescu, and G. Rosu. 2018. KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). 204–217. issn:2374-8303 https://doi.org/10.1109/CSF.2018.00022
[41]
J.J. Honig. 2020. Incremental symbolic execution. http://essay.utwente.nl/81526/
[42]
Ranjit Jhala and Rupak Majumdar. 2009. Software Model Checking. ACM Comput. Surv., 41, 4 (2009), Article 21, Oct., 54 pages. issn:0360-0300 https://doi.org/10.1145/1592434.1592438
[43]
Bo Jiang, Ye Liu, and W. K. Chan. 2018. ContractFuzzer: Fuzzing Smart Contracts for Vulnerability Detection. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE 2018). Association for Computing Machinery, New York, NY, USA. 259–269. isbn:9781450359375 https://doi.org/10.1145/3238147.3238177
[44]
James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM, 19, 7 (1976), July, 385–394. issn:0001-0782 https://doi.org/10.1145/360248.360252
[45]
Yoonseok Ko, Xavier Rival, and Sukyoung Ryu. 2017. Weakly Sensitive Analysis for Unbounded Iteration over JavaScript Objects. In Programming Languages and Systems, Bor-Yuh Evan Chang (Ed.). Springer International Publishing, Cham. 148–168. isbn:978-3-319-71237-6
[46]
Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor, and Prateek Saxena. 2019. Exploiting the Laws of Order in Smart Contracts. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2019). Association for Computing Machinery, New York, NY, USA. 363–373. isbn:9781450362245 https://doi.org/10.1145/3293882.3330560
[47]
Georgios Konstantopoulos. 2021. [Informal public comment, July 15, 2021]. ETHSecurity Community Telegram channel.
[48]
Johannes Krupp and Christian Rossow. 2018. TEETHER: Gnawing at Ethereum to Automatically Exploit Smart Contracts. In Proceedings of the 27th USENIX Conference on Security Symposium (SEC’18). USENIX Association, Berkeley, CA, USA. 1317–1333. isbn:978-1-931971-46-1 http://dl.acm.org/citation.cfm?id=3277203.3277303
[49]
Sifis Lagouvardos, Neville Grech, Ilias Tsatiris, and Yannis Smaragdakis. 2020. Precise Static Modeling of Ethereum “Memory”. Proc. ACM Program. Lang., 4, OOPSLA (2020), Article 190, Nov., 26 pages. https://doi.org/10.1145/3428258
[50]
You Li, Zhendong Su, Linzhang Wang, and Xuandong Li. 2013. Steering Symbolic Execution to Less Traveled Paths. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA ’13). Association for Computing Machinery, New York, NY, USA. 19–32. isbn:9781450323741 https://doi.org/10.1145/2509136.2509553
[51]
Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making Smart Contracts Smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS ’16). Association for Computing Machinery, New York, NY, USA. 254–269. isbn:9781450341394 https://doi.org/10.1145/2976749.2978309
[52]
B. Meyer. 2008. Seven Principles of Software Testing. Computer, 41, 8 (2008), 99–101. https://doi.org/10.1109/MC.2008.306
[53]
Michales, Jonah. 2021. Inside the War Room That Saved Primitive Finance. https://medium.com/immunefi/inside-the-war-room-that-saved-primitive-finance-6509e2188c86
[54]
Anders Møller and Michael I. Schwartzbach. 2018. Static Program Analysis. Department of Computer Science, Aarhus University, http://cs.au.dk/ãmoeller/spa/, Accessed: 2020-11-20.
[55]
M. Mossberg, F. Manzano, E. Hennenfent, A. Groce, G. Grieco, J. Feist, T. Brunson, and A. Dinaburg. 2019. Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts. In 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). 1186–1189. https://doi.org/10.1109/ASE.2019.00133
[56]
Tai D. Nguyen, Long H. Pham, Jun Sun, Yun Lin, and Quang Tran Minh. 2020. SFuzz: An Efficient Adaptive Fuzzer for Solidity Smart Contracts. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering (ICSE ’20). Association for Computing Machinery, New York, NY, USA. 778–788. isbn:9781450371216 https://doi.org/10.1145/3377811.3380334
[57]
Benjamin Barslev Nielsen and Anders Møller. 2020. Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript. In Proc. 34th European Conference on Object-Oriented Programming (ECOOP).
[58]
Flemming Nielson, Hanne R. Nielson, and Chris Hankin. 1999. Principles of Program Analysis. isbn:3540654100
[59]
Ivica Nikolić, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. 2018. Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. In Proceedings of the 34th Annual Computer Security Applications Conference (ACSAC ’18). ACM, New York, NY, USA. 653–663. isbn:978-1-4503-6569-7 https://doi.org/10.1145/3274694.3274743
[60]
C. Norris Ip and David L. Dill. 1993. Better Verification Through Symmetry. In Computer Hardware Description Languages and their Applications, DAVID AGNEW, LUC CLAESEN, and RAUL CAMPOSANO (Eds.). North-Holland, Amsterdam. 97 – 111. isbn:978-0-444-81641-2 https://doi.org/10.1016/B978-0-444-81641-2.50012-5
[61]
Rohan Padhye and Uday P. Khedker. 2013. Interprocedural Data Flow Analysis in Soot Using Value Contexts. In Proceedings of the 2nd ACM SIGPLAN International Workshop on State Of the Art in Java Program Analysis (SOAP ’13). Association for Computing Machinery, New York, NY, USA. 31–36. isbn:9781450322010 https://doi.org/10.1145/2487568.2487569
[62]
Sangmin Park, B. M. Mainul Hossain, Ishtiaque Hussain, Christoph Csallner, Mark Grechanik, Kunal Taneja, Chen Fu, and Qing Xie. 2012. CarFast: Achieving Higher Statement Coverage Faster. In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering (FSE ’12). Association for Computing Machinery, New York, NY, USA. Article 35, 11 pages. isbn:9781450316149 https://doi.org/10.1145/2393596.2393636
[63]
Daniel Perez and Ben Livshits. 2021. Smart Contract Vulnerabilities: Vulnerable Does Not Imply Exploited. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association, Vancouver, B.C. https://www.usenix.org/conference/usenixsecurity21/presentation/perez
[64]
A. Permenev, D. Dimitrov, P. Tsankov, D. Drachsler-Cohen, and M. Vechev. 2020. VerX: Safety Verification of Smart Contracts. In 2020 IEEE Symposium on Security and Privacy (SP). 1661–1677. https://doi.org/10.1109/SP40000.2020.00024
[65]
Primitive Finance. 2021. PrimitiveFi post-mortem analysis. https://primitivefinance.medium.com/postmortem-on-the-primitive-finance-whitehack-of-february-21st-2021-17446c0f3122
[66]
Xavier Rival and Laurent Mauborgne. 2007. The Trace Partitioning Abstract Domain. ACM Trans. Program. Lang. Syst., 29, 5 (2007), Aug., 26–es. issn:0164-0925 https://doi.org/10.1145/1275497.1275501
[67]
Clara Schneidewind, Ilya Grishchenko, Markus Scherer, and Matteo Maffei. 2020. EThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security (CCS ’20). Association for Computing Machinery, New York, NY, USA. 621–640. isbn:9781450370899 https://doi.org/10.1145/3372297.3417250
[68]
Koushik Sen and Gul Agha. 2006. Cute and jCute: Concolic Unit Testing and Explicit Path Model-Checking Tools. In Proc. International Conference on Computer Aided Verification (CAV). Springer, 419–423.
[69]
Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: A concolic unit testing engine for C. In Proc. 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE). ACM, 263–272.
[70]
Micha Sharir and Amir Pnueli. 1981. Two Approaches to Interprocedural Data Flow Analysis. In Program flow analysis: theory and applications, Steven S. Muchnick and Neil D. Jones (Eds.). Prentice-Hall, Inc., Englewood Cliffs, NJ. 189–233. isbn:0137296819
[71]
Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos, Konstantinos Triantafyllou, and Ilias Tsatiris. 2021. Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts (Artifact). https://doi.org/10.5281/zenodo.5494813
[72]
Benno Stein, Benjamin Barslev Nielsen, Bor-Yuh Evan Chang, and Anders Møller. 2019. Static Analysis with Demand-Driven Value Refinement. Proc. ACM Program. Lang., 3, OOPSLA (2019), Article 140, Oct., 29 pages. https://doi.org/10.1145/3360566
[73]
The Certora team. 2017. The Certora Prover. https://www.certora.com
[74]
Sergei Tikhomirov, Ekaterina Voskresenskaya, Ivan Ivanitskiy, Ramil Takhaviev, Evgeny Marchenko, and Yaroslav Alexandrov. 2018. SmartCheck: Static Analysis of Ethereum Smart Contracts. In Proceedings of the 1st International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB ’18). Association for Computing Machinery, New York, NY, USA. 9–16. isbn:9781450357265 https://doi.org/10.1145/3194113.3194115
[75]
Nikolai Tillmann and Jonathan de Halleux. 2008. Pex - White Box Test Generation for .Net. In Proc. 2nd International Conference on Tests And Proofs (TAP). Springer, 134–153.
[76]
Nikolai Tillmann and Wolfram Schulte. 2006. Unit Tests Reloaded: Parameterized Unit Testing with Symbolic Execution. IEEE Software, 23, 4 (2006), 38–47.
[77]
Christof Ferreira Torres, Julian Schütte, and Radu State. 2018. Osiris: Hunting for Integer Bugs in Ethereum Smart Contracts. In Proceedings of the 34th Annual Computer Security Applications Conference (ACSAC ’18). Association for Computing Machinery, New York, NY, USA. 664–676. isbn:9781450365697 https://doi.org/10.1145/3274694.3274737
[78]
Christof Ferreira Torres, Mathis Steichen, and Radu State. 2019. The Art of The Scam: Demystifying Honeypots in Ethereum Smart Contracts. In 28th USENIX Security Symposium (USENIX Security 19). USENIX Association, Santa Clara, CA. 1591–1607. isbn:978-1-939133-06-9 https://www.usenix.org/conference/usenixsecurity19/presentation/ferreira
[79]
Trail of Bits. 2020. Trail of Bits comments on average coverage. https://forum.openzeppelin.com/t/symbolic-execution/2158/3 Accessed: 2020-11-20.
[80]
Trail of Bits. 2020. Tweet on symbolic execution coverage. https://twitter.com/trailofbits/status/1223386823084384256 Accessed: 2020-11-20.
[81]
Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin Vechev. 2018. Securify: Practical Security Analysis of Smart Contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS ’18). ACM, New York, NY, USA. 67–82. isbn:978-1-4503-5693-0 https://doi.org/10.1145/3243734.3243780
[82]
Various. 2017. libFuzzer – a library for coverage-guided fuzz testing. https://llvm.org/docs/LibFuzzer.html
[83]
Various. 2020. SmartBugs: A Framework to Analyze Solidity Smart Contracts. https://github.com/smartbugs/smartbugs
[84]
Gavin Wood. 2014. Ethereum: A secure decentralised generalised transaction ledger. http://gavwood.com/paper.pdf.
[85]
Valentin Wüstholz and Maria Christakis. 2020. Harvey: A Greybox Fuzzer for Smart Contracts. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2020). Association for Computing Machinery, New York, NY, USA. 1398–1409. isbn:9781450370431 https://doi.org/10.1145/3368089.3417064
[86]
Valentin Wüstholz and Maria Christakis. 2020. Targeted Greybox Fuzzing with Static Lookahead Analysis. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering (ICSE ’20). Association for Computing Machinery, New York, NY, USA. 789–800. isbn:9781450371216 https://doi.org/10.1145/3377811.3380388

Cited By

View all
  • (2024)Practical Verification of Smart Contracts using Memory SplittingProceedings of the ACM on Programming Languages10.1145/36897968:OOPSLA2(2402-2433)Online publication date: 8-Oct-2024
  • (2024)Making Formulog Fast: An Argument for Unconventional Datalog EvaluationProceedings of the ACM on Programming Languages10.1145/36897548:OOPSLA2(1219-1248)Online publication date: 8-Oct-2024
  • (2024)Consolidating Smart Contracts with Behavioral ContractsProceedings of the ACM on Programming Languages10.1145/36564168:PLDI(965-989)Online publication date: 20-Jun-2024
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages  Volume 5, Issue OOPSLA
October 2021
2001 pages
EISSN:2475-1421
DOI:10.1145/3492349
Issue’s Table of Contents
This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 October 2021
Published in PACMPL Volume 5, Issue OOPSLA

Permissions

Request permissions for this article.

Check for updates

Badges

Author Tags

  1. Blockchain
  2. Ethereum
  3. Program Analysis
  4. Security
  5. Smart Contracts

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)381
  • Downloads (Last 6 weeks)48
Reflects downloads up to 18 Nov 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Practical Verification of Smart Contracts using Memory SplittingProceedings of the ACM on Programming Languages10.1145/36897968:OOPSLA2(2402-2433)Online publication date: 8-Oct-2024
  • (2024)Making Formulog Fast: An Argument for Unconventional Datalog EvaluationProceedings of the ACM on Programming Languages10.1145/36897548:OOPSLA2(1219-1248)Online publication date: 8-Oct-2024
  • (2024)Consolidating Smart Contracts with Behavioral ContractsProceedings of the ACM on Programming Languages10.1145/36564168:PLDI(965-989)Online publication date: 20-Jun-2024
  • (2024)Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence AnalysisProceedings of the ACM on Programming Languages10.1145/36564008:PLDI(567-592)Online publication date: 20-Jun-2024
  • (2024)Involuntary Transfer: A Vulnerability Pattern in Smart ContractsIEEE Access10.1109/ACCESS.2024.335173612(62459-62479)Online publication date: 2024
  • (2022)Elipmoc: advanced decompilation of Ethereum smart contractsProceedings of the ACM on Programming Languages10.1145/35273216:OOPSLA1(1-27)Online publication date: 29-Apr-2022

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media