"Crypto as trait" experiments

[chrysn]

In this PR I'm experimenting with making the edhoc-crypto module not re-export items from different crates (whose interface is implicitly defined by the shared pub items), but define a type (ideally as impl Trait, but until TAIT is stable, as public reexports) that is accessed through a defined trait interface.

Apart from cleaner separation of responsibilities, the longer goal here is to remove the need for one central and depending-on-everyone-depending-on-cfg edhoc-crypto crate, and to replace it with generics on the public structs and functions. While that could be used to run different back-ends in parallel (not sure why one would want that), its main goal is to sever the dependency from the library to the back-ends, making the library both easier to maintain and easier to upload to crates.io (#98). It'd then be up to the application to select its back-end, and propagate that through any intermediate crates that build on edhoc (which now don't have to pass on features any more, but can pass on types, which is also easier to maintain).

The first commit (after the ones from #102 that restore CI) only does this for hacspec -- this was tested locally, and I'm relying on CI to tell me where else changes are needed (while I'm still getting my bearings around the library).

[chrysn]

This is currently running into a situation where get_random_byte is U8 in hacspec cases and u8 in others. While this could be resolved with associated types and whatnot, I guess this best waits for @geonnave's hacspec simplifications.

[geonnave]

Hacspec simplifications merged on main!

[chrysn]

Rebased onto main, and is also much simpler now. Some back-ends still need to be updated, but that's mainly a formality. So far I don't expect any trouble with hacspec; the real test will come when edhoc.rs functions will suddenly start being edhoc_exporter<C: Crypto>(...), or (maybe more ergonomically) the state will take a Crypto generic argument.

[chrysn]

From CI not complaining about me having slumped around cc2538, I take it that platform is already on its way out? (Ignoring it for here unless it makes CI fail or I hear otherwise from you).

[malishav]

From CI not complaining about me having slumped around cc2538, I take it that platform is already on its way out? (Ignoring it for here unless it makes CI fail or I hear otherwise from you).

Yeah, you can safely ignore cc2538 for now.

[chrysn]

The latest changeset also contains first steps toward being generic over the crypto backend.

This is incredibly verbose because it is all standalone functions and not impls on a struct (where more typing would be grouped into one line). May make sense to pursue this if typestating goes ahead inside edhoc.rs.

In parallel, it'd be worth considering whether to pass it as a type or a (usually ZST) instance of a type -- adding an argument for the Crypto backend would also help with the verbosity. I'd like that because it'd mean that, say, on platforms like PSA that AIU need some initialization, you can't pass an instance into EDHOC without having initialized it first. (But that's probably best explored when the code is in a more impl-block style).

[geonnave]

This is looking great, and the CI passes! Also I tested with hax in this branch and there are no new errors, which is a good sign.

[malishav]

In parallel, it'd be worth considering whether to pass it as a type or a (usually ZST) instance of a type -- adding an argument for the Crypto backend would also help with the verbosity. I'd like that because it'd mean that, say, on platforms like PSA that AIU need some initialization, you can't pass an instance into EDHOC without having initialized it first. (But that's probably best explored when the code is in a more impl-block style).

Note that a big no-no in hacspec is any usage of mutable references. In fact, on a more historical note, we went a full circle: from the Crypto backend implemented as a Trait to the current state, and are now going back. Let's just make sure it is compatible with hax in order to merge this.

Also I tested with hax in this branch and there are no new errors, which is a good sign.

I had a brief chat with @W95Psp who indicated traits and generics are now supported.

[chrysn]

I'm curious: What is hax's entry point? If it previously tried to prove any properties of a sequence of r_parse_message_1 & co, those symbols are now gone (replaced with more generic symbols, and not monomorphized inside edhoc.rs). I've looked at the CI scripts (BTW, building that Dockerfile once and reusing it should speed this up a lot), but I'd guess that the actual verification happens from the fstar artifact, and is not done as part of CI.

[malishav]

The CI just translates the Rust code into fstar. So yes, the actual verification happens once the fstar artifact is generated, and is, for now, a manual process.

[chrysn]

Note that a big no-no in hacspec is any usage of mutable references.

Here's a relevant question then: How about

fn f<T: SomeTrait>(&mut T, ...)

when we (only for hacspec) limit this to T = &SomeType? Is that, from hacspec's point of view, mutable or not?

Background: If we make the "crypto engine" an instance, that'd be a ZST that's creatable out of thin air for any software implementation, and thus is Clone, Copy, Send, Sync and what-so-not), but a HW crypto engine would either be busy-polling for the engine to be free, or use some OS's synchronization primitives (bye bye portability), or would be instanciated into a single ZST (or maybe pointer sized type to carry its hardware base addess), and by means of being an exclusive reference (pedants don't call &mut a mutable reference, but an exclusive one) ensures serialization of all operations on it.

[malishav]

CC @W95Psp to clarify

[W95Psp]

To clarify about mutable references: they are forbidden everywhere but on function inputs. Basically, we forbid:

• aliasing (i.e. let y: &mut T = x;),
• &mut T in return position. On function inputs, mutable references actually implement state-passing: fn f(x: &mut T) -> U is understood by Hax (new name of hacspec) as fn f(x: T) -> (U, T).

So @chrysn, defining such a fn f<T: SomeTrait>(&mut T, ...) is completely fine! And indeed, as you state it @chrysn , &mut is great for imposing a linear discipline on resources, not only for mutation :+1:

[chrysn]

Thanks, that's good news. So we can have a Crypto usable through &mut, passed it that way into the low-level functions, and high-level structs can own a Crypto -- for the time being (with an option to have a storage form that outlives its Crypto to be added if ever a Crypto is not Clone and 'static).

[chrysn]

To keep things managable I've marked this as ready-for-review -- I think that this is now standalone enough for review at the lower layers.

Next steps would be pulling an implementation of Crypto into the high-level state. This has ergonomics downsides -- constructing a new EDHOC state now requires passing in the chosen crypto, and, IMO worse, helper functions such as generate_connection_identifier_cbor need it passed in as well. It's tempting to provide helpers that just resort to providing constructors with the default crypto, but then, we have the (optional but crates.io doesn't care) dependency back to all the implementations once more. A bit worse (aka "I don't know what's the best solution yet"), the tricks around #114 for temporarily taking out an owned State from a &mut State won't work unless the Crypto is Clone (which I'd generally hope to avoid requiring, plus we don't "really" need it there).

