Refinement, Probability and Security

compact course

Prof. Dr. Annabelle McIver, Macquarie University,
Sydney, Australia

Refinement, Probability and Security
When 9th – 12th November
Where Seminar Room I11 (ground floor, R 2002)
09.11., 13:30 Lecture 1: Probability, nondeterminism and refinement
10.11., 13:30: Lecture 2: Shadow semantics for security-aware refinement
11.11., 16:00: Lecture 3: Probabilistic Shadow Semantics for quantitative security refinement
The course is open to students of the Research Training Groups “AlgoSyn” and “Software for Mobile Communication Systems” and of the B-IT Research School.Other participants are welcome but should write a message to Prof. J.P. Katoen (katoen(at)cs.rwth-aachen.de).
Abstract Stepwise refinement [Wirth 71] is the top-down presentation of a software system’s functionality as a sequence of layers of increasing detail, beginning with the very abstract and ending with the very concrete, and with each layer an incremental “refinement” of the previous one. Making the separation between layers small means that each refinement step can be kept under conceptual control, in many cases even verified correct. Even though actually developing systems this way remains a theoretical ideal (sometime achieved), the refinement framework is in practice provides a framework for encouraging correct, accountable and even efficient code.

Lecture 1: Probability, nondeterminism and refinement

In this lecture we’ll introduce the basic semantic structures for sequential programs containing both probability and demonic nondeterminism
[McIver 05]. The role of determinism nondetermism is that, interpreted during development time, it corresponds to the abstraction of detail that forms the basis for stepwise refinement. Without it, proper refinement of probabilistic systems is not possible, in theory or in practice.

We’ll look at the underlying domains for operational (relational-style) semantics and a correponding quantitative program logic together with some applications to verification.

Lecture 2: Shadow semantics for security-aware refinement

This lecture describes recent advances in the stepwise-refinement method that incorporate the identification and preservation of security properties [Morgan 09, McIver09]. The model and logic presented is inspired by, but abstracted from, the probabilistic refinement discussed in Lecture 1 . The objectives of this lecture are to describe the underlying mathematics and resulting restrictions to standard refinement required in order to ensure that security properties are preserved. The methods will be illustrated by secure refinement laws and the verification of a non-trivial case study.

Lecture 3: Probabilistic Shadow Semantics for quantitative security refinement

This lecture takes the model from Lecture 2, which had no probability, and reintroduces probability in order to reason about programs that are proof against more powerful attackers. We’ll spend some time looking at the underlying probabilistic domain for security and its associated refinement relation. Finally we’ll show how, in spite of the abstractions made in the Shadow Semantics, we can promote verification in that simpler context to the more discriminating probabilistic context.

[Wirth 71] Program Development by Stepwise Refinement, Niklaus Wirth,
Communications of the ACM, Vol 14, No. 4, April 1971.

[McIver 05] Abstraction, Refinement and Proof for Probabilistic Systems,
A McIver and C Morgan, Monographs in Computer Science, Springer, 2005.

[Morgan 09] The Shadow Knows: Refinement of Ignorance in sequential
programs, C Morgan, Science of Computer Programming vol. 74(8)
(629–653) 2009.

[McIver 09] Sums and Lovers: Case studies in security and refinement,
FM09 (to appear).