A formal verification tool for Lending Pools

Abstract

Decentralised Finance (DeFi) applications compose an entire financial ecosystem deployed on the Ethereum blockchain. DeFi applications consist of complex and new protocols whose financial safety is not entirely clear. Besides, their adoption is rapidly growing, hence imperilling an increasingly higher amount of assets. Therefore, an accurate formalisation and verification of their behaviour is essential to deepen the understanding of their safety. A first step in this direction was taken by Bartoletti et al. (arXiv:2012.13230,2020) defining a formal model for the most widespread DeFi protocols: Lending Pools (LP).

The primary aim of this thesis was to develop a verification tool of the LP model. This was achieved by leveraging the Maude verification environment and the MultiVeStA statistical analyser. Maude is a verification toolset enabling to simulate and conduct various analyses on a model specified in the Maude specification language. MultiVeStA is a Java engine enabling statistical analyses via Monte-Carlo discrete-event simulations, such as the ones generated by a model specified in Maude. Thus, a simulator of lending pools was developed in the Maude language and it was integrated with MultiVeStA in order to support several analyses on LP, including reachability analysis, LTL model checking and statistical analyses. The Maude simulator was also validated by a complete suite of test cases.

Furthermore, the proposed tool allows to statistically analyse several parameters of LP, which are fundamental to enhance its safety. In order to illustrate this, a statistical analysis was developed by the means of the MultiVeStA engine. The results of the analysis was that the default parameters, presented by Bartoletti et al., appear to maximise the platform financial safety. Additionally, the verification tool is open to the public under GNU-GPLv2.0 and it is available at https://github.com/MMirelli/maude-lp.