diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index 2743bc5cfe..f11cf85292 100644 --- a/herd/AArch64Sem.ml +++ b/herd/AArch64Sem.ml @@ -1564,7 +1564,7 @@ module Make * +iico_data dependency between the event `ma` and `mop` or `mfault`, and an * iico_data dependency between `mv` and `mop` in case of a success. *) - let lift_pac_virt mop ma dir an ii domain = + let lift_pac_virt mop ma dir an ii branch domain = (* Addresses of memory operations must be canonical for the construction * of the rf, co and fr maps... *) let mfault ma a ft = @@ -1574,7 +1574,7 @@ module Make None ii >>! B.fault [AArch64Base.elr_el1, lbl_v] in - let mok ma = mop ma >>= M.ignore >>= B.next1T in + let mok ma = mop ma |> branch in check_pac_va_range mok ma mfault ii domain let lift_memtag_phy dir mop ma an ii mphy = @@ -1719,9 +1719,9 @@ Arguments: M.short (is_this_reg rA) (E.is_pred_txt (Some "color")) m else if checked then let mop ma = lift_memtag_virt mop ma dir an ii branch in - if pac then lift_pac_virt mop ma dir an ii domain else mop ma + if pac then lift_pac_virt mop ma dir an ii Fun.id domain else mop ma else if pac then - lift_pac_virt (mop Access.VIR) ma dir an ii domain + lift_pac_virt (mop Access.VIR) ma dir an ii branch domain else mop Access.VIR ma |> branch @@ -2264,13 +2264,13 @@ Arguments: (rmw_to_read rmw) ii - let do_cas_fail do_wb sz an rn ma mv mop tagcheck ii = + let do_cas_fail_with lift do_wb sz an rn ma mv mop tagcheck ii = let action checked ma = let do_action updatedb checked ma = (* Dir.W would force check for dbm bit: *) (* - if set then either update or not db bit per R_TXGHB *) (* - if unset raise Permission fault *) - lift_memop ~tag:"FAIL" rn Dir.W updatedb checked mop (to_perms "rw" sz) ma mv an ii + lift ~tag:"FAIL" rn Dir.W updatedb checked mop (to_perms "rw" sz) ma mv an ii in if do_wb then do_action true checked ma @@ -2304,14 +2304,13 @@ Arguments: else action memtag ma - let do_cas_fail_with_wb = do_cas_fail true - let do_cas_fail_no_wb = do_cas_fail false - - let do_cas sz an rn ma mv mop_success mop_fail_with_wb mop_fail_no_wb tagcheck ii = + let do_cas_with lift sz an rn ma mv mop_success mop_fail_with_wb mop_fail_no_wb tagcheck ii = + let do_cas_fail_with_wb = do_cas_fail_with lift true in + let do_cas_fail_no_wb = do_cas_fail_with lift false in M.altT ( (* CAS succeeds and generates an Explicit Write Effect *) (* there must be an update to the dirty bit of the TTD *) - lift_memop ~tag:"CAS" rn Dir.W true tagcheck mop_success (to_perms "rw" sz) ma mv an ii + lift ~tag:"CAS" rn Dir.W true tagcheck mop_success (to_perms "rw" sz) ma mv an ii )( (* CAS fails *) M.altT ( (* CAS generates an Explicit Write Effect *) @@ -2322,6 +2321,8 @@ Arguments: ) ) + let do_cas = do_cas_with (fun ~tag -> lift_memop ~tag) + let cas sz rmw rs rt rn ii = let an = rmw_to_read rmw in let read_rs = read_reg_data_sz sz rs ii @@ -3818,7 +3819,7 @@ Arguments: in (* Write to Rd depends on read from Shadow Stack *) M.short (E.is_mem_load) (is_this_reg rd) m in - lift_memop rA Dir.R false false + do_lift_memop rA Dir.R false false (fun ac ma _mv -> if Access.is_physical ac then M.bind_ctrldata ma (mop ac) @@ -3828,43 +3829,15 @@ Arguments: (M.unitT a_virt) mzero an - ii in + ii + Fun.id + DISide.Data + in (* Value writen to GCSPR depends on previous read *) let read e = (is_this_reg rA e) && (E.is_reg_load e ii.A.proc) and write e = (is_this_reg rA e) && (E.is_reg_store e ii.A.proc) in M.short read write m - (* - * Basically copy of lift_memop which allows mop to drive control flow - * (handy for BL{R}/RET instructions with GCS enabled) - *) - let lift_shadow_stack dir updatedb mop ma mv an ii = - let domain = DISide.Data in - let mop = apply_mv mop mv in - if kvm then - let mphy ma a_virt = - let ma = get_oa a_virt ma in - mop Access.PHY ma - in - (* lift_kvm dir updatedb mop ma an ii mphy in *) - let mfault ma a ft = emit_fault (Some a) ma dir an ft None ii in - let maccess a ma = - check_ptw ii.AArch64.proc dir updatedb false a ma an ii - (mop (Access.PTE domain) ma) - mphy - mfault - domain in - M.delay_kont "shadow_stack" - ma - (fun a ma -> - match Act.access_of_location_std (A.Location_global a) with - | Access.VIR|Access.PTE _ when not (A.V.is_instrloc a) -> - maccess a ma - | ac -> - mop ac ma) - else - mop Access.VIR ma - let blop v_ret write_linkreg branch bop ii = let open AArch64Base in let an = Annot.N @@ -3875,7 +3848,7 @@ Arguments: GCSSem.write ac an a v ii >>| write_reg rA a_virt ii >>| write_linkreg >>= M.ignore in - lift_shadow_stack Dir.W true + do_lift_memop rA Dir.W true false (fun ac ma mv -> let m = if is_branching && Access.is_physical ac then @@ -3887,10 +3860,13 @@ Arguments: let read e = (is_this_reg rA e) && (E.is_reg_load e ii.A.proc) and write e = (is_this_reg rA e) && (E.is_reg_store e ii.A.proc) in M.short read write m) + (to_perms "w" quad) (M.unitT a_virt) (M.unitT v_ret) an ii + Fun.id + DISide.Data let retop test i r ii = let open AArch64Base in @@ -3898,7 +3874,7 @@ Arguments: and rA = SysReg GCSPR_EL1 and off = MachSize.nbytes quad in read_reg_addr rA ii >>= fun a_virt -> - lift_shadow_stack Dir.R false + do_lift_memop rA Dir.R false false (fun ac ma mv -> let m = mv >>| @@ -3928,10 +3904,13 @@ Arguments: let m = M.short read write m in (* Branch depends on destination register (or LR) *) M.short (is_this_reg r) (E.is_bcc) m) + (to_perms "r" quad) (M.unitT a_virt) (read_reg_ord r ii) an ii + Fun.id + DISide.Data let gcsss1 r ii = let open AArch64Base in @@ -3951,7 +3930,7 @@ Arguments: branch >>*= fun () -> write_reg rA incoming ii >>= fun () -> B.nextSetT rA incoming in M.op Op.Eq data v >>= fun cond -> (* if data == cmpoperand then *) - M.assertT cond mok >>= M.ignore (* SetCurrentGCSPointer(incoming_pointer[63:3]:'000'); *) + M.assertT cond mok (* SetCurrentGCSPointer(incoming_pointer[63:3]:'000'); *) in let fault data = GCSSem.make_valid incoming >>= fun v -> @@ -3960,7 +3939,7 @@ Arguments: (fun cond action -> let open FaultType.AArch64 in (* GCSDataCheckException(GCSInstType_SS1); *) let mno = GCSSem.mk_fault action (GCSCheck SS1) ii in - M.assertT cond mno >>= M.ignore) + M.assertT cond mno) in let branch a = let cond1 = Some (Printf.sprintf "Valid([%s])" (V.pp_v a)) in @@ -4008,7 +3987,9 @@ Arguments: ) in let mv = read_reg_data rA ii in - do_cas quad Annot.N r ma mv mop_success mop_fail_with_wb mop_fail_no_wb false ii) + let lift_memop ~tag rA dir updatedb checked mop perms ma mv an ii = + do_lift_memop ~tag rA dir updatedb checked mop perms ma mv an ii Fun.id DISide.Data in + do_cas_with lift_memop quad Annot.N r ma mv mop_success mop_fail_with_wb mop_fail_no_wb false ii) let gcsss2 r ii = let open AArch64Base in @@ -4058,7 +4039,7 @@ Arguments: (* Register write and write to other stack depend on load from Shadow Stack *) let store e = (E.is_mem_store e) || (is_this_reg r e) in M.short (E.is_mem_load) store m in - lift_memop rA Dir.R false false + do_lift_memop rA Dir.R false false (fun ac ma _mv -> if Access.is_physical ac then M.bind_ctrldata ma (mop ac) @@ -4068,7 +4049,9 @@ Arguments: ma mzero an - ii) in + ii + Fun.id + DISide.Data) in (* Value writen to GCSPR depends on previous read *) let read e = (is_this_reg rA e) && (E.is_reg_load e ii.A.proc) and write e = (is_this_reg rA e) && (E.is_reg_store e ii.A.proc) in diff --git a/herd/eventsMonad.ml b/herd/eventsMonad.ml index 0156209200..5fec007e8b 100644 --- a/herd/eventsMonad.ml +++ b/herd/eventsMonad.ml @@ -577,7 +577,7 @@ Monad type: let do_aarch64_cas_ok (is_physical:bool) (prov_data: [`DataFromRRs | `DataFromRx]) (read_rn:'loc t) (read_rs:'v t) (read_rt: 'v t) - (write_rs:'v-> unit t) + (write_rs:'v-> 'a t) (read_mem: 'loc -> 'v t) (write_mem: 'loc -> 'v -> unit t) (branch: 'loc -> unit t) (req: 'v -> 'v -> unit t) @@ -597,7 +597,7 @@ Monad type: let ov,cl_rm,es_rm = Evt.as_singleton_nospecul read_mem and (),cl_wm,es_wm= Evt.as_singleton_nospecul write_mem in let eiid,write_rs = write_rs ov eiid in - let (),cl_wrs,es_wrs = Evt.as_singleton_nospecul write_rs in + let r,cl_wrs,es_wrs = Evt.as_singleton_nospecul write_rs in let eiid,branch = branch a eiid in let (),cl_br,es_br = Evt.as_singleton_nospecul branch in let eiid,eqm = req ov cv eiid in @@ -606,7 +606,7 @@ Monad type: let es = E.aarch64_cas is_physical prov_data es_rn es_rs es_rt es_wrs es_rm es_wm es_br in let cls = cl_a@cl_cv@cl_nv@cl_rm@cl_wm@cl_wrs@cl_br@cl_eq in - eiid,Evt.add ((),cls,es) acts) + eiid,Evt.add (r,cls,es) acts) acts_rn (eiid,Evt.empty) in eiid,(acts, None) @@ -656,7 +656,7 @@ Monad type: write_mem) let aarch64_cas_ok (is_physical: bool) (read_rn: 'loc t) (read_rs: 'v t) - (read_rt: 'v t) (write_rs: 'v -> unit t) (read_mem: 'loc -> 'v t) + (read_rt: 'v t) (write_rs: 'v -> 'a t) (read_mem: 'loc -> 'v t) (write_mem: 'loc -> 'v -> unit t) (branch: 'loc -> unit t) (req: 'v -> 'v -> unit t) = let do_ prov_data = do_aarch64_cas_ok is_physical prov_data read_rn read_rs read_rt @@ -665,7 +665,7 @@ Monad type: altT (do_ `DataFromRRs) (do_ `DataFromRx) let aarch64_cas_no (is_physical: bool) (read_rn: 'loc t) - (read_rs: 'v t) (write_rs: 'v -> unit t) (read_mem: 'loc -> 'v t) + (read_rs: 'v t) (write_rs: 'v -> 'a t) (read_mem: 'loc -> 'v t) (write_mem: 'loc -> 'v -> unit t) (branch: 'loc -> unit t) (rne: 'v -> 'v -> unit t) eiid = let eiid,read_rn = read_rn eiid in @@ -681,7 +681,7 @@ Monad type: let eiid,write_mem = write_mem a ov eiid in let (),cl_wm,es_wm= Evt.as_singleton_nospecul write_mem in let eiid,write_rs = write_rs ov eiid in - let (),cl_wrs,es_wrs = Evt.as_singleton_nospecul write_rs in + let r,cl_wrs,es_wrs = Evt.as_singleton_nospecul write_rs in let eiid,branch = branch a eiid in let (),cl_br,es_br = Evt.as_singleton_nospecul branch in let eiid,(acts_n,spec_n) = rne ov cv eiid in @@ -700,7 +700,7 @@ Monad type: es_wm es_br in let cls = cl_a@cl_cv@cl_rm@cl_wm@cl_wrs@cl_br@cl_ne in - eiid,Evt.add ((),cls,es) acts) acts_n (eiid,acts)) + eiid,Evt.add (r,cls,es) acts) acts_n (eiid,acts)) acts_rn (eiid,Evt.empty) in eiid,(acts, None) diff --git a/herd/monad.mli b/herd/monad.mli index 0c0dfecc0e..1c1cfd10f1 100644 --- a/herd/monad.mli +++ b/herd/monad.mli @@ -208,16 +208,16 @@ module type S = val aarch64_cas_no : bool -> (* physical access *) 'loc t -> 'v t -> - ('v -> unit t) -> ('loc -> 'v t) -> ('loc -> 'v -> unit t) -> + ('v -> 'a t) -> ('loc -> 'v t) -> ('loc -> 'v -> unit t) -> ('loc -> unit t) -> - ('v -> 'v -> unit t) -> unit t + ('v -> 'v -> unit t) -> 'a t val aarch64_cas_ok : bool -> (* physical access *) 'loc t -> 'v t -> 'v t -> - ('v -> unit t) -> ('loc -> 'v t) -> ('loc -> 'v -> unit t) -> + ('v -> 'a t) -> ('loc -> 'v t) -> ('loc -> 'v -> unit t) -> ('loc -> unit t) -> - ('v -> 'v -> unit t) -> unit t + ('v -> 'v -> unit t) -> 'a t (* Temporary morello variation of CAS *) val aarch64_cas_ok_morello : 'loc t -> 'v t -> 'v t -> ('loc -> 'v -> unit t) -> unit t diff --git a/herd/tests/instructions/AArch64.gcs/G005.litmus.expected b/herd/tests/instructions/AArch64.gcs/G005.litmus.expected index 16cdb9f402..7ab0a03680 100644 --- a/herd/tests/instructions/AArch64.gcs/G005.litmus.expected +++ b/herd/tests/instructions/AArch64.gcs/G005.litmus.expected @@ -1,12 +1,12 @@ Test G005 Required States 2 -0:X1=0; Fault(P0,GCS:POPM); Fault(P0,GCS:SS2); +0:X1=0; Fault(P0,GCS:SS2); 0:X1=4; ~Fault(P0); No Witnesses -Positive: 2 Negative: 4 +Positive: 2 Negative: 2 Flag Guarded-Control-Stack-is-work-in-progress Condition forall (0:X1=4 /\ not (fault(P0))) -Observation G005 Sometimes 2 4 +Observation G005 Sometimes 2 2 Hash=e49698900201be45b23a8f9f3ac0cb91 diff --git a/herd/tests/instructions/AArch64.gcs/G007.litmus b/herd/tests/instructions/AArch64.gcs/G007.litmus new file mode 100644 index 0000000000..b0ef46f769 --- /dev/null +++ b/herd/tests/instructions/AArch64.gcs/G007.litmus @@ -0,0 +1,13 @@ +AArch64 G007 +variant=shadowstack +{ + SS(x,1) = ssval_t: {1}; + 0:GCSPR_EL1=&x[0]; +} + + P0 ; +L0: ; + GCSPOPM X1 ; + MOV X2,#1 ; + +forall fault(P0:L0,GCS:POPM) /\ 0:X2=0 \ No newline at end of file diff --git a/herd/tests/instructions/AArch64.gcs/G007.litmus.expected b/herd/tests/instructions/AArch64.gcs/G007.litmus.expected new file mode 100644 index 0000000000..0549122e0e --- /dev/null +++ b/herd/tests/instructions/AArch64.gcs/G007.litmus.expected @@ -0,0 +1,11 @@ +Test G007 Required +States 1 +0:X2=0; Fault(P0:L0,GCS:POPM); +Ok +Witnesses +Positive: 1 Negative: 0 +Flag Guarded-Control-Stack-is-work-in-progress +Condition forall (fault(P0:L0,GCS:POPM) /\ 0:X2=0) +Observation G007 Always 1 0 +Hash=6a7093cbe2a7bbb87e5456efe4cf9513 + diff --git a/herd/tests/instructions/AArch64.gcs/G008.litmus b/herd/tests/instructions/AArch64.gcs/G008.litmus new file mode 100644 index 0000000000..440fcd935f --- /dev/null +++ b/herd/tests/instructions/AArch64.gcs/G008.litmus @@ -0,0 +1,15 @@ +AArch64 G008 +variant=shadowstack +{ + SS(x,1) = ssval_t: {1}; + 0:GCSPR_EL1=&x[0]; +} + + P0 ; + ADR X29,L1 ; +L0: ; + RET X29 ; + MOV X2,#1 ; +L1: ; + +forall fault(P0:L0,GCS:PRET) /\ 0:X2=0 \ No newline at end of file diff --git a/herd/tests/instructions/AArch64.gcs/G008.litmus.expected b/herd/tests/instructions/AArch64.gcs/G008.litmus.expected new file mode 100644 index 0000000000..d301debad2 --- /dev/null +++ b/herd/tests/instructions/AArch64.gcs/G008.litmus.expected @@ -0,0 +1,11 @@ +Test G008 Required +States 1 +0:X2=0; Fault(P0:L0,GCS:PRET); +Ok +Witnesses +Positive: 1 Negative: 0 +Flag Guarded-Control-Stack-is-work-in-progress +Condition forall (fault(P0:L0,GCS:PRET) /\ 0:X2=0) +Observation G008 Always 1 0 +Hash=d714c8d3cf36a41866635546960ebdbb + diff --git a/herd/tests/instructions/AArch64.gcs/G009.litmus b/herd/tests/instructions/AArch64.gcs/G009.litmus new file mode 100644 index 0000000000..666adf3421 --- /dev/null +++ b/herd/tests/instructions/AArch64.gcs/G009.litmus @@ -0,0 +1,15 @@ +AArch64 G009 +variant=shadowstack +{ + SS(x,1) = ssval_t: {1}; + SS(y,2) = ssval_t: {0, 0}; + 0:GCSPR_EL1=&x[0]; + 0:X0=&y[0] +} + + P0 ; +L0: ; + GCSSS1 X0 ; + MOV X2,#1 ; + +forall fault(P0:L0,GCS:SS1) /\ 0:X2=0 \ No newline at end of file diff --git a/herd/tests/instructions/AArch64.gcs/G009.litmus.expected b/herd/tests/instructions/AArch64.gcs/G009.litmus.expected new file mode 100644 index 0000000000..2be2a4b38c --- /dev/null +++ b/herd/tests/instructions/AArch64.gcs/G009.litmus.expected @@ -0,0 +1,11 @@ +Test G009 Required +States 1 +0:X2=0; Fault(P0:L0,GCS:SS1); +Ok +Witnesses +Positive: 2 Negative: 0 +Flag Guarded-Control-Stack-is-work-in-progress +Condition forall (fault(P0:L0,GCS:SS1) /\ 0:X2=0) +Observation G009 Always 2 0 +Hash=e3981f68ce692f53ca99113860aa2ef4 + diff --git a/herd/tests/instructions/AArch64.gcs/G010.litmus b/herd/tests/instructions/AArch64.gcs/G010.litmus new file mode 100644 index 0000000000..ad1f650225 --- /dev/null +++ b/herd/tests/instructions/AArch64.gcs/G010.litmus @@ -0,0 +1,15 @@ +AArch64 G010 +variant=shadowstack +{ + SS(x,1) = ssval_t: {1}; + SS(y,2) = ssval_t: {0, 0}; + 0:GCSPR_EL1=&x[0]; + 0:X0=&y[0] +} + + P0 ; +L0: ; + GCSSS2 X0 ; + MOV X2,#1 ; + +forall fault(P0:L0,GCS:SS2) /\ 0:X2=0 \ No newline at end of file diff --git a/herd/tests/instructions/AArch64.gcs/G010.litmus.expected b/herd/tests/instructions/AArch64.gcs/G010.litmus.expected new file mode 100644 index 0000000000..0115efcada --- /dev/null +++ b/herd/tests/instructions/AArch64.gcs/G010.litmus.expected @@ -0,0 +1,11 @@ +Test G010 Required +States 1 +0:X2=0; Fault(P0:L0,GCS:SS2); +Ok +Witnesses +Positive: 1 Negative: 0 +Flag Guarded-Control-Stack-is-work-in-progress +Condition forall (fault(P0:L0,GCS:SS2) /\ 0:X2=0) +Observation G010 Always 1 0 +Hash=fe95805b028a64198d39c03774439baf +