Skip to content

Commit 5f3781b

Browse files
JasonGrossclaude
JasonGross
and
claude
committed
Model one-operand imul as a signed multiply in the assembly checker
Fixes scrutineer security finding #2514. The one-operand form of `imul r/m` (rdx:rax := rax * src, or ax := al * src for 8-bit operands) shared a single branch with `mul` in both the symbolic executor (src/Assembly/Symbolic.v, SymexNormalInstruction) and the concrete semantics (src/Assembly/WithBedrock/Semantics.v, DenoteNormalInstruction). Both computed the *unsigned* full product. On real x86-64 hardware `mul` is unsigned but one-operand `imul` is signed (Intel SDM Vol. 2A, IMUL), so the high word written to rdx (ah for 8-bit) differs whenever an operand has its top bit set; the low word agrees. For example, with rax = 0xffffffff00000001 (the top limb of the P-256 prime) and rcx = 3, `imul rcx` leaves rdx = 0xffffffffffffffff on hardware, but the model computed 0x2. Consequently the equivalence checker (`--hints-file`) could certify assembly that uses `imul rcx` where the reference computation needs the unsigned high word from `mul rcx` / `mulx`, i.e. accept non-equivalent assembly. The two- and three-operand forms of `imul` only write the low half and were already correct. The fix splits the shared branch: - `mul` keeps its previous (unsigned) behaviour unchanged. - One-operand `imul` now computes the high word as `keep s ((Z.signed s rax * Z.signed s src) >> s)` in the concrete semantics, and in the symbolic executor as `shr s (mulZ (signed rax) (signed src)) s` where `signed x` is spelled with existing operators as `addZ (add s x (2^(s-1))) (-(2^(s-1)))`, which is exactly `Z.signed s x` unfolded. The low word is still the (unsigned) `mulZ` product, which agrees with the signed one after truncation. Flags are havocked as before. The 8-bit form (ah:al) is handled by the same code. - SymbolicProofs.v gains a small case for the new branch relating the unfolded sign extension to `Z.signed`. A new test file src/Assembly/WithBedrock/SemanticsTests.v pins down the hardware values of `mul`/`imul` (64- and 8-bit, top bit set or clear) for both the concrete semantics and the symbolic executor; the imul cases fail against the previous model. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD
1 parent 5691ca0 commit 5f3781b

4 files changed

Lines changed: 157 additions & 2 deletions

File tree

‎src/Assembly/Symbolic.v‎