Proposed way forward: Please give me a rough round of feedback on this one -- not for merging but just for the direction. If that's OK, I'd tackle pulling it through the rest (lib, c_wrappers, examples) so we can decide whether we're happy with the resulting API. In that stage, the current edhoc_crypto module would only be depended on by examples and test code. If we then move those tests out of the edhoc-rs crate, or by that time have one published crypto implementation instead on which the tests could depend directly, that'd make #98 (publication of edhoc-rs at crates.io) possible.

[geonnave]

Thanks for the update @chrysn, I gave it a look, and one advantage that I see is that with this new approach, we should be able to implement stateful initialization of crypto backends (#94) by adding the needed state fields to pub struct Crypto.

[chrysn]

It would be great if the trait would include an init() function. Feel free to leave it empty for now on all backends and we can populate it in follow-up PRs.

I don't think that should be part of the trait, because its signature is not constant: For hacspec or any software impl, it'd be fn init() -> Crypto. For #94, it'd be unsafe fn init() -> Crypto. For anything building on the MCU's peripherals through the device's pac crate, it'd be fn init(periph: CryptoPeripheral) -> Crypto. So it can't be part of the trait, and the trait can't just depend on Default, as that doesn't work for all possible back-ends.

But the comments that are coming in are high-level enough that I can look into threading this through the rest, because this will give a better view of how it'd be applied in the end.

[chrysn]

This has been replaced by https://github.com/openwsn-berkeley/edhoc-rs/pull/127 whcih is now merged.