"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. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
McIver, A. K. (2009). The secret art of computer programming. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5684 LNCS, pp. 61–78). https://doi.org/10.1007/978-3-642-03466-4_3
Mendeley helps you to discover research relevant for your work.