fixup! Add specs for XMSS signature verification

GaloisInc · Feb 12, 2025 · 76afaf0 · 76afaf0
1 parent 0e31dbc
commit 76afaf0
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 8 deletions.
diff --git a/components/platform_crypto/shave_trusted_boot/firmware.c b/components/platform_crypto/shave_trusted_boot/firmware.c
@@ -36,12 +36,12 @@ static bool xmss_verify_signature(XmssPublicKey *exported_public_key, uint8_t *m
 /*$
   requires
     take epki = Owned<XmssPublicKey>(exported_public_key);
-    take mi = Array_u8(msg, msg_size);
+    take mi = ArrayOwned_u8(msg, msg_size);
     take sbi = XmssSignatureBlobP(signature_blob);
 
   ensures
     take epko = Owned<XmssPublicKey>(exported_public_key);
-    take mo = Array_u8(msg, msg_size);
+    take mo = ArrayOwned_u8(msg, msg_size);
     take sbo = XmssSignatureBlobP(signature_blob);
     sbi.data_size == sbo.data_size;
 $*/

diff --git a/components/platform_crypto/shave_trusted_boot/xmss-library/include/signing.h b/components/platform_crypto/shave_trusted_boot/xmss-library/include/signing.h
@@ -251,7 +251,7 @@ XmssError xmss_generate_private_key(XmssKeyContext **key_context, XmssPrivateKey
     // key_usage
     take sri = Owned<XmssBuffer>(secure_random);
     sri.data_size == 96u64;
-    take sridata = Array_u8(sri.data, sri.data_size);
+    take sridata = ArrayOwned_u8(sri.data, sri.data_size);
     index_obfuscation_setting == (u32)XMSS_INDEX_OBFUSCATION_OFF;
     //random,
     take cxti = Owned<XmssSigningContext>(context);
@@ -266,7 +266,7 @@ XmssError xmss_generate_private_key(XmssKeyContext **key_context, XmssPrivateKey
     //key usage
     take sro = Owned<XmssBuffer>(secure_random);
     sro.data_size == 96u64;
-    take srodata = Array_u8(sro.data, sro.data_size);
+    take srodata = ArrayOwned_u8(sro.data, sro.data_size);
     //random,
     take cxto = Owned<XmssSigningContext>(context);
     return == (u32)XMSS_OKAY;

diff --git a/components/platform_crypto/shave_trusted_boot/xmss-library/include/structures.h b/components/platform_crypto/shave_trusted_boot/xmss-library/include/structures.h
@@ -216,7 +216,7 @@ predicate (struct XmssSignatureBlob) XmssSignatureBlobP(pointer p)
 {
   take sz = Owned<size_t>(member_shift<XmssSignatureBlob>(p, data_size));
   assert(sz >= 0u64);
-  take cont = Array_u8(member_shift<XmssSignatureBlob>(p, data), sz);
+  take cont = ArrayOwned_u8(member_shift<XmssSignatureBlob>(p, data), sz);
   return struct XmssSignatureBlob {data_size : sz, data : cont};
 }
 $*/

diff --git a/components/platform_crypto/shave_trusted_boot/xmss-library/include/types.h b/components/platform_crypto/shave_trusted_boot/xmss-library/include/types.h
@@ -337,7 +337,7 @@ typedef struct XmssBuffer {
 predicate (map<u64, u8>) AnXmssBuffer (pointer p)
 {
   take b = Owned<XmssBuffer>(p);
-  take dat = Array_u8(b.data, b.data_size);
+  take dat = ArrayOwned_u8(b.data, b.data_size);
   return dat;
 }
 $*/

diff --git a/components/platform_crypto/shave_trusted_boot/xmss-library/include/verification.h b/components/platform_crypto/shave_trusted_boot/xmss-library/include/verification.h
@@ -89,11 +89,11 @@ spec xmss_verification_update(pointer context, pointer part, u64 part_length,
     pointer part_verify);
 requires
   take ci = Owned<XmssVerificationContext>(context);
-  take pi = Array_u8(part, part_length);
+  take pi = ArrayOwned_u8(part, part_length);
   take pvi = Block<uint8_t*>(part_verify); // TODO make this optional
 ensures
   take co = Owned<XmssVerificationContext>(context);
-  take po = Array_u8(part, part_length);
+  take po = ArrayOwned_u8(part, part_length);
   take pvo = Owned<uint8_t*>(part_verify); // TODO make this optional
   !addr_eq(pvo, part) || (ptr_eq(pvo, part));
 $*/