Carroll Morgan
School of Computer Science and Engineering
University of New South Wales
Sydney, NSW, Australia
Security, Probability and Abstraction: Rigorous Methods for Source-Level Reasoning
Abstract
Since 1995 [1] there has been intensive research in source-level assertion-style reasoning for developing probabilistic systems via stepwise refinement [2] through layers of abstraction [3], which work was summarised in a comprehensive text [4] in 2005. Since then the method has been adapted to deal with non-interference-style security, initially without probability [5] but most recently with probability as well [6].
This course will build on a basic understanding of Hoare/Dijkstra reasoning to explain these recent developments and how they fit in to the modern focus of research into secure systems and quantitative reasoning. In particular it will focus on systematic source-level developments of a number of well known probabilistic and security-sensitive algorithms, as examples, as well as explaining and illustrating general principles for doing work of this kind. There are many opportunities of up-to-the-minute topics for further research.
References
- C. Morgan, A. McIver, K. Seidel. Probabilistic predicate transformers. ACM Trans. on Program. Lang. and Syst., v. 18, n. 3, pp. 325-353, 1996. [doi link]
- N. Wirth. Program development by stepwise refinement. Commun. of ACM, v. 14. n. 4, pp. 221-227, 1971. [doi link]
- J.-R. Abrial. The B Book. Cambridge University Press, 1996.
- A. McIver, C. Morgan. Abstraction, Refinement and Proof for Probabilistic Systems, Monographs in Computer Science. Springer, 2005.
- C. Morgan. The shadow knows: refinement of ignorance in sequential programs. Sci. of Comput. Program., v. 74, n. 8, pp. 629-653, 2009. [doi link]
- C. Morgan. Security, probability and nearly fair coins in the cryptographers' café. In A. Cavalcanti, D. Dams, eds., Proc. of FM 2009, v. 5850 of Lect. Notes in Comput. Sci. pp. 41-71. Springer, 2009. [doi link]
Course materials
- C. Morgan. Security, probability and abstraction: rigorous methods for source-level reasoning. Slides. Lecture 1 [mov], lecture 2 [mov], lecture 3 [mov], lecture 4 [mov].
- Chapter 1 of: A. McIver, C. Morgan. Abstraction, Refinement and Proof for Probabilistic Systems, Monographs in Computer Science. Springer, 2005.
- C. Morgan. Proof rules for probabilistic loops. In P. J. Wallis, J. Cooke, J. He, eds., Proc. of 7th BCS-FACS Refinement Wksh. (Bath, July 1996), Electronic Wkshs. in Computing. Springer, 1997. [pdf]
- C. Morgan. The shadow knows: refinement and security in sequential programs. Sci. of Comput. Program., v. 74, n. 8, pp. 629-653, 2009. [pdf]
- A. McIver, L. Meinicke, C. Morgan. Compositional closure for Bayes risk in probabilistic noninterference. Manuscript, 2010. [pdf]
Last changed
April 15, 2010 22:14 EET
by
local organizers, ewscs10(at)cs.ioc.ee
EWSCS'10 page:
http://cs.ioc.ee/ewscs/2010/