Reasoning about Risk and Trust in an Open World

Abstract

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.