Nguyen, Tai D;
Pham, Long H;
Jun, Sun;
Le, Quang Loc;
(2023)
An Idealist’s Approach for Smart Contract Correctness.
In:
Formal Methods and Software Engineering. ICFEM 2023.
(pp. pp. 11-28).
Springer: Singapore, Singapore.
Preview |
Text
paper_9.pdf - Other Download (345kB) | Preview |
Abstract
In this work, we experiment an idealistic approach for smart contract correctness verification and enforcement, based on the assump- tion that developers are either desired or required to provide a correctness specification due to the importance of smart contracts and the fact that they are immutable after deployment. We design a static verification system with a specification language which supports fully compositional verification (with the help of function specifications, contract invariants, loop invariants and call invariants). Our approach has been implemented in a tool named iContract which automatically proves the correctness of a smart contract statically or checks the unverified part of the specifica- tion during runtime. Using iContract, we have verified 10 high-profile smart contracts against manually developed detailed specifications, many of which are beyond the capacity of existing verifiers. Specially, we have uncovered two ERC20 violations in the BNB and QNT contracts.
| Type: | Proceedings paper |
|---|---|
| Title: | An Idealist’s Approach for Smart Contract Correctness |
| Event: | The 24th International Conference on Formal Engineering Methods (ICFEM 2023) |
| ISBN-13: | 978-981-99-7583-9 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-981-99-7584-6_2 |
| Publisher version: | https://doi.org/10.1007/978-981-99-7584-6_2 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10176153 |
Archive Staff Only
 |
View Item |
