Design Doc: Defining crypto primitives in Owl

Goal

Have a way of specifying in the .owl file itself what cryptographic primitives/ciphers to use, so that (e.g.) we can use both AES and ChaCha in the same protocol.

Considerations

• The typechecker needs to know about the primitive choices, so it can check that you don't use an AES key for ChaCha or similar. In future we may want to have a way to specify how to typecheck a certain crypto call in the Owl file itself.
• The choice of cipher will influence the behavior of various functions and length constants in the typechecker. For example, |enckey| now needs to be |enckey[AES]| or similar, and cipherlen(...) should be cipherlen[AES](...).
• Both name declarations and crypto calls should be annotated with what primitive they are using. For extraction, the name declaration should be annotated so that it knows what length to use, while the call should be annotated because using a different crypto routine means calling a different Rust function.
• We want a clean syntax to connect the Owl crypto primitives to the desired Rust implementations, accounting for any Rust-level type conversions that may be required (e.g., the routine wants a &[u8] but we have a Vec<u8>).
• We want to use this mechanism to specify crypto-related implementation details such as nonce patterns, since those are relevant for extraction and logically associated with the choice of cryptographic primitive.

Syntax

Names, counters, and crypto primitives will be annotated with a string defining a cryptographic scheme, as follows:

name k1 : enckey[AES] @ alice

name k2 : st_aead[ChaCha] (...)
  nonce ...
  aad ...
  @ alice
  
counter[ChaCha] N @ alice

def foo(...) : ... @ alice =
  ...
  let c1 = aenc[AES](get(k1), msg1) in
  let c2 = st_aead_enc[ChaCha]<N>(get(k2), msg2, 0xAEAD) in
  ...

TODO[Josh]: we might need some syntax for declaring these crypto annotations. We could probably just have something like:

crypto_family AES

or some other keyword. Or I guess it is fine to just have an uninterpreted string.

Typechecking

The typechecker should check that the crypto annotations match whenever it performs a crypto routine. For example, if we had:

name k1 : enckey[AES] @ alice

def foo(...) : ... @ alice =
  let c = aenc[ChaCha](get(k1), msg) in ...

the typechecker should complain that the aenc is using the wrong cipher type.

The typechecker should also generate different length constants for each cipher type and name kind. Alternatively we could leave this check to extraction, but ergonomically it seems better for the typechecker to tell you if you are doing something weird with lengths.

TODO: Do we need a way to specify that only some primitives can be used with each annotation? For example, it doesn't make sense to have pkenc[AES] or aenc[RSA] or similar.

Extraction

Extracting these routines is more complex. Currently, each crypto operation has a hardcoded wrapper function (in execlib.rs), marked #[verifier(external_body)], which calls into the appropriate RustCrypto library function. The spec of each wrapper function points to a corresponding spec function (in speclib.rs), which is treated essentially as an uninterpreted symbol. The spec itree calls the spec functions.

To allow for Owl-developer-defined crypto primitives, we need some way of connecting them to a desired implementation. We don't want the Owl developer to be including Rust snippets in the Owl file, or to be doing weird metaprogramming of the extraction. The simplest solution seems to be as follows.

For each crypto primitive and algorithm choice that we use, we have a directive like the following:

#extract {
    aenc[AES](k, m) -> evercrypt_rs::aes_encrypt(m as &mut [u8], k as &[u8]) -> Vec<u8>
}

This tells extraction that whenever it sees a call to aenc[AES], it should use evercrypt_rs::aes_encrypt as the implementation of that. Note the bindings of k and m: these allow the extraction to account for possibly differing argument order conventions between Owl and the underlying library. The type annotations m as &mut [u8] etc are so that extraction can insert the right type conversions to call into the function; the existing type-tracking machinery should be able to handle this, assuming that the specified Rust types are among those that we track.

Upon seeing the declaration above, extraction should produce:

#[verifier(external_body)]
spec fn owl_spec_evercrypt_rs_aes_encrypt(m: Seq<u8>, k: Seq<u8>) -> Seq<u8>
{ unimplemented!() }

#[verifier(external_body)]
exec fn owl_evercrypt_rs_aes_encrypt(m: &mut [u8], k: &[u8]) -> (res: Vec<u8>)
    ensures res.view() == owl_spec_evercrypt_rs_aes_encrypt(m.view(), k.view())
{ 
    evercrypt_rs::aes_encrypt(m, k) 
}

or similar. Then, when a call to aenc[AES](k,m) appears, we would extract it to:

owl_evercrypt_rs_aes_encrypt(&mut m[..], &k[..])

or whatever type conversion is required for the current types of k and m.

The path evercrypt_rs::aes_encrypt should be an unambiguous, globally valid path, assuming the crate evercrypt_rs is imported in the Cargo.toml of the output crate. We can include some set of libraries, like evercrypt_rs, RustCrypto, and ring (the BoringSSL library), by default for Owl developers to use; they are then free to add more if they see fit.

Name kind declarations should also have extraction directives to specify their lengths and formats, as follows:

#extract {
    enckey[AES] -> bytes[32]
}

Counter kinds can probably always be treated as u64 or usize---see below for how the nonce patterns are handled.

TODO: We might need other formatting restrictions on name kinds besides just length annotations? For example, some elliptic curve schemes have other requirements besides just length. How do we encode these?

During parsing, the Owl typechecker should just ignore everything within the curly braces of the #extract directive, passing them along as a string to extraction. Extraction can then parse these directives to generate its internal data structures specifying how to handle the built-in functions of Owl. Once all of the extraction directives have been parsed, extraction can proceed to handling the data structure and name declarations, then the procedure definitions.

Extraction should complain if it finds a crypto call for which no extraction directive has been given. This preserves the possibility to use just the Owl typechecker without any extraction features as a modeling tool, but makes sure that every implementation is fully specified in order to be compliant with an RFC.

Counters and nonce patterns

In Wireguard, the nonce pattern for stateful AEAD is as follows. Given a 64-bit (8-byte) integer counter, it is converted to a 12-byte ChaCha nonce by converting to little-endian, then prepending 4 bytes of zeros.

This should be an implementation detail of the cipher suite, not specified in Owl. It would be messy to add syntax in Owl for this kind of manipulation. Therefore, we want to be able to have:

#extract {
    st_aead_enc[Wireguard_AEAD]<counter>(key, plaintext, aad) ->
    owl_wireguard_crypto_lib::aead_encrypt(key as &[u8], plaintext as &[u8], nonce as usize, aad as [u8]) -> Vec<u8>
}

The path owl_wireguard_crypto_lib is intended to refer to some local module in the current crate, defined in a file owl_wireguard_crypto_lib.rs. Within that file, the developer would write their own function aead_encrypt which contains the logic of:

let mut iv = vec![0u8; 12];
iv[4..12].copy_from_slice(nonce.to_le_bytes());

or whatever nonce pattern is required. The developer would not add Verus specs to this file, since the compiler would generate the wrapper as above.

Ergonomics (for future)

Eventually, we may want the extraction directives to appear in a separate file, and include it by linking. We could provide a sort of "standard library" of extraction directives for common crypto routines. There is already support for linking, so maybe this would not be too hard.

In future, we might want some way of defining the typechecking procedure for each crypto routine---in this case, aenc would no longer be a hardcoded keyword of the Owl typechecker, but some user-defined kind of crypto routine. A similar #typecheck directive could be used here.