Current projects
Knox is a framework that enables developers to build correct and secure hardware security modules (HSMs) through formal verification spanning an implementation’s hardware and software.
vMVCC is a high-performance transaction library with a formal specification and a machine-checked proof of correctness.
Perennial is a Coq framework for verifying concurrent storage systems. It supports verifying systems written in Go by translating them to Coq to complete the proof using Perennial.
Past projects
Many PDOS research projects don't have a project page below. For the full list
of research done by PDOS, see the publications
page.
Vuvuzela is the first messaging system that provides strong metadata privacy while scaling to millions of users.
Noria is an attempt at designing a database specifically tailored for web applications, providing automatic caching, safe and effortless schema migrations, and native support for reactive use.
Biscuit is a monolithic, POSIX-subset operating system kernel in Go for x86-64
CPUs. We wrote it to study the performance trade-offs of using a high-level
language with garbage collection to implement a kernel with a common style of
architecture.
The goal of this line of research is to apply cryptographic techniques practically to secure web application databases and provide strong guarantees against realistic adversaries.
CSPEC is a framework in the Coq proof assistant for proving concurrent software correct using movers. The idea behind movers is to reduce the number of concurrent interleavings the programmer needs to consider. We've used CSPEC to prove a concurrent mail server correct which involves lock-free concurrency control with the file system.
FSCQ is the first file system with a machine-checkable proof (in the Coq proof assistant) that its implementation meets its specification and whose specification includes behavior under crashes.
We build and investigate software systems for multicore computers. We
have analyzed and fixed scalability problems in existing software, such
as the Linux kernel, and built scalable software from scratch, such as
RadixVM and the Corey kernel. To facilitate this work and help
identify scalability bottlenecks on multicore computers we have built
analysis tools, like DProf.
A project to collect a users' data in a common, federated storage, to give users control over their data's storage and facilitate better sharing among applications through the use of global, cross-cloud queries.
