Skip to content

Commit 6776884

Browse files
mkannwischermkannwischer
committed
HOL-Light/x86_64: Add constant-time proofs for compression functions
Add subroutine-level constant-time proofs for poly_compress_d{4,5,10,11}. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
1 parent 1d4054c commit 6776884

5 files changed

Lines changed: 481 additions & 0 deletions

File tree

‎proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d10.ml‎

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -945,3 +945,105 @@ let MLKEM_POLY_COMPRESS_D10_SUBROUTINE_CORRECT = prove(
945945
MAYCHANGE [memory :> bytes(r, 320)])`,
946946
MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLY_COMPRESS_D10_NOIBT_SUBROUTINE_CORRECT));;
947947

948+
(* ------------------------------------------------------------------------- *)
949+
(* Constant-time and memory safety proof. *)
950+
(* ------------------------------------------------------------------------- *)
951+
952+
needs "x86_64/proofs/mlkem_utils.ml";;
953+
needs "x86_64/proofs/subroutine_signatures.ml";;
954+
955+
let full_spec,public_vars = mk_safety_spec
956+
~keep_maychanges:true
957+
(assoc "mlkem_poly_compress_d10" subroutine_signatures)
958+
MLKEM_POLY_COMPRESS_D10_CORRECT
959+
MLKEM_POLY_COMPRESS_D10_TMC_EXEC;;
960+
961+
let MLKEM_POLY_COMPRESS_D10_SAFE = time prove
962+
(`exists f_events.
963+
forall e r a data (inlist:(16 word) list) pc.
964+
LENGTH inlist = 256 /\
965+
aligned 32 a /\
966+
aligned 32 data /\
967+
ALL (nonoverlapping (r,320))
968+
[word pc,LENGTH mlkem_poly_compress_d10_tmc; a,512; data,32]
969+
==> ensures x86
970+
(\s.
971+
bytes_loaded s (word pc)
972+
(BUTLAST mlkem_poly_compress_d10_tmc) /\
973+
read RIP s = word pc /\
974+
C_ARGUMENTS [r; a; data] s /\
975+
read events s = e)
976+
(\s.
977+
read RIP s = word (pc + MLKEM_POLY_COMPRESS_D10_CORE_END) /\
978+
(exists e2.
979+
read events s = APPEND e2 e /\
980+
e2 = f_events a data r pc /\
981+
memaccess_inbounds e2
982+
[a,512; data,32; r,320] [r,320]))
983+
(MAYCHANGE [events] ,,
984+
MAYCHANGE [memory :> bytes (r,320)] ,,
985+
MAYCHANGE [RIP] ,,
986+
MAYCHANGE [RAX] ,,
987+
MAYCHANGE [ZMM0; ZMM1; ZMM2; ZMM3; ZMM4; ZMM5; ZMM6; ZMM7; ZMM8; ZMM9; ZMM10])`,
988+
ASSERT_CONCL_TAC full_spec THEN
989+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
990+
PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars
991+
MLKEM_POLY_COMPRESS_D10_TMC_EXEC);;
992+
993+
let MLKEM_POLY_COMPRESS_D10_NOIBT_SUBROUTINE_SAFE = time prove
994+
(`exists f_events.
995+
forall e r a data (inlist:(16 word) list) pc stackpointer returnaddress.
996+
LENGTH inlist = 256 /\
997+
aligned 32 a /\
998+
aligned 32 data /\
999+
ALL (nonoverlapping (r,320))
1000+
[word pc,LENGTH mlkem_poly_compress_d10_tmc; a,512; data,32;
1001+
stackpointer,8]
1002+
==> ensures x86
1003+
(\s.
1004+
bytes_loaded s (word pc) mlkem_poly_compress_d10_tmc /\
1005+
read RIP s = word pc /\
1006+
read RSP s = stackpointer /\
1007+
read (memory :> bytes64 stackpointer) s = returnaddress /\
1008+
C_ARGUMENTS [r; a; data] s /\
1009+
read events s = e)
1010+
(\s. read RIP s = returnaddress /\
1011+
read RSP s = word_add stackpointer (word 8) /\
1012+
(exists e2.
1013+
read events s = APPEND e2 e /\
1014+
e2 = f_events a data r pc stackpointer returnaddress /\
1015+
memaccess_inbounds e2
1016+
[a,512; data,32; r,320; stackpointer,8]
1017+
[r,320; stackpointer,8]))
1018+
(\s s'. true)`,
1019+
X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_poly_compress_d10_tmc
1020+
(CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLY_COMPRESS_D10_SAFE) THEN
1021+
DISCHARGE_SAFETY_PROPERTY_TAC);;
1022+
1023+
let MLKEM_POLY_COMPRESS_D10_SUBROUTINE_SAFE = time prove
1024+
(`exists f_events.
1025+
forall e r a data (inlist:(16 word) list) pc stackpointer returnaddress.
1026+
LENGTH inlist = 256 /\
1027+
aligned 32 a /\
1028+
aligned 32 data /\
1029+
ALL (nonoverlapping (r,320))
1030+
[word pc,LENGTH mlkem_poly_compress_d10_mc; a,512; data,32;
1031+
stackpointer,8]
1032+
==> ensures x86
1033+
(\s.
1034+
bytes_loaded s (word pc) mlkem_poly_compress_d10_mc /\
1035+
read RIP s = word pc /\
1036+
read RSP s = stackpointer /\
1037+
read (memory :> bytes64 stackpointer) s = returnaddress /\
1038+
C_ARGUMENTS [r; a; data] s /\
1039+
read events s = e)
1040+
(\s. read RIP s = returnaddress /\
1041+
read RSP s = word_add stackpointer (word 8) /\
1042+
(exists e2.
1043+
read events s = APPEND e2 e /\
1044+
e2 = f_events a data r pc stackpointer returnaddress /\
1045+
memaccess_inbounds e2
1046+
[a,512; data,32; r,320; stackpointer,8]
1047+
[r,320; stackpointer,8]))
1048+
(\s s'. true)`,
1049+
MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLY_COMPRESS_D10_NOIBT_SUBROUTINE_SAFE));;

