Gradual Verification for Smart Contracts
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913415130251264 |
|---|---|
| author | Sun, Haojia Singh, Kunal Ramos-Dávila, Jan-Paul Aldrich, Jonathan DiVincenzo, Jenna |
| author_facet | Sun, Haojia Singh, Kunal Ramos-Dávila, Jan-Paul Aldrich, Jonathan DiVincenzo, Jenna |
| contents | Blockchains facilitate secure resource transactions through smart contracts, yet these digital agreements are prone to vulnerabilities, particularly when interacting with external contracts, leading to substantial monetary losses. Traditional verification techniques fall short in providing comprehensive security assurances, especially against re-entrancy attacks, due to the unavailable implementations of external contracts. This paper introduces an incremental approach: gradual verification. We combine static and dynamic verification techniques to enhance security, guarantee soundness and flexibility, and optimize resource usage in smart contract interactions. By implementing a prototype for gradually verifying Algorand smart contracts via the pyTEAL language, we demonstrate the effectiveness of our approach, contributing to the safe and efficient execution of smart contracts. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2311_13351 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Gradual Verification for Smart Contracts Sun, Haojia Singh, Kunal Ramos-Dávila, Jan-Paul Aldrich, Jonathan DiVincenzo, Jenna Cryptography and Security Logic in Computer Science Programming Languages Blockchains facilitate secure resource transactions through smart contracts, yet these digital agreements are prone to vulnerabilities, particularly when interacting with external contracts, leading to substantial monetary losses. Traditional verification techniques fall short in providing comprehensive security assurances, especially against re-entrancy attacks, due to the unavailable implementations of external contracts. This paper introduces an incremental approach: gradual verification. We combine static and dynamic verification techniques to enhance security, guarantee soundness and flexibility, and optimize resource usage in smart contract interactions. By implementing a prototype for gradually verifying Algorand smart contracts via the pyTEAL language, we demonstrate the effectiveness of our approach, contributing to the safe and efficient execution of smart contracts. |
| title | Gradual Verification for Smart Contracts |
| topic | Cryptography and Security Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2311.13351 |