Device driver isolation aims to protect kernels from faulty/malicious drivers, yet its security guarantees are not fully understood. Compartment Interface Vulnerabilities (CIVs), known in userspace applications, also impact driver isolation, but this area is underexplored. This paper surveys existing driver isolation frameworks, systematizes CIV classifications, and evaluates them in the driver isolation context. Our analysis reveals CIV prevalence under a baseline threat model, with large drivers exhibiting over 100 CIV instances and an average of 33 across the studied drivers. Enforcing additional security properties like CFI reduces average CIVs to approximately 28. This work offers insights into driver isolation security, CIV prevalence, and guidance for future systems.

Static information flow analysis has been studied for a long time. It is usually considered more precise than dynamic taint analysis and more flexible and indispensable when running individual modules or the entire program is difficult. The state-of-the-art static information flow analyses are scalable on analyzing Java programs or mobile apps, and several type systems have enforced information flow security on different languages. However, static information-flow analyses have rarely scaled up to real-world C programs. This work presents Sliver, a slicing-based approach to verify information flow security on real-world C programs. The principle of Sliver is to convert the information-flow-involved parts of the original program into behavior-equivalent slices and use bounded model checking to enforce the end-to-end noninterference property or detect security violations on the slices after self-composition. We develop automated path-signature-guided slicing and adaptive self-composition approaches to ensure Sliver's efficacy and scalability. We also develop a consistency testing technique and metrics to estimate the correctness of slices generated by Sliver. The evaluations demonstrate Sliver's effectiveness, scalability, and the correctness of the generated slices.

Our work explores the challenge of developing secure kernel-driver interfaces designed to protect the kernel from isolated kernel extensions. We first analyze a range of possible attack vectors that exist in current isolation frameworks. Then, we suggest a new approach to building secure isolation boundaries centered around ideas that originate in safe operating systems: isolation of heaps and single ownership.

Dynamic taint analysis (DTA) has been widely used in various security-relevant scenarios that need to track the runtime information flow of programs. Dynamic binary instrumentation (DBI) is a prevalent technique in achieving effective dynamic taint tracking on commodity hardware and systems. However, the significant performance overhead incurred by dynamic taint analysis restricts its usage in production systems. Previous efforts on mitigating the performance penalty fall into two categories, parallelizing taint tracking from program execution and abstracting the tainting logic to a higher granularity. Both approaches have only met with limited success. In this work, we propose Sdft, an efficient approach that combines the precision of DBI-based instruction-level taint tracking and the efficiency of function-level abstract taint propagation. First, we build the library function summaries automatically with reachability analysis on the program dependency graph (PDG) to specify the control- and data dependencies between the input parameters, output parameters, and global variables of the target library. Then we derive the taint rules for the target library functions and develop taint tracking for library function that is tightly integrated into the state-of-the-art DTA framework Libdft. By applying our approach to the core C library functions of glibc, we report an average of 1.58x speed up of the tracking performance compared with Libdft64. We also validate the effectiveness of the hybrid taint tracking and the ability on detecting real-world vulnerabilities.

Commodity operating systems execute core kernel subsystems in a single address space along with hundreds of dynamically loaded extensions and device drivers. Lack of isolation within the kernel implies that a vulnerability in any of the kernel subsystems or device drivers opens a way to mount a successful attack on the entire kernel.

Privilege separation is an effective technique to improve software security. However, past partitioning systems do not allow programmers to make quantitative tradeoffs between security and performance. In this paper, we describe our toolchain called PM. It can automatically find the optimal boundary in program partitioning. This is achieved by solving an integer-programming model that optimizes for a user-chosen metric while satisfying the remaining security and performance constraints on other metrics. We choose security metrics to reason about how well computed partitions enforce information flow control to: (1) protect the program from low-integrity inputs or (2) prevent leakage of program secrets. As a result, functions in the sensitive module that fall on the optimal partition boundaries automatically identify where declassification is necessary. We used PM to experiment on a set of real-world programs to protect confidentiality and integrity; results show that, with moderate user guidance, PM can find partitions that have better balance between security and performance than partitions found by a previous tool that requires manual declassification.