Skip to main content
SpringerLink
Log in

Formal Analysis of Composable DeFi Protocols

  • Conference paper
  • First Online:
Financial Cryptography and Data Security. FC 2021 International Workshops (FC 2021)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 12676))

Included in the following conference series:

Abstract

Decentralized finance (DeFi) has become one of the most successful applications of blockchain and smart contracts. The DeFi ecosystem enables a wide range of crypto-financial activities, while the underlying smart contracts often contain bugs, with many vulnerabilities arising from the unforeseen consequences of composing DeFi protocols together. In this paper, we propose a formal process-algebraic technique that models DeFi protocols in a compositional manner to allow for efficient property verification. We also conduct a case study to demonstrate the proposed approach in analyzing the composition of two interacting DeFi protocols, namely, Curve and Compound. Finally, we discuss how the proposed modeling and verification approach can be used to analyze financial and security properties of interest.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 99.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 129.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Depending on the application, pools are also referred to as markets, vaults, or pairs.

  2. 2.

    Most of the pools in DeFi support a single pool token.

  3. 3.

    https://www.curve.fi/compound.

References

  1. Harvest Finance (2020). https://harvest.finance/. Accessed 12 Oct 2020

  2. Introduction to Yearn - yearn.finance (2020). https://docs.yearn.finance/. Accessed 12 Nov 2020

  3. Whitepaper - Balancer (2020). https://balancer.finance/whitepaper/. Accessed 12 Oct 2020

  4. Adams, H., Zinsmeister, N., Robinson, D.: Uniswap v2 Core Whitepaper (2020). https://uniswap.org/whitepaper.pdf. Accessed 12 Oct 2020

  5. Angeris, G., Kao, H.T., Chiang, R., Noyes, C., Chitra, T.: An analysis of uniswap markets (2020). https://arxiv.org/abs/1911.03380

  6. Bartoletti, M., Chiang, J.H., Lluch-Lafuente, A.: SOK: lending pools in decentralized finance (2020). https://arxiv.org/abs/2012.13230

  7. Bernardi, T., et al.: WIP: finding bugs automatically in smart contracts with parameterized invariants (2020). https://www.certora.com/pubs/sbc2020.pdf. Accessed 14 July 2020

  8. Chen, W., Zhang, T., Chen, Z., Zheng, Z., Lu, Y.: Traveling the token world: a graph analysis of Ethereum ERC20 token ecosystem. In: Proceedings of The Web Conference 2020. WWW 2020, pp. 1411–1421. ACM (2020). https://doi.org/10.1145/3366423.3380215

  9. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  10. Coingape: DeFi success story continues as TVL peaks yet again; hits \$12 billion (2020). https://coinmarketcap.com/ru/headlines/news/defi-success-story-continues-as-tvl-peaks-yet-again-hits-12-billion. Accessed 18 Nov 2020

  11. Daian, P., et al.: Flash boys 2.0: Frontrunning, transaction reordering, and consensus instability in decentralized exchanges (2019). https://arxiv.org/abs/1904.05234

  12. Egorov, M.: StableSwap - efficient mechanism for Stablecoin liquidity — Curve. fi Whitepaper (2020). https://www.curve.fi/stableswap-paper.pdf. Accessed 18 Nov 18 2020

  13. Finance, H.: Harvest Flashloan Economic Attack Post-Mortem (2020). https://medium.com/harvest-finance/harvest-flashloan-economic-attack-post-mortem-3cf900d65217. Accessed 18 Nov 2020

  14. Foxley, W.: DeFi project Akropolis drained of \$2m in DAI (2020). https://www.coindesk.com/defi-project-akropolis-token-pool-drained. Accessed 14 Nov 2020

  15. Grossman, S., et al.: Online detection of effectively callback free objects with applications to smart contracts. Proc. ACM Program. Lang. pp. 1–28 (2017). https://doi.org/10.1145/3158136

  16. Gudgeon, L., Perez, D., Harz, D., Livshits, B., Gervais, A.: The decentralized financial crisis (2020). https://arxiv.org/abs/2002.08099

  17. Gudgeon, L., Werner, S.M., Perez, D., Knottenbelt, W.J.: DeFi protocols for loanable funds: interest rates, liquidity and market efficiency (2020). https://arxiv.org/abs/2006.13922

  18. Hoare, C.A.R.: Communicating Sequential Processes. International Series on Computer Science, Prentice-Hall (1985)

    Google Scholar 

  19. Kao, H.T., Chitra, T., Chiang, R., Morrow, J.: An Analysis of the Market Risk to Participants in the Compound Protocol (2020). https://scfab.github.io/2020/FAB2020_p5.pdf. Accessed 18 Nov 2020

  20. Klages-Mundt, A., Harz, D., Gudgeon, L., Liu, J.Y., Minca, A.: Stablecoins 2.0. In: Proceedings of the 2nd ACM Conference on Advances in Financial Technologies, October 2020. https://doi.org/10.1145/3419614.3423261

  21. Leshner, R., Hayes, G.: Compound: The Money Market Protocol — Whitepaper (2020). https://compound.finance/documents/Compound.Whitepaper.pdf. Accessed 18 Nov 2020

  22. Li, X., Su, C., Xiong, Y., Huang, W., Wang, W.: Formal verification of BNB smart contract. In: Proceedings of the BIGCOM, pp. 74–78, August 2019. https://doi.org/10.1109/BIGCOM.2019.00021

  23. Lin, S., Andre, E., Liu, Y., Sun, J., Dong, J.: Learning assumptions for compositional verification of timed systems. IEEE Trans. Software Eng. (02), 137–153 (2014). https://doi.org/10.1109/TSE.2013.57

  24. Lin, S.-W., Liu, Y., Sun, J., Dong, J.S., André, É.: Automatic compositional verification of timed systems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 272–276. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_24

    Chapter  Google Scholar 

  25. Lin, S.W., Sun, J., Nguyen, T.K., Liu, Y., Dong, J.S.: Interpolation guided compositional verification. In: Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering. ASE 2015, pp. 65–74. IEEE Press (2015). https://doi.org/10.1109/ASE.2015.33

  26. Liu, B., Szalachowski, P.: A first look into DeFi oracles (2020). https://arxiv.org/abs/2005.04377

  27. Liu, C., Liu, H., Cao, Z., Chen, Z., Chen, B., Roscoe, B.: ReGuard: finding reentrancy bugs in smart contracts. In: Proceedings of the 40th International Conference on Software Engineering: Companion Proceedings, pp. 65–68. ACM (2018). https://doi.org/10.1145/3183440.3183495

  28. Liu, Y., Sun, J., Dong, J.S.: Pat 3: An extensible architecture for building multi-domain model checkers. In: 2011 IEEE 22nd International Symposium on Software Reliability Engineering, pp. 190–199 (2011). https://doi.org/10.1109/ISSRE.2011.19

  29. Moin, A., Sirer, E.G., Sekniqi, K.: A classification framework for stablecoin designs (2019). https://arxiv.org/abs/1910.10098

  30. Perez, D., Werner, S.M., Xu, J., Livshits, B.: Liquidations: DeFi on a knife-edge (2020). https://arxiv.org/abs/2009.13235

  31. Pulse, D.: DeFi status report post-black thursday (2020). https://defipulse.com/blog/defi-status-report-black-thursday. Accessed 18 Nov 2020

  32. Qin, K., Zhou, L., Livshits, B., Gervais, A.: Attacking the DeFi ecosystem with flash loans for fun and profit (2020). https://arxiv.org/abs/2003.03810

  33. Qu, M., Huang, X., Chen, X., Wang, Y., Ma, X., Liu, D.: Formal verification of smart contracts from the perspective of concurrency. In: Qiu, M. (ed.) SmartBlock 2018. LNCS, vol. 11373, pp. 32–43. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-05764-0_4

    Chapter  Google Scholar 

  34. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall (1997). iSBN 0-13-674409-5

    Google Scholar 

  35. Samreen, N., Alalfi, M.H.: Reentrancy vulnerability identification in Ethereum smart contracts. In: 2020 IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE), pp. 22–29 (2020). https://doi.org/10.1109/IWBOSE50093.2020.9050260

  36. Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_59

    Chapter  Google Scholar 

  37. Sun, J., Liu, Y., Dong, J.S.: Model checking CSP revisited: introducing a process analysis toolkit. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 307–322. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88479-8_22

    Chapter  Google Scholar 

  38. Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating specification and programs for system modeling and verification. In: Proceedings of the 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 127–135 (2009). https://doi.org/10.1109/TASE.2009.32

  39. Tolmach, P., Li, Y., Lin, S.-W., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. ACM Comput. Surv. 54(7), 38 p. (2021). Article no. 148. https://doi.org/10.1145/3464421

  40. Totle: Building with Money Legos (2020). https://medium.com/totle/building-with-money-legos-ab63a58ae764. Accessed 17 Nov 2020

  41. Vogelsteller, F., Buterin, V.: ERC-20 token standard (2015). https://eips.ethereum.org/EIPS/eip-20. Accessed 14 July 2020

  42. Wang, D., et al.: Towards understanding flash loan and its applications in DeFi ecosystem (2020). https://arxiv.org/abs/2010.12252

  43. Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 1–36 (2009). https://doi.org/10.1145/1592434.1592436

    Article  Google Scholar 

