Formal Tools for Specifying Financial Smart Contracts

Financial smart contracts routinely manage billions of US dollars worth of digital assets, and as a consequence bugs in smart contracts can be extremely costly. Because of this, much work has been done in formal verification of smart contracts to prove a contract correct with regards to its specification. However, financial smart contracts have complicated specifications, and it is not all straightforward to write one which correctly describes its intended behaviors. As a response to this challenge, we develop formal tools for specifying financial smart contracts. We target aspects of contract specification which are typically difficult to address and which can be a source of expensive contract vulnerabilities. In doing so, we hope to expand the capability of formal methods to specify desired contract behavior and thereby prevent catastrophic loss of funds.

Name dc:type.qualificationname

Doctor of Philosophy (PhD)

Level dc:type.qualificationlevel

Doctoral

Grantor dc:publisher.institution

University of Cambridge

Year dc:date.issued

2023

Author dc:creator

• Sorensen, Derek

Advisors dc:contributor.advisor

• Madhavapeddy, Anil
• Srinivasan, Keshav

• blockchain
• formal methods
• formal verification
• interactive theorem prover
• smart contract verification
• smart contracts

Licence

• https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/c43b7177-8daa-4859-b278-9fd28f30586e/download
• http://purl.org/NET/rdflicense/allrightsreserved

Language dc:language

eng

Author Identifier

0000-0003-4937-6984

OAI identifier oai:identifier

oai:www.repository.cam.ac.uk:1810/384514