text: We present a taxonomy and an algebra for attack patterns on component-based operating systems. In a multilevel security scenario, where isolation of partitions containing data at different security classifications is the primary security goal and security breaches are mainly defined as undesired disclosure or modification of classified data, strict control of information flows is the ultimate goal. In order to prevent undesired information flows, we provide a classification of information flow types in a component-based operating system and, by this, possible patterns to attack the system. The systematic consideration of informations flows reveals a specific type of operating system covert channel, the covert physical channel, which connects two former isolated partitions by emitting physical signals into the computer's environment and receiving them at another interface.
  @cite_26: Trust and assurance of mobile platforms is a prime objective when considering their use in security-critical scenarios like in healthcare or e-government. Currently, several complementary approaches can be found in literature, ranging from purely hardware based to operating system level and application level solutions. Together, they build a "trusted and secured" technology stack. However, the complex policy configuration mechanisms at every single layer also represent the biggest stumbling block for a rapid adoption. We propose a practicable and efficient solution for leveraging operating system level and application level security mechanisms to realize security-critical applications and services.
  @cite_4: 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.
  @cite_41: With the rise of formally verified micro kernels, we finally have a trusted platform for secure IPC and rigorous enforcement of our mandatory access control policy. But, not every problem in computer security and privacy could possibly be solved by a trusted micro kernel, because we have higher level security and privacy concepts like packet filtering, data encryption and partitioning of shared hardware devices, which we also need to trust. Numerous authors have described the need for a trusted middleware, fulfilling these higher level security and privacy goals, but detailed requirements for the different security and privacy goals are still missing. We provide a collection of output filters that can be applied to trusted operating system components to enforce higher level security goals. We further provide a typology of operating system guards, which are essentially trusted components utilizing different compilations of input and output filters. The storage guard, the audio filtering guard and the sequencing guard are specifically targeted at providing solutions to three common security and privacy problems in component-based operating systems. Finally, we develop a guard reference architecture and present the concept of a guard construction kit for the development of new types of operating system guards, enabling operating system developers to build their own guard components for both component-based and commodity operating systems.
  @cite_9: In this work, we show how the abstraction layer created by a hypervisor, or virtual machine monitor, can be leveraged to reduce the complexity of mandatory access control policies throughout the system. Policies governing access control decisions in today's systems are complex and monolithic. Achieving strong security guarantees often means restricting usability across the entire system, which is a primary reason why mandatory access controls are rarely deployed. Our architecture uses a hypervisor and multiple virtual machines to decompose policies into multiple layers. This simplifies the policies and their enforcement, while minimizing the overall impact of security on the system. We show that the overhead of decomposing system policies into distinct policies for each layer can be negligible. Our initial implementation confirms that such layering leads to simpler security policies and enforcement mechanisms as well as a more robust layered trusted computing base. We hope that this work serves to start a dialog regarding the use of mandatory access controls within a hypervisor for both increasing security and improving manageability.
  @cite_6: In this paper, we present the design of a high assurance file server model developed to operate within the Multiple Independent Levels of Security framework. The file server model is a multilevel application that utilizes separation to mediate information flow by adhering to a security policy formulated from a modified version of the Bell and LaPadula Model and the GWVr2 policy, which is a separation kernel based policy developed for high assurance architectures. This paper focuses on the design aspects of the file server model and the underlying architecture. The purpose of this file server design is to develop a formal model to meet the formal methods requirement of Common Criteria, which is a system design and specification guideline for high assurance systems. The model is also an example application for the Multiple Independent Levels of Security architecture.
  @cite_40: A transfer guard built on a high-assurance multilevel secure (MLS) trusted computing base (TCB) must be a trusted subject with the capability to perform downgrades not otherwise permitted by the MLS security policy. Formal evaluations of MLS systems containing trusted subjects are complicated when the trusted subjects are evaluated as part of a monolithic TCB. While welldeveloped techniques of “TCB subsets” and “TCB partitions” for composing MLS systems exist, approaches for applying these techniques for reasoning about a guard downgrade policy are not as well-developed. If the trusted downgrade process must be evaluated as part of the TCB, an inability to adequately reason about the downgrade policy would make it difficult to reason about the policy implemented by the system as a whole. And if trusted subjects cannot be evaluated separately and composed with the underlying TCB, that could lead to to expensive and repetitive certification and recertification of the system when downgrade policies change. A necessary pre-requisite for feasible evaluation of high-assurance transfer guard systems is to be able to separately evaluate the assurance of the underlying system and the implementation of the downgrade policy. This paper suggests an approach to extending the well-developed technique of “balanced assurance” to the formal evaluation of high-assurance transfer guards that could permit the downgrade function to be evaluated separately from the underlying TCB and then composed with it into an overall system.
  @cite_31: SELinux can enforce a policy based on mandatory access control (MAC) for Linux so as to fulfill the security requirements of more strict access control for those hierarchical and classified management organizations or situations. But security policy configuration is a hard and intractable task for SELinux due to its recondite policy description language and huge number of complicated security policies. Thereafter, it is rather significant to build a powerful assistant tool to help security managers to perform security policy configurations. And the key problem is to analyze configured security policies automatically or semi-automatically so that as many configuration loopholes as possible can be detected and then be eliminated. In this paper, both security models and policy description language supported by SELinux are summarized at first. While methods for analyzing security policies are discussed in details secondly. Then a prototype for a tool to analyze security policies automatically is designed, implemented and tested as well as some preliminary test results are given. Finally, the research work in this paper is summed up and some further research directions are pointed out.
  @cite_16: onfining a program during its execution so that it cannot transmit information to any other program except its caller. A set of examples attempts to stake out the boundaries of the problem. Necessary conditions for a solution are stated and informally justified.
summary: Storage channels are also defined by Lampson @cite_16 , who notes that data is written by the service and read by an unconfined program, either shortly after it is written or at some later time'', describing a storage channel between a confined and an unconfined program. Corrupt policy channels that are present due to a misconfigured access control policy have been addressed by Agreiter @cite_26 , proposing automatic generation of an operating system's MAC policy, and @cite_31 , presenting a new method for automatic analysis of an operating system's MAC policy. Finally, exploiting illegitimate access to components would be a special case of a flawed system policy, where a policy circumvents an operating system guard @math that protects access to a component @math , managing a shared resource, and allows @math and @math to exchange messages via @math . The use of operating system guards to handle shared resources to protect applications from untrusted components has been described by @cite_9 , @cite_6 @cite_4 , @cite_40 , and Hanspach and Keller @cite_41 .