Writing high-performance low-level code that is correct, reliable, and secure is notoriously difficult, and yet increasingly critical. We are developing a new tool, Verus, that leverages the sophisticated design and engineering of the Rust language to enable full verification of such systems code. Verification enables developers to prove strong properties (including functional correctness, reliability and security) about their Rust code and, in many cases, avoid the risks of using unsafe Rust code. In the other direction, Rust's linearity and type checkers can simplify proofs about low-level code correctness, and even enable developers to ergonomically reason about shared-memory concurrency. Building on our prior experience with systems verification in the Ironclad and Everest projects, Verus includes dedicated automation to address the thorny verification problems that arise in a systems setting.

The HTTPS ecosystem (HTTPS and TLS protocols, X.509 public key infrastructure, crypto algorithms) is the foundation on which Internet security is built. Unfortunately, this ecosystem is extremely brittle, with headline-grabbing attacks such as FREAK and LogJam, and emergency patches many times a year.

Building on our experience with Ironclad, MiTLS, and other related projects, Project Everest proposes to definitively solve this problem by constructing a high-performance, standards-compliant, verified implementation of the full HTTPS ecosystem, from the HTTPS API down to and including cryptographic algorithms such as RSA and AES. At the TLS level, for instance, we will develop new implementations of existing protocol standards and formally prove, by reduction to cryptographic assumptions on their core algorithms, that our implementations provide a secure-channel abstraction between the communicating endpoints. Project Everest aims to be a drop-in replacement for the HTTPS library in mainstream web browsers, servers, and other popular tools.

While verifiable computation provides strong guarantees, even the best cryptographic system is useless if implemented badly, applied incorrectly, or used in a vulnerable system. Thus, the Ironclad project works to expand formal software verification to provide end-to-end guarantees about the security and reliability of complex systems. By creating a set of new tools and methodologies, Ironclad produced the first complete stack of verified-secure software. We also recently developed the first methodology for verifying both the safety and liveness of complex distributed systems implementations. Many interesting challenges remain, including verifying concurrent or probabilistic programs, improving the performance of verifiers and verified code, and enhancing the stability of automated proofs. Nonetheless, I expect that verification will fundamentally improve the software that underpins our digital and physical infrastructure.

To provide strong guarantees for outsourced computations, we developed a new cryptographic framework, Verifiable Computation, which allows clients to outsource general computations to completely untrusted services and efficiently verify the correctness of each returned result. Through improvements to the theory and the underlying systems over the last few years, we reduced the costs of verification by over twenty orders of magnitude. As a result, verifiable computation is now a thriving research area that has produced several startups, as well as enhancements to the security and privacy of X.509, MapReduce, and Bitcoin. We are continuing to explore improvements and applications in this space, as well as other settings where cryptographic advances can be deployed to create fundamentally more secure services.

In the last decade, we've seen the rise of modern client platforms like iOS, Android, and even web browsers. On each platform, unlike on the traditional desktop, applications are strongly isolated. A key challenge, however, is determining how and when the platform should grant applications access to user-owned resources, e.g., to sensitive devices like the camera or to user data residing in other applications. Previous systems either granted access by prompting the user (Windows 7, iOS), relied on install-time manifests (Android), or both (Windows Phone). Unfortunately, multiple studies indicate the futility of these measures; in practice, users ignore them both.

We designed a brand new approach called user-driven access control, whereby permission granting is built into existing user actions.

We also reenvisioned the web interface based on the notion of a client-side pico-datacenter. Just as in the cloud datacenter, the simple client semantics make isolation tractable while giving web applications the freedom to run any software stack. Since the datacenter model is designed to be robust to malicious tenants, it is never dangerous for the user to click on a URL.