Verification of Smart Contracts for Security Properties Rooted in Computational Complexity

Smart contracts are digital code similar to physical contracts, but hosted, executed and guaranteed by a trusted network called a blockchain. They are a significant step forward in the specification and enforcement of contracts because they can be executed and their conditions enforced much faster than physical contracts. A significant technical issue regards the verification that a smart contract indeed satisfies some desirable property, e.g., that a clause will indeed be triggered if some condition is satisfied. This issue arises because a smart contract is typically specified imperatively, whereas properties of interest are stated declaratively. While a number of software tools have been proposed for this problem, recent work has identified significant gaps in them. This proposed work takes a systematic approach to the design and implementation of two verification tools for smart contracts that is rooted in computing foundations. The partner organization has interest in exactly this kind of technology, and intends to leverage it to positively impact their core business.

Faculty Supervisor:

Mahesh Tripunitara

Student:

Partner:

Mosaixsoft Inc

Discipline:

Engineering

Sector:

Information and cultural industries

University:

University of Waterloo

Program: