A general theory of composition for trace sets closed under selective interleaving functions
Top Cited Papers
- 17 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 1, 79-93
- https://doi.org/10.1109/risp.1994.296590
Abstract
This paper presents a general theory of system composition for "possibilistic" security properties. We see that these properties fall outside of the Alpern-Schneider safety/liveness domain and hence, are not subject to the Abadi-Lamport composition principle. We then introduce a set of trace constructors called selective interleaving functions and show that possibilistic security properties are closure properties with respect to different classes of selective interleaving functions. This provides a uniform framework for analyzing these properties and allows us to construct a partial ordering for them. We present a number of composition constructs, show the extent to which each preserves closure with respect to different classes of selective interleaving functions, and show that they are sufficient for forming the general hook-up construction. We see that although closure under a class of selective interleaving functions is generally preserved by product and cascading, it is not generally preserved by feedback, internal system, composition constructs, or refinement. We examine the reason for this.Keywords
This publication has 13 references indexed in Scilit:
- On the derivation of secure componentsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Using traces based on procedure calls to reason about composabilityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Toward a mathematical foundation for information flow securityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- On the refinement of non-interferencePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Hookup security for synchronous machinesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Proving Noninterference and Functional Correctness Using TracesJournal of Computer Security, 1992
- Security models and information flowPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- Information flow in nondeterministic systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- Security Policies and Security ModelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1982
- Design and verification of secure systemsPublished by Association for Computing Machinery (ACM) ,1981