Compatibility of Safety Properties and Possibilistic Information Flow Security in MAKS

Thomas Bauereiß, Dieter Hutter

In: F. Cuppens , N. Cuppens-Boulahia (editor). IFIP SEC 2014 International Information Security and Privacy Conference. IFIP International Information Security and Privacy Conference (SEC-2014) June 2-4 Marrakech Morocco Pages 250-256 IFIP Advances in Information and Communication Technology Springer 2014.


Motivated by typical security requirements of workflow management systems, we consider the integrated verification of both safety properties (e.g. separation of duty) and information flow security predicates of the MAKS framework (e.g. modeling confidentiality requirements). Due to the refinement paradox, enforcement of safety properties might violate possibilistic information flow properties of a system. We present an approach where suffcient conditions for the compatibility of safety properties and information flow security are derived by performing an information flow analysis of a monitor enforcing the safety property and applying well-known compositionality results for MAKS security predicates. These conditions then guarantee that the composition of a target system with the monitor satisfies both kinds of properties. We illustrate our approach by deriving sufficient conditions for the security-preserving enforcement of separation of duty and ordered message delivery of in an asynchronous communication platform.


SEC2014_TR.pdf (pdf, 492 KB )

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz