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

Original language | English |
---|---|

Pages (from-to) | 320-360 |

Number of pages | 41 |

Journal | Mathematical Structures in Computer Science |

Volume | 25 |

Issue number | 2 |

Early online date | 10 Nov 2014 |

DOIs | |

Publication status | Published - 19 Feb 2015 |