Application security traditionally strongly relies upon security of the underlying operating system. However, operating systems often fall victim to software attacks, compromising security of applications as well. To overcome this dependency, Intel SGX allows to protect application code against a subverted or malicious OS by running it in a hardware-protected enclave. However, SGX lacks support for generic trusted I O paths to protect user input and output between enclaves and I O devices. This work presents SGXIO, a generic trusted path architecture for SGX, allowing user applications to run securely on top of an untrusted OS, while at the same time supporting trusted paths to generic I O devices. To achieve this, SGXIO combines the benefits of SGX's easy programming model with traditional hypervisor-based trusted path architectures. Moreover, SGXIO can tweak insecure debug enclaves to behave like secure production enclaves. SGXIO surpasses traditional use cases in cloud computing and digital rights management and makes SGX technology usable for protecting user-centric, local applications against kernel-level keyloggers and likewise. It is compatible to unmodified operating systems and works on a modern commodity notebook out of the box. Hence, SGXIO is particularly promising for the broad x86 community to which SGX is readily available.
Traditionally, security kernels are used to achieve strong process and resource isolation. One soon realized that security kernels itself are the Achilles' heel of the whole system security and need complexity reduction. This paved the way for microkernels, for which seL4 is a prominent example. The developers of seL4 reduced kernel code size to 8700 lines of C code and conducted formal verification to proof correctness @cite_51 . Even with a secure microkernel in place, designing a fully-featured, secure OS on top of it is still an unmet challenge @cite_63 . Hence, one has to live with a feature-rich but untrusted OS.
@cite_51 @cite_63
2136310957 2052801306 2062025743 168427334
Complete formal verification is the only known way to guarantee that a system is free of programming errors. We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, and hardware, and we used a unique design approach that fuses formal and operating systems techniques. To our knowledge, this is the first formal proof of functional correctness of a complete, general-purpose operating-system kernel. Functional correctness means here that the implementation always strictly follows our high-level abstract specification of kernel behaviour. This encompasses traditional design and implementation safety properties such as the kernel will never crash, and it will never perform an unsafe operation. It also proves much more: we can predict precisely how the kernel will behave in every possible situation. seL4, a third-generation microkernel of L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels. 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. To be trustworthy, security-sensitive applications must be formally verified and hence small and simple, i.e., wimpy. Thus, they cannot include a variety of basic services available only in large and untrustworthy commodity systems, i.e., in giants. Hence, wimps must securely compose with giants to survive on commodity systems, i.e., rely on giants' services but only after efficiently verifying their results. This paper presents a security architecture based on a wimpy kernel that provides on-demand isolated I O channels for wimp applications, without bloating the underlying trusted computing base. The size and complexity of the wimpy kernel are minimized by safely outsourcing I O subsystem functions to an untrusted commodity operating system and exporting driver and I O subsystem code to wimp applications. Using the USB subsystem as a case study, this paper illustrates the dramatic reduction of wimpy-kernel size and complexity, e.g., over 99 of the USB code base is removed. Performance measurements indicate that the wimpy-kernel architecture exhibits the desired execution efficiency. Today large software systems (i.e., giants) thrive in commodity markets, but are untrustworthy due to their numerous and inevitable software bugs that can be exploited by the adversary. Thus, the best hope of security is that some small, simple, and trustworthy software components (i.e., wimps) can be protected from attacks launched by adversary-controlled giants. However, wimps in isolation typically give up a variety of basic services (e.g., file system, networking, device I O), trading usefulness and viability with security. Among these basic services, isolated I O channels remained an unmet challenge over the past three decades. Isolated I O is a critical security primitive for a myriad of applications (e.g., secure user interface, remote device control). With this primitive, isolated wimps can transfer I O data to commodity peripheral devices and the data secrecy and authenticity are protected from the co-existing giants. This thesis addresses this challenge by proposing a new security architecture to provide services to isolated wimps. Instead of restructuring the giants or bloating the Trusted Computing Base that underpins wimp-giant isolation (dubbed underlying TCB), this thesis presents a unique on-demand I O isolation model and a trusted add-on component called wimpy kernel to instantiate this model. In our model, the wimpy kernel dynamically takes control of the devices managed by a commodity OS, connects them to the isolated wimps, and relinquishes controls to the OS when done. This model creates ample opportunities for the wimpy kernel to outsource I O subsystem functions to the untrusted OS and verify their results. The wimpy kernel further exports device drivers and I O subsystem code to wimps and mediates the operations of the exported code. These two methodologies help to significantly reduce the size and complexity of the wimpy kernel for high security assurance. Using the popular and complex USB subsystem as a case study, this thesis illustrates the dramatic reduction of the wimpy kernel; i.e., over 99 of the Linux USB code base is removed. In addition, the wimpy kernel also composes with the underlying TCB, by retaining its code size, complexity and security properties.