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,6 +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 = ~$(-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
@@ -376,7 +379,7 @@ 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 *)
@@ -606,10 +610,12 @@ 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

lib/interactive_ui.ml

@@ -165,11 +165,27 @@ 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,9 +201,39 @@ 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
     let ui (i : Ast.machine_op) = I.string A.(fg green) (Pretty_printer.string_of_machine_op i)
   end
@@ -315,8 +361,11 @@ 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
+        if show_stack then I.empty else I.empty
       in
 
       (img_of_dataline </> img_of_stack, start_prog, start_stk)
@@ -345,10 +394,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 +411,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,7 +473,10 @@ 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 ' ', _) -> (
+          | `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' ->
                   loop ~update_prog:Program_panel.follow_addr ~update_stk:Program_panel.follow_addr

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,7 @@ 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

@@ -86,10 +86,14 @@ let get_etbl (etbl_idx : Z.t) (conf : exec_conf) : (eid * e_counter) option =
 
 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 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 =
@@ -215,8 +219,8 @@ 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))
+      then (Infinite_z.z_lt b2 e1)
+      else (Infinite_z.z_lt b1 e2)
   | _,_ -> false
 
 (* sweep all the register, excluding the register src. *)
@@ -567,9 +571,91 @@ 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
+
+        | EInit (rdst, rsrc) ->
+            begin
+            match rsrc @! conf with
+            | Sealable (Cap (p,_,b,e,_)) when can_read p && is_exec p ->
+                begin
+                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 = (fun 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
+                end
+            | _ ->
+                fail_state
+            end
+        | EDeInit (rdst, rsrc) ->
+            begin
+            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
+            end
+        | EStoreId (rdst, rsrc1 , rsrc2) ->
+            begin
+            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
+            end
         | IsUnique (rdst, rsrc) ->
             match rsrc @! conf with
             | Sealable (Cap _)

lib/parameters.ml

@@ -219,7 +219,6 @@ let check_machine_op (i : Ast.machine_op) =
   | Jnz (r1, r2)
   | EInit (r1, r2)
   | EDeInit (r1, r2)
-  | EStoreId (r1, r2)
   | IsUnique (r1, r2) ->
       check_register r1;
       check_register r2
@@ -237,6 +236,7 @@ let check_machine_op (i : Ast.machine_op) =
       check_register r1;
       check_zreg zr2;
       check_zreg zr3
+  | EStoreId (r1, r2, r3)
   | Seal (r1, r2, r3) | UnSeal (r1, r2, r3) ->
       check_register r1;
       check_register r2;

lib/parser.mly

@@ -54,7 +54,7 @@ main:
   | PROMOTEU; r = reg; p = main ; { PromoteU r :: p }
   | EINIT; r1 = reg; r2 = reg; p = main; { EInit (r1, r2) :: p }
   | EDEINIT; r1 = reg; r2 = reg; p = main; { EDeInit (r1, r2) :: p }
-  | ESTOREID; r1 = reg; r2 = reg; p = main; { EStoreId (r1, r2) :: p }
+  | ESTOREID; r1 = reg; r2 = reg; r3 = reg ; p = main; { EStoreId (r1, r2, r3) :: p }
   | ISUNIQUE; r1 = reg; r2 = reg; p = main; { IsUnique (r1, r2) :: p }
   | FAIL; p = main; { Fail :: p }
   | HALT; p = main; { Halt :: p }

lib/pretty_printer.ml

@@ -11,6 +11,8 @@ let string_of_regname (r : regname) : string =
       else if r = ddc then "ddc"
       else "r" ^ string_of_int i
 
+let string_of_ec : string = "EC"
+
 let string_of_seal_perm (p : seal_perm) : string =
   match p with false, false -> "SO" | true, false -> "S" | false, true -> "U" | true, true -> "SU"
 
@@ -100,7 +102,7 @@ let string_of_machine_op (s : machine_op) : string =
   | PromoteU r -> "promoteU" ^- string_of_regname r
   | EInit (r1, r2) -> "EInit" ^- string_of_rr r1 r2
   | EDeInit (r1, r2) -> "EDeInit" ^- string_of_rr r1 r2
-  | EStoreId (r1, r2) -> "EStoreId" ^- string_of_rr r1 r2
+  | EStoreId (r1, r2, r3) -> "EStoreId" ^- string_of_rrr r1 r2 r3
   | IsUnique (r1, r2) -> "IsUnique" ^- string_of_rr r1 r2
   | Fail -> "fail"
   | Halt -> "halt"

lib/program.ml

@@ -29,5 +29,8 @@ let init_machine (prog : Ast.t) (init_regs : Ast.word Machine.RegMap.t) : Machin
   (* TODO lookup the PC *)
   let init_mems = Machine.init_mem_state addr_start prog in
   let init_etbl = Machine.ETableMap.empty in
+  (* let init_etbl = Machine.ETableMap.add Z.zero (Z.of_int (Hashtbl.hash init_mems), Z.zero) init_etbl in *)
+  (* let init_etbl = Machine.ETableMap.add Z.one (Z.of_int (Hashtbl.hash init_etbl), Z.one) init_etbl in *)
+  (* let init_etbl = Machine.ETableMap.add (Z.of_int 2) (Z.of_int (Hashtbl.hash init_etbl), (Z.of_int 2)) init_etbl in *)
   let init_ec : Machine.eid = Z.zero in
   Machine.init init_regs init_mems init_etbl init_ec