Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

Formal Analysis of Lending Pools in Decentralized Finance

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning (ISoLA 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13703))

Included in the following conference series:

Abstract

Decentralised Finance (DeFi) applications constitute an entire financial ecosystem deployed on blockchains. Such applications are based on complex protocols and incentive mechanisms whose financial safety is hard to determine. Besides, their adoption is rapidly growing, hence imperilling an increasingly higher amount of assets. Therefore, accurate formalisation and verification of DeFi applications is essential to assess their safety. We have developed a tool for the formal analysis of one of the most widespread DeFi applications: Lending Pools (LP). This was achieved by leveraging an existing formal model for LPs, the Maude verification environment and the MultiVeStA statistical analyser. The tool supports several analyses including reachability analysis, LTL model checking and statistical model checking. In this paper we show how the tool can be used to analyse several parameters of LPs that are fundamental to assess and predict their behaviour. In particular, we use statistical analysis to search for threshold and reward parameters that minimize the risk of unrecoverable loans.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 79.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

Similar content being viewed by others

References

  1. Aave, S.: Aave markets - webpage (2021). https://aave.com/

  2. Abdellatif, T., Brousmiche, K.L.: Formal verification of smart contracts based on users and blockchain behaviors models. In: 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS), pp. 1–5. IEEE (2018)

    Google Scholar 

  3. Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. (TOMACS) 28(1), 1–39 (2018)

    Article  MathSciNet  Google Scholar 

  4. Angeris, G., Kao, H.T., Chiang, R., Noyes, C., Chitra, T.: An analysis of Uniswap markets. Cryptoeconomic Syst. (1) (2021). https://doi.org/10.21428/58320208.c9738e64

  5. Bai, X., Cheng, Z., Duan, Z., Hu, K.: Formal modeling and verification of smart contracts. In: Proceedings of the 2018 7th International Conference on Software and Computer Applications, pp. 322–326 (2018)

    Google Scholar 

  6. Bartoletti, M., Chiang, J.H., Lafuente, A.L.: SoK: lending pools in decentralized finance. In: Bernhard, M., et al. (eds.) FC 2021. LNCS, vol. 12676, pp. 553–578. Springer, Heidelberg (2021). https://doi.org/10.1007/978-3-662-63958-0_40

    Chapter  Google Scholar 

  7. Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41–48 (2011)

    Article  Google Scholar 

  8. Bernardi, T., et al.: WIP: finding bugs automatically in smart contracts with parameterized invariants (2020). https://groups.csail.mit.edu/sdg/pubs/2020/sbc2020.pdf

  9. Bigi, G., Bracciali, A., Meacci, G., Tuosto, E.: Validation of decentralised smart contracts through game theory and formal methods. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 142–161. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25527-9_11

    Chapter  MATH  Google Scholar 

  10. Boado, E.: Aave whitepaper (2020). https://github.com/aave/protocol-v2/blob/master/aave-v2-whitepaper.pdf. Accessed 26 Feb 2021 - commit aeded1520c667e59a564cf69f33a6e489b2fe489

  11. Boado, E., Aave, S.: Aave protocol maximum liquidate threshold (2021). https://github.com/aave/aave-protocol/blob/1ff8418eb5c73ce233ac44bfb7541d07828b273f/contracts/lendingpool/LendingPoolLiquidationManager.sol#L181

  12. Buterin, V.: Ethereum whitepaper (2013). https://ethereum.org/en/whitepaper/. Accessed 24 Feb 2021

  13. Chitra, T., Evans, A.: Why stake when you can borrow? CoRR arXiv:2006.11156 (2020)

  14. Chitra, T., Quaintance, M., Haber, S., Martino, W.: Agent-based simulations of blockchain protocols illustrated via Kadena’s chainweb. In: 2019 IEEE European Symposium on Security and Privacy Workshops (EuroS &PW), pp. 386–395. IEEE (2019)

    Google Scholar 

  15. Clavel, M., et al.: Maude manual (version 3.0). Technical report, SRI International Computer Science Laboratory (2020)

    Google Scholar 

  16. Compound Labs, I.: Compound markets - webpage (2021). https://compound.finance/markets

  17. Dmouj, A.: Stock price modelling: theory and practice. Masters Degree Thesis, Vrije Universiteit (2006)

    Google Scholar 

  18. Entriken, W.: Introduction to smart contracts (2020). https://ethereum.org/en/developers/docs/smart-contracts/. Accessed 27 Feb 2021

  19. Gudgeon, L., Perez, D., Harz, D., Livshits, B., Gervais, A.: The decentralized financial crisis. In: 2020 Crypto Valley Conference on Blockchain Technology (CVCBT), pp. 1–15. IEEE (2020)

    Google Scholar 

  20. Hull, J.C.: Options Futures and Other Derivatives. Pearson Education India (2003)

    Google Scholar 

  21. Jeffrey, G.: Compound price oracle attack (2020). https://news.bitcoin.com/100-million-liquidated-on-defi-protocol-compound-following-oracle-exploit/

  22. Kao, H.T., Chitra, T., Chiang, R., Morrow, J.: An analysis of the market risk to participants in the Compound protocol. In: Third International Symposium on Foundations and Applications of Blockchains (2020)

    Google Scholar 

  23. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  24. Leshner, R., Hayes, G.: Compound: the money market protocol (2019). https://compound.finance/documents/Compound.Whitepaper.v04.pdf

  25. Mirelli, M.: A formal verification tool for lending pools. Master’s thesis, Aalto University. School of Science (2021). http://urn.fi/URN:NBN:fi:aalto-202108298504

  26. Mirelli, M.: A maude simulator for lending pools (2021). https://github.com/MMirelli/maude-lp. Accessed 22 June 2022 - commit 2dae39b035938f5f9791040c53121fb473b4b7dd

  27. Perez, D., Werner, S.M., Xu, J., Livshits, B.: Liquidations: DeFi on a knife-edge. In: Borisov, N., Diaz, C. (eds.) FC 2021. LNCS, vol. 12675, pp. 457–476. Springer, Heidelberg (2021). https://doi.org/10.1007/978-3-662-64331-0_24

    Chapter  Google Scholar 

  28. Peterins, E., Flatow, J., Hayes, G., Wolff, M., Greenberg, A.: Compound protocol maximum liquidate threshold (2021). https://github.com/compound-finance/compound-protocol/blob/4e99ea3a64ab4f1bdf9c07c7a1bf325db09ab809/scenario/src/Event/ComptrollerEvent.ts#L170

  29. Pulse: Defi pulse - webpage (2021). https://defipulse.com. Accessed 07 June 2021

  30. Qin, K., Zhou, L., Livshits, B., Gervais, A.: Attacking the DeFi ecosystem with flash loans for fun and profit. In: Borisov, N., Diaz, C. (eds.) FC 2021. LNCS, vol. 12674, pp. 3–32. Springer, Heidelberg (2021). https://doi.org/10.1007/978-3-662-64322-8_1

    Chapter  MATH  Google Scholar 

  31. Sebastio, S., Vandin, A.: Multivesta: Statistical model checking for discrete event simulators. Technical report, IMT Institute for Advanced Studies Lucca (2013)

    Google Scholar 

  32. Tolmach, P., Li, Y., Lin, S.W., Liu, Y.: Formal analysis of composable DeFi protocols. arXiv preprint arXiv:2103.00540 (2021)

  33. Vandin, A., Giachini, D., Lamperti, F., Chiaromonte, F.: Automated and distributed statistical analysis of economic agent-based models. arXiv preprint arXiv:2102.05405 (2021)

  34. Wackerow, P., Rhechler: Decentralized finance (DeFi) - webpage (2021). https://ethereum.org/en/defi/. Accessed 02 June 2021

  35. Werner, S.M., Perez, D., Gudgeon, L., Klages-Mundt, A., Harz, D., Knottenbelt, W.J.: SoK: decentralized Finance (DeFi). CoRR arXiv:2101.08778 (2021)

  36. Zhou, L., Qin, K., Cully, A., Livshits, B., Gervais, A.: On the just-in-time discovery of profit-generating transactions in DeFi protocols. In: IEEE Symposium on Security and Privacy, pp. 919–936. IEEE (2021). https://doi.org/10.1109/SP40001.2021.00113

