"Crypto as trait" experiments #103

chrysn · 2023-09-29T19:32:17Z

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 · 2023-09-29T20:54:48Z

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 · 2023-10-04T09:01:58Z

Hacspec simplifications merged on main!

chrysn · 2023-10-07T15:42:32Z

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.

This is incomplete in two aspects: * it only adjusts the hacspec and psa crypto backends, and * it still goes through the edhoc-crypto crate to create import-based dispatch. It also does not do a full cargo-fmt, because this allows the delta of this commit to be small.

chrysn · 2023-10-08T08:46:40Z

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 · 2023-10-08T10:57:43Z

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.

This is likely not a final version, as it is terribly verbose. The verbosity would be mitigated if the functions were methods of their states, as then, it would be concentrated atop the impl blocks. It is also incomplete in that it merely shifts the cfg-switched Crypto implementation from being referenced in edhdoc.rs to being referenced in lib.rs, instead of making the latter generic as well.

This is deferred from the previous commit to maintain its "minimality"

chrysn · 2023-10-08T18:45:10Z

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 · 2023-10-09T11:46:14Z

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 · 2023-10-09T13:06:52Z

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 · 2023-10-09T13:07:27Z

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 · 2023-10-09T13:13:03Z

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 · 2023-10-09T13:14:20Z

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 · 2023-10-09T13:17:12Z

CC @W95Psp to clarify

W95Psp · 2023-10-10T07:13:21Z

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 👍

chrysn · 2023-10-10T11:37:04Z

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).

…from crypto independent

chrysn · 2023-10-11T08:21:41Z

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 · 2023-10-11T09:53:31Z

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.

malishav

Thanks for providing this PR! Two comments:

do we still need the intermediate crypto crate? i.e. can we merge the crypto crate with edhoc-crypto-trait crate?
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.

malishav · 2023-10-11T08:54:39Z

crypto/src/lib.rs

@@ -1,13 +1,49 @@
+//! Cryptography dispatch for the edhoc-rs crate


Can this file be merged with crypto/edhoc-crypto-trait/src/lib.rs?

It can't: The whole point of crypto-trait is that it will not depend on any concrete back-ends.

Eventually this should only be needed for things like tests where you want to switch around back-ends by the flick of a feature (as it makes for easy test matrices). It may make sense to rename that crate to edhoc-crypto-preferred-impl -- but that crate would not make it to crates.io as long as it depends on a wide variety of not-on-crates optional dependencies.

malishav · 2023-10-11T08:55:24Z

crypto/src/lib.rs

-pub use edhoc_crypto_cryptocell310::*;
+pub type Crypto = edhoc_crypto_cryptocell310::Crypto;
+
+#[cfg(any(feature = "cryptocell310", feature = "cryptocell310-rust"))]


cryptocell310-rust does not exist any more, feel free to remove.

and same for psa-rust

malishav · 2023-10-11T08:57:21Z

lib/Cargo.toml

@@ -12,6 +12,7 @@ hex = { version = "0.4.3", default-features = false }

 hacspec-lib = { version = "0.1.0-beta.1", default-features = false, optional = true }
 edhoc-crypto = { path = "../crypto", default-features = false }
+edhoc-crypto-trait = { path = "../crypto/edhoc-crypto-trait" }


If edhoc-crypto-trait and edhoc-crypto were merged, this line should go away.

This line can only go away when the tests are moved out -- only then will lib work without depending on any concrete implementation.

chrysn · 2023-10-11T15:51:38Z

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.

This commit is not formatted to increase its readability.

This mostly changes the indentation of functions that moved from pure function to provided impls of a trait.

chrysn · 2023-11-09T20:04:41Z

This has been replaced by #127 whcih is now merged.

chrysn force-pushed the crypto-as-trait-experiments branch from 10fd043 to b965b4b Compare September 29, 2023 21:27

chrysn mentioned this pull request Oct 7, 2023

Enable publication at crates.io #98

Closed

2 tasks

chrysn force-pushed the crypto-as-trait-experiments branch 3 times, most recently from 86a429a to 0c14e76 Compare October 7, 2023 14:57

chrysn added 2 commits October 8, 2023 10:46

