Skip to content

Commit

Permalink
Update AES-GCM programs and their tests (#54)
Browse files Browse the repository at this point in the history 
### Description:

The AES-GCM programs are updated in the following two PRs,
aws/aws-lc#1403 and PR
aws/aws-lc#1639. Updating them in LNSym as well.

### Testing:

Make all succeeds and conformance testing is successful. 

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

Co-authored-by: Shilpi Goel <shigoel@gmail.com>
  • Loading branch information
@pennyannn @shigoel
pennyannn and shigoel authored Aug 5, 2024
1 parent 7d9c50e commit d71d7bc
Show file tree
Hide file tree
Showing 8 changed files with 2,017 additions and 2,038 deletions.
46 changes: 29 additions & 17 deletions Specs/GCMV8.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,39 +156,49 @@ private def gcm_polyval (x : BitVec 128) (y : BitVec 128) : BitVec 128 :=
/-- GCMInitV8 specification:
H : [128] -- initial H input
output : [12][128] -- precomputed Htable values
See for Hx_rev values: https://github.com/aws/aws-lc/pull/1403
-/
def GCMInitV8 (H : BitVec 128) : (List (BitVec 128)) :=
let H0 := GCMV8.gcm_init_H H
let H0_rev := (lo H0) ++ (hi H0)
let H2 := GCMV8.gcm_polyval H0 H0
let H2_rev := (lo H2) ++ (hi H2)
let H1 := ((hi H2) ^^^ (lo H2)) ++ ((hi H0) ^^^ (lo H0))
let H3 := GCMV8.gcm_polyval H0 H2
let H3_rev := (lo H3) ++ (hi H3)
let H5 := GCMV8.gcm_polyval H0 H3
let H5_rev := (lo H5) ++ (hi H5)
let H4 := ((hi H5) ^^^ (lo H5)) ++ ((hi H3) ^^^ (lo H3))
let H6 := GCMV8.gcm_polyval H0 H5
let H6_rev := (lo H6) ++ (hi H6)
let H8 := GCMV8.gcm_polyval H0 H6
let H8_rev := (lo H8) ++ (hi H8)
let H7 := ((hi H8) ^^^ (lo H8)) ++ ((hi H6) ^^^ (lo H6))
let H9 := GCMV8.gcm_polyval H0 H8
let H9_rev := (lo H9) ++ (hi H9)
let H11 := GCMV8.gcm_polyval H0 H9
let H11_rev := (lo H11) ++ (hi H11)
let H10 := ((hi H11) ^^^ (lo H11)) ++ ((hi H9) ^^^ (lo H9))
[H0, H1, H2, H3, H4, H5, H6, H7, H8, H9, H10, H11]

-- TODO: This test could not be proved using rfl nor decide
-- set_option maxRecDepth 1000000 in
-- set_option maxHeartbeats 1000000 in
-- unseal pmod.pmodTR degree.degreeTR pmult.pmultTR reverse.reverseTR in
example : GCMInitV8 0x66e94bd4ef8a2c3b884cfa59ca342b2e#128 =
[ 0xcdd297a9df1458771099f4b39468565c#128,
[H0_rev, H1, H2_rev, H3_rev, H4, H5_rev, H6_rev,
H7, H8_rev, H9_rev, H10, H11_rev]

-- set_option profiler true in
-- set_option maxRecDepth 20000 in
-- set_option maxHeartbeats 2000000 in
-- unseal pmod.pmodTR degree.degreeTR reverse.reverseTR pmult.pmultTR Nat.bitwise in
example : GCMInitV8 0x66e94bd4ef8a2c3b884cfa59ca342b2e#128 ==
[ 0x1099f4b39468565ccdd297a9df145877#128,
0x62d81a7fe5da3296dd4b631a4b7c0e2b#128,
0x88d320376963120dea0b3a488cb9209b#128,
0x8695e702c322faf935c1a04f8bfb2395#128,
0xea0b3a488cb9209b88d320376963120d#128,
0x35c1a04f8bfb23958695e702c322faf9#128,
0xb2261b4d0cb1e020b354474d48d9d96c#128,
0x568bd97348bd9145e4adc23e440c7165#128,
0xf9151b1f632d10b47d845b630bb0a55d#128,
0xe4adc23e440c7165568bd97348bd9145#128,
0x7d845b630bb0a55df9151b1f632d10b4#128,
0xa674eba8f9d7f2508491407c689db5e9#128,
0xec87cfb0e19d1c4e4af32418184aee1e#128,
0x7d1998bcfc545474f109e6e0b31d1eee#128,
0x4af32418184aee1eec87cfb0e19d1c4e#128,
0xf109e6e0b31d1eee7d1998bcfc545474#128,
0x7498729da40cd2808c107e5c4f494a9a#128,
0xd0e417a05fe61ba4a47c653dfbeac924#128 ] := by native_decide
0xa47c653dfbeac924d0e417a05fe61ba4#128 ] := by native_decide

/-- GCMGmultV8 specification:
H : [128] -- the first element in Htable, not the initial H input to GCMInitV8
Expand All @@ -197,9 +207,10 @@ example : GCMInitV8 0x66e94bd4ef8a2c3b884cfa59ca342b2e#128 =
-/
def GCMGmultV8 (H : BitVec 128) (Xi : List (BitVec 8)) (h : 8 * Xi.length = 128)
: (List (BitVec 8)):=
let H := (lo H) ++ (hi H)
split (GCMV8.gcm_polyval H (BitVec.cast h (BitVec.flatten Xi))) 8 (by omega)

example : GCMGmultV8 0xcdd297a9df1458771099f4b39468565c#128
example : GCMGmultV8 0x1099f4b39468565ccdd297a9df145877#128
[ 0x10#8, 0x54#8, 0x43#8, 0xb0#8, 0x2c#8, 0x4b#8, 0x1f#8, 0x24#8,
0x3b#8, 0xcd#8, 0xd4#8, 0x87#8, 0x16#8, 0x65#8, 0xb3#8, 0x2b#8 ] (by decide) =
[ 0xa2#8, 0xc9#8, 0x9c#8, 0x56#8, 0xeb#8, 0xa7#8, 0x91#8, 0xf6#8,
Expand All @@ -208,6 +219,7 @@ example : GCMGmultV8 0xcdd297a9df1458771099f4b39468565c#128

private def gcm_ghash_block (H : BitVec 128) (Xi : BitVec 128)
(inp : BitVec 128) : BitVec 128 :=
let H := (lo H) ++ (hi H)
GCMV8.gcm_polyval H (Xi ^^^ inp)

/-- GCMGhashV8 specification:
Expand Down Expand Up @@ -235,7 +247,7 @@ def GCMGhashV8 (H : BitVec 128) (Xi : List (BitVec 8))
let flat_inp := BitVec.flatten inp
split (GCMGhashV8TR H flat_Xi flat_inp 0 h3) 8 (by omega)

example : GCMGhashV8 0xcdd297a9df1458771099f4b39468565c#128
example : GCMGhashV8 0x1099f4b39468565ccdd297a9df145877#128
[ 0xa2#8, 0xc9#8, 0x9c#8, 0x56#8, 0xeb#8, 0xa7#8, 0x91#8, 0xf6#8,
0x9e#8, 0x15#8, 0xa6#8, 0x00#8, 0x67#8, 0x29#8, 0x7e#8, 0x0f#8 ]
(List.replicate 16 0x2a#8) (by simp) (by simp only [List.length_replicate]; omega) =
Expand Down
1,482 changes: 729 additions & 753 deletions Tests/AES-GCM/AESGCMDecKernelProgram.lean
View file

Large diffs are not rendered by default.

1,477 changes: 729 additions & 748 deletions Tests/AES-GCM/AESGCMEncKernelProgram.lean
View file

Large diffs are not rendered by default.

32 changes: 16 additions & 16 deletions Tests/AES-GCM/AESGCMProgramTests.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,18 +47,18 @@ def in_blocks : List (BitVec 8) := List.replicate 512 0x2a#8
def ivec : List (BitVec 8) := List.replicate 16 0x00#8

def Htable : List (BitVec 64) :=
[ 0x1099f4b39468565c#64, 0xcdd297a9df145877#64,
[ 0xcdd297a9df145877#64, 0x1099f4b39468565c#64,
0xdd4b631a4b7c0e2b#64, 0x62d81a7fe5da3296#64,
0xea0b3a488cb9209b#64, 0x88d320376963120d#64,
0x35c1a04f8bfb2395#64, 0x8695e702c322faf9#64,
0x88d320376963120d#64, 0xea0b3a488cb9209b#64,
0x8695e702c322faf9#64, 0x35c1a04f8bfb2395#64,
0xb354474d48d9d96c#64, 0xb2261b4d0cb1e020#64,
0xe4adc23e440c7165#64, 0x568bd97348bd9145#64,
0x7d845b630bb0a55d#64, 0xf9151b1f632d10b4#64,
0x568bd97348bd9145#64, 0xe4adc23e440c7165#64,
0xf9151b1f632d10b4#64, 0x7d845b630bb0a55d#64,
0x8491407c689db5e9#64, 0xa674eba8f9d7f250#64,
0x4af32418184aee1e#64, 0xec87cfb0e19d1c4e#64,
0xf109e6e0b31d1eee#64, 0x7d1998bcfc545474#64,
0xec87cfb0e19d1c4e#64, 0x4af32418184aee1e#64,
0x7d1998bcfc545474#64, 0xf109e6e0b31d1eee#64,
0x8c107e5c4f494a9a#64, 0x7498729da40cd280#64,
0xa47c653dfbeac924#64, 0xd0e417a05fe61ba4#64,
0xd0e417a05fe61ba4#64, 0xa47c653dfbeac924#64,
0x0#64, 0x0#64,
0x0#64, 0x0#64,
0x0#64, 0x0#64,
Expand All @@ -85,7 +85,7 @@ def aes_gcm_enc_kernel_test (n : Nat) (plain_blocks : BitVec 4096)
| _ => 0#64
let s := { gpr := init_gpr,
sfp := (fun (_ : BitVec 5) => 0#128),
pc := 0x7a0cf0#64,
pc := 0x7cf610#64,
pstate := PState.zero,
mem := (fun (_ :BitVec 64) => 0#8),
program := AESGCMEncKernelProgram.aes_gcm_enc_kernel_program,
Expand Down Expand Up @@ -123,7 +123,7 @@ def aes_gcm_dec_kernel_test (n : Nat) (cipher_blocks : BitVec 4096)
| _ => 0#64
let s := { gpr := init_gpr,
sfp := (fun (_ : BitVec 5) => 0#128),
pc := 0x7a1880#64,
pc := 0x7d0150#64,
pstate := PState.zero,
mem := (fun (_ :BitVec 64) => 0#8),
program := AESGCMDecKernelProgram.aes_gcm_dec_kernel_program,
Expand Down Expand Up @@ -209,7 +209,7 @@ def final_state : ArmState :=
have h : 8 * in_blocks.length = 4096 := by
unfold in_blocks
simp only [List.length_replicate]
aes_gcm_enc_kernel_test 1514 (BitVec.cast h $ revflat in_blocks) (revflat Xi) (revflat Htable)
aes_gcm_enc_kernel_test 1495 (BitVec.cast h $ revflat in_blocks) (revflat Xi) (revflat Htable)
rounds (revflat key) (revflat ivec)

def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state
Expand All @@ -227,7 +227,7 @@ namespace dec

-- AES_128_GCM decrypt test
def final_state : ArmState :=
aes_gcm_dec_kernel_test 1519 (revflat ciphertext) (revflat Xi) (revflat Htable)
aes_gcm_dec_kernel_test 1495 (revflat ciphertext) (revflat Xi) (revflat Htable)
rounds (revflat key) (revflat ivec)

def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state
Expand Down Expand Up @@ -310,7 +310,7 @@ def final_state : ArmState :=
have h : 8 * in_blocks.length = 4096 := by
unfold in_blocks
simp only [List.length_replicate]
aes_gcm_enc_kernel_test 1650 (BitVec.cast h $ revflat in_blocks) (revflat Xi) (revflat Htable)
aes_gcm_enc_kernel_test 1631 (BitVec.cast h $ revflat in_blocks) (revflat Xi) (revflat Htable)
rounds (revflat key) (revflat ivec)

def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state
Expand All @@ -328,7 +328,7 @@ namespace dec

-- AES_192_GCM decrypt test
def final_state : ArmState :=
aes_gcm_dec_kernel_test 1655 (revflat ciphertext) (revflat Xi) (revflat Htable)
aes_gcm_dec_kernel_test 1631 (revflat ciphertext) (revflat Xi) (revflat Htable)
rounds (revflat key) (revflat ivec)

def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state
Expand Down Expand Up @@ -414,7 +414,7 @@ def final_state : ArmState :=
have h : 8 * in_blocks.length = 4096 := by
unfold in_blocks
simp only [List.length_replicate]
aes_gcm_enc_kernel_test 1778 (BitVec.cast h $ revflat in_blocks) (revflat Xi) (revflat Htable)
aes_gcm_enc_kernel_test 1759 (BitVec.cast h $ revflat in_blocks) (revflat Xi) (revflat Htable)
rounds (revflat key) (revflat ivec)

def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state
Expand All @@ -432,7 +432,7 @@ namespace dec

-- AES_256_GCM decrypt test
def final_state : ArmState :=
aes_gcm_dec_kernel_test 1783 (revflat ciphertext) (revflat Xi) (revflat Htable)
aes_gcm_dec_kernel_test 1759 (revflat ciphertext) (revflat Xi) (revflat Htable)
rounds (revflat key) (revflat ivec)

def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state
Expand Down
Loading

0 comments on commit d71d7bc

Please sign in to comment.