Download references

Acknowledgements

Massimo Bartoletti is partially supported by Conv. Fondazione di Sardegna & Atenei Sardi project F75F21001220007 ASTRID. James Hsin-yu Chiang is supported by the PhD School of DTU Compute. Alberto Lluch Lafuente is partially supported by the EU H2020-SU-ICT-03-2018 Project No. 830929 CyberSec4Europe (cybersec4europe.eu). Andrea Vandin is partially supported by the DFF project REDUCTO 9040-00224B.

Author information

Authors and Affiliations

  1. Università degli Studi di Cagliari, Cagliari, Italy

    Massimo Bartoletti

  2. Technical University of Denmark, DTU Compute, Copenhagen, Denmark

    James Chiang, Alberto Lluch Lafuente, Massimiliano Mirelli & Andrea Vandin

  3. Aalto University, Espoo, Finland

    Tommi Junttila

  4. Sant’Anna School of Advanced Studies, Pisa, Italy

    Andrea Vandin

Authors
  1. Massimo Bartoletti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. James Chiang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tommi Junttila
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Alberto Lluch Lafuente
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Massimiliano Mirelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Andrea Vandin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alberto Lluch Lafuente .

Editor information

Editors and Affiliations

  1. University of Limerick, CSIS and Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Figures

Figures

Fig. 9.
figure 9

Trimester closing prices, collected from CoinGecko APIs

Full size image
Fig. 10.
figure 10

Prices predictions produced, for each scenario in Table 3, by GBMs instantiated with the parameters in Fig. 5.

Full size image
Fig. 11.
figure 11

Per-borrower collateralization (\(\textrm{b}_{1}\) to \(\textrm{b}_{5}\)) in the three prices scenarios, for varying CMin-rliq choices.

Full size image
Fig. 12.
figure 12

Per-borrower collateralization (\(\textrm{b}_{3}\) to \(\textrm{b}_{7}\)) in the three prices scenarios, for varying CMin-rliq choices.

Full size image

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bartoletti, M., Chiang, J., Junttila, T., Lluch Lafuente, A., Mirelli, M., Vandin, A. (2022). Formal Analysis of Lending Pools in Decentralized Finance. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning. ISoLA 2022. Lecture Notes in Computer Science, vol 13703. Springer, Cham. https://doi.org/10.1007/978-3-031-19759-8_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-19759-8_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-19758-1

  • Online ISBN: 978-3-031-19759-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation