Jump to Content

Swapsies on the Internet: First Steps towards Reasoning about Risk and Trust in an Open World

Sophia Drossopoulou
James Noble
Mark S. Miller
Tenth Workshop on Programming Languages and Analysis for Security (PLAS 2015), ACM


Contemporary open systems use components developed by many different parties, linked together dynamically in unforeseen constellations. Code needs to live up to strict security specifications: it has to ensure the correct functioning of its objects when they collaborate with external objects which may be malicious. In this paper we propose specifications that model risk and trust in such open systems. We specify Miller, Van Cutsem, and Tulloh’s escrow exchange example, and discuss the meaning of such a specification. We argue informally that the code satisfies its specification.