Overview

Owl is a programming language and proof assistant designed to help developers build cryptographic security protocols with mathematical guarantees of correctness and security.

The intended workflow of Owl is as follows: first, the developer writes a protocol in the Owl language, which uses information-flow and refinement types to specify and prove security. Then, the protocol can be extracted using our compiler into a high-performance implementation in Verus, an extension of Rust with formal verification capabilities, that is guaranteed by construction to be functionally correct and secure against source-level side channels.

The repository for Owl can be found here.

Owl's Design

The Owl language is backed by two main programming language technologies: information-flow types, which reasons about the secrecy information of data in the program; and refinement types, which use SMT solvers (we use Z3) to imbue types with logical specifications.

The key novelty of Owl is that information-flow and refinement types, on their own, are not enough. We also need to faithfully model the security guarantees of cryptographic operations, such as encryption. To do this, Owl's type system comes with a soundness proof that every well-typed protocol is cryptographically secure.

In addition to formal verification of protocol designs, Owl also enables protocol developers to automatically extract real-world code that one can link with. Our compiler, described in our USENIX Security paper, uses Verus to compile Owl protocols into efficient, interoperable, side-channel resistant Rust libraries that are automatically formally verified to be correct.

Comparisons between Owl and Other Tools

There are two classes of verification tools which Owl intersects with: game-hopping cryptographic provers, based on relational program logics, such as EasyCrypt; and "security protocol verifiers", such as CryptoVerif and Tamarin.

Compared to EasyCrypt, Owl is less general but significantly more automated. EasyCrypt allows the user to prove arbitrary cryptographic theorems using an expressive probabilistic logic; on the other hand, Owl is specifically targeted at security protocols, such as WireGuard HPKE.

Compared to CryptoVerif and Tamarin, the advantage of Owl is that its type system guarantees the properties of computational security, compositionality, and a high degree of proof automation.

Calling Owl

Owl is a Haskell package, built with cabal. Run cabal run owl to see options for the executable. If developing a protocol, the most useful option is --log-typecheck:

cabal run owl -- test.owl --log-typecheck

which will output debug and progress information.