The secret art of computer programming

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

3 Citations (Scopus)


"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.

Original languageEnglish
Title of host publicationTheoretical aspects of computing - ICTAC 2009
Subtitle of host publication6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009, proceedings
EditorsMartin Leucker, Carroll Morgan
Place of PublicationBerlin
PublisherSpringer, Springer Nature
Number of pages18
ISBN (Print)3642034659, 9783642034657
Publication statusPublished - 2009
Event6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009 - Kuala Lumpur, Malaysia
Duration: 16 Aug 200920 Aug 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5684 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349


Other6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009
CityKuala Lumpur

Fingerprint Dive into the research topics of 'The secret art of computer programming'. Together they form a unique fingerprint.

Cite this