Owl is a tool for developing cryptographic protocols with formal, machine-checked guarantees of security. Cryptographic protocols, such as WireGuard and TLS, form the foundation of secure digital infrastructure, but vulnerabilities are discovered in them with alarming frequency. To ameliorate this situation, Owl allows developers to prove that their protocols are secure, providing a high degree of assurance that many common classes of vulnerabilities will not arise.
Owl consists of an automated verifier and secure compiler for cryptographic protocols. Owl's verifier enables developers to prove security against a strong adversary model, analogous to models used by pen-and-paper cryptographers1; unlike pen-and-paper proofs, however, Owl provides powerful proof automation to aid with scaling proofs to realistic protocols. The verifier is based on a novel type system for secure protocol code, which guarantees that any well-typed protocol is secure. Owl's secure compiler translates verified protocol designs into performant, interoperable Rust libraries, ready for deployment. The libraries are automatically formally verified to be correct implementations of the verified protocol design, using Verus, a deductive program verifier for Rust; they also use Rust's type system to guarantee the absence of certain digital side-channel attacks.
Developers first describe their protocol in the Owl language, a high-level, functional domain-specific language with built-in cryptographic primitives. They then prove computational security for their protocol using Owl's information-flow and refinement types. Finally, they use Owl's secure compiler to generate a verified Rust library of protocol routines, which they can then integrate into a larger application or codebase.
Owl is still under active development, and the language, verifier, and compiler are all subject to change. Please report bugs and problems via GitHub issues. We also welcome contributions from the community via pull requests!
Owl currently supports the following cryptographic primitives:
- Authenticated Symmetric Encryption (e.g., ChaCha20-Poly1305, or AES-GCM)
- CCA-secure PKE (e.g., RSA with OAEP)
- Message Authentication Codes (e.g., HMAC)
- Digital Signatures (e.g., RSA signatures)
- Diffie-Hellman Key Exchange
- HKDF for key derivations
- Unique Nonces for checking equality
Work-in-progress documentation is in the docs directory. A number of example Owl protocols are in the tests/success directory, illustrating various features of the Owl language and type system.
The main branch tracks recent developments, so the Owl syntax and language features are subject to change.
Our release here corresponds to our S&P 2023 publication.
To build and run Owl, you need cabal and ghc in your PATH. You can use ghcup to install them.
Additionally, you need the Z3 Prover installed
and in your PATH; binary releases are here. Owl has been tested with Z3 version 4.12.1.
To build and run, type cabal run owl -- path/to/protocol.owl. For more options, type cabal run owl -- --help.
To compile a protocol to Verus using Owl's secure compiler, use the --extract argument: cabal run owl -- --extract path/to/protocol.owl.
Then, in the extraction/ directory, run ./run_verus.sh $PWD to verify the generated code with Verus.
The run_verus script assumes you have verus and verusfmt
in your PATH.
Add the following to your vimrc:
set runtimepath+=$OWL_HOME/vim
where $OWL_HOME is set accordingly.
See vscode/README.md for details.
Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, & Bryan Parno. (2023). Owl: Compositional Verification of Security Protocols via an Information-Flow Type System.
Footnotes
-
Owl's verifier works in the computational model, in which adversaries are modeled as probabilistic Turing machines operating over bytestrings; this is in contrast to the symbolic model, which abstracts away some details of cryptography to simplify analysis. For more details, see this survey or our S&P 2023 paper. ↩
