{"id":606273,"date":"2019-09-05T09:01:41","date_gmt":"2019-09-05T16:01:41","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?p=606273"},"modified":"2020-06-08T10:18:25","modified_gmt":"2020-06-08T17:18:25","slug":"project-everest-advancing-the-science-of-program-proof","status":"publish","type":"post","link":"https:\/\/www.microsoft.com\/en-us\/research\/blog\/project-everest-advancing-the-science-of-program-proof\/","title":{"rendered":"Project Everest: Advancing the science of program proof"},"content":{"rendered":"

\"image (opens in new tab)<\/span><\/a><\/p>\n

Project Everest (opens in new tab)<\/span><\/a> is a multiyear collaborative effort focused on building a verified, secure communications stack designed to improve the security of HTTPS, a key internet safeguard. This post\u2014about the proving methodology and verification tools of Project Everest\u2014is the third in a series exploring the groundbreaking work, which is available on GitHub (opens in new tab)<\/span><\/a> now.<\/em><\/p>\n

Building, deploying, and maintaining software at scale is a large engineering effort, and when that software is intertwined with machine-checked proofs of correctness, the engineering involved is largely without precedent. In Project Everest (opens in new tab)<\/span><\/a>, dozens of researchers and engineers push to five open-source GitHub repositories, building about 600,000 lines of code and proofs, continuously integrated using Azure DevOps, hundreds of times every day. There have been countless hard-won lessons on software and proof-engineering best practices, ranging from developing and maintaining robust proofs in the face of an evolving codebase to tweaking the format of our compilers to enable humans to audit the C and assembly-language code produced by our software verification toolchain.<\/p>\n

But this post isn’t about the engineering. It\u2019s about the science that underlies it\u2014the science of program proof. I mean proving deep theorems<\/em> about programs, proofs that establish that the full semantics of a program adhere to a mathematical model of all<\/em> its behaviors, not just theorems proving, say, the absence of specific kinds of bugs (which is, of course, also useful!).<\/p>\n

From the early days of computer science, the potential of program proof to eradicate large classes of software errors has been widely recognized; however, until recently, few practical applications were feasible. The proof techniques were difficult to apply to full-fledged programming languages, and proofs were hard to scale to large programs. Oftentimes, the proofs that were done came at the cost of other important aspects of software, such as performance. But today, what seemed impossible just a few years ago is becoming a reality. We can, in certain domains, produce fully verified software at a nontrivial scale and with runtime performance that meets or exceeds the best unverified software.<\/p>\n

Fast\u2014and verified\u2014secure communication code<\/h3>\n

Project Everest is a case in point: We produce verified cryptographic routines, parsers, and protocols that are deployed in production settings with strong correctness and security guarantees and<\/em> great performance. Our recently released EverCrypt cryptographic provider (opens in new tab)<\/span><\/a> consists of 23,000 lines of verified C code and 18,000 lines of verified assembly code extracted from 107,000 lines of code and proof in the F* programming language and proof assistant\u2014a development effort of roughly three person-years. The chart below shows the throughput of several verified cryptographic routines since 2014. Over the last five years, there\u2019s been slow but steady improvement, but this year, with EverCrypt, we made a noticeable jump to finally verify the fastest assembly code of OpenSSL (opens in new tab)<\/span><\/a> for AES-GCM, a crypto routine used by 90 percent of secure internet connections.<\/p>\n

\"After

(opens in new tab)<\/span><\/a> After years of slow but steady gains in the throughput of verified cryptographic routines, Project Everest made significant progress with the verification of the fastest assembly code of OpenSSL for AES-GCM.<\/p><\/div>\n

What made it possible for verified code to finally catch up to the fastest unverified code out there? Program verification tools and methodologies have passed a tipping point that has allowed large, previously intractable problems to be decomposed effectively and smaller problems to be solved with increasing automation.<\/p>\n

A trinity of program proof<\/h3>\n

\"trinity (opens in new tab)<\/span><\/a>Program verification researchers have long sought a proof methodology and tool to excel in three dimensions that can often be at odds, where maximizing for one diminishes the ability to achieve the highest level of another:<\/p>\n

Automation<\/strong>: Proving a large program requires proving thousands or even millions of small theorems. Without automation, the task is hopelessly tedious. Recent advances in SMT solving are well documented\u2014Z3 (opens in new tab)<\/span><\/a>, developed by Microsoft Research, is a leading example\u2014and many program verification tools have leveraged these advances to automate vast numbers of simple proofs.<\/p>\n

Expressiveness<\/strong>: Proving millions of simple theorems alone doesn\u2019t cut it. At the crux of any significant software verification effort is a genuinely complex proof involving sophisticated mathematics. As such, one needs a full-featured modern language coupled with a powerful logic in which to conduct deep mathematical reasoning. Less widely appreciated than advances in SMT solvers, but no less important, are advances that have led to logics that provide both a theoretical foundation for mathematics as well as a practical foundation for software. A significant milestone was the emergence of large verified software artifacts, notably the CompCert C verified compiler (opens in new tab)<\/span><\/a> in 2006. These advances demonstrated that type theory (opens in new tab)<\/span><\/a>, which was originally conceived in the 1970s as a new foundation for logic and mathematics, could also be a viable basis for verified software.<\/p>\n

Control<\/strong>: To harness the power of type theory and to combine it with the automation of SMT solvers, advances in metaprogramming have allowed proof engineers to tune automated proofs, diagnose failures, develop new domain-specific decision procedures, and script how their programs are proven, generated, and compiled.<\/p>\n

Devising a proof methodology and tool that truly excels on all three dimensions is an ongoing research challenge. But several modern proof assistants, such as Coq (opens in new tab)<\/span><\/a>, Lean (opens in new tab)<\/span><\/a>, Isabelle (opens in new tab)<\/span><\/a>, and Agda (opens in new tab)<\/span><\/a>, are beginning to deliver simultaneously on all three fronts. F*, the proving methodology and tool of Project Everest (opens in new tab)<\/span><\/a>, is as well.<\/p>\n

The F* balancing act<\/h3>\n

The research agenda of F*, now nearly a decade and about 10 research papers in, is to balance automation, expressiveness, and control within a full-fledged programming language and proof assistant. F* is based on type theory but with SMT solving and metaprogramming as essential elements.<\/p>\n

Some of the key challenges that we\u2019ve addressed include the following:<\/p>\n

    \n
  1. Effects in type theory<\/strong>: Type theory is a logic of pure functions. No real programming language can be purely functional. One of F*\u2019s main innovations is in encoding effects\u2014state, exceptions, I\/O\u2014within type theory. A key concept is the Dijkstra monad<\/em>, invented and applied in F* in a 2013 paper (opens in new tab)<\/span><\/a> and refined (opens in new tab)<\/span><\/a> and generalized (opens in new tab)<\/span><\/a> repeatedly (opens in new tab)<\/span><\/a> since then. Dijkstra monads give a semantics to effects within type theory using predicate transformers in the style of Dijkstra\u2019s weakest preconditions.<\/li>\n
  2. SMT integration<\/strong>: At the very heart of F* is an encoding of type theory into the logic of an SMT solver. While SMT solvers can\u2019t automate all proofs in type theory (far from it!), they\u2019re remarkably effective at proving a large number of the kinds of goals that arise in a typical program proof. A single complete build of Project Everest\u2019s code produces nearly a million proofs that are dispatched by the Z3 SMT solver.<\/li>\n
  3. Metaprogramming<\/strong>: Building on ideas from Microsoft Research\u2019s Lean theorem prover, Meta-F* (opens in new tab)<\/span><\/a>\u2014a metaprogramming framework\u2014makes F* its own metaprogramming language. It provides Everest proof engineers with the control to construct and inspect proofs and programs programmatically. Meta-F* is at the leading edge of F*, and it continues to evolve and be used in new ways.<\/li>\n
  4. Embedded domain-specific languages<\/strong>: Rather than program and prove directly in type theory, we\u2019ve designed new domain-specific languages (DSLs) within F* and use them to develop precise models and effective automation for specific tasks. We have DSLs embedded in F* for C-like programming (opens in new tab)<\/span><\/a>; for verified assembly language (opens in new tab)<\/span><\/a> (with which we finally cracked the AES-GCM verification challenge); and even for low-level parsers and serializers (opens in new tab)<\/span><\/a>, which can produce verified code that can be, in some cases, orders of magnitude faster than existing unverified handwritten code.<\/li>\n<\/ol>\n

    Advances in the programming language and verification technology have proven crucial to our work while also providing new insights into application areas. Project Everest\u2019s focus on verified cryptographic communication protocols has generated techniques for doing cryptographic correctness and security proofs on executable implementations of complex algorithms (opens in new tab)<\/span><\/a>, constructions (opens in new tab)<\/span><\/a>, protocols (opens in new tab)<\/span><\/a>, and even cryptographic providers (opens in new tab)<\/span><\/a>, relating low-level optimized implementations to high-level mathematical and security properties.<\/p>\n

    Looking ahead: Program proof at scale<\/h3>\n

    We finally have methods to build and deploy verified performant secure communication code, but more research is needed to broaden the reach of program proof.<\/p>\n