{-# LANGUAGE Trustworthy #-} {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} {- | Privileges are instances of the class called 'Priv'. They represent the ability to bypass the protection of certain labels. Specifically, privilege allows you to behave as if @L_1 ``canFlowTo`` L_2@ even when that is not the case. The process of making data labeled @L_1@ affect data labeled @L_2@ when @not (L_1 ``canFlowTo`` L_2)@ is called /downgrading/. The basic method of the 'Priv' class is 'canFlowToP', which performs a more permissive can-flow-to check by exercising particular privileges (in literature this relation is a pre-order, commonly written as ⊑ₚ). Almost all 'LIO' operations have variants ending @...P@ that take a privilege argument to act in a more permissive way. All 'Priv' types are 'Monoid's, and so privileges can be combined with 'mappend'. The creation of 'Priv' values is specific to the particular label type in use; the method used is 'mintTCB', but the arguments depend on the particular label type. -} module LIO.Privs ( -- * Privilege descriptions PrivDesc(..) -- * Privileges , Priv(..) , NoPrivs(..) ) where import Data.Monoid import LIO.Label import LIO.Privs.TCB -- | This class defines privileges and the more-permissive relation -- ('canFlowToP') on labels using privileges. Additionally, it defines -- 'partDowngradeP' which is used to downgrage a label up to a limit, -- given a set of privilege. class (Label l, PrivTCB p, Monoid p) => Priv l p where -- | The \"can-flow-to given privileges\" pre-order used to compare -- two labels in the presence of privileges. If @'canFlowToP' p L_1 -- L_2@ holds, then privileges @p@ are sufficient to downgrade data -- from @L_1@ to @L_2@. Note that @'canFlowTo' L_1 L_2@ implies -- @'canFlowToP' p L_1 L_2@ for all @p@, but for some labels and -- privileges, 'canFlowToP' will hold even where 'canFlowTo' does -- not. canFlowToP :: p -> l -> l -> Bool canFlowToP p a b = partDowngradeP p a b `canFlowTo` b -- | Roughly speaking, @L_r = partDowngradeP p L L_g@ computes how -- close one can come to downgrading data labeled @L@ to the goal label -- @L_g@, given privileges @p@. When @p == 'NoPrivs'@, the resulting -- label @L_r == L ``upperBound`` L_g@. If @p@ contains /all/ -- possible privileges, then @L_r == L_g@. -- -- More specifically, @L_r@ is the greatest lower bound of the -- set of all labels @L_l@ satisfying: -- -- 1. @ L_g ⊑ L_l@, and -- -- 2. @ L ⊑ₚ L_l@. -- -- Operationally, @partDowngradeP@ captures the minimum change required -- to the current label when viewing data labeled @L_l@. A common -- pattern is to use the result of 'getLabel' as @L_g@ (i.e., the -- goal is to use privileges @p@ to avoid changing the label at all), -- and then compute @L_r@ based on the label of data the code is -- about to observe. partDowngradeP :: p -- ^ Privileges -> l -- ^ Label from which data must flow -> l -- ^ Goal label -> l -- ^ Result -- -- No privileges -- -- | Generic privilege type used to denote the lack of privileges. data NoPrivs = NoPrivs deriving (Show, Read) instance PrivTCB NoPrivs instance PrivDesc NoPrivs NoPrivs where privDesc = id instance MintTCB NoPrivs NoPrivs where mintTCB = id instance Monoid NoPrivs where mempty = NoPrivs mappend _ _ = NoPrivs -- | With lack of privileges, 'canFlowToP' is simply 'canFlowTo', and -- 'partDowngradeP' is the least 'upperBound'. instance Label l => Priv l NoPrivs where canFlowToP _ l1 l2 = l1 `canFlowTo` l2 partDowngradeP _ l lg = l `upperBound` lg