08:30-10:00
Welcome and Keynote
10:30-12:00
Static Analyses
Finding Resource-Release Omission Faults in Linux
The management of the releasing of allocated resources is a continual
problem in ensuring the robustness of systems code. Missing
resource-releasing operations lead to memory leaks and deadlocks.
A number of approaches have been proposed to detect such problems,
but they often have a high rate of false positives, or focus
only on commonly used functions. In this paper we observe that
resource-releasing operations are often found in error-handling code,
and that the choice of resource-releasing operation may depend on
the context in which it is to be used. We propose an approach to
finding resource-release omission faults in C code that takes into
account these issues. We use our approach to find over 100 faults in
the drivers directory of Linux 2.6.34, with a false positive rate of
only 16%, well below the 30% that has been found to be acceptable
to developers.
Configuration Coverage in the Analysis of Large-Scale System Software
System software, especially operating systems, tends to be
highly configurable. Like every complex piece of software, a
considerable amount of bugs in the implementation has to
be expected. In order to improve the general code quality,
tools for static analysis provide means to check for source
code defects without having to run actual test cases on
real hardware. Still, for proper type checking a specific
configuration is required so that all header include paths are
available and all types are properly resolved.
In order to find as many bugs as possible, usually a “full
configuration” is used for the check. However, mainly because
of alternative blocks in form of #else-blocks, a single configuration
is insufficient to achieve full coverage. In this paper, we
present a metric for configuration coverage (CC) and explain
the challenges for (properly) calculating it. Furthermore, we
present an efficient approach for determining a sufficiently
small set of configurations that achieve (nearly) full coverage
and evaluate it on a recent Linux kernel version.
Rounding Pointers — Type Safe Capabilities with C++ Meta Programming
Recent trends in secure operating systems indicate that an
object-capability system is the security model with pre-eminent
characteristics and practicality. Unlike traditional
operating systems, which use a single global name space,
object-capability systems name objects per protection
domain. This allows a fine-grained isolation of the domains
and follows the principle of least authority.
Programming in such an environment differs considerably
from traditional programming models. The fine-grained
access to functionality requires a programming environment
that supports the programmer when using a capability
system. In this paper, we present an object-oriented framework
that uses the C++ programming language to offer a
framework for building and using operating-system components
and applications.
Preliminary Design of the SAFE Platform
SAFE is a clean-slate design for a secure host architecture.
It integrates advances in programming languages, operating
systems, and hardware and incorporates formal methods
at every step. Though the project is still at an early stage,
we have assembled a set of basic architectural choices that
we believe will yield a high-assurance system. We sketch
the current state of the design and discuss several of these
choices.
13:30-15:00
Dynamic Safety and Performance
Dynamic Deadlock Avoidance in Systems Code Using Statically Inferred Effects
Deadlocks can have devastating effects in systems code. We have
developed a type and effect system that provably avoids them and
in this paper we present a tool that uses a sound static analysis
to instrument multithreaded C programs and then links these programs
with a run-time system that avoids possible deadlocks. In
contrast to most other purely static tools for deadlock freedom, our
tool does not insist that programs adhere to a strict lock acquisition
order or use lock primitives in a block-structured way, thus it
is appropriate for systems code and OS applications. We also report
some very promising benchmark results which show that all
possible deadlocks can automatically be avoided with only a small
run-time overhead. More importantly, this is done without having
to modify the original source program by altering the order of resource
acquisition operations or by adding annotations.
Using Declarative Invariants for Protecting File-System Integrity
We have been developing a framework, called Recon, that
uses runtime checking to protect the integrity of file-system
metadata on disk. Recon performs consistency checks at
commit points in transaction-based file systems. We define
declarative statements called consistency invariants for a file
system, which must be satisfied by each transaction being
committed to disk. By checking each transaction before it
commits, we prevent any corruption to file-system metadata
from reaching the disk.
Our prototype system required writing the consistency invariants
in C. In this paper, we argue that using a declarative
language to express and check these invariants improves
the clarity of the rules, making them easier to reason about,
verify, and port to new file systems. We describe how file system
invariants can be written and checked using the Datalog
declarative language in the Recon framework.
Assessing the Scalability of Garbage Collectors on Many Cores
Managed Runtime Environments (MRE) are increasingly
used for application servers that use large multi-core hardware.
We find that the garbage collector is critical for overall
performance in this setting. We explore the costs and scalability
of the garbage collectors on a contemporary 48-core
multiprocessor machine. We present experimental evaluation
of the parallel and concurrent garbage collectors present
in OpenJDK, a widely-used Java virtual machine. We show
that garbage collection represents a substantial amount of
an application’s execution time, and does not scale well as
the number of cores increases. We attempt to identify some
critical scalability bottlenecks for garbage collectors.
URDB: A Universal Reversible Debugger Based on Decomposing Debugging Histories
Reversible debuggers have existed since the early 1970s. A
novel approach, URDB, is introduced based on
checkpoint/reexecute. It adds reversibility to a debugger,
while still placing the end user within the familiar environment of their
preferred debugger. The URDB software layer currently
includes modes that understand the syntax for four debuggers:
GDB for C/C++/Java/Fortran, Python (pdb), MATLAB,
and Perl (perl -d). It does so by adding a thin URDB
software layer on top of the DMTCP checkpoint-restart package.
URDB passes native debugging commands between the end
user and the underlying debugging session. URDB models
the four common debugging primitives that form the basis
for most debuggers: step, next, continue, break. For
example, given a debugging history of the form [step, next,
step], URDB's reverse-step produces a new history, [step,
next]. Further, subtle algorithms are described for
reverse-xxx. For example, reverse-step operates correctly when
the last instruction of the history is next or continue.
URDB calls DMTCP to create a checkpoint during a
debugging session, and then replays the history from there. An
essential novelty of this work is the extension of DMTCP to
be the first checkpointing package capable of checkpointing
a GDB sesssion to disk (through checkpointing the Linux
ptrace system call). This was a significant barrier to earlier
attempts toward checkpoint/re-execute for GDB. Support
for the GDB debugger is important to any reversible
debugger claiming universality. Experimental results are described
for GDB, MATLAB, Python (pdb), and Perl.
15:30-17:00
Demonstrations and Working Groups
17:00-18:30
Working Groups and Wrap-up