‎proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d11.ml‎

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1011,3 +1011,105 @@ let MLKEM_POLY_COMPRESS_D11_SUBROUTINE_CORRECT = prove(
10111011
MAYCHANGE [memory :> bytes(r, 352)])`,
10121012
MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLY_COMPRESS_D11_NOIBT_SUBROUTINE_CORRECT));;
10131013

1014+
(* ------------------------------------------------------------------------- *)
1015+
(* Constant-time and memory safety proof. *)
1016+
(* ------------------------------------------------------------------------- *)
1017+
1018+
needs "x86_64/proofs/mlkem_utils.ml";;
1019+
needs "x86_64/proofs/subroutine_signatures.ml";;
1020+
1021+
let full_spec,public_vars = mk_safety_spec
1022+
~keep_maychanges:true
1023+
(assoc "mlkem_poly_compress_d11" subroutine_signatures)
1024+
MLKEM_POLY_COMPRESS_D11_CORRECT
1025+
MLKEM_POLY_COMPRESS_D11_TMC_EXEC;;
1026+
1027+
let MLKEM_POLY_COMPRESS_D11_SAFE = time prove
1028+
(`exists f_events.
1029+
forall e r a data (inlist:(16 word) list) pc.
1030+
LENGTH inlist = 256 /\
1031+
aligned 32 a /\
1032+
aligned 32 data /\
1033+
ALL (nonoverlapping (r,352))
1034+
[word pc,LENGTH mlkem_poly_compress_d11_tmc; a,512; data,64]
1035+
==> ensures x86
1036+
(\s.
1037+
bytes_loaded s (word pc)
1038+
(BUTLAST mlkem_poly_compress_d11_tmc) /\
1039+
read RIP s = word pc /\
1040+
C_ARGUMENTS [r; a; data] s /\
1041+
read events s = e)
1042+
(\s.
1043+
read RIP s = word (pc + MLKEM_POLY_COMPRESS_D11_CORE_END) /\
1044+
(exists e2.
1045+
read events s = APPEND e2 e /\
1046+
e2 = f_events a data r pc /\
1047+
memaccess_inbounds e2
1048+
[a,512; data,64; r,352] [r,352]))
1049+
(MAYCHANGE [events] ,,
1050+
MAYCHANGE [memory :> bytes (r,352)] ,,
1051+
MAYCHANGE [RIP] ,,
1052+
MAYCHANGE [RAX] ,,
1053+
MAYCHANGE [ZMM0; ZMM1; ZMM2; ZMM3; ZMM4; ZMM5; ZMM6; ZMM7; ZMM8; ZMM9; ZMM10; ZMM11])`,
1054+
ASSERT_CONCL_TAC full_spec THEN
1055+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
1056+
PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars
1057+
MLKEM_POLY_COMPRESS_D11_TMC_EXEC);;
1058+
1059+
let MLKEM_POLY_COMPRESS_D11_NOIBT_SUBROUTINE_SAFE = time prove
1060+
(`exists f_events.
1061+
forall e r a data (inlist:(16 word) list) pc stackpointer returnaddress.
1062+
LENGTH inlist = 256 /\
1063+
aligned 32 a /\
1064+
aligned 32 data /\
1065+
ALL (nonoverlapping (r,352))
1066+
[word pc,LENGTH mlkem_poly_compress_d11_tmc; a,512; data,64;
1067+
stackpointer,8]
1068+
==> ensures x86
1069+
(\s.
1070+
bytes_loaded s (word pc) mlkem_poly_compress_d11_tmc /\
1071+
read RIP s = word pc /\
1072+
read RSP s = stackpointer /\
1073+
read (memory :> bytes64 stackpointer) s = returnaddress /\
1074+
C_ARGUMENTS [r; a; data] s /\
1075+
read events s = e)
1076+
(\s. read RIP s = returnaddress /\
1077+
read RSP s = word_add stackpointer (word 8) /\
1078+
(exists e2.
1079+
read events s = APPEND e2 e /\
1080+
e2 = f_events a data r pc stackpointer returnaddress /\
1081+
memaccess_inbounds e2
1082+
[a,512; data,64; r,352; stackpointer,8]
1083+
[r,352; stackpointer,8]))
1084+
(\s s'. true)`,
1085+
X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_poly_compress_d11_tmc
1086+
(CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLY_COMPRESS_D11_SAFE) THEN
1087+
DISCHARGE_SAFETY_PROPERTY_TAC);;
1088+
1089+
let MLKEM_POLY_COMPRESS_D11_SUBROUTINE_SAFE = time prove
1090+
(`exists f_events.
1091+
forall e r a data (inlist:(16 word) list) pc stackpointer returnaddress.
1092+
LENGTH inlist = 256 /\
1093+
aligned 32 a /\
1094+
aligned 32 data /\
1095+
ALL (nonoverlapping (r,352))
1096+
[word pc,LENGTH mlkem_poly_compress_d11_mc; a,512; data,64;
1097+
stackpointer,8]
1098+
==> ensures x86
1099+
(\s.
1100+
bytes_loaded s (word pc) mlkem_poly_compress_d11_mc /\
1101+
read RIP s = word pc /\
1102+
read RSP s = stackpointer /\
1103+
read (memory :> bytes64 stackpointer) s = returnaddress /\
1104+
C_ARGUMENTS [r; a; data] s /\
1105+
read events s = e)
1106+
(\s. read RIP s = returnaddress /\
1107+
read RSP s = word_add stackpointer (word 8) /\
1108+
(exists e2.
1109+
read events s = APPEND e2 e /\
1110+
e2 = f_events a data r pc stackpointer returnaddress /\
1111+
memaccess_inbounds e2
1112+
[a,512; data,64; r,352; stackpointer,8]
1113+
[r,352; stackpointer,8]))
1114+
(\s s'. true)`,
1115+
MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLY_COMPRESS_D11_NOIBT_SUBROUTINE_SAFE));;

