Past & present projects at PDOS

Current projects

Verified hardware/software systems
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.

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.

Noria: data-flow for web applications
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: An OS kernel in a high-level language

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.

Secure web-application databases
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: Concurrency verification with movers
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: File-system verification
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.
Multicore scalability

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.

Amber: User-centric cloud storage
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.