From dd3f64b8f320716a376ecd5b604f2af9ece06831 Mon Sep 17 00:00:00 2001 From: Nick Spinale Date: Tue, 24 Mar 2026 13:49:25 -0700 Subject: [PATCH] add support for XN vm attributes This includes removing the use of the grant permission to encode executable permissions for frames. The kernel does not use the grant permission to determine whether a frame is executable, so this encoding was not doing anything. Signed-off-by: Nick Spinale --- capDL-tool/CapDL/AST.hs | 2 + capDL-tool/CapDL/MakeModel.hs | 9 ++- capDL-tool/CapDL/Model.hs | 1 + capDL-tool/CapDL/ParserUtils.hs | 7 +- capDL-tool/CapDL/PrintC.hs | 2 +- capDL-tool/CapDL/PrintIsabelle.hs | 5 +- capDL-tool/CapDL/PrintUtils.hs | 25 +++--- capDL-tool/CapDL/PrintXml.hs | 2 +- capDL-tool/CapDL/STCC.hs | 4 +- capDL-tool/CapDL/State.hs | 4 +- capDL-tool/camkes-adder-arm.cdl | 88 +++++++++++----------- capDL-tool/camkes-adder-arm.right | 88 +++++++++++----------- capDL-tool/camkes-adder-arm.thy.right | 88 +++++++++++----------- capDL-tool/cap-dist-elf-simpleserver.cdl | 6 +- capDL-tool/cap-dist-elf-simpleserver.right | 6 +- capDL-tool/capdl.dtd | 1 + capDL-tool/doc/capDL.md | 4 +- capDL-tool/tools/capdl.vim | 2 +- python-capdl-tool/capdl/Cap.py | 6 +- python-capdl-tool/capdl/PageCollection.py | 2 +- 20 files changed, 185 insertions(+), 167 deletions(-) diff --git a/capDL-tool/CapDL/AST.hs b/capDL-tool/CapDL/AST.hs index 67147461..3fbf5f85 100644 --- a/capDL-tool/CapDL/AST.hs +++ b/capDL-tool/CapDL/AST.hs @@ -166,6 +166,8 @@ data CapParam asid :: Asid } | Cached { cached :: Bool } + | Executable { + executable :: Bool } | FrameMapping { container :: NameRef, slotIndex :: Word } diff --git a/capDL-tool/CapDL/MakeModel.hs b/capDL-tool/CapDL/MakeModel.hs index c6e24f7f..ccd0eab9 100644 --- a/capDL-tool/CapDL/MakeModel.hs +++ b/capDL-tool/CapDL/MakeModel.hs @@ -612,6 +612,11 @@ getCached [] = True getCached (Cached c : _) = c getCached (_ : ps) = getCached ps +getExecutable :: [CapParam] -> Bool +getExecutable [] = True +getExecutable (Executable e : _) = e +getExecutable (_ : ps) = getExecutable ps + getMaybeMapping :: [CapParam] -> Maybe (ObjID, Word) getMaybeMapping [] = Nothing getMaybeMapping (FrameMapping c s : _) = Just (refToID c, s) @@ -629,7 +634,7 @@ validCapPars (TCB {}) ps = (not (containsConstr Reply ps) || not (containsConstr MasterReply ps)) validCapPars (CNode {}) ps = subsetConstrs ps [Guard undefined, GuardSize undefined] validCapPars (Frame {}) ps = - subsetConstrs (removeConstr (Rights undefined) ps) [Asid undefined, Cached undefined, + subsetConstrs (removeConstr (Rights undefined) ps) [Asid undefined, Cached undefined, Executable undefined, FrameMapping undefined undefined] validCapPars (PD {}) ps = subsetConstrs ps [Asid undefined] validCapPars (PT {}) ps = subsetConstrs ps [Asid undefined] @@ -655,7 +660,7 @@ objCapOf containerName obj objRef params = Untyped {} -> UntypedCap objRef CNode _ 0 -> IRQHandlerCap objRef --FIXME: This should check if the obj is in the irqNode CNode {} -> CNodeCap objRef (getGuard params) (getGuardSize params) - Frame {} -> FrameCap objRef (getRights params) (getMaybeAsid params) (getCached params) + Frame {} -> FrameCap objRef (getRights params) (getMaybeAsid params) (getCached params) (getExecutable params) (getMaybeMapping params) PML4 {} -> PML4Cap objRef (getMaybeAsid params) PDPT {} -> PDPTCap objRef (getMaybeAsid params) diff --git a/capDL-tool/CapDL/Model.hs b/capDL-tool/CapDL/Model.hs index a6c1476b..42346fe1 100644 --- a/capDL-tool/CapDL/Model.hs +++ b/capDL-tool/CapDL/Model.hs @@ -90,6 +90,7 @@ data Cap capRights :: CapRights, capMaybeAsid :: Maybe Asid, capCached :: Bool, + capExecutable :: Bool, capMaybeMapping :: Maybe (ObjID, Word) } | PTCap { capObj :: ObjID, diff --git a/capDL-tool/CapDL/ParserUtils.hs b/capDL-tool/CapDL/ParserUtils.hs index 7fc519aa..5f88ac54 100644 --- a/capDL-tool/CapDL/ParserUtils.hs +++ b/capDL-tool/CapDL/ParserUtils.hs @@ -511,7 +511,6 @@ right = chr 'R' Read <|> chr 'W' Write <|> chr 'G' Grant - <|> chr 'X' Grant <|> chr 'P' GrantReply parse_rights :: MapParser CapRights @@ -600,6 +599,12 @@ cap_param = <|> do reserved "uncached" return $ Cached False + <|> do + reserved "executable" + return $ Executable True + <|> do + reserved "execute_never" + return $ Executable False <|> do reserved "mapping" colon diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index 17f3f3c8..da02723e 100644 --- a/capDL-tool/CapDL/PrintC.hs +++ b/capDL-tool/CapDL/PrintC.hs @@ -138,7 +138,7 @@ showCap _ (ARMIRQHandlerCap id) irqNode is_orig _ = ", .is_orig = " ++ is_orig ++ ", .irq = " ++ show (lookupByValue (== id) irqNode) ++ "}" -- Caps have obj_ids, or IRQs, but not both. -showCap objs (FrameCap id rights _ cached maybe_mapping) _ is_orig _ = +showCap objs (FrameCap id rights _ cached _ maybe_mapping) _ is_orig _ = "{.type = CDL_FrameCap, .obj_id = " ++ showObjID objs id ++ ", .is_orig = " ++ is_orig ++ ", .rights = " ++ showRights rights ++ diff --git a/capDL-tool/CapDL/PrintIsabelle.hs b/capDL-tool/CapDL/PrintIsabelle.hs index acca1d2b..2dc48b85 100644 --- a/capDL-tool/CapDL/PrintIsabelle.hs +++ b/capDL-tool/CapDL/PrintIsabelle.hs @@ -254,12 +254,13 @@ printCap _ _ _ _ IRQControlCap = text "IrqControlCap" printCap _ irqNode _ _ (IRQHandlerCap id) = text "IrqHandlerCap" <+> num (fromJust (lookupElem id irqNode)) printCap _ _ _ _ DomainCap = text "DomainCap" -printCap ms _ _ real (FrameCap id rights asid cached _) = text "FrameCap" <+> +printCap ms _ _ real (FrameCap id rights asid cached executable _) = text "FrameCap" <+> -- is_device flag, assumed always false. FIXME: add to model? text "False" <+> printID id <+> printRights rights <+> printFrameSize id ms <+> printReal real <+> printMaybeAsid asid <+> - text (if cached then "" else isaComment "uncached") + text (if cached then "" else isaComment "uncached") <+> + text (if executable then "" else isaComment "execute_never") printCap _ _ _ real (PTCap id asid) = text "PageTableCap" <+> printID id <+> printReal real <+> printMaybeAsid asid diff --git a/capDL-tool/CapDL/PrintUtils.hs b/capDL-tool/CapDL/PrintUtils.hs index 41d8413f..de83cfe0 100644 --- a/capDL-tool/CapDL/PrintUtils.hs +++ b/capDL-tool/CapDL/PrintUtils.hs @@ -277,16 +277,15 @@ maybeNum t n = prettyParemNum t n maybeBadge = maybeNum "badge" -prettyRight _ Read = text "R" -prettyRight _ Write = text "W" -prettyRight True Grant = text "X" -prettyRight False Grant = text "G" -prettyRight _ GrantReply = text "P" +prettyRight Read = text "R" +prettyRight Write = text "W" +prettyRight Grant = text "G" +prettyRight GrantReply = text "P" -maybeRightsList _ [] = [] -maybeRightsList isFrame xs = [hcat (map (prettyRight isFrame) xs)] +maybeRightsList [] = [] +maybeRightsList xs = [hcat (map prettyRight xs)] -maybeRights isFrame r = maybeRightsList isFrame (Set.toList r) +maybeRights r = maybeRightsList (Set.toList r) maybeGuard = maybeNum "guard" maybeGSize = maybeNum "guard_size" @@ -312,17 +311,17 @@ maybeFrameMapping (Just mapping) = prettyFrameMapping mapping maybeCapParams :: Cap -> Doc maybeCapParams cap = case cap of EndpointCap _ badge rights -> - capParams (maybeBadge badge ++ maybeRights False rights) + capParams (maybeBadge badge ++ maybeRights rights) NotificationCap _ badge rights -> - capParams (maybeBadge badge ++ maybeRights False rights) + capParams (maybeBadge badge ++ maybeRights rights) ARMSMCCap _ badge -> capParams (maybeBadge badge) ReplyCap _ -> capParams [text "reply"] MasterReplyCap _ -> capParams [text "master_reply"] CNodeCap _ guard gsize -> capParams (maybeGuard guard ++ maybeGSize gsize) - FrameCap _ rights asid cached mapping -> capParams (maybeRights True rights ++ maybeAsid asid ++ - (if cached then [] else [text "uncached"]) ++ maybeFrameMapping mapping) + FrameCap _ rights asid cached executable mapping -> capParams (maybeRights rights ++ maybeAsid asid ++ + (if cached then [] else [text "uncached"]) ++ (if executable then [] else [text "execute_never"]) ++ maybeFrameMapping mapping) PTCap _ asid -> capParams (maybeAsid asid) PDCap _ asid -> capParams (maybeAsid asid) SchedControlCap core -> capParams (prettyCore core) @@ -351,7 +350,7 @@ sameParams cap1 cap2 = b1 == b2 ((CNodeCap _ g1 gs1), (CNodeCap _ g2 gs2)) -> g1 == g2 && gs1 == gs2 - ((FrameCap _ r1 a1 c1 m1), (FrameCap _ r2 a2 c2 m2)) -> r1 == r2 && a1 == a2 && c1 == c2 && m1 == m2 + ((FrameCap _ r1 a1 c1 e1 m1), (FrameCap _ r2 a2 c2 e2 m2)) -> r1 == r2 && a1 == a2 && c1 == c2 && e1 == e2 && m1 == m2 ((PTCap _ a1), (PTCap _ a2)) -> a1 == a2 ((PDCap _ a1), (PDCap _ a2)) -> a1 == a2 _ -> True diff --git a/capDL-tool/CapDL/PrintXml.hs b/capDL-tool/CapDL/PrintXml.hs index 42e3d9a3..35765844 100644 --- a/capDL-tool/CapDL/PrintXml.hs +++ b/capDL-tool/CapDL/PrintXml.hs @@ -170,7 +170,7 @@ showExtraCapAttributes (NotificationCap _ capBadge _) = [("badge", show capBadge showExtraCapAttributes (ARMSMCCap _ capBadge) = [("badge", show capBadge)] showExtraCapAttributes (CNodeCap _ guard guardSize) = [("guard", show guard), ("guardSize", show guardSize)] -showExtraCapAttributes (FrameCap _ _ _ False _) = [("cached", "False")] +showExtraCapAttributes (FrameCap _ _ _ cached executable _) = [ ("cached", "False") | not cached ] ++ [ ("executable", "False") | not executable ] showExtraCapAttributes _ = [] -- diff --git a/capDL-tool/CapDL/STCC.hs b/capDL-tool/CapDL/STCC.hs index ee51afaa..96b19732 100644 --- a/capDL-tool/CapDL/STCC.hs +++ b/capDL-tool/CapDL/STCC.hs @@ -32,7 +32,7 @@ projectEndpoint capset = projectNtfn capset = Set.fromList $ concat [[(r, capObj) | r <- Set.toList rights] | (NotificationCap capObj _ rights) <- Set.toList capset] projectFrame capset = - Set.fromList $ concat [[(r, capObj) | r <- Set.toList rights] | (FrameCap capObj rights Nothing True Nothing) <- Set.toList capset] + Set.fromList $ concat [[(r, capObj) | r <- Set.toList rights] | (FrameCap capObj rights Nothing True _ Nothing) <- Set.toList capset] somefn :: Model Word -> IO () somefn (Model _ objects _ _ _ _ _ _) = @@ -301,7 +301,7 @@ getFrames' objects visited cap = PTCap capObj _ | capObj `Set.member` visited -> [] | otherwise -> cap : getFrames'' objects visited capObj - FrameCap _ _ _ _ _ -> + FrameCap _ _ _ _ _ _ -> [cap] _ -> [] diff --git a/capDL-tool/CapDL/State.hs b/capDL-tool/CapDL/State.hs index d43bb872..3b312866 100644 --- a/capDL-tool/CapDL/State.hs +++ b/capDL-tool/CapDL/State.hs @@ -624,7 +624,7 @@ flattenCNodeSlots ((_, CNode slots _) : xs) = map snd (Map.toList slots) ++ flat flattenCNodeSlots (_ : xs) = flattenCNodeSlots xs isMappedFrameCap :: Cap -> Bool -isMappedFrameCap (FrameCap _ _ _ _ (Just _)) = True +isMappedFrameCap (FrameCap _ _ _ _ _ (Just _)) = True isMappedFrameCap _ = False -- Returns list containing each element in argument list occuring more than once. @@ -708,7 +708,7 @@ checkMappedFrameCapsOnlyInCNodes m = -- mapping to a frame. checkMappedFrameCaps :: Model Word -> Logger Bool checkMappedFrameCaps m = do - let mappings = map (\(FrameCap _ _ _ _ (Just x)) -> x) $ + let mappings = map (\(FrameCap _ _ _ _ _ (Just x)) -> x) $ filter isMappedFrameCap $ flattenCNodeSlots $ allObjs m no_duplicates <- checkDuplicateMappedFrameCaps mappings sane_mappings <- checkMappedFrameCapsSanity m mappings diff --git a/capDL-tool/camkes-adder-arm.cdl b/capDL-tool/camkes-adder-arm.cdl index 78575f91..27f0bcd5 100644 --- a/capDL-tool/camkes-adder-arm.cdl +++ b/capDL-tool/camkes-adder-arm.cdl @@ -266,31 +266,31 @@ client_group_bin_pd { 0x1: pt_client_group_bin_0003 } pt_adder_group_bin_0000 { -0x10: frame_adder_group_bin_0000 (RWX) -0x20: frame_adder_group_bin_0001 (RWX) -0x30: frame_adder_group_bin_0004 (RWX) -0x40: frame_adder_group_bin_0011 (RWX) -0x50: frame_adder_group_bin_0036 (RWX) -0x60: frame_adder_group_bin_0015 (RWX) -0x70: frame_adder_group_bin_0039 (RWX) -0x80: frame_adder_group_bin_0017 (RWX) -0x90: frame_adder_group_bin_0041 (RWX) -0xa0: frame_adder_group_bin_0019 (RWX) -0xb0: frame_adder_group_bin_0043 (RWX) -0xc0: frame_adder_group_bin_0021 (RWX) -0xd0: frame_adder_group_bin_0045 (RWX) -0xe0: frame_adder_group_bin_0023 (RWX) -0xf0: frame_adder_group_bin_0047 (RWX) +0x10: frame_adder_group_bin_0000 (RW) +0x20: frame_adder_group_bin_0001 (RW) +0x30: frame_adder_group_bin_0004 (RW) +0x40: frame_adder_group_bin_0011 (RW) +0x50: frame_adder_group_bin_0036 (RW) +0x60: frame_adder_group_bin_0015 (RW) +0x70: frame_adder_group_bin_0039 (RW) +0x80: frame_adder_group_bin_0017 (RW) +0x90: frame_adder_group_bin_0041 (RW) +0xa0: frame_adder_group_bin_0019 (RW) +0xb0: frame_adder_group_bin_0043 (RW) +0xc0: frame_adder_group_bin_0021 (RW) +0xd0: frame_adder_group_bin_0045 (RW) +0xe0: frame_adder_group_bin_0023 (RW) +0xf0: frame_adder_group_bin_0047 (RW) } pt_adder_group_bin_0003 { -0x0: frame_adder_group_bin_0025 (RWX) -0x10: frame_adder_group_bin_0049 (RWX) -0x20: frame_adder_group_bin_0027 (RWX) -0x30: frame_adder_group_bin_0002 (RWX) -0x40: frame_adder_group_bin_0029 (RWX) -0x41: frame_adder_group_bin_0013 (RWX) -0x42: frame_adder_group_bin_0014 (RWX) -0x43: frame_adder_group_bin_0016 (RWX) +0x0: frame_adder_group_bin_0025 (RW) +0x10: frame_adder_group_bin_0049 (RW) +0x20: frame_adder_group_bin_0027 (RW) +0x30: frame_adder_group_bin_0002 (RW) +0x40: frame_adder_group_bin_0029 (RW) +0x41: frame_adder_group_bin_0013 (RW) +0x42: frame_adder_group_bin_0014 (RW) +0x43: frame_adder_group_bin_0016 (RW) 0x45: stack__camkes_stack_adder_0_control_0_adder_obj (RW) 0x46: stack__camkes_stack_adder_0_control_1_adder_obj (RW) 0x47: stack__camkes_stack_adder_0_control_2_adder_obj (RW) @@ -306,30 +306,30 @@ pt_adder_group_bin_0003 { 0x59: stack__camkes_stack_adder_0_fault_handler_2_adder_obj (RW) 0x5a: stack__camkes_stack_adder_0_fault_handler_3_adder_obj (RW) 0x5d: adder_frame__camkes_ipc_buffer_adder_0_fault_handler (RW) -0x5f: s_data_0_obj (RWX, uncached) +0x5f: s_data_0_obj (RW, uncached, execute_never) } pt_client_group_bin_0000 { -0x10: frame_client_group_bin_0000 (RWX) -0x20: frame_client_group_bin_0001 (RWX) -0x30: frame_client_group_bin_0003 (RWX) -0x40: frame_client_group_bin_0004 (RWX) -0x50: frame_client_group_bin_0029 (RWX) -0x60: frame_client_group_bin_0008 (RWX) -0x70: frame_client_group_bin_0032 (RWX) -0x80: frame_client_group_bin_0010 (RWX) -0x90: frame_client_group_bin_0033 (RWX) -0xa0: frame_client_group_bin_0012 (RWX) -0xb0: frame_client_group_bin_0034 (RWX) -0xc0: frame_client_group_bin_0014 (RWX) -0xd0: frame_client_group_bin_0035 (RWX) -0xe0: frame_client_group_bin_0016 (RWX) -0xf0: frame_client_group_bin_0036 (RWX) +0x10: frame_client_group_bin_0000 (RW) +0x20: frame_client_group_bin_0001 (RW) +0x30: frame_client_group_bin_0003 (RW) +0x40: frame_client_group_bin_0004 (RW) +0x50: frame_client_group_bin_0029 (RW) +0x60: frame_client_group_bin_0008 (RW) +0x70: frame_client_group_bin_0032 (RW) +0x80: frame_client_group_bin_0010 (RW) +0x90: frame_client_group_bin_0033 (RW) +0xa0: frame_client_group_bin_0012 (RW) +0xb0: frame_client_group_bin_0034 (RW) +0xc0: frame_client_group_bin_0014 (RW) +0xd0: frame_client_group_bin_0035 (RW) +0xe0: frame_client_group_bin_0016 (RW) +0xf0: frame_client_group_bin_0036 (RW) } pt_client_group_bin_0003 { -0x0: frame_client_group_bin_0018 (RWX) -0x10: frame_client_group_bin_0037 (RWX) -0x20: frame_client_group_bin_0020 (RWX) -0x30: frame_client_group_bin_0002 (RWX) +0x0: frame_client_group_bin_0018 (RW) +0x10: frame_client_group_bin_0037 (RW) +0x20: frame_client_group_bin_0020 (RW) +0x30: frame_client_group_bin_0002 (RW) 0x41: stack__camkes_stack_client_0_control_0_client_obj (RW) 0x42: stack__camkes_stack_client_0_control_1_client_obj (RW) 0x43: stack__camkes_stack_client_0_control_2_client_obj (RW) @@ -340,7 +340,7 @@ pt_client_group_bin_0003 { 0x4c: stack__camkes_stack_client_0_fault_handler_2_client_obj (RW) 0x4d: stack__camkes_stack_client_0_fault_handler_3_client_obj (RW) 0x50: client_frame__camkes_ipc_buffer_client_0_fault_handler (RW) -0x52: s_data_0_obj (RWX, uncached) +0x52: s_data_0_obj (RW, uncached, execute_never) } } diff --git a/capDL-tool/camkes-adder-arm.right b/capDL-tool/camkes-adder-arm.right index c574bd64..e96a6382 100644 --- a/capDL-tool/camkes-adder-arm.right +++ b/capDL-tool/camkes-adder-arm.right @@ -265,32 +265,32 @@ objects { } pt_adder_group_bin_0000 { - 16: frame_adder_group_bin_0000 (RWX) - 32: frame_adder_group_bin_0001 (RWX) - 48: frame_adder_group_bin_0004 (RWX) - 64: frame_adder_group_bin_0011 (RWX) - 80: frame_adder_group_bin_0036 (RWX) - 96: frame_adder_group_bin_0015 (RWX) - 112: frame_adder_group_bin_0039 (RWX) - 128: frame_adder_group_bin_0017 (RWX) - 144: frame_adder_group_bin_0041 (RWX) - 160: frame_adder_group_bin_0019 (RWX) - 176: frame_adder_group_bin_0043 (RWX) - 192: frame_adder_group_bin_0021 (RWX) - 208: frame_adder_group_bin_0045 (RWX) - 224: frame_adder_group_bin_0023 (RWX) - 240: frame_adder_group_bin_0047 (RWX) + 16: frame_adder_group_bin_0000 (RW) + 32: frame_adder_group_bin_0001 (RW) + 48: frame_adder_group_bin_0004 (RW) + 64: frame_adder_group_bin_0011 (RW) + 80: frame_adder_group_bin_0036 (RW) + 96: frame_adder_group_bin_0015 (RW) + 112: frame_adder_group_bin_0039 (RW) + 128: frame_adder_group_bin_0017 (RW) + 144: frame_adder_group_bin_0041 (RW) + 160: frame_adder_group_bin_0019 (RW) + 176: frame_adder_group_bin_0043 (RW) + 192: frame_adder_group_bin_0021 (RW) + 208: frame_adder_group_bin_0045 (RW) + 224: frame_adder_group_bin_0023 (RW) + 240: frame_adder_group_bin_0047 (RW) } pt_adder_group_bin_0003 { - 0: frame_adder_group_bin_0025 (RWX) - 16: frame_adder_group_bin_0049 (RWX) - 32: frame_adder_group_bin_0027 (RWX) - 48: frame_adder_group_bin_0002 (RWX) - 64: frame_adder_group_bin_0029 (RWX) - 65: frame_adder_group_bin_0013 (RWX) - 66: frame_adder_group_bin_0014 (RWX) - 67: frame_adder_group_bin_0016 (RWX) + 0: frame_adder_group_bin_0025 (RW) + 16: frame_adder_group_bin_0049 (RW) + 32: frame_adder_group_bin_0027 (RW) + 48: frame_adder_group_bin_0002 (RW) + 64: frame_adder_group_bin_0029 (RW) + 65: frame_adder_group_bin_0013 (RW) + 66: frame_adder_group_bin_0014 (RW) + 67: frame_adder_group_bin_0016 (RW) 69: stack__camkes_stack_adder_0_control_0_adder_obj (RW) 70: stack__camkes_stack_adder_0_control_1_adder_obj (RW) 71: stack__camkes_stack_adder_0_control_2_adder_obj (RW) @@ -306,32 +306,32 @@ objects { 89: stack__camkes_stack_adder_0_fault_handler_2_adder_obj (RW) 90: stack__camkes_stack_adder_0_fault_handler_3_adder_obj (RW) 93: adder_frame__camkes_ipc_buffer_adder_0_fault_handler (RW) - 95: s_data_0_obj (RWX, uncached) + 95: s_data_0_obj (RW, uncached, execute_never) } pt_client_group_bin_0000 { - 16: frame_client_group_bin_0000 (RWX) - 32: frame_client_group_bin_0001 (RWX) - 48: frame_client_group_bin_0003 (RWX) - 64: frame_client_group_bin_0004 (RWX) - 80: frame_client_group_bin_0029 (RWX) - 96: frame_client_group_bin_0008 (RWX) - 112: frame_client_group_bin_0032 (RWX) - 128: frame_client_group_bin_0010 (RWX) - 144: frame_client_group_bin_0033 (RWX) - 160: frame_client_group_bin_0012 (RWX) - 176: frame_client_group_bin_0034 (RWX) - 192: frame_client_group_bin_0014 (RWX) - 208: frame_client_group_bin_0035 (RWX) - 224: frame_client_group_bin_0016 (RWX) - 240: frame_client_group_bin_0036 (RWX) + 16: frame_client_group_bin_0000 (RW) + 32: frame_client_group_bin_0001 (RW) + 48: frame_client_group_bin_0003 (RW) + 64: frame_client_group_bin_0004 (RW) + 80: frame_client_group_bin_0029 (RW) + 96: frame_client_group_bin_0008 (RW) + 112: frame_client_group_bin_0032 (RW) + 128: frame_client_group_bin_0010 (RW) + 144: frame_client_group_bin_0033 (RW) + 160: frame_client_group_bin_0012 (RW) + 176: frame_client_group_bin_0034 (RW) + 192: frame_client_group_bin_0014 (RW) + 208: frame_client_group_bin_0035 (RW) + 224: frame_client_group_bin_0016 (RW) + 240: frame_client_group_bin_0036 (RW) } pt_client_group_bin_0003 { - 0: frame_client_group_bin_0018 (RWX) - 16: frame_client_group_bin_0037 (RWX) - 32: frame_client_group_bin_0020 (RWX) - 48: frame_client_group_bin_0002 (RWX) + 0: frame_client_group_bin_0018 (RW) + 16: frame_client_group_bin_0037 (RW) + 32: frame_client_group_bin_0020 (RW) + 48: frame_client_group_bin_0002 (RW) 65: stack__camkes_stack_client_0_control_0_client_obj (RW) 66: stack__camkes_stack_client_0_control_1_client_obj (RW) 67: stack__camkes_stack_client_0_control_2_client_obj (RW) @@ -342,7 +342,7 @@ objects { 76: stack__camkes_stack_client_0_fault_handler_2_client_obj (RW) 77: stack__camkes_stack_client_0_fault_handler_3_client_obj (RW) 80: client_frame__camkes_ipc_buffer_client_0_fault_handler (RW) - 82: s_data_0_obj (RWX, uncached) + 82: s_data_0_obj (RW, uncached, execute_never) } } cdt { diff --git a/capDL-tool/camkes-adder-arm.thy.right b/capDL-tool/camkes-adder-arm.thy.right index cb8db3c7..3a1aa308 100644 --- a/capDL-tool/camkes-adder-arm.thy.right +++ b/capDL-tool/camkes-adder-arm.thy.right @@ -702,21 +702,21 @@ lemma client_client_0_fault_handler_tcb_object_slots: by (simp add: client_client_0_fault_handler_tcb_def object_slots_def) definition pt_adder_group_bin_0000_caps :: "cdl_cap_map" where -"pt_adder_group_bin_0000_caps \ [16 \ Types_D.FrameCap False frame_adder_group_bin_0000_id {Read, Write, Grant} 16 Fake None , - 32 \ Types_D.FrameCap False frame_adder_group_bin_0001_id {Read, Write, Grant} 16 Fake None , - 48 \ Types_D.FrameCap False frame_adder_group_bin_0004_id {Read, Write, Grant} 16 Fake None , - 64 \ Types_D.FrameCap False frame_adder_group_bin_0011_id {Read, Write, Grant} 16 Fake None , - 80 \ Types_D.FrameCap False frame_adder_group_bin_0036_id {Read, Write, Grant} 16 Fake None , - 96 \ Types_D.FrameCap False frame_adder_group_bin_0015_id {Read, Write, Grant} 16 Fake None , - 112 \ Types_D.FrameCap False frame_adder_group_bin_0039_id {Read, Write, Grant} 16 Fake None , - 128 \ Types_D.FrameCap False frame_adder_group_bin_0017_id {Read, Write, Grant} 16 Fake None , - 144 \ Types_D.FrameCap False frame_adder_group_bin_0041_id {Read, Write, Grant} 16 Fake None , - 160 \ Types_D.FrameCap False frame_adder_group_bin_0019_id {Read, Write, Grant} 16 Fake None , - 176 \ Types_D.FrameCap False frame_adder_group_bin_0043_id {Read, Write, Grant} 16 Fake None , - 192 \ Types_D.FrameCap False frame_adder_group_bin_0021_id {Read, Write, Grant} 16 Fake None , - 208 \ Types_D.FrameCap False frame_adder_group_bin_0045_id {Read, Write, Grant} 16 Fake None , - 224 \ Types_D.FrameCap False frame_adder_group_bin_0023_id {Read, Write, Grant} 16 Fake None , - 240 \ Types_D.FrameCap False frame_adder_group_bin_0047_id {Read, Write, Grant} 16 Fake None ]" +"pt_adder_group_bin_0000_caps \ [16 \ Types_D.FrameCap False frame_adder_group_bin_0000_id {Read, Write} 16 Fake None , + 32 \ Types_D.FrameCap False frame_adder_group_bin_0001_id {Read, Write} 16 Fake None , + 48 \ Types_D.FrameCap False frame_adder_group_bin_0004_id {Read, Write} 16 Fake None , + 64 \ Types_D.FrameCap False frame_adder_group_bin_0011_id {Read, Write} 16 Fake None , + 80 \ Types_D.FrameCap False frame_adder_group_bin_0036_id {Read, Write} 16 Fake None , + 96 \ Types_D.FrameCap False frame_adder_group_bin_0015_id {Read, Write} 16 Fake None , + 112 \ Types_D.FrameCap False frame_adder_group_bin_0039_id {Read, Write} 16 Fake None , + 128 \ Types_D.FrameCap False frame_adder_group_bin_0017_id {Read, Write} 16 Fake None , + 144 \ Types_D.FrameCap False frame_adder_group_bin_0041_id {Read, Write} 16 Fake None , + 160 \ Types_D.FrameCap False frame_adder_group_bin_0019_id {Read, Write} 16 Fake None , + 176 \ Types_D.FrameCap False frame_adder_group_bin_0043_id {Read, Write} 16 Fake None , + 192 \ Types_D.FrameCap False frame_adder_group_bin_0021_id {Read, Write} 16 Fake None , + 208 \ Types_D.FrameCap False frame_adder_group_bin_0045_id {Read, Write} 16 Fake None , + 224 \ Types_D.FrameCap False frame_adder_group_bin_0023_id {Read, Write} 16 Fake None , + 240 \ Types_D.FrameCap False frame_adder_group_bin_0047_id {Read, Write} 16 Fake None ]" definition pt_adder_group_bin_0000 :: "cdl_object" where "pt_adder_group_bin_0000 \ Types_D.PageTable \ cdl_page_table_caps = pt_adder_group_bin_0000_caps \" @@ -726,14 +726,14 @@ lemma pt_adder_group_bin_0000_object_slots: by (simp add: pt_adder_group_bin_0000_def object_slots_def) definition pt_adder_group_bin_0003_caps :: "cdl_cap_map" where -"pt_adder_group_bin_0003_caps \ [0 \ Types_D.FrameCap False frame_adder_group_bin_0025_id {Read, Write, Grant} 16 Fake None , - 16 \ Types_D.FrameCap False frame_adder_group_bin_0049_id {Read, Write, Grant} 16 Fake None , - 32 \ Types_D.FrameCap False frame_adder_group_bin_0027_id {Read, Write, Grant} 16 Fake None , - 48 \ Types_D.FrameCap False frame_adder_group_bin_0002_id {Read, Write, Grant} 16 Fake None , - 64 \ Types_D.FrameCap False frame_adder_group_bin_0029_id {Read, Write, Grant} 12 Fake None , - 65 \ Types_D.FrameCap False frame_adder_group_bin_0013_id {Read, Write, Grant} 12 Fake None , - 66 \ Types_D.FrameCap False frame_adder_group_bin_0014_id {Read, Write, Grant} 12 Fake None , - 67 \ Types_D.FrameCap False frame_adder_group_bin_0016_id {Read, Write, Grant} 12 Fake None , +"pt_adder_group_bin_0003_caps \ [0 \ Types_D.FrameCap False frame_adder_group_bin_0025_id {Read, Write} 16 Fake None , + 16 \ Types_D.FrameCap False frame_adder_group_bin_0049_id {Read, Write} 16 Fake None , + 32 \ Types_D.FrameCap False frame_adder_group_bin_0027_id {Read, Write} 16 Fake None , + 48 \ Types_D.FrameCap False frame_adder_group_bin_0002_id {Read, Write} 16 Fake None , + 64 \ Types_D.FrameCap False frame_adder_group_bin_0029_id {Read, Write} 12 Fake None , + 65 \ Types_D.FrameCap False frame_adder_group_bin_0013_id {Read, Write} 12 Fake None , + 66 \ Types_D.FrameCap False frame_adder_group_bin_0014_id {Read, Write} 12 Fake None , + 67 \ Types_D.FrameCap False frame_adder_group_bin_0016_id {Read, Write} 12 Fake None , 69 \ Types_D.FrameCap False stack__camkes_stack_adder_0_control_0_adder_obj_id {Read, Write} 12 Fake None , 70 \ Types_D.FrameCap False stack__camkes_stack_adder_0_control_1_adder_obj_id {Read, Write} 12 Fake None , 71 \ Types_D.FrameCap False stack__camkes_stack_adder_0_control_2_adder_obj_id {Read, Write} 12 Fake None , @@ -749,7 +749,7 @@ definition pt_adder_group_bin_0003_caps :: "cdl_cap_map" where 89 \ Types_D.FrameCap False stack__camkes_stack_adder_0_fault_handler_2_adder_obj_id {Read, Write} 12 Fake None , 90 \ Types_D.FrameCap False stack__camkes_stack_adder_0_fault_handler_3_adder_obj_id {Read, Write} 12 Fake None , 93 \ Types_D.FrameCap False adder_frame__camkes_ipc_buffer_adder_0_fault_handler_id {Read, Write} 12 Fake None , - 95 \ Types_D.FrameCap False s_data_0_obj_id {Read, Write, Grant} 12 Fake None \ \uncached\]" + 95 \ Types_D.FrameCap False s_data_0_obj_id {Read, Write} 12 Fake None \ \uncached\ \ \execute_never\]" definition pt_adder_group_bin_0003 :: "cdl_object" where "pt_adder_group_bin_0003 \ Types_D.PageTable \ cdl_page_table_caps = pt_adder_group_bin_0003_caps \" @@ -759,21 +759,21 @@ lemma pt_adder_group_bin_0003_object_slots: by (simp add: pt_adder_group_bin_0003_def object_slots_def) definition pt_client_group_bin_0000_caps :: "cdl_cap_map" where -"pt_client_group_bin_0000_caps \ [16 \ Types_D.FrameCap False frame_client_group_bin_0000_id {Read, Write, Grant} 16 Fake None , - 32 \ Types_D.FrameCap False frame_client_group_bin_0001_id {Read, Write, Grant} 16 Fake None , - 48 \ Types_D.FrameCap False frame_client_group_bin_0003_id {Read, Write, Grant} 16 Fake None , - 64 \ Types_D.FrameCap False frame_client_group_bin_0004_id {Read, Write, Grant} 16 Fake None , - 80 \ Types_D.FrameCap False frame_client_group_bin_0029_id {Read, Write, Grant} 16 Fake None , - 96 \ Types_D.FrameCap False frame_client_group_bin_0008_id {Read, Write, Grant} 16 Fake None , - 112 \ Types_D.FrameCap False frame_client_group_bin_0032_id {Read, Write, Grant} 16 Fake None , - 128 \ Types_D.FrameCap False frame_client_group_bin_0010_id {Read, Write, Grant} 16 Fake None , - 144 \ Types_D.FrameCap False frame_client_group_bin_0033_id {Read, Write, Grant} 16 Fake None , - 160 \ Types_D.FrameCap False frame_client_group_bin_0012_id {Read, Write, Grant} 16 Fake None , - 176 \ Types_D.FrameCap False frame_client_group_bin_0034_id {Read, Write, Grant} 16 Fake None , - 192 \ Types_D.FrameCap False frame_client_group_bin_0014_id {Read, Write, Grant} 16 Fake None , - 208 \ Types_D.FrameCap False frame_client_group_bin_0035_id {Read, Write, Grant} 16 Fake None , - 224 \ Types_D.FrameCap False frame_client_group_bin_0016_id {Read, Write, Grant} 16 Fake None , - 240 \ Types_D.FrameCap False frame_client_group_bin_0036_id {Read, Write, Grant} 16 Fake None ]" +"pt_client_group_bin_0000_caps \ [16 \ Types_D.FrameCap False frame_client_group_bin_0000_id {Read, Write} 16 Fake None , + 32 \ Types_D.FrameCap False frame_client_group_bin_0001_id {Read, Write} 16 Fake None , + 48 \ Types_D.FrameCap False frame_client_group_bin_0003_id {Read, Write} 16 Fake None , + 64 \ Types_D.FrameCap False frame_client_group_bin_0004_id {Read, Write} 16 Fake None , + 80 \ Types_D.FrameCap False frame_client_group_bin_0029_id {Read, Write} 16 Fake None , + 96 \ Types_D.FrameCap False frame_client_group_bin_0008_id {Read, Write} 16 Fake None , + 112 \ Types_D.FrameCap False frame_client_group_bin_0032_id {Read, Write} 16 Fake None , + 128 \ Types_D.FrameCap False frame_client_group_bin_0010_id {Read, Write} 16 Fake None , + 144 \ Types_D.FrameCap False frame_client_group_bin_0033_id {Read, Write} 16 Fake None , + 160 \ Types_D.FrameCap False frame_client_group_bin_0012_id {Read, Write} 16 Fake None , + 176 \ Types_D.FrameCap False frame_client_group_bin_0034_id {Read, Write} 16 Fake None , + 192 \ Types_D.FrameCap False frame_client_group_bin_0014_id {Read, Write} 16 Fake None , + 208 \ Types_D.FrameCap False frame_client_group_bin_0035_id {Read, Write} 16 Fake None , + 224 \ Types_D.FrameCap False frame_client_group_bin_0016_id {Read, Write} 16 Fake None , + 240 \ Types_D.FrameCap False frame_client_group_bin_0036_id {Read, Write} 16 Fake None ]" definition pt_client_group_bin_0000 :: "cdl_object" where "pt_client_group_bin_0000 \ Types_D.PageTable \ cdl_page_table_caps = pt_client_group_bin_0000_caps \" @@ -783,10 +783,10 @@ lemma pt_client_group_bin_0000_object_slots: by (simp add: pt_client_group_bin_0000_def object_slots_def) definition pt_client_group_bin_0003_caps :: "cdl_cap_map" where -"pt_client_group_bin_0003_caps \ [0 \ Types_D.FrameCap False frame_client_group_bin_0018_id {Read, Write, Grant} 16 Fake None , - 16 \ Types_D.FrameCap False frame_client_group_bin_0037_id {Read, Write, Grant} 16 Fake None , - 32 \ Types_D.FrameCap False frame_client_group_bin_0020_id {Read, Write, Grant} 16 Fake None , - 48 \ Types_D.FrameCap False frame_client_group_bin_0002_id {Read, Write, Grant} 16 Fake None , +"pt_client_group_bin_0003_caps \ [0 \ Types_D.FrameCap False frame_client_group_bin_0018_id {Read, Write} 16 Fake None , + 16 \ Types_D.FrameCap False frame_client_group_bin_0037_id {Read, Write} 16 Fake None , + 32 \ Types_D.FrameCap False frame_client_group_bin_0020_id {Read, Write} 16 Fake None , + 48 \ Types_D.FrameCap False frame_client_group_bin_0002_id {Read, Write} 16 Fake None , 65 \ Types_D.FrameCap False stack__camkes_stack_client_0_control_0_client_obj_id {Read, Write} 12 Fake None , 66 \ Types_D.FrameCap False stack__camkes_stack_client_0_control_1_client_obj_id {Read, Write} 12 Fake None , 67 \ Types_D.FrameCap False stack__camkes_stack_client_0_control_2_client_obj_id {Read, Write} 12 Fake None , @@ -797,7 +797,7 @@ definition pt_client_group_bin_0003_caps :: "cdl_cap_map" where 76 \ Types_D.FrameCap False stack__camkes_stack_client_0_fault_handler_2_client_obj_id {Read, Write} 12 Fake None , 77 \ Types_D.FrameCap False stack__camkes_stack_client_0_fault_handler_3_client_obj_id {Read, Write} 12 Fake None , 80 \ Types_D.FrameCap False client_frame__camkes_ipc_buffer_client_0_fault_handler_id {Read, Write} 12 Fake None , - 82 \ Types_D.FrameCap False s_data_0_obj_id {Read, Write, Grant} 12 Fake None \ \uncached\]" + 82 \ Types_D.FrameCap False s_data_0_obj_id {Read, Write} 12 Fake None \ \uncached\ \ \execute_never\]" definition pt_client_group_bin_0003 :: "cdl_object" where "pt_client_group_bin_0003 \ Types_D.PageTable \ cdl_page_table_caps = pt_client_group_bin_0003_caps \" diff --git a/capDL-tool/cap-dist-elf-simpleserver.cdl b/capDL-tool/cap-dist-elf-simpleserver.cdl index e24d3268..d09968b1 100644 --- a/capDL-tool/cap-dist-elf-simpleserver.cdl +++ b/capDL-tool/cap-dist-elf-simpleserver.cdl @@ -24,7 +24,7 @@ cnode { tcb ep (RWG) cnode (guard: 0, guard_size: 28) - frame[5] (RWG) + frame[5] (RW) } ap { pd1 } @@ -32,7 +32,7 @@ ap { pd1 } pd1 { 0: pt1 } pt1 { - 0x10: frame[] (RWG) + 0x10: frame[] (RW) } cnode2 { 5: cnode (guard: 1, guard_size: 28) } @@ -40,6 +40,6 @@ cnode2 { 5: cnode (guard: 1, guard_size: 28) } tcb { cspace: cnode2 (guard: 0, guard_size: 28) vspace: pd1 - ipc_buffer_slot: frame[5] (RWG) + ipc_buffer_slot: frame[5] (RW) } } diff --git a/capDL-tool/cap-dist-elf-simpleserver.right b/capDL-tool/cap-dist-elf-simpleserver.right index a0798f88..c2fba984 100644 --- a/capDL-tool/cap-dist-elf-simpleserver.right +++ b/capDL-tool/cap-dist-elf-simpleserver.right @@ -20,19 +20,19 @@ objects { 0: tcb 1: ep (RWG) 2: cnode (guard_size: 28) - 3: frame[5] (RWX) + 3: frame[5] (RW) } cnode2 {5: cnode (guard: 1, guard_size: 28)} pd1 {0: pt1} - pt1 {16: frame[0..5] (RWX)} + pt1 {16: frame[0..5] (RW)} tcb { 0: cnode2 (guard_size: 28) 1: pd1 - 4: frame[5] (RWX) + 4: frame[5] (RW) } } cdt { diff --git a/capDL-tool/capdl.dtd b/capDL-tool/capdl.dtd index 88aa2a42..b9998ac8 100644 --- a/capDL-tool/capdl.dtd +++ b/capDL-tool/capdl.dtd @@ -30,6 +30,7 @@ + diff --git a/capDL-tool/doc/capDL.md b/capDL-tool/doc/capDL.md index 09063fb6..c8b42557 100644 --- a/capDL-tool/doc/capDL.md +++ b/capDL-tool/doc/capDL.md @@ -128,8 +128,10 @@ in section [Modules](#modules). | 'asid' ':' asid | 'cached' | 'uncached' + | 'executable' + | 'execute_never' - right ::= 'R' | 'W' | 'G' | 'X' + right ::= 'R' | 'W' | 'G' | 'P' asid ::= '(' number ',' number ')' parent ::= '- child_of' slot_ref diff --git a/capDL-tool/tools/capdl.vim b/capDL-tool/tools/capdl.vim index 8f727393..fe2b96f7 100644 --- a/capDL-tool/tools/capdl.vim +++ b/capDL-tool/tools/capdl.vim @@ -20,7 +20,7 @@ syn keyword CapDLKeyword arch caps objects arm11 ia32 syn match CapDLIRQMap "\" syn match CapDLIRQ "\\( maps\)\@!" syn keyword CapDLObject notification asid_pool cnode ep frame io_device io_ports io_pt pd pt tcb ut -syn keyword CapDLAttribute addr affinity badge dom fault_ep G guard guard_size init ip max_prio prio sp R RG RX RW RWG RWX W WG WX paddr cached uncached +syn keyword CapDLAttribute addr affinity badge dom fault_ep G guard guard_size init ip max_prio prio sp R RG RX RW RWG W WG WX paddr cached uncached execute execute_never syn match CapDLCPP "[ \t]*#.*$" syn match CapDLLiteral "\<\(0x\)\?[0-9]\+\(k\|M\)\?\( bits\)\?\>" syn match CapDLLiteral "\<0x[0-f]\+\>" diff --git a/python-capdl-tool/capdl/Cap.py b/python-capdl-tool/capdl/Cap.py index 89965331..51be28cd 100644 --- a/python-capdl-tool/capdl/Cap.py +++ b/python-capdl-tool/capdl/Cap.py @@ -27,6 +27,7 @@ def __init__(self, referent, **kwargs): self.guard_size = 0 self.badge = None self.cached = True + self.executable = True self.ports = None self.mapping_container = None self.mapping_slot = None @@ -92,14 +93,15 @@ def __repr__(self): rights = [sym for sym, flag in [('R', self.read), ('W', self.write), - ('X', is_frame and self.grant), - ('G', not is_frame and self.grant), + ('G', self.grant), ('P', self.grantreply)] if flag] extra.append(''.join(rights)) if isinstance(self.referent, Frame) and not self.cached: extra.append('uncached') + if isinstance(self.referent, Frame) and not self.executable: + extra.append('execute_never') if isinstance(self.referent, Frame) and \ self.mapping_container is not None: extra.append('mapping: (%s, %d)' % (self.mapping_container.name, self.mapping_slot)) diff --git a/python-capdl-tool/capdl/PageCollection.py b/python-capdl-tool/capdl/PageCollection.py index 2be2fc5a..5c239cd1 100644 --- a/python-capdl-tool/capdl/PageCollection.py +++ b/python-capdl-tool/capdl/PageCollection.py @@ -86,7 +86,7 @@ def _get_page_cap(self, existing_frames, page, page_vaddr, page_counter, spec): page['size']) spec.add_object(frame) return Cap(frame, read=page['read'], write=page['write'], - grant=page['execute']) + executable=page['execute']) def get_spec(self, existing_frames={}): if self._spec is not None: