The Secret Art of Computer Programming

“Classical” program development by refinement [12, 2, 3] is a technique for ensuring that source-level program code remains faithful to the semantic goals set out in its corresponding specification. Until recently the method has not extended to security-style properties, principally because classical refinement semantics is inadequate in security contexts [7]. ow semantics introduced by Morgan [13] is an abstraction of probabilistic program semantics [11], and is rich enough to distinguish between refinements that do preserve noninterference security properties and those that don’t. In this paper we give a formal development of Private Information Retrieval [4]; in doing so we extend the general theory of secure refinement by introducing a new kind of security annotation for programs.

• Type: Conference
• Year: 2009
• Where: ICTAC
• Authors: Annabelle McIver
• Keywords: Applied Computing, Classical Refinement Semantics, ICTAC 2009, Probabilistic Program Semantics, Semantics