Compact Course:  Prof. Dr. Annabelle McIver, Macquarie University, Sydney,
Australia

"Refinement, Probability and Security"

 Seminar Room I11 (ground floor,  Room 2002, "Altbau")

• 9.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

(click titles for the slides)

 

 

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 [Morgan09, 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.