Replace E-perm by reserved sealed otype

logsem · Jun 13, 2024 · a57daa3 · a57daa3
1 parent 7a84d72
commit a57daa3
Show file tree

Hide file tree

Showing 17 changed files with 78 additions and 83 deletions.
diff --git a/lib/ast.ml b/lib/ast.ml
@@ -7,7 +7,6 @@ let mtdc = Reg 31
 
 module Perm = struct
   type t =
-    | E (* sentry                  ---  sealed value with otype 1, 2 or 3 *)
     | R (* read                    ---  LG, MC and LD *)
     | X (* execute                 ---  EX *)
     | W (* write                   ---  LM, MC and SD *)
@@ -21,7 +20,7 @@ module Perm = struct
     else
       (* Just an order for pretty printing *)
       let weight p =
-        match p with E -> 0 | R -> 1 | X -> 2 | W -> 3 | WL -> 4 | SR -> 5 | DL -> 6 | DI -> 7
+        match p with  R -> 0 | X -> 1 | W -> 2 | WL -> 3 | SR -> 4 | DL -> 5 | DI -> 6
       in
       weight p2 - weight p1
 end

diff --git a/lib/encode.ml b/lib/encode.ml
@@ -87,14 +87,13 @@ let perm_encoding (p : Perm.t) : Z.t =
   Z.of_int
   @@
   match p with
-  | E -> 0b10000000
-  | R -> 0b01000000
-  | X -> 0b00100000
-  | W -> 0b00010000
-  | WL -> 0b00001000
-  | SR -> 0b00000100
-  | DL -> 0b00000010
-  | DI -> 0b00000001
+  | R -> 0b1000000
+  | X -> 0b0100000
+  | W -> 0b0010000
+  | WL -> 0b0001000
+  | SR -> 0b0000100
+  | DL -> 0b0000010
+  | DI -> 0b0000001
 
 let fperm_encoding (fp : PermSet.t) : Z.t =
   PermSet.fold (fun p res -> Z.logor (perm_encoding p) res) fp (Z.of_int 0b0)
@@ -103,18 +102,17 @@ let perm_decoding (i : Z.t) : Perm.t =
   let dec_perm_exception _ =
     raise @@ DecodeException "Error decoding permission: unexpected encoding"
   in
-  if Z.(i > of_int 0b11111111) then dec_perm_exception ()
+  if Z.(i > of_int 0b1111111) then dec_perm_exception ()
   else
     let b k = Z.testbit i k in
-    match (b 7, b 6, b 5, b 4, b 3, b 2, b 1, b 0) with
-    | true, false, false, false, false, false, false, false -> E
-    | false, true, false, false, false, false, false, false -> R
-    | false, false, true, false, false, false, false, false -> X
-    | false, false, false, true, false, false, false, false -> W
-    | false, false, false, false, true, false, false, false -> WL
-    | false, false, false, false, false, true, false, false -> SR
-    | false, false, false, false, false, false, true, false -> DL
-    | false, false, false, false, false, false, false, true -> DI
+    match (b 6, b 5, b 4, b 3, b 2, b 1, b 0) with
+    | true, false, false, false, false, false, false -> R
+    | false, true, false, false, false, false, false -> X
+    | false, false, true, false, false, false, false -> W
+    | false, false, false, true, false, false, false -> WL
+    | false, false, false, false, true, false, false -> SR
+    | false, false, false, false, false, true, false -> DL
+    | false, false, false, false, false, false, true -> DI
     | _ -> dec_perm_exception ()
 
 let fperm_decoding (i : Z.t) : PermSet.t =

diff --git a/lib/lexer.mll b/lib/lexer.mll
@@ -81,7 +81,6 @@ rule token = parse
 
 (* permissions *)
 | 'O' { O }
-| 'E' { E }
 | 'R' { R }
 | 'X' { X }
 | 'W' { W }

diff --git a/lib/lexer_regfile.mll b/lib/lexer_regfile.mll
@@ -54,7 +54,6 @@ rule token = parse
 
 (* permissions *)
 | 'O' { O }
-| 'E' { E }
 | 'R' { R }
 | 'X' { X }
 | 'W' { W }