chore: cargo fmt

82d40fe

refactor: Use explicit imports now that they're few

717abb1

chrysn added 2 commits October 8, 2023 20:36

chore: cargo fmt

2685ffd

This is deferred from the previous commit to maintain its "minimality"

chrysn force-pushed the crypto-as-trait-experiments branch from 0b51c40 to 2685ffd Compare October 8, 2023 18:41

geonnave mentioned this pull request Oct 9, 2023

copy_from_slice on a array is not accepted hacspec/hax#256

Closed

geonnave added the new feature label Oct 9, 2023

refactor: Shuffle sequence of functions to separate crypto dependent …

8d278a7

…from crypto independent

chrysn marked this pull request as ready for review October 11, 2023 08:07

malishav reviewed Oct 11, 2023

View reviewed changes

chrysn mentioned this pull request Oct 11, 2023

Stateful initialization of crypto backends #94

Open

chrysn added 2 commits November 4, 2023 14:47

refactor!: Pass crypto implementation around as an argument

84e9d24

This commit is not formatted to increase its readability.

chore: cargo fmt

3e9b45d

This mostly changes the indentation of functions that moved from pure function to provided impls of a trait.

chrysn force-pushed the crypto-as-trait-experiments branch from c93f352 to 3e9b45d Compare November 4, 2023 13:48

chrysn mentioned this pull request Nov 5, 2023

refactor!: Move crypto operations into a trait. #127

Merged

chrysn closed this Nov 9, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

"Crypto as trait" experiments #103

"Crypto as trait" experiments #103

chrysn commented Sep 29, 2023

chrysn commented Sep 29, 2023

geonnave commented Oct 4, 2023

chrysn commented Oct 7, 2023

chrysn commented Oct 8, 2023

malishav commented Oct 8, 2023

chrysn commented Oct 8, 2023

geonnave commented Oct 9, 2023 •

edited

Loading

malishav commented Oct 9, 2023

chrysn commented Oct 9, 2023

malishav commented Oct 9, 2023

chrysn commented Oct 9, 2023

malishav commented Oct 9, 2023

W95Psp commented Oct 10, 2023

chrysn commented Oct 10, 2023 via email

chrysn commented Oct 11, 2023

geonnave commented Oct 11, 2023 •

edited

Loading

malishav left a comment

malishav Oct 11, 2023

chrysn Oct 11, 2023

malishav Oct 11, 2023

geonnave Oct 12, 2023

malishav Oct 11, 2023

chrysn Oct 11, 2023

chrysn commented Oct 11, 2023

chrysn commented Nov 9, 2023

		@@ -1,13 +1,49 @@
		//! Cryptography dispatch for the edhoc-rs crate

"Crypto as trait" experiments #103

"Crypto as trait" experiments #103

Conversation

chrysn commented Sep 29, 2023

chrysn commented Sep 29, 2023

geonnave commented Oct 4, 2023

chrysn commented Oct 7, 2023

chrysn commented Oct 8, 2023

malishav commented Oct 8, 2023

chrysn commented Oct 8, 2023

geonnave commented Oct 9, 2023 • edited Loading

malishav commented Oct 9, 2023

chrysn commented Oct 9, 2023

malishav commented Oct 9, 2023

chrysn commented Oct 9, 2023

malishav commented Oct 9, 2023

W95Psp commented Oct 10, 2023

chrysn commented Oct 10, 2023 via email

chrysn commented Oct 11, 2023

geonnave commented Oct 11, 2023 • edited Loading

malishav left a comment

Choose a reason for hiding this comment

malishav Oct 11, 2023

Choose a reason for hiding this comment

chrysn Oct 11, 2023

Choose a reason for hiding this comment

malishav Oct 11, 2023

Choose a reason for hiding this comment

geonnave Oct 12, 2023

Choose a reason for hiding this comment

malishav Oct 11, 2023

Choose a reason for hiding this comment

chrysn Oct 11, 2023

Choose a reason for hiding this comment

chrysn commented Oct 11, 2023

chrysn commented Nov 9, 2023

geonnave commented Oct 9, 2023 •

edited

Loading

geonnave commented Oct 11, 2023 •

edited

Loading