feat(cerisier): add support for TEE and attestation

lib/ast.ml

@@ -46,7 +46,7 @@ type machine_op =
   | PromoteU of regname
   | EInit of regname * regname
   | EDeInit of regname * regname
-  | EStoreId of regname * regname
+  | EStoreId of regname * regname * regname
   | IsUnique of regname * regname
   | Fail
   | Halt

lib/encode.ml

@@ -243,7 +243,9 @@ let decode_reg (i : Z.t) : regname = if i = Z.zero then PC else Reg (Z.to_int @@
 
 let rec split_int (i : Z.t) : Z.t * Z.t =
   let open Z in
-  if i = zero then (zero, zero)
+  if i = ~$(-1) then
+    raise @@ DecodeException (Printf.sprintf "Error decoding integer: %0x" (Z.to_int i))
+  else if i = zero then (zero, zero)
   else
     let x1 = i land one in
     let y1 = (i asr 1) land one in
@@ -376,7 +378,8 @@ let encode_machine_op (s : machine_op) : Z.t =
   | PromoteU r -> ~$0x37 ^! encode_reg r
   | EInit (r1, r2) -> ~$0x38 ^! encode_int_int (encode_reg r1) (encode_reg r2)
   | EDeInit (r1, r2) -> ~$0x39 ^! encode_int_int (encode_reg r1) (encode_reg r2)
-  | EStoreId (r1, r2) -> ~$0x3a ^! encode_int_int (encode_reg r1) (encode_reg r2)
+  | EStoreId (r1, r2, r3) ->
+      ~$0x3a ^! encode_int_int (encode_reg r1) (encode_int_int (encode_reg r2) (encode_reg r3))
   | IsUnique (r1, r2) -> ~$0x3b ^! encode_int_int (encode_reg r1) (encode_reg r2)
   | Fail -> ~$0x3c
   | Halt -> ~$0x3d
@@ -387,6 +390,7 @@ let decode_machine_op (i : Z.t) : machine_op =
   (* in *)
   let opc = Z.extract i 0 8 in
   let payload = Z.(i asr 8) in
+
   (* Jmp *)
   if opc = ~$0x00 then Jmp (decode_reg payload)
   else if (* Jnz *)
@@ -591,7 +595,6 @@ let decode_machine_op (i : Z.t) : machine_op =
     StoreU (r, c1, c2)
   else if (* PromoteU *)
           opc = ~$0x37 && !Parameters.flags.unitialized then PromoteU (decode_reg payload)
-
   else if (* EInit *)
           opc = ~$0x38 then
     let r1_enc, r2_enc = decode_int payload in
@@ -606,17 +609,18 @@ let decode_machine_op (i : Z.t) : machine_op =
     EDeInit (r1, r2)
   else if (* EStoreId *)
           opc = ~$0x3a then
-    let r1_enc, r2_enc = decode_int payload in
+    let r1_enc, payload' = decode_int payload in
+    let r2_enc, r3_enc = decode_int payload' in
     let r1 = decode_reg r1_enc in
     let r2 = decode_reg r2_enc in
-    EStoreId (r1, r2)
+    let r3 = decode_reg r3_enc in
+    EStoreId (r1, r2, r3)
   else if (* IsUnique *)
           opc = ~$0x3b then
     let r1_enc, r2_enc = decode_int payload in
     let r1 = decode_reg r1_enc in
     let r2 = decode_reg r2_enc in
     IsUnique (r1, r2)
-
   else if (* Fail *)
           opc = ~$0x3c then Fail
   else if (* Halt *)

lib/interactive_ui.ml

@@ -165,11 +165,23 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
       I.hsnap ~align:`Right width (I.string A.empty (Pretty_printer.string_of_regname r))
   end
 
+  module EC_register = struct
+    (* pc or rNN *)
+    let width = Regname.width
+    let ui = I.hsnap ~align:`Right width (I.string A.empty Pretty_printer.string_of_ec)
+  end
+
+  module EC_counter = struct
+    let width = Word.width
+    let ui ?(attr = A.empty) z = I.hsnap ~align:`Right width (I.string attr (Int.ui width z))
+  end
+
   module Regs_panel = struct
     (* <reg>: <word>  <reg>: <word>  <reg>: <word>
        <reg>: <word>  <reg>: <word>
+       EC: <ecounter>
     *)
-    let ui width (regs : Machine.reg_state) =
+    let ui width (regs : Machine.reg_state) (ecounter : Machine.e_counter) =
       let reg_width = Regname.width + 2 + Word.width + 2 in
       let ncols = max 1 (width / reg_width) in
       let nregs_per_col = 33. (* nregs *) /. float ncols |> ceil |> int_of_float in
@@ -185,7 +197,32 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
             I.empty col
           <|> loop false regs
       in
-      loop true (Machine.RegMap.to_seq regs |> List.of_seq) |> I.hsnap ~align:`Left width
+      let ec_reg =
+        (* I.empty *)
+        I.empty <|> EC_register.ui <|> I.string A.empty ": " <|> EC_counter.ui ecounter
+      in
+      loop true (Machine.RegMap.to_seq regs |> List.of_seq) <-> ec_reg |> I.hsnap ~align:`Left width
+  end
+
+  module Identity = struct
+    let width = 1 + int_of_float (floor @@ (log (float max_int) /. log 16.))
+    let ui ?(attr = A.empty) z = I.hsnap ~align:`Right width (I.string attr (Int.ui width z))
+  end
+
+  module ETable_panel = struct
+    (* <eid>: <identity>
+       <eid>: <identity>
+       <eid>: <identity>
+    *)
+    let ui width (etbl : Machine.e_table) =
+      (* let eid_width = EC_counter.width + 2 + Identity.width +2 in *)
+      let render_etbl enclaves =
+        List.fold_left
+          (fun img (eid, (id, _)) ->
+            img <-> (I.empty <|> EC_counter.ui eid <|> I.string A.empty ": " <|> Identity.ui id))
+          I.empty enclaves
+      in
+      render_etbl (Machine.ETableMap.to_seq etbl |> List.of_seq) |> I.hsnap ~align:`Left width
   end
 
   module Instr = struct
@@ -315,9 +352,10 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
       let start_stk = upd_stk stk height start_stk 2 in
 
       let img_of_dataline = render_prog width pc (addr_show start_prog) in
-      let img_of_stack =
-        if show_stack then render_stack width stk (addr_show start_stk) else I.empty
-      in
+      (* let img_of_stack = *)
+      (*   if show_stack then render_stack width stk (addr_show start_stk) else I.empty *)
+      (* in *)
+      let img_of_stack = if show_stack then I.empty else I.empty in
 
       (img_of_dataline </> img_of_stack, start_prog, start_stk)
   end
@@ -345,10 +383,13 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
         let term_width, term_height = Term.size term in
         let reg = (snd m).Machine.reg in
         let mem = (snd m).Machine.mem in
-        let regs_img = Regs_panel.ui term_width reg in
+        let etbl = (snd m).Machine.etbl in
+        let ec = (snd m).Machine.ec in
+        let regs_img = Regs_panel.ui term_width reg ec in
+        let etbl_img = ETable_panel.ui term_width etbl in
         let mem_img, panel_start, panel_stk =
           Program_panel.ui ~upd_prog:update_prog ~upd_stk:update_stk ~show_stack
-            (term_height - 1 - I.height regs_img)
+            (term_height - 1 - I.height regs_img - I.height etbl_img)
             term_width mem (Machine.RegMap.find Ast.PC reg)
             (if !flags.stack then Machine.RegMap.find Ast.stk reg else Ast.I Z.zero)
             !prog_panel_start !stk_panel_start
@@ -359,7 +400,7 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
           I.hsnap ~align:`Right term_width
             (I.string A.empty "machine state: " <|> Exec_state.ui (fst m))
         in
-        let img = regs_img <-> mach_state_img <-> mem_img in
+        let img = regs_img <-> mach_state_img <-> etbl_img <-> mem_img in
         Term.image term img;
         (* watch for a relevant event *)
         let rec process_events () =
@@ -421,6 +462,9 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
               | _ -> loop ~update_prog:Program_panel.follow_addr show_stack m history)
           | `Key (`ASCII 's', _) ->
               loop ~update_prog:Program_panel.id (toggle_show_stack show_stack) m history
