edhoc-hacspec: declassify numbers before return from parse #60

geonnave · 2023-04-21T16:12:33Z

Addressing #49.

malishav

Thanks for hte PR! My main comment/question is whether we can homogenize the code such that declassify does not appear in top-level functions? With the current code, some parts are declassified and some are not, which is not ideal IMO

malishav · 2023-04-24T09:09:47Z

hacspec/out/Edhoc_hacspec.fst

@@ -0,0 +1,1129 @@
+module Edhoc_hacspec


Why is the .fst file part of this PR?

Committed it by mistake... removing.

malishav · 2023-04-24T09:11:16Z

hacspec/src/lib.rs

            // Step 2: verify that the selected cipher suite is supported
-            if supported_suites[0u8].declassify() == EDHOC_SUPPORTED_SUITES[0u8].declassify() {
+            if supported_suites[0] == EDHOC_SUPPORTED_SUITES[0u8].declassify() {


Let's homogenize this so declassify does not appear any more in *_process_message?

malishav · 2023-04-24T09:13:10Z

hacspec/src/lib.rs

@@ -220,7 +220,7 @@ pub fn r_process_message_3(
            let (kid, mac_3) = decode_plaintext_3(&plaintext_3);

            // compare the kid received with the kid expected in id_cred_i
-            if kid.declassify() == id_cred_i_expected[id_cred_i_expected.len() - 1].declassify() {
+            if kid == id_cred_i_expected[id_cred_i_expected.len() - 1].declassify() {


same comment as above

malishav · 2023-04-24T09:13:24Z

hacspec/src/lib.rs

@@ -420,7 +420,7 @@ pub fn i_process_message_2(

        // Check MAC before checking KID
        if mac_2.declassify_eq(&expected_mac_2) {
-            if kid.declassify() == id_cred_r_expected[id_cred_r_expected.len() - 1].declassify() {
+            if kid == id_cred_r_expected[id_cred_r_expected.len() - 1].declassify() {


geonnave · 2023-04-24T09:54:36Z

whether we can homogenize the code such that declassify does not appear in top-level functions? With the current code, some parts are declassified and some are not, which is not ideal IMO

I think it is a good idea to be more homogeneous. Just checking how we would do it:

update EDHOC_SUPPORTED_SUITES to not use secret integers (not sure if this makes sense)
modify id_cred_[ir]_expected to [u8; ID_CRED_LEN], in * _process_message_* (but then I would have to call from_public_slice before passing it to functions such as compute_mac_3.

malishav · 2023-04-24T09:59:36Z

update EDHOC_SUPPORTED_SUITES to not use secret integers (not sure if this makes sense)

Why not? Is it used elsewhere? It seems the cleanest IMO

malishav · 2023-04-24T15:27:50Z

hacspec/src/lib.rs

@@ -899,7 +900,10 @@ fn encode_kdf_context(
    // encode context in line
    // assumes ID_CRED_R and CRED_R are already CBOR-encoded
    let mut output = BytesMaxContextBuffer::new();
-    output = output.update(0, id_cred);
+    for i in 0..id_cred.len() {


why dont you use copy_from_slice here? also, remove the code that is commented out

Oh, I see why.. output is a hacspec type.. nevermind the comment

malishav · 2023-04-24T15:31:15Z

hacspec/src/lib.rs

@@ -1292,7 +1297,7 @@ mod tests {
    fn test_compute_mac_3() {
        let prk_4e3m_tv = BytesHashLen::from_hex(PRK_4E3M_TV);
        let th_3_tv = BytesHashLen::from_hex(TH_3_TV);
-        let id_cred_i_tv = BytesIdCred::from_hex(ID_CRED_I_TV);


why not use ID_CRED_I_TV directly in the call to compute_mac_3 below? i.e. you could remove line 1300

Could you also update it ssimilarly for other occurences, noted with "same comment"

Oh sure, done.

geonnave · 2023-04-25T13:06:15Z

PR should be ready now, just need to be able to check that fstar generation is still working.

malishav · 2023-04-25T13:24:26Z

hacspec/src/lib.rs

@@ -1426,7 +1429,7 @@ mod tests {

    #[test]
    fn test_encode_plaintext_3() {
-        let id_cred_i_tv = BytesIdCred::from_hex(ID_CRED_I_TV);
+        let id_cred_i_tv = ID_CRED_I_TV;


same comment on using ID_CRED_I_TV directly applies

malishav · 2023-04-25T13:24:49Z

hacspec/src/lib.rs

@@ -1345,14 +1348,14 @@ mod tests {
            0,
            PLAINTEXT_2_TV.len() / 2,
        );
-        let id_cred_r_tv = BytesIdCred::from_hex(ID_CRED_R_TV);
+        let id_cred_r_tv = ID_CRED_R_TV;


same comment applies

malishav · 2023-04-25T13:25:09Z

hacspec/src/lib.rs

@@ -1330,7 +1333,7 @@ mod tests {
    #[test]
    fn test_encode_plaintext_2() {
        let plaintext_2_tv = BytesPlaintext2::from_hex(PLAINTEXT_2_TV);
-        let id_cred_r_tv = BytesIdCred::from_hex(ID_CRED_R_TV);
+        let id_cred_r_tv = ID_CRED_R_TV;


same comment

malishav · 2023-04-25T13:25:24Z

hacspec/src/lib.rs

@@ -1310,7 +1313,7 @@ mod tests {
    #[test]
    fn test_compute_and_verify_mac_2() {
        let prk_3e2m_tv = BytesHashLen::from_hex(PRK_3E2M_TV);
-        let id_cred_r_tv = BytesIdCred::from_hex(ID_CRED_R_TV);
+        let id_cred_r_tv = ID_CRED_R_TV;


same comment

malishav · 2023-04-25T13:26:04Z

hacspec/src/lib.rs

@@ -1292,7 +1297,7 @@ mod tests {
    fn test_compute_mac_3() {
        let prk_4e3m_tv = BytesHashLen::from_hex(PRK_4E3M_TV);
        let th_3_tv = BytesHashLen::from_hex(TH_3_TV);
-        let id_cred_i_tv = BytesIdCred::from_hex(ID_CRED_I_TV);


Could you also update it ssimilarly for other occurences, noted with "same comment"

geonnave · 2023-04-26T08:37:52Z

Still needed: test fstar generation after type changes.
Obstacle: cargo circus not working in my personal computer.
Solution: wait for a fix from the hacspec team, or go to Inria run the tests (maybe tomorrow).

geonnave · 2023-10-04T09:11:44Z

After the merge of #105 this is not applicable anymore.

geonnave mentioned this pull request Apr 21, 2023

Declassify numbers before returning from the parsing routine #49

Closed

malishav reviewed Apr 24, 2023

View reviewed changes

edhoc-hacspec: declassify numbers before return from parse

caea2ad

geonnave force-pushed the declassify_numbers_in_parse_routine branch from 2675302 to caea2ad Compare April 24, 2023 09:21

geonnave added 4 commits April 24, 2023 16:04

hacspec: change some values to u8 arrays

2eb6e5e

Merge branch 'main' into declassify_numbers_in_parse_routine

b414a84

fix: adjust after conflict merge

c25d365

hacspec: make BytesIdCred a regular u8 array

c451ab0

malishav reviewed Apr 24, 2023

View reviewed changes

geonnave added enhancement New feature or request cleanup and removed enhancement New feature or request labels Apr 25, 2023

malishav reviewed Apr 25, 2023

View reviewed changes

hacspec: remove unused variables

838baf6

geonnave force-pushed the declassify_numbers_in_parse_routine branch from b393e38 to 838baf6 Compare April 25, 2023 13:32

geonnave added the depends-on-third-party label May 11, 2023

geonnave closed this Oct 4, 2023

geonnave deleted the declassify_numbers_in_parse_routine branch November 23, 2023 09:19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

edhoc-hacspec: declassify numbers before return from parse #60

edhoc-hacspec: declassify numbers before return from parse #60

geonnave commented Apr 21, 2023

malishav left a comment

malishav Apr 24, 2023

geonnave Apr 24, 2023

malishav Apr 24, 2023

malishav Apr 24, 2023

malishav Apr 24, 2023

geonnave commented Apr 24, 2023

malishav commented Apr 24, 2023

malishav Apr 24, 2023

malishav Apr 24, 2023

geonnave Apr 25, 2023

malishav Apr 24, 2023

geonnave Apr 25, 2023

malishav Apr 25, 2023

geonnave Apr 25, 2023

geonnave commented Apr 25, 2023 •

edited

Loading

malishav Apr 25, 2023

malishav Apr 25, 2023

malishav Apr 25, 2023

malishav Apr 25, 2023

malishav Apr 25, 2023

geonnave commented Apr 26, 2023

geonnave commented Oct 4, 2023

edhoc-hacspec: declassify numbers before return from parse #60

edhoc-hacspec: declassify numbers before return from parse #60

Conversation

geonnave commented Apr 21, 2023

malishav left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

geonnave commented Apr 24, 2023

malishav commented Apr 24, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

geonnave commented Apr 25, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

geonnave commented Apr 26, 2023

geonnave commented Oct 4, 2023

geonnave commented Apr 25, 2023 •

edited

Loading