Verifying smart contracts for blockchain

Blockchain based technologies are a large and growing area underpinning the rapid growth in digital finance and distributed ledger technologies and markets. However, fundamental obstacles with transaction time, trust and cost remain which restricts their widespread adoption. One of the key problem areas to be addressed is the verification of smart contracts. EIT Digital is therefore offering an industrial Doctorate at IOHK and the University of Edinburgh to develop  prototypes for verifying smart contracts.

This PhD will develop techniques for specifying and verifying smart contracts written in Plutus and incorporated into a proof of concept prototype. This development of this technology may have wider impact on other Blockchain variants that support smart contracts, of which there are dozens.

Verification smart contracts

One key issue with current blockchain technology is an absence of trust. Until this is resolved the wider adoption of blockchain technology and the consequential societal and business advantages will not be fully realised. The implementation of smart verification technology will greatly increase trust, and hence is an area of great interest to the Blockchain community.

Thanks to the known vulnerabilities of Ethereum, there is a high commercial interest in systems that can specify and validate smart contracts. Because of well-known exploits in Ethereum and elsewhere with costs in the hundreds of millions of dollars, specification and validation has moved from being unthinkably expensive to highly desirable.

There is little existing work on verification of smart contracts. One of the most crucial questions is to understand what are the most important properties to verify. Proposed properties include preservation, ensuring that no currency is lost, and progress, ensuring that the contract can always take a step (this last has also been called liquidity). This industrial doctorate research will seek to answer these questions.

Plutus is the smart contract language of the Cardano blockchain. It is implemented as a library for Haskell, and compiles into Plutus Core, a dialect of System F, for on-chain execution. Ada, the cryptocurrency of Cardano, is a leading cryptocurrency, in the top ten by market capitalisation.

The most widely-used smart contract blockchain, Ethereum has a market capitalisation of US$44B. It is famous for regular exploits losing hundreds of millions of pounds worth of Ether, including the DAO and Parity bugs, creating a demand for validation of smart contracts. both the DAO and Parity bugs might have been avoided by the technique we will develop, specification and proof of full functional correctness.

Intended solution

The extended UTxO model used in Plutus is unique, in that continuity of a smart contract across several transactions is ensured by a contract on the input of a transaction checking that the same contract is attached to an output of that transaction. Methods of specifying and validating contracts that stretch over many transactions will be a focus of the research. One technique to explore is the use of state machines, which is already supported by Plutus libraries.

Another way in which Plutus is unique is its “batteries included” design, where both onchain and offchain actions are contained in a single contract. (In Ethereum, in contrast, onchain actions are in Solidity/EVM while offchain are in JavaScript.) We will consider how to validate onchain and offchain components together, which so far as we know has not been considered before.

We will make available a repository of validated smart contracts, working with Plutus engineers and IOHK business developers to produce a collection of relevant contracts. Plutus Playground includes four smart contracts and the Plutus open source repository includes fourteen smart contracts, but none of these yet include validation.

Related work includes ConCert, a smart contract validation library based on Coq (Annekov et al 2020), and Imandra, a verification environment for financial applications (Passmore and Ignatovich, 2018).The work will build on top of existing tools for specification and verification, such as Agda or Coq. It is recognised by the industry that there is little existing work on verification of smart contracts. One of the most crucial questions is to understand what are the most important properties to verify. Proposed properties include preservation, ensuring that no currency is lost, and progress, ensuring that the contract can always take a step (this last has also been called liquidity). This research will seek to answer these questions.

Expected outcome

The industrial doctorate is expected to publish papers in high-profile conferences, and to  create  an open source tool and verification software to further academic research. Alongside the academic expectations, the industrial doctorate will also produce prototypes for verifying Plutus smart contracts.

The outcome of the work would be a prototype library for specification and validation of Plutus smart contracts, most likely built on top of Coq and hs2coq (Breitner et al 2018). The industrial candidate will produce:

  • A prototype library for specification and validation of Plutus smart contracts, encompassing support for both Plutus and Coq.
  • Case studies and documentation to enable developers to build on our work. These will include a number of cases of commercial interest, developed in cooperation with the Plutus team and Cardano business experts. No standard repository of smart contracts currently exists.
  • A repository of smart contract examples across multiple systems (Plutus, Ethereum, and others) to support comparison of systems and serve as a model for commercial development.

The research will produce a prototype system suitable as the starting point for a system to be put into production. IOHK and Plutus are poised to be a leader in this market, because functional programs like Haskell provide excellent support for rapidly building reliable systems. This is why, for instance, Haskell and other functional languages have seen much take up from banks and financial institutions. Most proof assistants, such as Coq and Agda, are built on top of functional languages, and there has already been a large body of work on specifying and validating functional programs.

The IOHK Plutus team will aid in converting the prototype to a product and deploying the result so that is widely available to Plutus users.

Location

The doctoral student involved in this programme will share its time between the Co-Location Centre of the EIT Digital Edinburgh Satellite Node, The work will be carried out at IOHK premises in Edin-burgh in close collaboration with the Plutus development team and IOHK business experts. In addition to the industrial doctorate research, the PhD student will also be following leadership seminars.

Facts

  • Industrial partner: IOHK
  • Academic/research partner: University of Edinburgh
  • Number of available PhD positions: 1 
  • Duration: 4 years 
  • Innovation Focus Area: Digital Industry and Digital Finance
  • This PhD will be funded by EIT Digital and IOHK

Apply

Those interested in applying should should complete the EIT Digital application form, including a CV, a motivation letter, and documents showing their academic track records. 

IOHK is poised to be a leader in reliable smart contracts and their verification. This project will play a critical role in positioning IOHK as a global leader in reliable smart contracts and their verification, and strengthening the use of Cardano.

Verification will be carried out directly by some developers, but also there may emerge an ecosystem of validation services. IOHK is already partnered with Emergo to support an ecosystem around Cardano, which may include verification services.

© 2010-2021 EIT Digital IVZW. All rights reserved. Legal notice