+          | `Key (`ASCII '$', _) ->
+              loop ~update_prog:Program_panel.follow_addr ~update_stk:Program_panel.follow_addr
+                show_stack (Machine.run m) (m :: history)
           | `Key (`ASCII ' ', _) -> (
               match Machine.step m with
               | Some m' ->

lib/ir.ml

@@ -63,7 +63,7 @@ type machine_op =
   | PromoteU of regname
   | EInit of regname * regname
   | EDeInit of regname * regname
-  | EStoreId of regname * regname
+  | EStoreId of regname * regname * regname
   | IsUnique of regname * regname
   | Fail
   | Halt
@@ -226,7 +226,8 @@ let translate_instr (envr : env) (instr : machine_op) : Ast.machine_op =
   | PromoteU r -> Ast.PromoteU (translate_regname r)
   | EInit (r1, r2) -> Ast.EInit (translate_regname r1, translate_regname r2)
   | EDeInit (r1, r2) -> Ast.EDeInit (translate_regname r1, translate_regname r2)
-  | EStoreId (r1, r2) -> Ast.EStoreId (translate_regname r1, translate_regname r2)
+  | EStoreId (r1, r2, r3) ->
+      Ast.EStoreId (translate_regname r1, translate_regname r2, translate_regname r3)
   | IsUnique (r1, r2) -> Ast.IsUnique (translate_regname r1, translate_regname r2)
   | Fail -> Ast.Fail
   | Halt -> Ast.Halt

lib/machine.ml

@@ -26,7 +26,7 @@ type exec_state = Running | Halted | Failed
 type reg_state = word RegMap.t
 type mem_state = word MemMap.t
 type e_table = (eid * e_counter) ETableMap.t
-type exec_conf = { reg : reg_state; mem : mem_state; etbl : e_table ; ec : e_counter }
+type exec_conf = { reg : reg_state; mem : mem_state; etbl : e_table; ec : e_counter }
 
 (* using a record to have notation similar to the paper *)
 type mchn = exec_state * exec_conf
@@ -73,23 +73,28 @@ let get_reg (r : regname) ({ reg; _ } : exec_conf) : word = RegMap.find r reg
 let ( @! ) x y = get_reg x y
 
 let upd_reg (r : regname) (w : word) ({ reg; mem; etbl; ec } : exec_conf) : exec_conf =
-  { reg = RegMap.add r w reg; mem ; etbl ; ec}
+  { reg = RegMap.add r w reg; mem; etbl; ec }
 
 let get_mem (addr : Z.t) (conf : exec_conf) : word option = MemMap.find_opt addr conf.mem
 let ( @? ) x y = get_mem x y
 
-let upd_mem (addr : Z.t) (w : word) ({ reg; mem ; etbl ; ec } : exec_conf) : exec_conf =
-  { reg; mem = MemMap.add addr w mem ; etbl ; ec }
+let upd_mem (addr : Z.t) (w : word) ({ reg; mem; etbl; ec } : exec_conf) : exec_conf =
+  { reg; mem = MemMap.add addr w mem; etbl; ec }
 
 let get_etbl (etbl_idx : Z.t) (conf : exec_conf) : (eid * e_counter) option =
   ETableMap.find_opt etbl_idx conf.etbl
 
-let upd_etbl (etbl_idx : Z.t) (identity : eid) (ecounter : e_counter) ({ reg; mem ; etbl ; ec } : exec_conf) : exec_conf =
-  { reg; mem ; etbl = ETableMap.add etbl_idx (identity, ecounter) etbl ; ec }
+let upd_etbl (etbl_idx : Z.t) (identity : eid) (ecounter : e_counter)
+    ({ reg; mem; etbl; ec } : exec_conf) : exec_conf =
+  { reg; mem; etbl = ETableMap.add etbl_idx (identity, ecounter) etbl; ec }
 
-let upd_ec (n : e_counter) ({ reg; mem ; etbl ; _ } : exec_conf) : exec_conf =
-  { reg; mem ; etbl ; ec = n }
+let del_etbl (etbl_idx : Z.t) ({ reg; mem; etbl; ec } : exec_conf) : exec_conf =
+  { reg; mem; etbl = ETableMap.remove etbl_idx etbl; ec }
 
+let upd_ec (n : e_counter) ({ reg; mem; etbl; _ } : exec_conf) : exec_conf =
+  { reg; mem; etbl; ec = n }
+
+let incr_ec (conf : exec_conf) : exec_conf = upd_ec Z.(conf.ec + ~$1) conf
 
 let init_mem_state (addr_start : Z.t) (prog : t) : mem_state =
   let zeroed_mem =
@@ -118,8 +123,9 @@ let init_mem_state (addr_start : Z.t) (prog : t) : mem_state =
   in
   MemMap.add_seq enc_prog zeroed_mem
 
-let init (initial_regs : reg_state) (initial_mems : mem_state) (initial_etbl : e_table) (initial_ec : e_counter) =
-  (Running, { reg = initial_regs; mem = initial_mems ; etbl = initial_etbl ; ec = initial_ec })
+let init (initial_regs : reg_state) (initial_mems : mem_state) (initial_etbl : e_table)
+    (initial_ec : e_counter) =
+  (Running, { reg = initial_regs; mem = initial_mems; etbl = initial_etbl; ec = initial_ec })
 
 let get_word (conf : exec_conf) (roc : reg_or_const) : word =
   match roc with Register r -> get_reg r conf | Const i -> I i
@@ -207,53 +213,36 @@ let is_cap (sb : sealable) = match sb with Cap _ -> true | _ -> false
 
 let get_scap (w : word) : sealable option =
   match w with
-  | Sealable (Cap (p,l,b,e,a)) -> Some (Cap (p,l,b,e,a))
-  | Sealed (_, (Cap (p,l,b,e,a))) -> Some (Cap (p,l,b,e,a))
+  | Sealable (Cap (p, l, b, e, a)) -> Some (Cap (p, l, b, e, a))
+  | Sealed (_, Cap (p, l, b, e, a)) -> Some (Cap (p, l, b, e, a))
   | _ -> None
 
 let overlap_word (w1 : word) (w2 : word) : bool =
-  match get_scap w1, get_scap w2 with
-  | Some (Cap (_,_,b1,e1,_)), Some (Cap (_,_,b2,e2,_)) ->
-      if (b1 < b2)
-      then (Infinite_z.z_leq b2 (Infinite_z.sub_z e1 Z.one))
-      else (Infinite_z.z_leq b1 (Infinite_z.sub_z e2 Z.one))
-  | _,_ -> false
+  match (get_scap w1, get_scap w2) with
+  | Some (Cap (_, _, b1, e1, _)), Some (Cap (_, _, b2, e2, _)) ->
+      if b1 < b2 then Infinite_z.z_lt b2 e1 else Infinite_z.z_lt b1 e2
+  | _, _ -> false
 
 (* sweep all the register, excluding the register src. *)
 (* Returns false if there exists an overlapping word *)
 let sweep_registers_reg (conf : exec_conf) (src : regname) : bool =
   let w = get_reg src conf in
-  RegMap.for_all
-      (fun r w' ->
-        if r = src
-        then true
-        else not (overlap_word w w'))
-      conf.reg
+  RegMap.for_all (fun r w' -> if r = src then true else not (overlap_word w w')) conf.reg
 
 let sweep_registers_mem (conf : exec_conf) (a : Z.t) : bool =
   match get_mem a conf with
   | None -> false
-  | Some w ->
-      RegMap.for_all
-          (fun _ w' -> not (overlap_word w w'))
-          conf.reg
-
+  | Some w -> RegMap.for_all (fun _ w' -> not (overlap_word w w')) conf.reg
 
 let sweep_memory_reg (conf : exec_conf) (src : regname) : bool =
   let w = get_reg src conf in
