Solvent: liquidity verification of smart contracts
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917081827508224 |
|---|---|
| author | Bartoletti, Massimo Ferrando, Angelo Lipparini, Enrico Malvone, Vadim |
| author_facet | Bartoletti, Massimo Ferrando, Angelo Lipparini, Enrico Malvone, Vadim |
| contents | Smart contracts are an attractive target for attackers, as evidenced by a long history of security incidents. A current limitation of smart contract verification tools is that they are not really effective in expressing and verifying liquidity properties regarding the exchange of crypto-assets: for example, is it true that in every reachable state a user can fire a sequence of transactions to withdraw a given amount of crypto-assets? We propose Solvent, a tool aimed at verifying these kinds of properties, which are beyond the reach of existing verification tools for Solidity. We evaluate the effectiveness and performance of Solvent through a common benchmark of smart contracts. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_17864 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Solvent: liquidity verification of smart contracts Bartoletti, Massimo Ferrando, Angelo Lipparini, Enrico Malvone, Vadim Cryptography and Security Programming Languages Smart contracts are an attractive target for attackers, as evidenced by a long history of security incidents. A current limitation of smart contract verification tools is that they are not really effective in expressing and verifying liquidity properties regarding the exchange of crypto-assets: for example, is it true that in every reachable state a user can fire a sequence of transactions to withdraw a given amount of crypto-assets? We propose Solvent, a tool aimed at verifying these kinds of properties, which are beyond the reach of existing verification tools for Solidity. We evaluate the effectiveness and performance of Solvent through a common benchmark of smart contracts. |
| title | Solvent: liquidity verification of smart contracts |
| topic | Cryptography and Security Programming Languages |
| url | https://arxiv.org/abs/2404.17864 |