Removing hacspec

[geonnave]

The plan is to delete all things related to the hacspec sub-crate.

On the other hand, we are keeping the hacspec-crypto crypto backend, as it both (1) serves as a good software-only alternative crypto backend and (2) can be used to along with the cargo hax into fstar command. Note that to do this, I had to do a "mini-wrapper" of secret integers inside hacspec-crypto. The reason is that all the cryptographic functions in hacspec-crypto expect arrays of secret integers, but our EDHOC implementation has no concept of them anymore. Later, we may want to re-add secret integer handling (in places where it makes sense), but for now let's keep it simple and have it isolated in hacspec-crypto.

[chrysn]

Just for context (for observers such as me who are not deeply involved in the crate's development), does that mean that formal verification is going out, or does some successor to hacspec not need so many hoops any more?

[geonnave]

@chrysn TLDR; it's the second option.

When @malishav started working towards having formal verification of edhoc-rs, hacspec was in v1 and had many restrictions on what Rust constructs could be used. With time, after hacspec-v2 was introduced, support for and more more constructs have been added.

Thus, the current recommendation from the hacspec team is that we write the code in pure Rust, and the hax command should be able to handle it. By "handle it" I mean that cargo hax into fstar will translate edhoc-rs into *.fstar files, which can be used in the formal verification.

That said, some Rust idioms may not yet be supported by hax/hacspec, but in my experience these cases have been usually easy fixes (e.g. use ifs instead of match with @ bindings). In addition, as posted in the first comment, we may later re-add secret integers (U8 and friends) to parts of the code that are relevant to cryptographic operations.

[geonnave]

This is almost there and ready for review, I'm just tweaking the CI step for fstar generation.

[geonnave]

At this point, I've ran out of ideas to fix the fstar step on CI. While there are a few things that we could do on our side (like putting generate_connection_identifier_cbor behind a feature flag), having fstar generation run without any errors depends on fixes from the hacspec side. Maybe we should just comment it out until hax is updated. What do you think @malishav ?

[malishav]

Congrats on this PR, it is massive and simplifies things so much! I just have a small remark regarding the name of the new features. I find cb-{{backend}} a bit obscure. Could you rename the corresponding features to crypto-{{backend}} to be crystal clear what it refers to? Other than that, feel free to merge.

[malishav]

At this point, I've ran out of ideas to fix the fstar step on CI. While there are a few things that we could do on our side (like putting generate_connection_identifier_cbor behind a feature flag), having fstar generation run without any errors depends on fixes from the hacspec side. Maybe we should just comment it out until hax is updated. What do you think @malishav ?

@geonnave: How about we move the F* generation step to be triggered only on releases and we wait for the hacspec team to fix this before releasing a new version?
@W95Psp: do you have any update on the updates needed to get the Rust version to generate F*?

[karthikbhargavan]

We may need to schedule another session for resolving the fstar, say in the third week of October?

…

On Tue, Oct 3, 2023, 18:38 Mališa Vučinić ***@***.***> wrote: At this point, I've ran out of ideas to fix the fstar step on CI. While there are a few things that we could do on our side (like putting generate_connection_identifier_cbor behind a feature flag), having fstar generation run without any errors depends on fixes from the hacspec side. Maybe we should just comment it out until hax is updated. What do you think @malishav <https://github.com/malishav> ? @geonnave <https://github.com/geonnave>: How about we move the F* generation step to be triggered only on releases and we wait for the hacspec team to fix this before releasing a new version? @W95Psp <https://github.com/W95Psp>: do you have any update on the updates needed to get the Rust version to generate F*? — Reply to this email directly, view it on GitHub <#106 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFUVSYIOZAIQVW4ZC64D4DX5Q5P3AVCNFSM6AAAAAA5PN2N62VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONBVGM2DKNZRGM> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[W95Psp]

That looks nice!
Quick report on the Hax point of view:

Skip c_wrapper

We don't want the module c_wrapper to be extracted. The flag -i on the into subcommand of Hax can be used to skip certain items, i.e.:
cargo hax -C -p edhoc-rs -p edhoc-crypto -p edhoc-ead --no-default-features --features='cb-hacspec, ead-none' --release \; into -i '-c_wrapper::**' fstar

Errors I get running that command

1. error[HAX0008]: (reject_RawOrMutPointer) ExplicitRejection: I need to investigate this one, we get no span information.

2. error[HAX0010] (edhoc.rs:849:17): we discussed that, I need to look into it. Issue copy_from_slice on a array is not accepted hacspec/hax#256

3. error[HAX0001]:
   while loops are not supported yet, see while let .. = .. {} hacspec/hax#113
   In general, while loops are not very handy to work with from a proof perspective (i.e. there is no built-in invariant about termination; when you write a for loop over a finite iterator, you get termination for free)

   There is four times that error, but actually that's only two errors (just two slightly different diagnostics each):

   1. edhoc.rs:940:9: why not convert that while loop into a for loop? e.g.

      for i in 0..suites_len {
         if suites[i] <= CBOR_UINT_1BYTE {
             output.content[1 + raw_suites_len] = suites[i];
             raw_suites_len += 1;
         } else {
             output.content[1 + raw_suites_len] = CBOR_UINT_1BYTE;
             output.content[2 + raw_suites_len] = suites[i];
             raw_suites_len += 2;
         }
      }

      instead of:

      let mut i: usize = 0;
      while i < suites_len {
          if suites[i] <= CBOR_UINT_1BYTE {
              output.content[1 + raw_suites_len] = suites[i];
              raw_suites_len += 1;
          } else {
              output.content[1 + raw_suites_len] = CBOR_UINT_1BYTE;
              output.content[2 + raw_suites_len] = suites[i];
              raw_suites_len += 2;
          }
          i += 1;
      }

   2. lib.rs:337:5: here get_random_byte is not pure, we won't able to verify anything that uses that. I think you need something like: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=d84fb15c9531eb195c76ea629932b5cd (I just wrote that quickly, we can chat more about this kind of model later if that's something interesting)

To conclude

• I should investigate 1 and 2.
• I think 3.i should be rewrote into a for loop, and we should chat about 3.2 and determinism.
• the -i flag can help for the CI

[geonnave]

@malishav thanks for the review, did the suggested renaming.

@karthikbhargavan I created a group chat on Zulip so we can coordinate the meeting.

@W95Psp excellent, thanks for the detailed report.

• edhoc.rs: I replaced the while with a for as suggested.
• lib.rs: in fact, we originally intended for this file to be outside the proof, since its main goal is just to provide a developer-friendly wrapper for the core implementation of the protocol. I am playing with the -i flag to try to remove it from the verification.

[W95Psp]

Oh, right! Then, if lib.rs is excluded that's simplifying things indeed, that's great news 🥳
(though we'll have to review the code to make sure there's no seemingly undeterministic calls in the parts we want to extract)

[geonnave]

With the interim change of having the generate-fstar job running only on releases or manual dispatch, all CI tests are passing, and this is now ready to merge.

[chrysn]

Awesome, congrats on getting this through.

I've gathered from following the discussions that there are some style preferences or requirements that are (now that fstar is generated only on releases) not forcibly upheld now, such as a strong no-go for while loops (which is actually nice b/c we don't really need an unbounded Turing machine for EDHOC) and a soft preference against early return. Is there a comprehensive list somewhere that contributors can read up on to avoid?

[geonnave]

Is there a comprehensive list somewhere that contributors can read up on to avoid?

@W95Psp tagging you here, so that we can maybe avoid bothering you too much with hax-compatibility questions in the future 😄