@inproceedings{49802a3178354ad0bb4324bd9790bcd4,
title = "The secret art of computer programming",
abstract = "{"}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]. The Shadow 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.",
author = "McIver, \{Annabelle K.\}",
year = "2009",
doi = "10.1007/978-3-642-03466-4\_3",
language = "English",
isbn = "3642034659",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer, Springer Nature",
pages = "61--78",
editor = "Martin Leucker and Carroll Morgan",
booktitle = "Theoretical aspects of computing - ICTAC 2009",
address = "United States",
note = "6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009 ; Conference date: 16-08-2009 Through 20-08-2009",
}