Skip to content

Add additional instructions required by AES-XTS on x86_64 #215

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Apr 18, 2025
Merged

Add additional instructions required by AES-XTS on x86_64 #215

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
510ec92
Add additional instructions required by AES-XTS on x86
pennyannn Mar 26, 2025
9af7d7b
Remove unnecessary type annotations and cleanup allowed_asm
pennyannn Apr 11, 2025
4c7ba83
Scratch XORPS from the PR
pennyannn Apr 17, 2025
fdaffdb
Use {u}simdN, bring the EXPAND_SIMD_RULE from Arm to x86
aqjune-aws Apr 18, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 37 additions & 8 deletions x86/allowed_asm
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,3 @@
: aesdec$
: aesdeclast$
: aesenc$
: aesenclast$
: aeskeygenassist$
: adc$
: adcl$
: adcq$
Expand All @@ -12,6 +7,11 @@
: addq$
: adox$
: adoxq$
: aesdec$
: aesdeclast$
: aesenc$
: aesenclast$
: aeskeygenassist$
: and$
: andl$
: andq$
Expand All @@ -21,6 +21,12 @@
: bswapq$
: bt$
: btq$
: btc$
: btcq$
: btr$
: btrq$
: bts$
: btsq$
: call$
: callq$
: cmc$
Expand All @@ -47,15 +53,15 @@
: lea$
: leaq$
: mov$
: movl$
: movq$
: movw$
: movabs$
: movabsq$
: movaps$
: movdqa$
: movdqu$
: movups$
: movl$
: movq$
: movw$
: mul$
: mulq$
: mulx$
Expand All @@ -66,17 +72,39 @@
: notq$
: or$
: orq$
: paddd$
: paddq$
: pand$
: pop$
: popq$
: pshufd$
: psrad$
: push$
: pushq$
: pxor$
: rcr$
: ret$
: retq$
: sar$
: sbb$
: sbbl$
: sbbq$
: setb$
: setbe$
: setl$
: setle$
: setnb$
: setnbe$
: setnl$
: setnle$
: setno$
: setnp$
: setns$
: setnz$
: seto$
: setp$
: sets$
: setz$
: shl$
: shld$
: shldq$
Expand All @@ -90,6 +118,7 @@
: subq$
: test$
: testq$
: vpxor$
: xchg$
: xor$
: xorl$
Expand Down
64 changes: 51 additions & 13 deletions x86/proofs/decode.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -293,6 +293,18 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
let rm = simd_of_RM sz rm in
let dest,src = if d then rm,reg else reg,rm in
SOME (MOVUPS dest src, l)
| [0x1e:8] ->
read_byte l >>= \(b,l).
(bitmatch b with
| [0xfa:8] ->
(match pfxs with
| (F, RepZ) -> SOME (ENDBR64,l)
| _ -> NONE)
| _ -> NONE)
| [0x1f:8] -> if has_unhandled_pfxs pfxs then NONE else
let sz = op_size_W rex T pfxs in
read_ModRM_operand rex sz l >>= \((_,rm),l).
SOME (NOP_N rm,l)
| [0b0010100:7; d] -> if has_pfxs pfxs then NONE else
let sz = Lower_128 in
read_ModRM rex l >>= \((reg,rm),l).
Expand Down Expand Up @@ -334,14 +346,14 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
read_imm Byte l >>= \(imm8,l).
SOME (AESKEYGENASSIST (mmreg reg sz) (simd_of_RM sz rm) imm8, l)
| _ -> NONE)
| [0b11001:5; r:3] -> if has_pfxs pfxs then NONE else
let sz = op_size_W rex T pfxs in
let reg = rex_reg (rex_B rex) r in
SOME (BSWAP (%(gpr_adjust reg sz)),l)
| [0x4:4; c:4] -> if has_pfxs pfxs then NONE else
let sz = op_size T (rex_W rex) T pfxs in
read_ModRM_operand rex sz l >>= \((reg,rm),l).
SOME (CMOV (decode_condition c) reg rm,l)
| [0x66:8] -> if has_unhandled_pfxs pfxs then NONE else
let sz = Lower_128 in
read_ModRM rex l >>= \((reg,rm),l).
SOME (PCMPGTD (mmreg reg sz) (simd_of_RM sz rm), l)
| [0b011:3; d; 0b1111:4] ->
let sz = Lower_128 in
read_ModRM rex l >>= \((reg,rm),l).
Expand All @@ -352,6 +364,20 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
| (T, Rep0) -> SOME (MOVDQA dest src, l)
| (F, RepZ) -> SOME (MOVDQU dest src, l)
| _ -> NONE)
| [0x70:8] -> if has_unhandled_pfxs pfxs then NONE else
let sz = Lower_128 in
read_ModRM rex l >>= \((reg,rm),l).
read_imm Byte l >>= \(imm8,l).
SOME (PSHUFD (mmreg reg sz) (simd_of_RM sz rm) imm8, l)
| [0x72:8] -> if has_unhandled_pfxs pfxs then NONE else
let sz = Lower_128 in
(read_ModRM rex l >>= \((reg,rm),l).
match rm with
| RM_reg _ -> if (word_zx reg):(3 word) = word 0b100 then
(read_imm Byte l >>= \(imm8,l).
SOME (PSRAD (simd_of_RM sz rm) imm8, l))
else NONE
| _ -> NONE)
| [0x8:4; c:4] -> if has_pfxs pfxs then NONE else
read_int32 l >>= \(imm,l).
SOME (JUMP (decode_condition c) (Imm32 imm),l)
Expand Down Expand Up @@ -404,14 +430,26 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
read_ModRM rex l >>= \((reg,rm),l).
let op = if s then MOVSX else MOVZX in
SOME (op (%(gpr_adjust reg sz2)) (operand_of_RM sz rm),l)
| [0x1e:8] ->
read_byte l >>= \(b,l).
(bitmatch b with
| [0xfa:8] ->
(match pfxs with
| (F, RepZ) -> SOME (ENDBR64,l)
| _ -> NONE)
| _ -> NONE)
| [0b11001:5; r:3] -> if has_pfxs pfxs then NONE else
let sz = op_size_W rex T pfxs in
let reg = rex_reg (rex_B rex) r in
SOME (BSWAP (%(gpr_adjust reg sz)),l)
| [0xd4:8] -> if has_unhandled_pfxs pfxs then NONE else
let sz = Lower_128 in
read_ModRM rex l >>= \((reg,rm),l).
SOME (PADDQ (mmreg reg sz) (simd_of_RM sz rm), l)
| [0xdb:8] -> if has_unhandled_pfxs pfxs then NONE else
let sz = Lower_128 in
read_ModRM rex l >>= \((reg,rm),l).
SOME (PAND (mmreg reg sz) (simd_of_RM sz rm), l)
| [0xef:8] -> if has_unhandled_pfxs pfxs then NONE else
let sz = Lower_128 in
read_ModRM rex l >>= \((reg,rm),l).
SOME (PXOR (mmreg reg sz) (simd_of_RM sz rm), l)
| [0xfe:8] -> if has_unhandled_pfxs pfxs then NONE else
let sz = Lower_128 in
read_ModRM rex l >>= \((reg,rm),l).
SOME (PADDD (mmreg reg sz) (simd_of_RM sz rm), l)
| _ -> NONE)
| [0b01010:5; r:3] -> if has_pfxs pfxs then NONE else
SOME (PUSH (%(Gpr (rex_reg (rex_B rex) r) Full_64)),l)
Expand Down Expand Up @@ -467,7 +505,7 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
if opc = word 0 then
SOME (POP rm,l)
else NONE
| [0x90:8] -> if has_pfxs pfxs then NONE else
| [0x90:8] -> if has_unhandled_pfxs pfxs then NONE else
SOME (NOP,l)
| [0b1010100:7; v] -> if has_pfxs pfxs then NONE else
let sz = op_size T (rex_W rex) v pfxs in
Expand Down
12 changes: 10 additions & 2 deletions x86/proofs/instruction.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -237,10 +237,10 @@ let instruction_INDUCTION,instruction_RECURSION = define_type
| ADCX operand operand
| ADD operand operand
| ADOX operand operand
| AESENC operand operand
| AESENCLAST operand operand
| AESDEC operand operand
| AESDECLAST operand operand
| AESENC operand operand
| AESENCLAST operand operand
| AESKEYGENASSIST operand operand operand
| AND operand operand
| BSF operand operand
Expand Down Expand Up @@ -276,10 +276,18 @@ let instruction_INDUCTION,instruction_RECURSION = define_type
| MULX4 (operand#operand) (operand#operand)
| NEG operand
| NOP
| NOP_N operand
| NOT operand
| OR operand operand
| PADDD operand operand
| PADDQ operand operand
| PAND operand operand
| PCMPGTD operand operand
| POP operand
| PSHUFD operand operand operand
| PSRAD operand operand
| PUSH operand
| PXOR operand operand
| RCL operand operand
| RCR operand operand
| RET
Expand Down
17 changes: 17 additions & 0 deletions x86/proofs/simulator.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -273,6 +273,23 @@ let iclasses = iclasses @
[0x66; 0x0f; 0x3a; 0xdf; 0xc8; 0x01]; (*AESKEYGENASSIST (%_% xmm1) (%_% xmm0) (Imm8 (word 1)) *)
[0x66; 0x0f; 0x3a; 0xdf; 0xf8; 0xff]; (*AESKEYGENASSIST (%_% xmm15) (%_% xmm0) (Imm8 (word 255)) *)
[0x66; 0x0f; 0x3a; 0xdf; 0xdc; 0x19]; (*AESKEYGENASSIST (%_% xmm3) (%_% xmm12) (Imm8 (word 25)) *)
[0x66; 0x0f; 0x70; 0xc9; 0x55]; (*PSHUFD (%_% xmm1) (%_% xmm1) (Imm8 (word 85)) *)
[0x66; 0x44; 0x0f; 0x70; 0xca; 0x5f]; (*PSHUFD (%_% xmm9) (%_% xmm2) (Imm8 (word 95)) *)
[0x66; 0x0f; 0xef; 0xd3]; (*PXOR (%_% xmm2) (%_% xmm3) *)
[0x66; 0x41; 0x0f; 0xef; 0xff]; (*PXOR (%_% xmm7) (%_% xmm15) *)
[0x66; 0x0f; 0xdb; 0xd3]; (*PAND (%_% xmm2) (%_% xmm3) *)
[0x66; 0x41; 0x0f; 0xdb; 0xff]; (*PAND (%_% xmm7) (%_% xmm15) *)
[0x66; 0x0f; 0xfe; 0xd3]; (*PADDD (%_% xmm2) (%_% xmm3) *)
[0x66; 0x41; 0x0f; 0xfe; 0xff]; (*PADDD (%_% xmm7) (%_% xmm15) *)
[0x66; 0x0f; 0xd4; 0xd3]; (*PADDQ (%_% xmm2) (%_% xmm3) *)
[0x66; 0x41; 0x0f; 0xd4; 0xff]; (*PADDQ (%_% xmm7) (%_% xmm15) *)
[0x66; 0x0f; 0x72; 0xe1; 0x1f]; (*PSRAD (%_% xmm1) (Imm8 (word 31)) *)
[0x66; 0x41; 0x0f; 0x72; 0xe4; 0x38]; (*PSRAD (%_% xmm12) (Imm8 (word 56)) *)
[0x66; 0x45; 0x0f; 0x66; 0xfe]; (*PCMPGTD (%_% xmm15) (%_% xmm14) *)
[0x66; 0x0f; 0x66; 0xcb]; (*PCMPGTD (%_% xmm1) (%_% xmm3) *)
[0x66; 0x90]; (* NOP *)
[0x0f; 0x1f; 0x4f; 0x00]; (* NOP_N (Memop Doubleword (%% (rdi,0))) *)
[0x66; 0x0f; 0x1f; 0x84; 0x00; 0x00; 0x01; 0x02; 0x03]; (* NOP_N (Memop Word (%%%% (rax,0,rax,&50462976))) *)
];;

(* ------------------------------------------------------------------------- *)
Expand Down
Loading