diff --git a/lib/machine.ml b/lib/machine.ml
@@ -26,6 +26,8 @@ let arch_root_memory_perm = PermSet.of_list [ R; W; WL ]
 (* - executable root, EX_LD_LG_LM_MC_SR --> R_X_SR *)
 let arch_root_executable_perm = PermSet.of_list [ R; X; SR ]
 
+let otype_sentry : Z.t = Z.zero
+
 let get_perm (w : Ast.word) : Ast.PermSet.t =
   match w with
   | I _ -> Ast.PermSet.empty
@@ -34,16 +36,24 @@ let get_perm (w : Ast.word) : Ast.PermSet.t =
 
 let is_derived_from (p_dst : PermSet.t) (p_src : PermSet.t) =
   if PermSet.equal p_dst p_src (* p <= p *) then true
-  else if PermSet.mem E p_dst (* E <= RX *) then
-    PermSet.equal (PermSet.of_list [ E ]) p_dst
-    && PermSet.mem R p_src && PermSet.mem X p_src
-    && (not (PermSet.mem DL p_src))
-    && not (PermSet.mem DI p_src)
   else
     (* p_dst ⊆ p_src, except that we can add DI or DL *)
     PermSet.subset (PermSet.remove DL (PermSet.remove DI p_dst)) p_src
 
+let is_sentry (w : Ast.word) : bool =
+  match w with
+  | Sealed (ot, Cap (_, _, _, _, _)) -> ot = otype_sentry
+  | _ -> false
+
 let check_word_derived (w : Ast.word) : unit =
+  if is_sentry w
+  then
+    (
+      if is_derived_from (get_perm w) arch_root_executable_perm
+      then ()
+      else raise (CheckInitFailed w)
+    )
+  else
   if is_derived_from (get_perm w) arch_root_executable_perm then ()
   else if is_derived_from (get_perm w) arch_root_memory_perm then ()
   else raise (CheckInitFailed w)
@@ -165,8 +175,8 @@ let ( !> ) conf = upd_pc conf
 
 let upd_pc_perm (w : word) =
   match w with
-  | Sealable (Cap (p, g, b, e, a)) when PermSet.equal p (PermSet.singleton E) ->
-      Sealable (Cap (PermSet.of_list [ R; X ], g, b, e, a))
+  | Sealed ( ot, (Cap (p, g, b, e, a))) when ot = otype_sentry ->
+      Sealable (Cap (p, g, b, e, a))
   | _ -> w
 
 let fetch_decode (conf : exec_conf) : machine_op option =