‎proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d4.ml‎

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -478,3 +478,105 @@ let MLKEM_POLY_COMPRESS_D4_SUBROUTINE_CORRECT = prove(
478478
MAYCHANGE [memory :> bytes(r, 128)])`,
479479
MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLY_COMPRESS_D4_NOIBT_SUBROUTINE_CORRECT));;
480480

481+
(* ------------------------------------------------------------------------- *)
482+
(* Constant-time and memory safety proof. *)
483+
(* ------------------------------------------------------------------------- *)
484+
485+
needs "x86_64/proofs/mlkem_utils.ml";;
486+
needs "x86_64/proofs/subroutine_signatures.ml";;
487+
488+
let full_spec,public_vars = mk_safety_spec
489+
~keep_maychanges:true
490+
(assoc "mlkem_poly_compress_d4" subroutine_signatures)
491+
MLKEM_POLY_COMPRESS_D4_CORRECT
492+
MLKEM_POLY_COMPRESS_D4_TMC_EXEC;;
493+
494+
let MLKEM_POLY_COMPRESS_D4_SAFE = time prove
495+
(`exists f_events.
496+
forall e r a data (inlist:(16 word) list) pc.
497+
LENGTH inlist = 256 /\
498+
aligned 32 a /\
499+
aligned 32 data /\
500+
ALL (nonoverlapping (r,128))
501+
[word pc,LENGTH mlkem_poly_compress_d4_tmc; a,512; data,32]
502+
==> ensures x86
503+
(\s.
504+
bytes_loaded s (word pc)
505+
(BUTLAST mlkem_poly_compress_d4_tmc) /\
506+
read RIP s = word pc /\
507+
C_ARGUMENTS [r; a; data] s /\
508+
read events s = e)
509+
(\s.
510+
read RIP s = word (pc + MLKEM_POLY_COMPRESS_D4_CORE_END) /\
511+
(exists e2.
512+
read events s = APPEND e2 e /\
513+
e2 = f_events a data r pc /\
514+
memaccess_inbounds e2
515+
[a,512; data,32; r,128] [r,128]))
516+
(MAYCHANGE [events] ,,
517+
MAYCHANGE [memory :> bytes (r,128)] ,,
518+
MAYCHANGE [RIP] ,,
519+
MAYCHANGE [RAX] ,,
520+
MAYCHANGE [ZMM0; ZMM1; ZMM2; ZMM3; ZMM4; ZMM5; ZMM6; ZMM7; ZMM8])`,
521+
ASSERT_CONCL_TAC full_spec THEN
522+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
523+
PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars
524+
MLKEM_POLY_COMPRESS_D4_TMC_EXEC);;
525+
526+
let MLKEM_POLY_COMPRESS_D4_NOIBT_SUBROUTINE_SAFE = time prove
527+
(`exists f_events.
528+
forall e r a data (inlist:(16 word) list) pc stackpointer returnaddress.
529+
LENGTH inlist = 256 /\
530+
aligned 32 a /\
531+
aligned 32 data /\
532+
ALL (nonoverlapping (r,128))
533+
[word pc,LENGTH mlkem_poly_compress_d4_tmc; a,512; data,32;
534+
stackpointer,8]
535+
==> ensures x86
536+
(\s.
537+
bytes_loaded s (word pc) mlkem_poly_compress_d4_tmc /\
538+
read RIP s = word pc /\
539+
read RSP s = stackpointer /\
540+
read (memory :> bytes64 stackpointer) s = returnaddress /\
541+
C_ARGUMENTS [r; a; data] s /\
542+
read events s = e)
543+
(\s. read RIP s = returnaddress /\
544+
read RSP s = word_add stackpointer (word 8) /\
545+
(exists e2.
546+
read events s = APPEND e2 e /\
547+
e2 = f_events a data r pc stackpointer returnaddress /\
548+
memaccess_inbounds e2
549+
[a,512; data,32; r,128; stackpointer,8]
550+
[r,128; stackpointer,8]))
551+
(\s s'. true)`,
552+
X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_poly_compress_d4_tmc
553+
(CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLY_COMPRESS_D4_SAFE) THEN
554+
DISCHARGE_SAFETY_PROPERTY_TAC);;
555+
556+
let MLKEM_POLY_COMPRESS_D4_SUBROUTINE_SAFE = time prove
557+
(`exists f_events.
558+
forall e r a data (inlist:(16 word) list) pc stackpointer returnaddress.
559+
LENGTH inlist = 256 /\
560+
aligned 32 a /\
561+
aligned 32 data /\
562+
ALL (nonoverlapping (r,128))
563+
[word pc,LENGTH mlkem_poly_compress_d4_mc; a,512; data,32;
564+
stackpointer,8]
565+
==> ensures x86
566+
(\s.
567+
bytes_loaded s (word pc) mlkem_poly_compress_d4_mc /\
568+
read RIP s = word pc /\
569+
read RSP s = stackpointer /\
570+
read (memory :> bytes64 stackpointer) s = returnaddress /\
571+
C_ARGUMENTS [r; a; data] s /\
572+
read events s = e)
573+
(\s. read RIP s = returnaddress /\
574+
read RSP s = word_add stackpointer (word 8) /\
575+
(exists e2.
576+
read events s = APPEND e2 e /\
577+
e2 = f_events a data r pc stackpointer returnaddress /\
578+
memaccess_inbounds e2
579+
[a,512; data,32; r,128; stackpointer,8]
580+
[r,128; stackpointer,8]))
581+
(\s s'. true)`,
582+
MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLY_COMPRESS_D4_NOIBT_SUBROUTINE_SAFE));;

0 commit comments

Comments
 (0)