### 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/