@@ -252,9 +262,9 @@ let exec_single (conf : exec_conf) : mchn =
         | Halt -> (Halted, conf)
         | Jalr (r_dst, r_src) when (not (r_dst = mtdc)) && not (r_src = mtdc) -> (
             match PC @! conf with
-            | Sealable (Cap (_, g, b, e, a)) ->
+            | Sealable (Cap (p, g, b, e, a)) ->
                 let new_pc = upd_pc_perm (r_src @! conf) in
-                let link_cap = Sealable (Cap (PermSet.singleton E, g, b, e, Z.(a + Z.one))) in
+                let link_cap = Sealed (otype_sentry, (Cap (p, g, b, e, Z.(a + Z.one)))) in
                 (Running, upd_reg PC new_pc (upd_reg r_dst link_cap conf))
             | _ -> fail_state)
         | Jmp c when not (c = Register mtdc) -> (
@@ -343,7 +353,7 @@ let exec_single (conf : exec_conf) : mchn =
                 let w2 = get_word conf c2 in
                 match (w1, w2) with
                 | I z1, I z2 ->
-                    if b <= z1 && Z.(~$0 <= z2) && Z.zero <= e && not (PermSet.mem E p) then
+                    if b <= z1 && Z.(~$0 <= z2) && Z.zero <= e then
                       let w = Sealable (Cap (p, g, z1, z2, a)) in
                       !>(upd_reg r w conf)
                     else fail_state
@@ -364,8 +374,7 @@ let exec_single (conf : exec_conf) : mchn =
             | Sealable (Cap (p, g, b, e, a)) -> (
                 let w = get_word conf c in
                 match w with
-                | I z when not (PermSet.mem E p) ->
-                    !>(upd_reg r (Sealable (Cap (p, g, b, e, Z.(a + z)))) conf)
+                | I z -> !>(upd_reg r (Sealable (Cap (p, g, b, e, Z.(a + z)))) conf)
                 | _ -> fail_state)
             | Sealable (SealRange (p, g, b, e, a)) -> (
                 let w = get_word conf c in
@@ -447,11 +456,19 @@ let exec_single (conf : exec_conf) : mchn =
         | Seal (dst, r1, r2) when (not (dst = mtdc)) && (not (r1 = mtdc)) && not (r2 = mtdc) -> (
             match (r1 @! conf, r2 @! conf) with
             | Sealable (SealRange ((true, _), _, b, e, a)), Sealable sb when b <= a && a < e ->
+              if a = otype_sentry
+              then
+                (match sb with
+                  | Cap (p,_,_,_,_) when PermSet.mem X p ->
+                    !>(upd_reg dst (Sealed (a, sb)) conf)
+                  | _ -> fail_state)
+              else
                 !>(upd_reg dst (Sealed (a, sb)) conf)
             | _ -> fail_state)
         | UnSeal (dst, r1, r2) when (not (dst = mtdc)) && (not (r1 = mtdc)) && not (r2 = mtdc) -> (
             match (r1 @! conf, r2 @! conf) with
-            | Sealable (SealRange ((_, true), _, b, e, a)), Sealed (a', sb) ->
+            | Sealable (SealRange ((_, true), _, b, e, a)), Sealed (a', sb)
+              when not (a = otype_sentry) ->
                 if b <= a && a < e && a = a' then !>(upd_reg dst (Sealable sb) conf) else fail_state
             | _ -> fail_state)
         | _ -> fail_state)

diff --git a/lib/parser.mly b/lib/parser.mly
@@ -10,7 +10,7 @@
 %token GETL GETB GETE GETA GETP GETOTYPE GETWTYPE SEAL UNSEAL
 %token FAIL HALT
 %token LOCAL GLOBAL
-%token O E R X W WL SR DI DL
+%token O R X W WL SR DI DL
 %token SO S U SU
 %token Int Cap SealRange Sealed
 %left PLUS MINUS EXPR
@@ -110,7 +110,6 @@ locality:
   | GLOBAL; { Global }
 
 perm_enc:
-  | E; { E: Perm.t }
   | R; { R: Perm.t }
   | X; { X: Perm.t }
   | W; { W: Perm.t }

diff --git a/lib/parser_regfile.mly b/lib/parser_regfile.mly
@@ -5,7 +5,7 @@
 %token MAX_ADDR
 %token LPAREN RPAREN LSBRK RSBRK LCBRK RCBRK
 %token PLUS MINUS AFFECT COMMA COLON
-%token O E R X W WL SR DI DL
+%token O R X W WL SR DI DL
 %token SO S U SU
 %token LOCAL GLOBAL
 %left PLUS MINUS EXPR
@@ -54,7 +54,6 @@ seal_perm:
   | SU; { (true, true) }
 
 perm_enc:
-  | E; { E: Perm.t }
   | R; { R: Perm.t }
   | X; { X: Perm.t }
   | W; { W: Perm.t }

diff --git a/lib/pretty_printer.ml b/lib/pretty_printer.ml
@@ -17,7 +17,6 @@ let string_of_seal_perm (p : seal_perm) : string =
 
 let string_of_perm (p : Perm.t) : string =
   match p with
-  | E -> "E"
   | R -> "R"
   | X -> "X"
   | W -> "W"

diff --git a/tests/test_files/default/neg/bad_flow1.s b/tests/test_files/default/neg/bad_flow1.s
@@ -1,4 +1,4 @@
 	mov r1 pc
-	restrict r1 (E, GLOBAL)
-	restrict r1 ([R W X], GLOBAL)			; FAIL: attempt to flow from E to RWX
+    seal r1 r0 r1
+	unseal r1 r0 r1             ; FAIL: attempt to unseal a sentry
 	halt
diff --git a/tests/test_files/default/neg/bad_flow2.s b/tests/test_files/default/neg/bad_flow2.s
@@ -1,4 +1,4 @@
 	mov r1 pc
 	restrict r1 (O, GLOBAL)
-	restrict r1 (E, GLOBAL) 				; FAIL: attempt to flow from O to E
+	seal r1 r0 r1
 	halt
diff --git a/tests/test_files/default/neg/lea_perm_not_entry.s b/tests/test_files/default/neg/lea_perm_not_entry.s
diff --git a/tests/test_files/default/pos/jmper_jalr.s b/tests/test_files/default/pos/jmper_jalr.s
@@ -1,6 +1,6 @@
 	mov r1 pc
 	lea r1 5
-	restrict r1 (E, GLOBAL)
+	seal r1 r0 r1
 	jalr r0 r1
 	fail
 	add r2 5 7

diff --git a/tests/test_files/default/pos/seal_unseal.s b/tests/test_files/default/pos/seal_unseal.s
@@ -1,4 +1,5 @@
     subseg r0 0 2
+    lea r0 1
     mov r1 r0
     restrict r0 (S, Global)
     restrict r1 (U, Global)

diff --git a/tests/test_files/default/pos/sealing_counter.s b/tests/test_files/default/pos/sealing_counter.s
@@ -15,12 +15,11 @@ init:
 	mov r0 pc             	; r0 = (RWX, init, end, init)
 	mov r1 r0             	; r1 = (RWX, init, end, init)
 	lea r1 (data-init)		; r1 = (RWX, init, end, data)
-	load r1 r1				; r1 = {0: (RO, counter, counter+1, counter)}
+	load r1 r1				; r1 = {1: (RO, counter, counter+1, counter)}
 
 	;; prepare the main capability in r0
 	lea r0 (main+1-init)   	; r0 = (RWX, init, end, main+1)
 	subseg r0 main data		; r0 = (RWX, main, data, main+1)
-	restrict r0 (E, Global)	; r0 = (E, main, data, main+1)
 	jalr r0 r0   			; jump to main main
 
 main:
@@ -48,20 +47,23 @@ main:
 
 	halt
 data:
-	#{0: ([R W], Global, counter, counter+1, counter)}
+	#{1: ([R W], Global, counter, counter+1, counter)}
 linking_table:
-	#(E, Global, get, incr, get+1) 		; get
-	#(E, Global, incr, end, incr+2)		; incr
+	;; #(E, Global, get, incr, get+1) 		; get
+	;; #(E, Global, incr, end, incr+2)		; incr
+	#{0: ([R X], Global, get, incr, get+1)}		; get
+	#{0: ([R X], Global, incr, end, incr+2)}	; incr
 counter:
-	#0
+	#1
 get: 							; check whether the otype matches with the actual value
-	#[SU, Global, 0, 10, 0]
+	#[SU, Global, 1, 10, 1]
 	;; r0 contains callback / r1 = {ot: (RO, counter, counter+1, counter)}
 	mov r2 pc 					; r2 = (RX, get, incr, get+1)
 	lea r2 (-1)					; r2 = (RX, get, incr, get)
-	load r2 r2					; r2 = #[SU, 0, 10, 0]
+	load r2 r2					; r2 = #[SU, 1, 10, 1]
 	getotype r3 r1				; r3 = ot
-	lea r2 r3					; r2 = #[SU, 0, 10, ot]
+	lea r2 r3					; r2 = #[SU, 1, 10, ot+1]
+	lea r2 -1					; r2 = #[SU, 1, 10, ot]
 	unseal r2 r2 r1				; r2 = (RO, counter, counter+1, counter)
 	load r2 r2					; r2 = val_counter
 	sub r3 r2 r3				; r3 = val_counter - ot
@@ -72,17 +74,17 @@ get: 							; check whether the otype matches with the actual value
 	jalr r0 r0					; r2 contains the return value
 	fail 						; Case r3 != 0, then fail
 incr:
-	#[SU, Global, 0, 10, 0]
+	#[SU, Global, 1, 10, 1]
 	#([R W], Global, incr, incr+1, incr)
 	;; r0 contains callback / r1 = {ot: (RO, counter, counter+1, counter)}
 	mov r2 pc 					; r2 = (RX, incr, end, incr+2)
 	lea r2 (-2)					; r2 = (RX, incr, end, incr)
-	load r3 r2					; r3 = #[SU, 0, 10, ot]
+	load r3 r2					; r3 = #[SU, 1, 10, ot]
 	unseal r1 r3 r1				; r1 = (RO, counter, counter+1, counter)
 	load r4 r1					; r4 = val_counter
 	add r4 r4 1					; r4 = val_counter + 1
 	store r1 r4					; stores new counter value
-	lea r3 1					; r3 = #[SU, 0, 10, ot+1]
+	lea r3 1					; r3 = #[SU, 1, 10, ot+1]
 	lea r2 1					; r2 = (RX, incr, end, incr+1)
 	load r2 r2					; r2 = (RW, incr, incr+1, incr)
 	store r2 r3					; stores new sealrange

diff --git a/tests/test_files/default/pos/test1_labels.s b/tests/test_files/default/pos/test1_labels.s
@@ -8,7 +8,8 @@ init:
 	store r1 r2           		; mem[data] <- (RWL, init, end, data+1) 6
 	lea r3 (code-init)			; r3 = (RX, init, end, code) 			7
 	subseg r3 code end 			; r3 = (RX, code, end, code) 			8
-	restrict r3 (E, GLOBAL)  	; r3 = (E, code, end, code) 			9
+	seal r3 r0 r3  	            ; r3 = {0: (RX, code, end, code)}		9
+	;; restrict r3 (E, GLOBAL)  	; r3 = (E, code, end, code) 			9
 	mov r2 0 					; r2 = 0 								10
 	mov r1 0 					; r1 = 0 								11
 	jalr r2 r3   				; jump to unknown code:

diff --git a/tests/tester.ml b/tests/tester.ml
@@ -97,8 +97,6 @@ let test_jmper_jalr =
     test_case "jmper_jalr.s should end in halted state" `Quick (test_state Halted (fst m));
     test_case "jmper_jalr.s should end with r2 containing 12" `Quick
       (test_const_word Z.(~$12) (get_reg_int_word (Ast.Reg 2) m Z.zero));
-    test_case "jmper_jalr.s should contain E permission in r1" `Quick
-      (test_perm (PermSet.singleton E) (get_reg_cap_perm (Reg 1) m PermSet.empty));
   ]
 
 let test_locality_flow =
@@ -151,29 +149,29 @@ let test_getwtype =
   let open Alcotest in
   let m = run_prog (test_path "pos/get_wtype.s") in
   [
-    test_case "get_otype.s should end in halted state" `Quick (test_state Halted (fst m));
-    test_case "get_otype.s should end with r0 containing 0" `Quick
+    test_case "get_wtype.s should end in halted state" `Quick (test_state Halted (fst m));
+    test_case "get_wtype.s should end with r0 containing 0" `Quick
       (test_const_word Z.zero (get_reg_int_word (Ast.Reg 0) m Z.zero));
-    test_case "get_otype.s should end with r1 containing 0" `Quick
+    test_case "get_wtype.s should end with r1 containing 0" `Quick
       (test_const_word Z.zero (get_reg_int_word (Ast.Reg 1) m Z.zero));
-    test_case "get_otype.s should end with r2 containing 0" `Quick
+    test_case "get_wtype.s should end with r2 containing 0" `Quick
       (test_const_word Z.zero (get_reg_int_word (Ast.Reg 2) m Z.zero));
-    test_case "get_otype.s should end with r3 containing 0" `Quick
+    test_case "get_wtype.s should end with r3 containing 0" `Quick
       (test_const_word Z.zero (get_reg_int_word (Ast.Reg 3) m Z.zero));
   ]
 
 let test_sealing =
   let open Alcotest in
   let m = run_prog (test_path "pos/seal_unseal.s") in
-  [ test_case "get_otype.s should end in halted state" `Quick (test_state Halted (fst m)) ]
+  [ test_case "seal_unseal.s should end in halted state" `Quick (test_state Halted (fst m)) ]
 
 let test_sealing_counter =
   let open Alcotest in
   let m = run_prog (test_path "pos/sealing_counter.s") in
   [
     test_case "sealing_counter.s should end in halted state" `Quick (test_state Halted (fst m));
-    test_case "sealing_counter.s should end with r2 containing 3" `Quick
-      (test_const_word Z.(~$3) (get_reg_int_word (Ast.Reg 2) m Z.zero));
+    test_case "sealing_counter.s should end with r2 containing 4" `Quick
+      (test_const_word Z.(~$4) (get_reg_int_word (Ast.Reg 2) m Z.zero));
   ]
 
 let () =