While privacy-preserving mechanisms aim to protect sensitive information at the attribute level, distributed complex event processing (DCEP) systems remain vulnerable to privacy breaches through the detection of event patterns. Even if individual events are not inherently private, their combination into patterns can reveal sensitive knowledge. This article investigates the integration of pattern-level privacy within the APP-CEP context. We address the challenge of selectively applying obfuscation techniques to event-based systems to safeguard sensitive information. Unlike existing methods, we aim to establish event-stream-agnostic privacy by formulating queries and privacy constraints using CEP-like patterns, and constructing pattern dependency graphs to dynamically select obfuscation techniques that have no consequences on detecting other sensitive patterns, as well as non-sensitive patterns required to provide an acceptable quality of service. Additionally, we model potential adversary’s knowledge that could compromise privacy and analyze its influence on the obfuscation process. We evaluated APP-CEP’s performance using two real-world datasets: online retail transactions and medical records, replayed as temporally ordered event streams. Our results indicate that APP-CEP effectively balances privacy and utility. By modeling background knowledge, we also successfully prevented adversaries from detecting modifications to the input streams.

Although being well-adopted and in widespread use, attribute-based access control (ABAC) remains a hard-to-master security paradigm in application software development. Despite considerable research towards ABAC policy engineering and ABAC policy correctness, this mainly is because there is still no unified workflow to encompass both the versatility of application domains and the strong guarantees promised by formal modeling methods. This work contributes to improving this situation. By presenting a flexible, yet highly formalized modeling scheme for designing and analyzing ABAC policies (DABAC), a reference implementation in Rust (dabac-rs), and a reference architecture for its integration into applications (AppSPEAR) including developer support (appspear-rs), we put together loose pieces of a tool-supported model-based security engineering workflow. The effectiveness of our approach is demonstrated based on a real-world engineering scenario.

Attribute-based access control (ABAC) has made its way into the mainstream of engineering secure IT systems. At the same time, ABAC models are still lagging behind well-understood, yet more basic access control models in terms of dynamic analyzability. This has led to a plethora of methods, languages, and tools for designing and integrating ABAC policies, but only few to formally reason about them in the process. We present DABAC, a modeling scheme to pick up that missing piece and put it right into its place in the security engineering workflow. Based on an automaton calculus, we demonstrate how DABAC can be leveraged as a holistic formal basis for engineering ABAC models, analyzing their dynamic properties, and providing a functional specification for their implementation. This sets the stage for comprehensive tool support in building future ABAC systems.

Despite defining a de-facto standard in model-based security engineering, role-based access control models still suffer from limited analysis capabilities. This is especially true for dynamic security properties in the lineage of HRU safety. As a consequence, despite of their widespread use for policy specification and implementation, it is difficult to provide and preserve correctness guarantees for such models. We propose a formal framework, called DRBAC, to resolve this dilemma: While retaining application-oriented model abstractions, our approach allows to configure their dynamics in terms of state transitions. This enables a security engineer to tailor both a model and its analysis method to certain safety-related analysis goals. We demonstrate this claim based on a practical security policy.

Software engineering for security-critical systems is based on manual translations between languages from different domains: an informal security policy is translated to a formally verifiable model, and further to actual source code. This is an error-prone task, put at the risk of losing hard-acquired correctness guarantees. To mitigate this problem, we argue for a methodical support by domain-specific languages and tools. We present ongoing work on two languages that substantiate this thesis, including their usage in a practical setting, and discuss the benefits from combining them with appropriate tool support.

Cyber security management requires fast and cost efficient responses to threat alerts. Automation of cyber threat sensing and responding is one way to achieve immediate reactions to imminent threats. There are already tools for an extensive automation of threat sensing, e.g. threat intelligence sharing platforms. Methods, techniques and tools for reacting to menacing states and events, e.g. security-policy-controlled systems, have also been explored and published for some time. What is still missing, however, is the integration of these two approaches. This paper describes first steps towards an integration of threat intelligence sharing platforms and security-policy-controlled systems. We present a conceptual design for threat reaction strategies, security architectures and mechanisms and information representation requirements. We use two exemplary threat scenarios to demonstrate our proposals.

