Hidden-Markov Program Algebra with iteration

TL;DR

This paper develops a quantitative program algebra using Hidden Markov Models to analyze and compare information leakage in programs with iteration, supporting formal reasoning and automation.

Contribution

It extends previous qualitative work to a quantitative setting with iteration, introducing algebraic laws for noninterference analysis and refinement.

Findings

Algebraic laws support reasoning about information leakage.

Demonstration on a password-guessing attack example.

Framework enables source-level verification of security properties.

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. <p>This joins two themes: we extend our earlier work, having iteration but only qualitative, by making it quantitative; and we extend our earlier quantitative work by including iteration. <p>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.