Operating Systems Design and Implementation · 2006 · 170 citations · 33 references
EngineeringInformation SecurityComputer ArchitectureSoftware EngineeringSoftware AnalysisFormal VerificationHardware SecuritySource CodeRuntime VerificationSoftware System SafetyOperating System SecurityComputer EngineeringLanguage-based TechniquesComputer ScienceDevice DriverLanguage-based SecurityData SecuritySoftware SecurityOperating SystemsProgram AnalysisSafedrive Tracks InvariantsSoftware TestingType Safety ViolationsUnikernelsSystem Software
We present SafeDrive, a system for detecting and recovering from type safety violations in software extensions. SafeDrive has low overhead and requires minimal changes to existing source code. To achieve this result, SafeDrive uses a novel type system that provides fine-grained isolation for existing extensions written in C. In addition, SafeDrive tracks invariants using simple wrappers for the host system API and restores them when recovering from a violation. This approach achieves fine-grained memory error detection and recovery with few code changes and at a significantly lower performance cost than existing solutions based on hardware-enforced domains, such as Nooks [33], L4 [21], and Xen [13], or software-enforced domains, such as SFI [35]. The principles used in SafeDrive can be applied to any large system with loadable, error-prone extension modules.In this paper we describe our experience using SafeDrive for protection and recovery of a variety of Linux device drivers. In order to apply SafeDrive to these device drivers, we had to change less than 4% of the source code. SafeDrive recovered from all 44 crashes due to injected faults in a network card driver. In experiments with 6 different drivers, we observed increases in kernel CPU utilization of 4--23% with no noticeable degradation in end-to-end performance.
33
Xen and the art of virtualization
Paul Barham, Boris Dragovic, Keir Fraser et al. · ACM SIGOPS Operating Systems Review · 2003 · 5.9K citations
Efficient software-based fault isolation
Robert Wahbe, Steven Lucco, Thomas E. Anderson et al. · 1993 · 1.2K citations · Full text
Software Maintenance, Engineering, Computer Architecture +19
An empirical study of operating systems errors
Andy Chou, Junfeng Yang, Benjamin Chelf et al. · 2001 · 706 citations
Automatic predicate abstraction of C programs
Thomas Ball, Rupak Majumdar, Todd Millstein et al. · ACM SIGPLAN Notices · 2012 · 696 citations
Trevor Jim, J. Greg Morrisett, Dan Grossman et al. · 2002 · 617 citations