Lines changed: 26 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4298,7 +4298,7 @@ Definition SymexNormalInstruction {opts : symbolic_options_computed_opt} {descr:
42984298
vh <- Symeval (shrZ@(v,PreARG (Z.of_N s)));
42994299
_ <- SetOperand lo v;
43004300
SetOperand hi vh
4301-
| (Syntax.mul | imul), [src2] =>
4301+
| Syntax.mul, [src2] =>
43024302
let src1 : ARG := rax in
43034303
v <- Symeval (mulZ@(src1,src2));
43044304
vh <- Symeval (shrZ@(v,PreARG (Z.of_N s)));
@@ -4309,6 +4309,31 @@ Definition SymexNormalInstruction {opts : symbolic_options_computed_opt} {descr:
43094309
_ <- SetOperand (lo:ARG) v;
43104310
_ <- SetOperand (hi:ARG) vh;
43114311
HavocFlags (* This is conservative and can be made more precise *)
4312+
| imul, [src2] =>
4313+
(* One-operand [imul] is a *signed* widening multiply (Intel SDM Vol. 2A,
4314+
IMUL): rdx:rax (ah:al for s = 8) := signed(rax) * signed(src2). The low
4315+
half agrees with the unsigned product, but the high half does not
4316+
whenever an operand has its top bit set, so it must not share the
4317+
unsigned [mul] branch above. [signed_ x] is [Z.signed s x] for an
4318+
s-bit value [x], spelled with existing operators. *)
4319+
let src1 : ARG := rax in
4320+
let half : Z := Z.shiftl 1 (Z.of_N s-1) in
4321+
let signed_ (x : idx) : pre_expr
4322+
:= addZ@(add s@(x, PreApp (const half) nil), PreApp (const (-half)) nil) in
4323+
a <- GetOperand src1;
4324+
b <- GetOperand src2;
4325+
v <- Symeval (mulZ@(a,b));
4326+
sa <- Symeval (signed_ a);
4327+
sb <- Symeval (signed_ b);
4328+
p <- Symeval (mulZ@(sa,sb));
4329+
vh <- Symeval (shr s@(p, PreApp (const (Z.of_N s)) nil));
4330+
lo <- resize_reg rax;
4331+
hi <- (if (s =? 8)%N
4332+
then ret ah
4333+
else resize_reg rdx);
4334+
_ <- SetOperand (lo:ARG) v;
4335+
_ <- SetOperand (hi:ARG) vh;
4336+
HavocFlags (* This is conservative and can be made more precise *)
43124337
| Syntax.shl, [dst; cnt] =>
43134338
let cnt := andZ@(cnt, (PreApp (const (Z.of_N s-1)%Z) nil)) in
43144339
v <- Symeval (shl s@(dst, cnt));

‎src/Assembly/WithBedrock/Semantics.v‎

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -245,7 +245,7 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
245245
let v := v1 * v2 in
246246
st <- SetOperand sa s st lo v;
247247
SetOperand sa s st hi (Z.shiftr v (Z.of_N s))
248-
| (Syntax.mul | imul), [src2] =>
248+
| Syntax.mul, [src2] =>
249249
let src1 : ARG := rax in
250250
v1 <- DenoteOperand sa s st src1;
251251
v2 <- DenoteOperand sa s st src2;
@@ -257,6 +257,24 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
257257
st <- SetOperand sa s st lo v;
258258
st <- SetOperand sa s st hi (Z.shiftr v (Z.of_N s));
259259
Some (HavocFlags st) (* conservative *)
260+
| imul, [src2] =>
261+
(* One-operand [imul] is a *signed* widening multiply (Intel SDM Vol. 2A,
262+
IMUL): rdx:rax (ah:al for s = 8) := signed(rax) * signed(src2). The low
263+
half agrees with the unsigned product [v1 * v2], but the high half does
264+
not whenever an operand has its top bit set, so it must not share the
265+
unsigned [mul] branch above. *)
266+
let src1 : ARG := rax in
267+
v1 <- DenoteOperand sa s st src1;
268+
v2 <- DenoteOperand sa s st src2;
269+
let v := v1 * v2 in
270+
let vs := Z.signed s v1 * Z.signed s v2 in
271+
lo <- resize_reg rax;
272+
hi <- (if (s =? 8)%N
273+
then Some ah
274+
else resize_reg rdx);
275+
st <- SetOperand sa s st lo v;
276+
st <- SetOperand sa s st hi (Z.land (Z.shiftr vs (Z.of_N s)) (Z.ones (Z.of_N s)));
277+
Some (HavocFlags st) (* conservative *)
260278
| imul, ([src1 as dst; src2] | [dst; src1; src2]) =>
261279
v1 <- DenoteOperand sa s st src1;
262280
v2 <- DenoteOperand sa s st src2;

‎src/Assembly/WithBedrock/SemanticsTests.v‎

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
(** Regression tests for the semantics of one-operand [mul] and [imul].
2+
3+
The one-operand form of [imul] is a *signed* widening multiply
4+
(rdx:rax := signed(rax) * signed(src)), whereas [mul] is unsigned. The
5+
two agree on the low half of the product but not on the high half
6+
whenever an operand has its top bit set. The concrete semantics
7+
([Semantics.DenoteNormalInstruction]) and the symbolic executor
8+
([Symbolic.SymexNormalInstruction]) used to share a single unsigned
9+
branch for both mnemonics (scrutineer finding #2514); these tests pin
10+
down the hardware behaviour for both models, on the same inputs.
11+
12+
The expected values were obtained by executing the instructions on
13+
x86-64 hardware. *)
14+
From Coq Require Import ZArith.
15+
From Coq Require Import List.
16+
From Coq Require Import String.
17+
Require Import Crypto.Util.ErrorT.
18+
Require Import Crypto.Util.Tuple.
19+
Require Import Crypto.Assembly.Syntax.
20+
Require Import Crypto.Assembly.Symbolic.
21+
Require Import Crypto.Assembly.Equivalence.
22+
Require Import Crypto.Assembly.WithBedrock.Semantics.
23+
Require Import coqutil.Map.Interface.
24+
Import ListNotations.
25+
Local Open Scope Z_scope.
26+
Local Open Scope list_scope.
27+
Local Open Scope string_scope.
28+
29+
(** ** Concrete semantics *)
30+
31+
Definition initial_machine_state (rax_val rcx_val : Z) : machine_state
32+
:= {| machine_reg_state := Semantics.set_reg (Semantics.set_reg (Tuple.repeat 0 _) rax rax_val) rcx rcx_val
33+
; machine_flag_state := havoc_flags
34+
; machine_mem_state := map.empty |}.
35+
36+
Definition denote_one (instr : NormalInstruction) (rax_val rcx_val : Z) (out : REG) : option Z
37+
:= option_map (fun st : machine_state => Semantics.get_reg st out) (DenoteNormalInstruction (initial_machine_state rax_val rcx_val) instr).
38+
39+
Definition mul_rcx : NormalInstruction := {| Syntax.prefix := None ; Syntax.op := Syntax.mul ; Syntax.args := [reg rcx] |}.
40+
Definition imul_rcx : NormalInstruction := {| Syntax.prefix := None ; Syntax.op := Syntax.imul ; Syntax.args := [reg rcx] |}.
41+
Definition mul_cl : NormalInstruction := {| Syntax.prefix := None ; Syntax.op := Syntax.mul ; Syntax.args := [reg cl] |}.
42+
Definition imul_cl : NormalInstruction := {| Syntax.prefix := None ; Syntax.op := Syntax.imul ; Syntax.args := [reg cl] |}.
43+
44+
(** rax = 0xffffffff00000001 (the top limb of the P-256 prime; bit 63 set), rcx = 3 *)
45+
Example denote_mul_rcx_hi : denote_one mul_rcx 0xffffffff00000001 3 rdx = Some 0x2. Proof. vm_compute; reflexivity. Qed.
46+
Example denote_mul_rcx_lo : denote_one mul_rcx 0xffffffff00000001 3 rax = Some 0xfffffffd00000003. Proof. vm_compute; reflexivity. Qed.
47+
Example denote_imul_rcx_hi : denote_one imul_rcx 0xffffffff00000001 3 rdx = Some 0xffffffffffffffff. Proof. vm_compute; reflexivity. Qed.
48+
Example denote_imul_rcx_lo : denote_one imul_rcx 0xffffffff00000001 3 rax = Some 0xfffffffd00000003. Proof. vm_compute; reflexivity. Qed.
49+
50+
(** both operands with bit 63 set: rax = -2, rcx = -2^63+1 as signed values *)
51+
Example denote_mul_rcx_hi' : denote_one mul_rcx 0xfffffffffffffffe 0x8000000000000001 rdx = Some 0x7fffffffffffffff. Proof. vm_compute; reflexivity. Qed.
52+
Example denote_imul_rcx_hi' : denote_one imul_rcx 0xfffffffffffffffe 0x8000000000000001 rdx = Some 0x0. Proof. vm_compute; reflexivity. Qed.
53+
Example denote_mul_rcx_lo' : denote_one mul_rcx 0xfffffffffffffffe 0x8000000000000001 rax = Some 0xfffffffffffffffe. Proof. vm_compute; reflexivity. Qed.
54+
Example denote_imul_rcx_lo' : denote_one imul_rcx 0xfffffffffffffffe 0x8000000000000001 rax = Some 0xfffffffffffffffe. Proof. vm_compute; reflexivity. Qed.
55+
56+
(** no top bit set: signed and unsigned agree *)
57+
Example denote_mul_rcx_hi'' : denote_one mul_rcx 0x123456789 0x23456789a rdx = Some 0x2. Proof. vm_compute; reflexivity. Qed.
58+
Example denote_imul_rcx_hi'' : denote_one imul_rcx 0x123456789 0x23456789a rdx = Some 0x2. Proof. vm_compute; reflexivity. Qed.
59+
60+
(** 8-bit form writes ah:al; al = 0xff (-1), cl = 3 *)
61+
Example denote_mul_cl_ah : denote_one mul_cl 0xff 3 ah = Some 0x2. Proof. vm_compute; reflexivity. Qed.
62+
Example denote_mul_cl_al : denote_one mul_cl 0xff 3 al = Some 0xfd. Proof. vm_compute; reflexivity. Qed.
63+
Example denote_imul_cl_ah : denote_one imul_cl 0xff 3 ah = Some 0xff. Proof. vm_compute; reflexivity. Qed.
64+
Example denote_imul_cl_al : denote_one imul_cl 0xff 3 al = Some 0xfd. Proof. vm_compute; reflexivity. Qed.
65+
(** the untouched upper bytes of rax are preserved *)
66+
Example denote_imul_cl_rax : denote_one imul_cl 0x11223344556677ff 3 rax = Some 0x112233445566fffd. Proof. vm_compute; reflexivity. Qed.
67+
68+
(** ** Symbolic executor *)
69+
70+
Local Instance test_symbolic_options : symbolic_options_computed_opt
71+
:= {| asm_rewriting_passes := default_rewriting_passes (rewriting_pipeline:=default_rewrite_pass_order) (rewriting_pass_filter:=fun _ => true)
72+
; asm_debug_symex_asm_first_computed := false
73+
; asm_node_reveal_depth_computed := default_node_reveal_depth |}.
74+
75+
(** Symbolically execute [instr] from a state where every register holds a
76+
fresh symbol, then evaluate the requested output register with the
77+
symbols for [rax] and [rcx] instantiated to the given values (and every
78+
other register to [0]). *)
79+
Definition symex_one (instr : NormalInstruction) (rax_val rcx_val : Z) (out : REG) : option Z
80+
:= let st := init_symbolic_state dag.empty in
81+
let ctx : symbol -> option Z
82+
:= fun n => if (n =? reg_index rax)%N then Some rax_val
83+
else if (n =? reg_index rcx)%N then Some rcx_val
84+
else Some 0 in
85+
match (_ <- SymexNormalInstruction (descr:=Build_description "SemanticsTests" true) instr;
86+
GetReg (descr:=Build_description "SemanticsTests" true) out)%x86symex st with
87+
| Success (i, st) => interp_expr ctx (reveal st 100 i)
88+
| Error _ => None
89+
end.
90+
91+
Example symex_mul_rcx_hi : symex_one mul_rcx 0xffffffff00000001 3 rdx = Some 0x2. Proof. vm_compute; reflexivity. Qed.
92+
Example symex_mul_rcx_lo : symex_one mul_rcx 0xffffffff00000001 3 rax = Some 0xfffffffd00000003. Proof. vm_compute; reflexivity. Qed.
93+
Example symex_imul_rcx_hi : symex_one imul_rcx 0xffffffff00000001 3 rdx = Some 0xffffffffffffffff. Proof. vm_compute; reflexivity. Qed.
94+
Example symex_imul_rcx_lo : symex_one imul_rcx 0xffffffff00000001 3 rax = Some 0xfffffffd00000003. Proof. vm_compute; reflexivity. Qed.
95+
96+
Example symex_mul_rcx_hi' : symex_one mul_rcx 0xfffffffffffffffe 0x8000000000000001 rdx = Some 0x7fffffffffffffff. Proof. vm_compute; reflexivity. Qed.
97+
Example symex_imul_rcx_hi' : symex_one imul_rcx 0xfffffffffffffffe 0x8000000000000001 rdx = Some 0x0. Proof. vm_compute; reflexivity. Qed.
98+
Example symex_mul_rcx_lo' : symex_one mul_rcx 0xfffffffffffffffe 0x8000000000000001 rax = Some 0xfffffffffffffffe. Proof. vm_compute; reflexivity. Qed.
99+
Example symex_imul_rcx_lo' : symex_one imul_rcx 0xfffffffffffffffe 0x8000000000000001 rax = Some 0xfffffffffffffffe. Proof. vm_compute; reflexivity. Qed.
100+
101+
Example symex_mul_rcx_hi'' : symex_one mul_rcx 0x123456789 0x23456789a rdx = Some 0x2. Proof. vm_compute; reflexivity. Qed.
102+
Example symex_imul_rcx_hi'' : symex_one imul_rcx 0x123456789 0x23456789a rdx = Some 0x2. Proof. vm_compute; reflexivity. Qed.
103+
104+
Example symex_mul_cl_ah : symex_one mul_cl 0xff 3 ah = Some 0x2. Proof. vm_compute; reflexivity. Qed.
105+
Example symex_mul_cl_al : symex_one mul_cl 0xff 3 al = Some 0xfd. Proof. vm_compute; reflexivity. Qed.
106+
Example symex_imul_cl_ah : symex_one imul_cl 0xff 3 ah = Some 0xff. Proof. vm_compute; reflexivity. Qed.
107+
Example symex_imul_cl_al : symex_one imul_cl 0xff 3 al = Some 0xfd. Proof. vm_compute; reflexivity. Qed.
108+
Example symex_imul_cl_rax : symex_one imul_cl 0x11223344556677ff 3 rax = Some 0x112233445566fffd. Proof. vm_compute; reflexivity. Qed.

‎src/Assembly/WithBedrock/SymbolicProofs.v‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1361,6 +1361,10 @@ Proof using Type.
13611361
Unshelve. all : match goal with H : context[push] |- _ => idtac | H : context[pop] |- _ => idtac | _ => shelve end; shelve_unifiable.
13621362
all: rewrite !Z.land_ones by lia; push_Zmod; pull_Zmod; f_equal; lia.
13631363

1364+
Unshelve. all : match goal with H : context[Syntax.imul] |- _ => idtac | _ => shelve end; shelve_unifiable.
1365+
(* one-operand imul: the symbolic sign extension [(x + 2^(s-1)) land ones s - 2^(s-1)] is [Z.signed s x] unfolded *)
1366+
all: cbv [Z.signed]; rewrite ?Z.add_opp_r, ?(Z.add_comm _ (Z.shiftl 1 _)); reflexivity.
1367+
13641368
Unshelve. all: shelve_unifiable.
13651369
all: fail_if_goals_remain ().
13661370
Qed.

0 commit comments

Comments
 (0)