compact course |
Prof. Dr. Annabelle McIver, Macquarie University, |
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 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, [McIver 05] Abstraction, Refinement and Proof for Probabilistic Systems, [Morgan 09] The Shadow Knows: Refinement of Ignorance in sequential [McIver 09] Sums and Lovers: Case studies in security and refinement, |
Event calendar
- Subscribe to the ics feed.
Upcoming Events
- No Events