The framework of selective interleaving functions and the modular assembly kit

The Framework of Selective Interleaving Functions and the Modular Assembly Kit for Security Properties both provide a basis for the uniform representation and formal analysis of noninterference-like properties. In this article, we clarify the relationship between these two frameworks. Our main result is that each property that can be represented in the Framework of Selective Interleaving Functions can also be represented in the assembly kit. In fact, the latter framework is strictly more expressive, which we demonstrate by several example properties. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification–Formal Methods; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs–Specification techniques General Terms Security, verification Keywords Formal specification and analysis of security properties, information flow security, noninterference

• Type: Conference
• Year: 2005
• Where: CCS
• Authors: Heiko Mantel
• Keywords: Assembly Kit, CCS 2005, Security Privacy, Security Properties, Selective Interleaving Functions