Blogs (61) >>
Mon 16 Jul 2018 14:00 - 15:00 at Hanoi - Session 2

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.

Mon 16 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30
Session 2FTfJP at Hanoi
Towards specifications of robustness -- the things that programs do *not* doKeynote
Sophia Drossopoulou Imperial College London
Specification Idioms from Industrial Experience
David Cok CEA, LIST, Software Safety and Security Laboratory