-  MemMap.for_all (fun _ w' -> not (overlap_word w w'))
-      conf.mem
+  MemMap.for_all (fun _ w' -> not (overlap_word w w')) conf.mem
 
 let sweep_memory_mem (conf : exec_conf) (a : Z.t) : bool =
   match get_mem a conf with
   | None -> false
   | Some w ->
-      MemMap.for_all (fun a' w' ->
-            if a' = a
-            then true
-            else not (overlap_word w w'))
-          conf.mem
-
+      MemMap.for_all (fun a' w' -> if a' = a then true else not (overlap_word w w')) conf.mem
 
 let sweep_reg (conf : exec_conf) (src : regname) : bool =
   let unique_mem = sweep_memory_reg conf src in
@@ -567,16 +556,72 @@ let exec_single (conf : exec_conf) : mchn =
                     !>(upd_reg r (Sealable (Cap (p', g, b, e', a))) conf)
                 | _ -> fail_state)
             | _ -> fail_state)
-        | EInit (_, _) -> fail_state
-        | EDeInit (_, _) -> fail_state
-        | EStoreId (_, _) -> fail_state
-        | IsUnique (rdst, rsrc) ->
+        | EInit (rdst, rsrc) -> (
+            match rsrc @! conf with
+            | Sealable (Cap (p, _, b, e, _)) when can_read p && is_exec p -> (
+                match b @? conf with
+                | Some (Sealable (Cap (p', _, b', e', _))) when can_read p' && can_write p' ->
+                    let isunique_code = sweep_reg conf rsrc in
+                    let isunique_data = sweep_addr conf b in
+                    if isunique_data then
+                      if isunique_code then
+                        let ot = Z.(~$2 * conf.ec) in
+                        let seal_keys =
+                          Sealable (SealRange ((true, true), Global, ot, Z.(ot + ~$2), ot))
+                        in
+                        let to_list mem = MemMap.bindings mem in
+                        let region_filter b e a _ = b <= a && Infinite_z.z_leq a e in
+                        let region b e =
+                          List.map
+                            (fun (_, w) -> w)
+                            (to_list (MemMap.filter (region_filter b e) conf.mem))
+                        in
+                        let code_region = region Z.(b + ~$1) e in
+                        let data_region = region b' e' in
+                        let enclave_region = List.append code_region data_region in
+                        let identity : Z.t = Z.of_int (Hashtbl.hash enclave_region) in
+
+                        let conf_etbl' = upd_etbl conf.ec identity conf.ec conf in
+                        let conf_mem' = upd_mem b' seal_keys conf_etbl' in
+                        let conf_ec' = incr_ec conf_mem' in
+                        (* upd_ec Z.(conf.ec + ~$1) conf_mem' in *)
+                        !>(upd_reg rdst (Sealable (Cap (E, Global, b, e, Z.(b + ~$1)))) conf_ec')
+                      else (Failed, upd_reg rdst (I ~$3) conf)
+                    else (Failed, upd_reg rdst (I ~$4) conf)
+                    (* fail_state *)
+                | _ -> fail_state)
+            | _ -> fail_state)
+        | EDeInit (rdst, rsrc) -> (
+            match rsrc @! conf with
+            | Sealable (SealRange ((true, true), Global, b, e, _)) when e = Z.(b + ~$2) ->
+                if Z.is_even b then
+                  let eid = Z.(b / ~$2) in
+                  let res = match get_etbl eid conf with Some _ -> I ~$1 | None -> I ~$0 in
+                  !>(upd_reg rdst res (del_etbl eid conf))
+                else fail_state
+            | _ -> fail_state)
+        | EStoreId (rdst, rsrc1, rsrc2) -> (
+            match rsrc1 @! conf with
+            | I s -> (
+                let eid =
+                  let open Z in
+                  if is_even s then s / of_int 2 else (s - Z.one) / of_int 2
+                in
+                match get_etbl eid conf with
+                | Some (identity, _) -> (
+                    match rsrc2 @! conf with
+                    | Sealable (Cap (p, _, b, e, a))
+                      when can_write p && b <= a && Infinite_z.z_leq a e ->
+                        !>(upd_mem a (I identity) (upd_reg rdst (I ~$1) conf))
+                        (* !> (upd_mem a (I ~$357232418) (upd_reg rdst (I ~$1) conf)) *)
+                    | _ -> fail_state)
+                | None -> !>(upd_reg rdst (I ~$0) conf))
+            | _ -> fail_state)
+        | IsUnique (rdst, rsrc) -> (
             match rsrc @! conf with
-            | Sealable (Cap _)
-            | Sealed (_, Cap _) ->
-                !> (upd_reg rdst (I (if sweep_reg conf rsrc then Z.one else Z.zero)) conf)
-            | _ -> fail_state
-    )
+            | Sealable (Cap _) | Sealed (_, Cap _) ->
+                !>(upd_reg rdst (I (if sweep_reg conf rsrc then Z.one else Z.zero)) conf)
+            | _ -> fail_state))
   else fail_state
 
 let step (m : mchn) : mchn option =