Identifying the root cause and impact of a system intrusion remains a foundational challenge in computer security. Digital provenance provides a detailed history of the flow of information within a computing system, connecting suspicious events to their root causes. Although existing provenance-based auditing techniques provide value in forensic analysis, they assume that such analysis takes place only retrospectively. Such post-hoc analysis is insufficient for realtime security applications, moreover, even for forensic tasks, prior provenance collection systems exhibited poor performance and scalability, jeopardizing the timeliness of query responses. We present CamQuery, which provides inline, realtime provenance analysis, making it suitable for implementing security applications. CamQuery is a Linux Security Module that offers support for both userspace and in-kernel execution of analysis applications. We demonstrate the applicability of CamQuery to a variety of runtime security applications including data loss prevention, intrusion detection, and regulatory compliance. In evaluation, we demonstrate that CamQuery reduces the latency of realtime query mechanisms, while imposing minimal overheads on system execution. CamQuery thus enables the further deployment of provenance-based technologies to address central challenges in computer security.
Information Flow Control Systems. Previous work on information flow control enforcement at the OS level, such as HiStar @cite_87 , Flume @cite_27 , and Weir @cite_65 , uses labels to define security and integrity contexts that constrain information flows between kernel objects. Labels map to kernel objects, and a process requires decentralised management capabilities to modify its labels. Point-to-point access control decisions are made to evaluate the validity of an information flow. Through transitivity, it is possible to express constraints on a workflow ( collected user information can only be shared with third parties as an aggregate). SELinux @cite_23 provides a similar information flow control mechanism but without decentralised management. A typical way of representing and thinking about information flow in a system is through a directed graph. However, current object labelling abstractions do not take advantage of this representation, and it is difficult to reason about when defining policies. differs from these systems in that it allows the implementation of such mechanisms directly on the graph abstraction.
@cite_27 @cite_65 @cite_23 @cite_87
2116860113 2145936802 2090390229 2162283517
In this paper, we present a systematic way to determine the information flow security goals achieved by systems running a secure O S, specifically systems running Security-Enhanced Linux. A formalization of the access control mechanism of the SELinux security server, together with a labeled transition system representing an SELinux configuration, provides our framework. Information flow security goal statements expressed in linear temporal logic provide a clear description of the objectives that SELinux is intended to achieve. We use model checking to determine whether security goals hold in a given system. These formal models combined with appropriate algorithms have led to automated tools for the verification of security properties in an SELinux system. Our approach has been used in other security management contexts over the past decade, under the name rigorous automated security management. Privacy and integrity are important security concerns. These concerns are addressed by controlling information flow, i.e., restricting how information can flow through a system. Most proposed systems that restrict information flow make the implicit assumption that the hardware used by the system is fully correct'' and that the hardware's instruction set accurately describes its behavior in all circumstances. The truth is more complicated: modern hardware designs defy complete verification; many aspects of the timing and ordering of events are left totally unspecified; and implementation bugs present themselves with surprising frequency. In this work we describe Sapper, a novel hardware description language for designing security-critical hardware components. Sapper seeks to address these problems by using static analysis at compile-time to automatically insert dynamic checks in the resulting hardware that provably enforce a given information flow policy at execution time. We present Sapper's design and formal semantics along with a proof sketch of its security. In addition, we have implemented a compiler for Sapper and used it to create a non-trivial secure embedded processor with many modern microarchitectural features. We empirically evaluate the resulting hardware's area and energy overhead and compare them with alternative designs. This paper discusses the design and implementation of a middleware guard for purposes of content filtering and information flow control in the Multiple Independent Levels of Security (MILS) architecture. The MILS initiative is a joint research effort between academia, industry, and government to develop and implement a high assurance real-time architecture for embedded systems. The MILS architecture incorporates a separation kernel with formal system security policies that are evaluatable, non-bypassable, tamper-proof, and always invoked. Vendor specific high-level applications are assumed to be untrustworthy components; information flow control needs to be performed by middleware entities external to the applications. In the MILS architecture, a MILS Message Router and guards are placed between communicating entities to act as message content filters and enforce information flow control. As the MILS architecture does not restrict the protocols that can be employed for communications between applications, a distinct guard is needed for filtering messages within each protocol. Incorporating protocol specific guards in MILS embedded systems aids in the formal certification of those systems or the high-assurance safety critical formally-proven applications. The guards enable formally-proven security policies that guarantee information flow control, data isolation, predictable process control, damage limitation, and resource availability. An example is provided using a multi-level secure file server that uses a GIOP guard for fine-grained access control. The inclusion of a GIOP guard reduces the complexity and the effort necessary for system certification. Decentralized Information Flow Control (DIFC) is an approach to security that allows application writers to control how data flows between the pieces of an application and the outside world. As applied to privacy, DIFC allows untrusted software to compute with private data while trusted security code controls the release of that data. As applied to integrity, DIFC allows trusted code to protect untrusted software from unexpected malicious inputs. In either case, only bugs in the trusted code, which tends to be small and isolated, can lead to security violations. We present Flume, a new DIFC model that applies at the granularity of operating system processes and standard OS abstractions (e.g., pipes and file descriptors). Flume was designed for simplicity of mechanism, to ease DIFC's use in existing applications, and to allow safe interaction between conventional and DIFC-aware processes. Flume runs as a user-level reference monitor onLinux. A process confined by Flume cannot perform most system calls directly; instead, an interposition layer replaces system calls with IPCto the reference monitor, which enforces data flowpolicies and performs safe operations on the process's behalf. We ported a complex web application (MoinMoin Wiki) to Flume, changingonly 2 of the original code. Performance measurements show a 43 slowdown on read workloadsand a 34 slowdown on write workloads, which aremostly due to Flume's user-level implementation.