Document Open Access Logo

Towards Verified Price Oracles for Decentralized Exchange Protocols

Authors Kinnari Dave, Vilhelm Sjöberg, Xinyuan Sun

PDF
Thumbnail PDF

File

OASIcs.FMBC.2021.1.pdf
  • Filesize: 0.59 MB
  • 14 pages

Document Identifiers

Author Details

Kinnari Dave
  • CertiK, New York, NY, USA
Vilhelm Sjöberg
  • CertiK, New York, NY, USA
Xinyuan Sun
  • CertiK, New York, NY, USA

Acknowledgements

The work was partially supported by a Conflux Ecosystem Grant (October 2020).

Cite As Get BibTex

Kinnari Dave, Vilhelm Sjöberg, and Xinyuan Sun. Towards Verified Price Oracles for Decentralized Exchange Protocols. In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 1:1-1:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/OASIcs.FMBC.2021.1

Abstract

Various smart contracts have been designed and deployed on blockchain platforms to enable cryptocurrency trading, leading to an ever expanding user base of decentralized exchange platforms (DEXs). Automated Market Maker contracts enable token exchange without the need of third party book-keeping. These contracts also serve as price oracles for other contracts, by using a mathematical formula to calculate token exchange rates based on token reserves. However, the price oracle mechanism is vulnerable to attacks both from programming errors and from mistakes in the financial model, and so far their complexity makes it difficult to formally verify them. We present a verified AMM contract and validate its financial model by proving a theorem about a lower bound on the cost of manipulation of the token prices to the attacker. The contract is implemented using the DeepSEA system, which ensures that the theorem applies to the actual EVM bytecode of the contract. This theorem could be used as proof of correctness for other contracts using the AMM, so this is a step towards a verified DeFi landscape.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
Keywords
  • Smart Contract Verification
  • Interactive Theorem Proving
  • Blockchain
  • Decentralized Finance

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Hayden Adams, Noah Zinsmeister, and Dan Robinson. Uniswap v2 core. 2020, 2020. URL: https://uniswap.org/whitepaper.pdf.
  2. Hayden Adams, Noah Zinsmeister, Moody Salem, River Keefer, and Dan Robinson. Uniswap v3 core, 2021. Google Scholar
  3. Guillermo Angeris and Tarun Chitra. Improved price oracles: Constant function market makers. In Proceedings of the 2nd ACM Conference on Advances in Financial Technologies, pages 80-91, 2020. Google Scholar
  4. Guillermo Angeris, Hsien-Tang Kao, Rei Chiang, Charlie Noyes, and Tarun Chitra. An analysis of uniswap markets. arXiv preprint, 2019. URL: http://arxiv.org/abs/1911.03380.
  5. Korantin Auguste. The bzx attacks explained. Blog post. https://www.palkeo.com/en/projects/ethereum/bzx.html#second-transaction., 2020. (Accessed on 05/23/2021).
  6. Massimo Bartoletti, James Hsin-yu Chiang, and Alberto Lluch-Lafuente. Sok: Lending pools in decentralized finance. CoRR, abs/2012.13230, 2020. URL: http://arxiv.org/abs/2012.13230.
  7. Massimo Bartoletti, James Hsin-yu Chiang, and Alberto Lluch-Lafuente. A theory of automated market makers in defi. arXiv preprint, 2021. URL: http://arxiv.org/abs/2102.11350.
  8. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for coq. Mathematics in Computer Science, 9(1):41-62, 2015. Google Scholar
  9. Vitalik Buterin. On path independence. Blog post, 2017. URL: https://vitalik.ca/general/2017/06/22/marketmakers.html.
  10. CertiK Foundation. DeepSEA. (Accessed on 05/23/2021). URL: https://github.com/certikfoundation/deepsea.
  11. Wanyun Catherine Gu, Anika Raghuvanshi, and Dan Boneh. Empirical measurements on pricing oracles and decentralized governance for stablecoins. Available at SSRN 3611231, 2020. Google Scholar
  12. Xavier Leroy. The CompCert verified compiler. http://compcert.inria.fr/, 2005-2021.
  13. Bowen Liu, Pawel Szalachowski, and Jianying Zhou. A first look into defi oracles. arXiv preprint, 2020. URL: http://arxiv.org/abs/2005.04377.
  14. Érik Martin-Dorel, Laurence Rideau, Laurent Théry, Micaela Mayero, and Ioana Pasca. Certified, efficient and sharp univariate taylor models in coq. In 2013 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pages 193-200. IEEE, 2013. Google Scholar
  15. Guillaume Melquiond. Coq-interval. Retrieved June, 17:2017, 2011. Google Scholar
  16. miscellanous. Cryptocurrency statistics. Blog post, 2020. URL: https://duneanalytics.com/queries/4494/8769.
  17. miscellanous. Defi statistics. Blog post, 2020. URL: https://cointelegraph.com/news/defi-hacks-and-exploits-total-285m-since-2019-messari-reports.
  18. Vilhelm Sjöberg, Yuyang Sang, Shu-chun Weng, and Zhong Shao. DeepSEA: a language for certified system software. Proceedings of the ACM on Programming Languages, 3(OOPSLA):1-27, 2019. Google Scholar
  19. Xinyuan Sun, Shaokai Lin, Vilhelm Sjöberg, and Jay Jie. How to exploit a defi project (extended talk abstract). Talk at the 1st Workshop on Decentralized Finance (DeFi), colocated with Financial Cryptography and Data Security 2021 (fc21), March 2021. Google Scholar
  20. The Coq Development Team. The Coq proof assistant. https://coq.inria.fr/. Accessed: 28/5/2019.
  21. Palina Tolmach, Yi Li, Shang-Wei Lin, and Yang Liu. Formal analysis of composable defi protocols. CoRR, abs/2103.00540, 2021. URL: http://arxiv.org/abs/2103.00540.
  22. Dabao Wang, Siwei Wu, Ziling Lin, Lei Wu, Xingliang Yuan, Yajin Zhou, Haoyu Wang, and Kui Ren. Towards understanding flash loan and its applications in defi ecosystem. CoRR, abs/2010.12252, 2020. URL: http://arxiv.org/abs/2010.12252.
  23. Daejun Park Yi Zhang, Xiaohong Chen. Formal specification of constant product market maker model and implementation, 2018. URL: https://github.com/runtimeverification/verified-smart-contracts/blob/uniswap/uniswap/x-y-k.pdf.
  24. Liyi Zhou, Kaihua Qin, Antoine Cully, Benjamin Livshits, and Arthur Gervais. On the just-in-time discovery of profit-generating transactions in defi protocols. arXiv preprint, 2021. URL: http://arxiv.org/abs/2103.02228.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact