LIO.DCLabel.Privs

Privileges allow a piece of code to bypass certain information flow restrictions imposed by labels. A privilege is simply a conjunction of disjunctions of Principals, i.e., a Component. We say that a piece of code containing a singleton Clause owns the Principal composing the Clause. However, we allow for the more general notion of ownership of a clause, or category, as to create a privilege-hierarchy. Specifically, a piece of code exercising a privilege P can always exercise privilege P' (instead), if P' => P. (This is similar to the DLM notion of "can act for".) Hence, if a piece of code with certain privileges implies a clause, then it is said to own the clause. Consequently it can bypass the restrictions of the clause in any label.

Note that the privileges form a partial order over logicla implication (=>), such that allPrivTCB => P and P => noPriv for any privilege P. Hence, a privilege hierarchy which can be concretely built through delegation, with allPrivTCB corresponding to the root, or all, privileges from which all others may be created. More specifically, given a privilege P' of type DCPriv, and a privilege description P of type DCPrivDesc, any piece of code can use delegatePriv to "mint" P, assuming P' => P.

Documentation

type DCPrivDesc = Component

A privilege description is simply a conjunction of disjunctions. Unlike (actually minted) privileges (see DCPriv), privilege descriptions may be created by untrusted code.

data DCPriv

A privilege is a minted and protected privilege description (DCPrivDesc) that may only be created by trusted code or delegated from an existing DCPriv.

Instances

Eq DCPriv

Show DCPriv

Typeable DCPriv

Monoid DCPriv

Privileges can be combined using mappend

PrivTCB DCPriv

MintTCB DCPriv DCPrivDesc

PrivDesc DCPriv DCPrivDesc

Priv DCLabel DCPriv

Helpers

noPriv :: DCPriv

The empty privilege, or no privileges, corresponds to logical True.

dcDelegatePriv :: DCPriv -> DCPrivDesc -> Maybe DCPriv

Given a privilege and a privilege description turn the privilege description into a privilege (i.e., mint). Such delegation succeeds only if the supplied privilege implies the privilege description.

dcOwns :: DCPrivDesc -> Clause -> Bool

We say a piece of code having a privilege object (of type DCPriv) owns a clause when the privileges allow code to bypass restrictions imposed by the clause. This is the case if and only if the DCPriv object contains one of the Principals in the Clause. This function can be used to make such checks.