Closed chrysn closed 9 months ago
I think the proposed change is beneficial, give me one more day and I will report back on the state of the hacspec cleaning.
This is targeting remove-hacspec now, given that that's the way forward and much easier with this PR -- every change made against main would need manual rebasing after #106 is merged anyway. I'm having trouble building locally with the remove-hacspec branch so far (from psa-crypto-sys); until I've managed to resolve that, I may be a bit force-pushy while I iron out bugs CI finds.
Applying this to all the remaining hex parts, I think I'm done, except that I have questions / notes:
Responding to some comments:
I'm having trouble building locally with the remove-hacspec branch so far (from psa-crypto-sys)
Just to make sure, this is how I call it as of today in the remove-hacspec
branch: cargo test --package edhoc-rs --package edhoc-crypto --package edhoc-ead --no-default-features --features="cb-psa, ead-none" --no-fail-fast
.
You could also try cb-hacspec
instead.
There is trouble with f-star generation. Could you help me out here?
Don't worry about it, we will likely skip this test from CI until the hacspec side is adjusted.
@chrysn remove-hacspec
has been merged, targeting main
should be fine now :)
Way ahead of y... oh, that comment came in 4 minutes before I rebased, so things all have their proper sequence :-)
I've also given converting the CRED_x buffers into slices a try; that leaves only comments with on likely need for change from my side. It works in the first tests, but the big question is whether there is anything hax doesn't like about it.
(And the build issues, but that's a combination of "I don't have the right PSA sources installed" and "some examples don't respect the crypto- features and pull in PSA crypto unconditionally", which I think I can address separately).
Regarding the compilation for PSA, I've easily made it work on Ubuntu but not on MacOS. As a result, when I'm on the Mac, I cargo test
it within a multipass
Ubuntu VM.
The changes look great! Some notes:
I don't know if I got it right but should it be updated as follows?
Use
static const uint8_t ID_CRED_I[] = {0xa1, ... };
Instead of
static const uint8_t ID_CRED_I[] = "a104412b";
@W95Psp could you give a quick look? Here's one example of the kind of change we're looking at:
fn compute_mac_2(
prk_3e2m: &BytesHashLen,
id_cred_r: &BytesIdCred,
cred_r: &[u8], // <--- this type changed from `&BytesMaxBuffer` (note that `type BytesMaxBuffer = [u8; MAX_BUFFER_LEN]`)
th_2: &BytesHashLen,
) -> BytesMac2 {
Good catch on the C side; fixed. (That's why I like statically typed languages :-D).
Looks good to me! The only unknown is the use of &[u8]
with hax
, but since hax
only targets lib/src/lib.rs
, that means only cred_X
are impacted, which would be easy to modify if needed.
This first commit only changes the
i
part of the EdhocInitiator for review.Apart from the obvious API break, the weirdest part here is the classify loop. @geonnave, how would I best sequence this against your pending changes that remove the hacspec arrays? Is there a branch I can build this on, should I hold it off for a few days, or should I just wrap the classify loop in a one-shot compatibility wrapper that doesn't need to be pretty, is used for all the conversions where the un-hexification conveniently hid the classify before, and wait for it to be removed later?
Contributes-to: https://github.com/openwsn-berkeley/edhoc-rs/issues/99