A semiring-based trace semantics for processes with applications to information leakage analysis
A semiring-based trace semantics for processes with applications to information leakage analysis
复制标题
DOI：
10.1017/s0960129513000601
复制
发表时间：
2010-09
影响因子：
0.5
通讯作者：
Michele Boreale;D. Clark;D. Gorla
中科院分区：
文献类型：
--
作者：
Michele Boreale;D. Clark;D. Gorla
我们提出了一个框架，以推理有关语言理论和煤炭概念的计划安全构建的框架。系统的行为被视为从高（可观察）事件的痕迹到低（可观察）事件的映射：低轨迹对高轨迹的依赖程度越小，系统越安全。我们采用抽象的观点，即从通用的半程中得出低个性事件，可以在其中使用产品和总操作组合它们。在整个论文中，我们提供了该框架的实例，该实例是通过基础半导体的具体实例来获得的。我们通过一个简单的过程表明系统，其语义是从微积分到一组行为的独特同质性的，即形式的功率序列，被视为最终的煤层。我们就形式功率系列的理性操作员为微积分提供了一种构图语义，并表明最终语义和组成语义是一致的。这个组成，语法驱动的框架为自动化和抽象的基础奠定了量化的系统规范流安全性。
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. This compositional, syntax-driven framework lays a foundation for automation and abstraction of a quantified approach to flow security of system specifications.