Termination is an important non-functional property of distributed algorithms. In an event-driven setting, the interesting aspect of termination is the possibility of control flow loops through communication, which this paper aims to investigate. In practice, it is often difficult to spot the possible communication behaviour of an algorithm at a glance. With a static analysis, the design process can be supported by visualizing possible flow of messages and give hints on possible sources of non-termination. We propose a termination analysis for distributed algorithms formulated in an event-driven specification language. The idea is to construct a message flow graph describing the possible communication between components (input-action pairs). We show that acyclicity of that graph implies termination. While many interesting algorithms indeed contain cycles, we also suggest ways of detecting cycles which cannot lead to non-termination. As a practical evaluation, we describe a concrete programming language together with a tool for automated termination analysis.

Being of paramount importance for the correctness of a security policy, the property of safety has received decades of attention in the field of model-based security engineering. To analyze the safety of a security model, heuristic approaches are used to avoid restrictions of the model calculus while accepting semi-decidability of this property. Within this field, this paper addresses three open problems concerning the DEPSEARCH heuristic safety analysis framework: Inefficient state-space exploration, static verification of unsafety-unsatisfiability, and parameter dependency analysis. We describe these problems on a formal basis, specify solution proposals, and implement these in the current, model-independent f DS framework. A practical evaluation based on SELinux is performed to study effectiveness and future optimization of the framework.

Security-critical system requirements are increasingly enforced through mandatory access control systems. These systems are controlled by security policies, highly sensitive system components, which emphasizes the paramount importance of formally verified security properties regarding policy correctness. For the class of safety-properties, addressing potential dynamic right proliferation, a number of known and tested formal analysis methods and tools already exist. Unfortunately, these methods need to be redesigned from scratch for each particular policy from a broad range of different application domains. In this paper, we seek to mitigate this problem by proposing a uniform formal framework, tailorable to a safety analysis algorithm for a specific application domain. We present a practical workflow, guided by model-based knowledge, that is capable of producing a meaningful formal safety definition along with an algorithm to heuristically analyze that safety. Our method is demonstrated based on security policies for the SELinux operating system. Keywords: Security engineering, security policies, access control systems, access control models, safety, heuristic analysis, SELinux.

To meet tightening security requirements, modern operating systems enforce mandatory access control based on formal security policies. To ensure the critical property of policy correctness, formal methods and models for both their specification and verification are used. The variety of these approaches reflects the diversity and heterogeneity of policy semantics, which makes policy engineering an intricate and error-prone process. Therefore, a common formal framework is needed that unifies both diverse access control systems on the one hand and diverse formal criteria of correctness on the other hand.This paper presents a step towards this goal. We propose to leverage core-based model engineering, a uniform approach to policy formalization, and refine it by adding typical semantic abstractions of contemporary policy-controlled operating systems. This results in a simple, yet highly flexible framework for formalization, specification and analysis of operating system security policies. We substantiate this claim by applying our method to the SELinux system and demonstrating the practical usage of the resulting model.

Modern operating systems increasingly rely on enforcing mandatory access control through the use of security policies. Given the critical property of policy correctness in such systems, formal methods and models are applied for both specification and verification of these policies. Due to the heterogeneity of their respective semantics, this is an intricate and error-prone engineering process. However, diverse access control systems on the one hand and diverse formal criteria of correctness on the other hand have so far impeded a unifying framework for this task. This paper presents a step towards this goal. We propose to leverage core-based model engineering, a uniform approach to security policy formalization, and refine it by adding typical semantic abstractions of contemporary policy-controlled operating systems. This results in a simple, yet highly flexible framework for formalization, specification and analysis of operating system security policies. We substantiate this claim by applying our method to the SELinux system and practically demonstrate how to map policy semantics to an instance of the model.

Contemporary mobile devices have become universal and versatile tools that increasingly are used in sensitive application scenarios. They inevitably carry confidential information such as passwords, encryption keys, mission-critical company data, or location information in combat areas. In order to meet sophisticated security requirements, recent technology focuses on policy-oriented approaches that allow for the definition and enforcement of rigorous and precise rules for protecting confidential information. State-of-the-art development of security policies is a critical process, because of the involved quality assurance measures, it is quite heavy-weighted and tends to antagonize the distinguished virtues of mobile devices for lightweight, spontaneous communication and cooperation. This paper presents an approach to support secure, mobile device based cooperation in temporary, sporadically and spontaneously fashioned cliques within open communication infrastructures. The approach is based upon light-weight security domains protected by security policies that are dynamically and automatically composed during group formation. Due to the volatile nature of such groups simplicity, adaptability, efficiency and compatibility with today's security policy implementation techniques have been a major design goal.

