Sophia Drossopoulou, James Noble, Toby Murray, Mark S. Miller
Contemporary open systems use components developed by different parties, linked
together dynamically in unforeseen constellations. Code needs to live up to strict
security requirements, and ensure the correct functioning of its objects even when
they collaborate with external, potentially malicious, objects. In this paper we
propose special specification predicates that model risk and trust in open systems.
We specify Miller, Van Cutsem, and Tulloh’s escrow exchange example, and discuss
the meaning of such a specification. We propose a novel Hoare logic, based on
four-tuples, including an invariant describing properties preserved by the
execution of a statement as well as a post-condition describing the state after
execution. We model specification and programing languages based on the Hoare
logic, prove soundness, and prove the key steps of the Escrow protocol.