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 be incorporated into larger projects (both verified and unverified). 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

Owl's approach intersects with two classes of verification tools: 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 and HPKE.

Compared to CryptoVerif and Tamarin, Owl's advantage 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.

Owl: Compositional Verification of Security Protocols via an Information-Flow Type System. Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, & Bryan Parno. In Proceedings of the IEEE Symposium on Security and Privacy, 2023.

OwlC: Compiling Security Protocols to Verified, Secure, High-Performance Libraries. Pratap Singh, Joshua Gancher, & Bryan Parno. In Proceedings of the USENIX Security Symposium, 2025.

Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust. Yi Cai, Pratap Singh, Zhengyao Lin, Jay Bosamiya, Joshua Gancher, Milijana Surbatovich, Bryan Parno. In Proceedings of the USENIX Security Symposium, 2025.