Sciweavers

IFIPTCS
2010

A Semiring-Based Trace Semantics for Processes with Applications to Information Leakage Analysis

13 years 8 months ago
A Semiring-Based Trace Semantics for Processes with Applications to Information Leakage Analysis
Abstract. 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, 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.
Michele Boreale, David Clark, Daniele Gorla
Added 13 Feb 2011
Updated 13 Feb 2011
Type Journal
Year 2010
Where IFIPTCS
Authors Michele Boreale, David Clark, Daniele Gorla
Comments (0)