Projects Open for Recruitment

Titles and summaries of PhD projects

Project: Verifying smart contracts for Blockchain

Supervisor: Professor Philip Wadler


Open for recruitment - UK/EU/International applicants welcome

This work will develop techniques for specifying and verifying smart contracts written in Plutus, the smart contract language of the Cardano Blockchain. Ada, the cryptocurrency of Cardano, is a leading cryptocurrency, in the top ten by market capitalisation.

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. 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.

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.

Email Philip Wadler

Project: Securing IoT Implementations with Robust Malware Classifiers via Semantic Modelling

Supervisor: Professor David Aspinall



Securing the IoT is one of the big barriers to IoT reaching its full potential. To truly protect the billions of devices entering the field, security needs to be considered at the very beginning of device design—built in from the ground up and throughout the full lifecycle of the device.

Fast and accurate Intrusion Detection Systems (IDSes) are a cornerstone of cyber security defences and increasingly rely on AI and machine-learning based techniques.  But current machine-learning based malware detection methods are vulnerable to adversarial attack and fail to be robust over time; they fail to recognise new viruses, worms and other malware which look superficially different from old ones.  Damage can be caused until detection signatures are updated manually.  The proposed PhD research will confront this lack of robustness by developing novel classification methods using semantic features which capture program meanings. These semantic-based features can improve the robustness of malware Classifiers in both changing data and adversarial examples. This will future proof IoT implementation security.

Email David Aspinall