Download references

Acknowledgements

This research is partially supported by the Ministry of Education, Singapore, under its Academic Research Fund Tier 1 (Award No. 2018-T1-002-069) and Tier 2 (Award No. MOE2018-T2-1-068), and by the National Research Foundation, Singapore, and the Energy Market Authority, under its Energy Programme (EP Award No. NRF2017EWT-EP003-023). Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not reflect the views of National Research Foundation, Singapore and the Energy Market Authority.

Author information

Authors and Affiliations

  1. Institute of High Performance Computing, Agency for Science, Technology and Research, Singapore, Singapore

    Palina Tolmach

  2. Nanyang Technological University, Singapore, Singapore

    Palina Tolmach, Yi Li, Shang-Wei Lin & Yang Liu

Authors
  1. Palina Tolmach
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yi Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Shang-Wei Lin
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yang Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Palina Tolmach .

Editor information

Editors and Affiliations

  1. University of Michigan–Ann Arbor, Ann Arbor, MI, USA

    Matthew Bernhard

  2. Computer Science and Mathematics, Stirling University, Stirling, UK

    Andrea Bracciali

  3. Imperial College London, London, UK

    Lewis Gudgeon

  4. Norwegian University of Science and Technology, Trondheim, Norway

    Thomas Haines

  5. Ithaca College, Ithaca, USA

    Ariah Klages-Mundt

  6. Department of Computer Science, Georgetown University, Washington, WA, USA

    Shin'ichiro Matsuo

  7. Imperial College London, London, UK

    Daniel Perez

  8. Dipartimento di Matematica, University of Trento, Trento, Trento, Italy

    Massimiliano Sala

  9. Imperial College London, London, UK

    Sam Werner

Rights and permissions

Reprints and permissions

Copyright information

© 2021 International Financial Cryptography Association

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Tolmach, P., Li, Y., Lin, SW., Liu, Y. (2021). Formal Analysis of Composable DeFi Protocols. In: Bernhard, M., et al. Financial Cryptography and Data Security. FC 2021 International Workshops. FC 2021. Lecture Notes in Computer Science(), vol 12676. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-63958-0_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-63958-0_13

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-63957-3

  • Online ISBN: 978-3-662-63958-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation