Work with James Noble (VUW), Mark Miller (Agoric), and Toby Murray (Univ. Melbourne)

Functional correctness provides guarantees about programs when they are used correctly, while robustness is about the guarantees when programs are used arbitrarily, incorrectly or even maliciously. Robust programs ensure that certain things will not happen, e.g. money will not disappear from a DAO-contract unless an account holder requested payment, or a DOM-tree protected by a wrapper will not be modified beyond the part allowed by the wrapper.

To specify robustness, we propose holistic specifications: a simple logic which includes both temporal and spatial aspects. We use this logic to specify robustness aspects of certain popular program patterns from object-capabilities and smart contracts: the membrane, Mint-and-Purse, DOM-wrappers, the DAO, and ERC-20. Using these specifications we can then reason about preservation of non-trivial properties of our data when passed to unknown, adversarial code.

I am a Professor of Programming Languages in the Department of Computing, Imperial College, London, UK.