Paper
to appear in the 6th intern. IFIP conference on Theoreticaql Computer Science
(IFIP-TCS 2010), Brisbane (Australia), September 20th-23rd, 2010.
Long version.
We propose a framework for reasoning about program security building on language-theoretic and coalgebraic concepts. The behaviour of a system is viewed as a mapping from traces of high (unobservable) events to low (observable) events: the less the degree of dependency of low events on high traces, the more secure the system. We take the abstract view that low events are drawn from a generic semiring, where they can be combined using product and sum operations; throughout the paper, we provide instances of this framework, obtained by concrete instantiations of the underlying semiring. We specify systems via a simple process calculus, whose semantics is given as the unique homomorphism from the calculus into the set of behaviours, i.e. formal power series, seen as a final coalgebra. We provide a compositional semantics for the calculus in terms of rational operators on formal power series and show that the final and the compositional semantics coincide.
@InProceedings{BCG:IFIPTCS10,
author = {M. Boreale, D. Clark and D. Gorla},
title = {A Semiring-based Trace Semantics for Processes with Applications to Information Leakage Analysis},
editor = {C. Calude and V. Sassone},
booktitle = {Proc. of 6th International IFIP Conference on Theoretical Computer Science (IFIP-TCS 2010)},
series = {},
volume = {},
pages = {},
year = {2010},
publisher = {Springer},
}