Hidden-Markov program algebra with iteration

McIver, Annabelle, Meinicke, Larissa and Morgan, Carroll (2015) Hidden-Markov program algebra with iteration. Mathematical Structures in Computer Science, 25 S02: 320-360. doi:10.1017/S0960129513000625

Author McIver, Annabelle
Meinicke, Larissa
Morgan, Carroll
Title Hidden-Markov program algebra with iteration
Journal name Mathematical Structures in Computer Science   Check publisher's open access policy
ISSN 0960-1295
Publication date 2015-02
Year available 2014
Sub-type Article (original research)
DOI 10.1017/S0960129513000625
Open Access Status
Volume 25
Issue S02
Start page 320
End page 360
Total pages 41
Place of publication Cambridge, United Kingdom
Publisher Cambridge University Press
Collection year 2015
Language eng
Formatted abstract
We use hidden Markov models to motivate a quantitative compositional semantics for noninterference-based security with iteration, including a refinement- or ‘implements’ relation that compares two programs with respect to their information leakage; and we propose a program algebra for source-level reasoning about such programs, in particular as a means of establishing that an ‘implementation’ program leaks no more than its ‘specification’ program.

This joins two themes: we extend our earlier work, having iteration but only qualitative (Morgan 2009), by making it quantitative; and we extend our earlier quantitative work (McIver et al. 2010) by including iteration.

We advocate stepwise refinement and source-level program algebra – both as conceptual reasoning tools and as targets for automated assistance. A selection of algebraic laws is given to support this view in the case of quantitative noninterference; and it is demonstrated on a simple iterated password-guessing attack.
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ
Additional Notes Published online ahead of print 10 Nov 2014

Document type: Journal Article
Sub-type: Article (original research)
Collections: Official 2015 Collection
School of Information Technology and Electrical Engineering Publications
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 3 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Tue, 09 Dec 2014, 05:17:43 EST by System User on behalf of School of Information Technol and Elec Engineering