Tuesday, October 31, 2006

Paper: "SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques"

SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques
Feng Zhou, Jeremy Condit, Zachary Anderson, and Ilya Bagrak, University of California, Berkeley; Rob Ennals, Intel Research Berkeley; Matthew Harren, George Necula, and Eric Brewer, University of California, Berkeley


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, L4, and Xen, or software-enforced domains, such as SFI. 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.


Blogger Ethan L. Miller said...

This approach works well for certain classes of data structures, particularly arrays and simple linked lists. Can the technique be adapted to more complex data structures, such as B-trees, or are those simply treated as combinations of arrays and linked lists? If the latter, can SafeDrive handle the dynamic nature of the arrays in such data structures?

4:18 PM  
Blogger Feng said...

A B-tree (internal one, not on disk) will be treated as a combination of arrays and linked lists, all of which can be annotated to indicate the size and type of the
allocated objects. For example, if a B-tree node contains an array of
data and an array of child pointers, then we will annotate these arrays as count(n) (where n is the allocated size of the array), and
we will annotate the child pointers as safe pointers. These annotations will allow SafeDrive to prevent any accesses outside the allocation boundaries of these arrays and to prevent any null pointer dereferences. Some of these errors can be found at compile time,
particularly if n is a compile-time constant. SafeDrive does not currently track any higher-level properties of such data structures;
for example, we do not enforce correct ordering of elements in the

2:16 PM  
Blogger Geoffrey Lefebvre said...


5:19 PM  
Blogger Geoffrey Lefebvre said...

SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques

Feng Zhou, Jeremy Condit, Zachary Anderson, and Ilya Bagrak, University of California, Berkeley; Rob Ennals, Intel Research Berkeley; Matthew Harren, George Necula, and Eric Brewer, University of California, Berkeley

Presented by Feng Zhou

Feng Zhou began his talk by noting that many operating systems and applications run loadable extensions. These extensions are often buggier than their hosts and execute in the same protection domain. To address this issue, the authors present SafeDrive, a language based approach to extension safety. Safedrive can be decomposed into two principal component. The Deputy source to source compiler and the run-time recovery system.

Although the principles presented could be applied to other systems, the talk and the paper focused on adding type-based checking and restart capability to existing Linux device drivers. The core idea is to transform code written in C into a safe variant addressing issues such as out-of-bound array accesses, null terminated strings, and unions.

Previous approaches to retro-fitting type safety to C, such as CCured, required the use of fat pointers, which contain both the pointer and bound information. This approach unfortunately requires changing the memory layout of data structures making the modified extensions incompatible with their host's binaries. Instead of using fat pointers, Deputy relies on the programmer adding lightweight annotations to header files and extension source code. The authors note that the content of these annotations is often already present in the source code in the form of constants or comments. The programmer must transform this information into a form that the Deputy compiler can understand so that the compiler is able to add the appropriate run-time checks.

Since SafeDrive relies on run-time checks, it must provide mechanisms to deal with violations. SafeDrive enforces the invariant that no driver code will execute after a failure. Instead of relying on driver code to cleanup, SafeDrive provides this functionality. The SafeDrive run-time system tracks all kernel resources used by a device driver using wrappers around kernel API functions. Each tracked resource is paired with a compensation operation that performs an "undo" when a fault occurs in a driver. As an example, the compensation operation for a spinlock is to release the lock.

Compared to approaches using hardware memory protection such as Nooks, Safedrive provides finer grain memory protection. This allows it to catch more errors at compile time and exhibit less run-time overhead.

Andrew Baumann from University of New South Whales stated that many bugs are concurrency related and asked if SafeDrive can detect and recover from such errors. Feng Zhou answered that SafeDrive does not currently address this issue. Brad Karp from University College London asked if SafeDrive handled integer overflow, more specifically the case where a signed integer overflow could result in a different memory allocation than the size requested. Feng Zhou answered that SafeDrive doesn't deal with integer overflow but that in most cases, memory allocation routines should handle this issue.

Rik Farrow asked what happens when programmers make errors writing the annotations. The answer is that the Deputy type system will catch some of the errors. Michael Swift from University of Wisconsin asked how easy would it be to integrate this with Nooks to allow catching errors that only Nooks is able to catch. Feng Zhou answered that it should be feasible to do so. Finally Someone from University of California, Santa Cruz asked if SafeDrive was able to cope with complex data structures. Feng replied that by being able to deal directly with pointers, Deputy is able to do so.

5:25 PM  

Post a Comment

<< Home