Formal Analysis of Lending Pools in Decentralized Finance

Massimo Bartoletti; James Chiang; Tommi Junttila; Alberto Lluch Lafuente; Massimiliano Mirelli; Andrea Vandin

doi:10.1007/978-3-031-19759-8_21

Formal Analysis of Lending Pools in Decentralized Finance

Massimo Bartoletti, James Chiang, Tommi Junttila, Alberto Lluch Lafuente^*, Massimiliano Mirelli, Andrea Vandin

^*Tämän työn vastaava kirjoittaja

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussa › Conference contribution › Scientific › vertaisarvioitu

1 Sitaatiot (Scopus)

Abstrakti

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.

Alkuperäiskieli	Englanti
Otsikko	Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Proceedings
Toimittajat	Tiziana Margaria, Bernhard Steffen
Kustantaja	SPRINGER
Sivut	335-355
Sivumäärä	21
ISBN (painettu)	9783031197581
DOI - pysyväislinkit	https://doi.org/10.1007/978-3-031-19759-8_21
Tila	Julkaistu - 2022
OKM-julkaisutyyppi	A4 Artikkeli konferenssijulkaisuussa
Tapahtuma	International Symposium on Leveraging Applications of Formal Methods, Verification and Validation - Rhodes, Kreikka Kesto: 22 lokak. 2022 → 30 lokak. 2022 Konferenssinumero: 11

Julkaisusarja

Nimi	Lecture Notes in Computer Science
Kustantaja	Springer
Vuosikerta	13703 LNCS
ISSN (painettu)	0302-9743
ISSN (elektroninen)	1611-3349

Conference

Conference	International Symposium on Leveraging Applications of Formal Methods, Verification and Validation
Lyhennettä	ISoLA
Maa/Alue	Kreikka
Kaupunki	Rhodes
Ajanjakso	22/10/2022 → 30/10/2022

Pääsy asiakirjaan

10.1007/978-3-031-19759-8_21

https://arxiv.org/abs/2206.01333

SFX-saatavuus

Koko teksti

Muut tiedostot ja linkit

Linkki julkaisuun Scopuksessa

Siteeraa tätä

Bartoletti, M., Chiang, J., Junttila, T., Lluch Lafuente, A., Mirelli, M., & Vandin, A. (2022). Formal Analysis of Lending Pools in Decentralized Finance. teoksessa T. Margaria, & B. Steffen (Toimittajat), Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Proceedings (Sivut 335-355). (Lecture Notes in Computer Science ; Vuosikerta 13703 LNCS). SPRINGER. https://doi.org/10.1007/978-3-031-19759-8_21

Bartoletti, Massimo ; Chiang, James ; Junttila, Tommi et al. / Formal Analysis of Lending Pools in Decentralized Finance. Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Proceedings. Toimittaja / Tiziana Margaria ; Bernhard Steffen. SPRINGER, 2022. Sivut 335-355 (Lecture Notes in Computer Science ).

@inproceedings{5ce8f50c1e684e6ca0b44d9eef49c13d,

title = "Formal Analysis of Lending Pools in Decentralized Finance",

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.",

author = "Massimo Bartoletti and James Chiang and Tommi Junttila and {Lluch Lafuente}, Alberto and Massimiliano Mirelli and Andrea Vandin",

note = "Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.; International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA ; Conference date: 22-10-2022 Through 30-10-2022",

year = "2022",

doi = "10.1007/978-3-031-19759-8_21",

language = "English",

isbn = "9783031197581",

series = "Lecture Notes in Computer Science ",

publisher = "SPRINGER",

pages = "335--355",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Proceedings",

address = "Germany",

}

Bartoletti, M, Chiang, J, Junttila, T, Lluch Lafuente, A, Mirelli, M & Vandin, A 2022, Formal Analysis of Lending Pools in Decentralized Finance. julkaisussa T Margaria & B Steffen (toim), Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Proceedings. Lecture Notes in Computer Science , Vuosikerta 13703 LNCS, SPRINGER, Sivut 335-355, International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Rhodes, Kreikka, 22/10/2022. https://doi.org/10.1007/978-3-031-19759-8_21

Formal Analysis of Lending Pools in Decentralized Finance. / Bartoletti, Massimo; Chiang, James; Junttila, Tommi et al.

Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Proceedings. toim. / Tiziana Margaria; Bernhard Steffen. SPRINGER, 2022. s. 335-355 (Lecture Notes in Computer Science ; Vuosikerta 13703 LNCS).

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussa › Conference contribution › Scientific › vertaisarvioitu

TY - GEN

T1 - Formal Analysis of Lending Pools in Decentralized Finance

AU - Bartoletti, Massimo

AU - Chiang, James

AU - Junttila, Tommi

AU - Lluch Lafuente, Alberto

AU - Mirelli, Massimiliano

AU - Vandin, Andrea

N1 - Conference code: 11

PY - 2022

Y1 - 2022

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85142761249&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-19759-8_21

DO - 10.1007/978-3-031-19759-8_21

M3 - Conference contribution

AN - SCOPUS:85142761249

SN - 9783031197581

T3 - Lecture Notes in Computer Science

SP - 335

EP - 355

BT - Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Proceedings

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - SPRINGER

T2 - International Symposium on Leveraging Applications of Formal Methods, Verification and Validation

Y2 - 22 October 2022 through 30 October 2022

ER -

Bartoletti M, Chiang J, Junttila T, Lluch Lafuente A, Mirelli M, Vandin A. Formal Analysis of Lending Pools in Decentralized Finance. julkaisussa Margaria T, Steffen B, toimittajat, Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Proceedings. SPRINGER. 2022. s. 335-355. (Lecture Notes in Computer Science ). https://doi.org/10.1007/978-3-031-19759-8_21