IT systems with sophisticated security requirements increasingly apply problem-specific security policies for specifying, analyzing, and implementing security properties. Due to their key role for defining and enforcing strategic security concepts, security polices are extremely critical, and quality assets such as policy correctness or policy consistency are essential objectives in policy engineering. This paper argues for a tool-supported policy engineering approach to increase the efficiency and quality of security policy making. The paper's general topic is WorSE, a policy engineering workbench encompassing the automation of engineering steps, prebuilt model patterns, integrated plausibility checks, and model analysis tools; the paper especially focuses on tools supporting model engineering and model analysis, and describes their theoretical foundations and practical application. (C) 2014 Elsevier Ltd. All rights reserved.

Model-based security engineering uses formal security models for specifying and analyzing access control systems. Tool-based model analysis encounters a fundamental difficulty here: on the one hand, real-world access control systems generally are quite large and complex and require models that have high expressive power. On the other hand, analysis of such models is often pestered by computational complexity or even non-decidability, making it difficult to devise algorithms for automated analysis tools. One approach to this problem is to limiting the expressive power of the modeling calculus, resulting in restrictions to the spectrum of application scenarios that can be modeled. In this paper we propose a different approach: a heuristic-based method for analyzing the safety properties of access control models with full expressive power. Aiming at generality, the paper focuses on the lineage of HRU-style, automaton-based access control models that are fundamental for modeling the dynamic behavior of contemporary role-based or attribute-based access control systems. The paper motivates a heuristics-based approach to model analysis, describes in detail a heuristic model safety analysis algorithm, and discusses its computational complexity. The algorithm is the core of a security model analysis tool within the context of a security policy engineering workbench; a formal description of major components of its heuristic-based symbolic model execution engine is given, and its capacity to analyze complex real-world access control systems is evaluated.

Since security has become an essential asset in numerous application areas, the integration of security policies has become a major issue in the design of security architectures, and many commodity operating systems have been furnished with abstractions to support policy protection and enforcement. Given a security policy's key position in defining and implementing a system's security properties, quality attributes such as policy correctness, completeness, or consistency are essential objectives in policy engineering. On the other hand, considering the large amount of their responsibilities, security policies often are large and complex, rendering the analysis and proof of crucial quality attributes difficult. This paper is a step towards tool-supported security policy analysis. It presents a model-based approach to analyze the dynamic proliferation of access rights in a policy-controlled SELinux access control system.

Zugriffsschutzsysteme spielen beim Schutz von Informationen in IT-Systemen eine kritische Rolle; sie verhindern auch dann noch den Zugriff auf Informationen, wenn virtuelle private Netzwerke, Firewalls oder Intrusion-Detection-Systeme nicht mehr greifen können. Entgegen ersten Anscheins ist die korrekte Konfiguration von Zu griffsschutzsystemen sehr subtil: wäh- rend direkte Zugriffe von Benutzern auf Dokumente sehr einfach zu steuern sind, ist es dagegen sehr schwierig auszuschließen, dass durch Umwege über Zwischenobjekte verdeckte Informationsflussmög- lichkeiten bestehen; und dies sind dann exakt diejenigen Wege, über die Insider Zugriff auf Informatio- nen erhalten, zu denen sie gemäß der intendierten Sicherheitspolitik keinen Zugang haben dürfen. Dieses Papier stellt eine Methode zum Auffinden von Informati onsflusspotenzialen vor, die auf der Transformation einer Zugriffsmatrix in einen Informationsflussgraphen und seiner Reduktion auf Informationsfluss-Äquivalenzklassen beruht. Hierauf aufb auend wurde in ein Werkzeug entwickelt, wel- ches die Analyse von Zugriffssteuerungssystemen hinsichtlich verdeckter Informationsflusspotenziale weitgehend automatisiert. Die Ergebnisse der Anwendung von Methode und Werkzeug auf einen mit- telgroßen Fileserver mit einer diskreten, Unix-artigen Zugr iffssteuerungssemantik weisen einige Über- raschungen auf. Schlüsselworte: Zugriffssteuerung, Zugriffsmatrix, Informationsfluss, Informationsflussgraph, obligato- rische und diskrete Zugriffssteuerung