Hails.PolicyModule.DSL

This module exports a domain specific language for specifying policy module policies. It is recommended that all policy modules use this code when specifying security policies as it simplifies auditing and building trust in the authors. Policy modules are described in Hails.PolicyModule, which is a pre-required reading to this module's documentation.

Consider creating a policy module where anybody can read and write freely to the databse. In this databsae we wish to create a simple user model collecting user names and passwords. This collection "users" is also readable and writable by anybody. However, the passwords must always belong to the named user. Specifically, only the user (or policy module) may read and modify the password. This policy is implemented below:

data UsersPolicyModule = UsersPolicyModuleTCB DCPriv
  deriving Typeable

instance PolicyModule UsersPolicyModule where
  initPolicyModule priv = do
    setPolicy priv $ do
      database $ do
        readers ==> unrestricted
        writers ==> unrestricted
        admins  ==> this
      collection "users" $ do
        access $ do
          readers ==> unrestricted
          writers ==> unrestricted
        clearance $ do
          secrecy   ==> this
          integrity ==> unrestricted
        document $ doc -> do
          readers ==> unrestricted
          writers ==> unrestricted
        field "name"     $ searchable
        field "password" $ labeled $ doc -> do
          let user = "name" ``at`` doc :: String
          readers ==> this \/ user
          writers ==> this \/ user
    return $ UsersPolicyModuleTCB priv
      where this = privDesc priv

Notice that the database is public, as described above, but only this policy module may modify the internal collection names (as indicated by the admin keyword). Similarly the collection is publicly accessible (as set with the access keyword), and may contain data at most as sensitve as the policy module can read (i.e., the clearance).

Documents retrieved from the "users" collection are public (as indicated by the document data-dependent policy that sets the readers and writers). The field "name" is searchable (i.e., it is a SearchableField) and thus can be used in query predicates. Conversely, the "password" field is labeled using a data-dependent policy. Specifically the field is labed using the "name" value contained in the document (i.e., the user's name): hence only the user having the right privilege or the policy module (this) may read and create such data.

Documentation

setPolicy :: DCPriv -> PolicyExpM () -> PMAction ()

High level function used to set the policy in a PolicyModule. This function takes the policy module's privileges and a policy expression, and produces a PMAction that sets the policy.

Label components (or roles)

readers :: Readers

Set secrecy component of the label, i.e., the principals that can read.

secrecy :: Readers

Set secrecy component of the label, i.e., the principals that can read.

writers :: Writers

Set integrity component of the label, i.e., the principals that can write.

integrity :: Writers

Set integrity component of the label, i.e., the principals that can write.

unrestricted :: CNF

admins :: Admins

Synonym for Admins.

(==>) :: (Role r s m, ToCNF c) => r -> c -> m () infixl 5

r ==> c effectively states that role r (i.e., readers, writers, admins must imply label component c).

(<==) :: (Role r s m, ToCNF c) => r -> c -> m () infixl 5

Inverse implication. Purely provided for readability. The direction is not relevant to the internal representation.

Creating databases label policies

database :: DBExpM () -> PolicyExpM ()

Create a database lebeling policy The policy must set the label of the database, i.e., the readers and writers. Additionally it must state the admins that can modify the underlying collection-set

For example, the policy

database $ do
  readers ==> "Alice" \/ "Bob" \/ "Clarice"
  writers ==> "Alice" \/ "Bob"
  admins  ==> "Alice"

states that Alice, Bob, and Clarice can read from the database, including the collections in the database (the readers is used as the secrecy component in the collection-set label). Only Alice or Bob may, however, write to the database. Finally, only Alice can add additional collections in the policy module code.

Creating collection policies

collection :: CollectionName -> ColExpM () -> PolicyExpM ()

Set the collection labels and policies. Each collection, must at least specify who can access the collection, what the clearance of the data in the collection is, and how documents are labeled. Below is an example that also labels the password field and declares name a searchable key.

collection "w00t" $ do
  access $ do
    readers ==> "Alice" \/ "Bob"
    writers ==> "Alice"          
  clearance $ do
    secrecy   ==> "Users"
    integrity ==> "Alice"          
  document $ \doc ->  do
    readers ==> 'unrestricted'
    writers ==> "Alice" \/ (("name" `at`doc) :: String)
  field "name" searchable
  field "password" $ labeled $ \doc -> do
    readers ==> (("name" `at`doc) :: String)
    writers ==> (("name" `at`doc) :: String)

access :: ColAccExpM () -> ColExpM ()

Set the collection access label. For example,

collection "w00t" $ do
  ...
  access $ do
    readers ==> "Alice" \/ "Bob"
    writers ==> "Alice"

states that Alice and Bob can read documents from the collection, but only Alice can insert new documents or modify existing ones.

clearance :: ColClrExpM () -> ColExpM ()

Set the collection clearance. For example,

collection "w00t" $ do
  ...
  clearance $ do
    secrecy ==> "Alice" \/ "Bob"
    integrity ==> "Alice"

states that all data in the collection is always readable by Alice and Bob, and no more trustworthy than data Alice can create.

document :: (HsonDocument -> ColDocExpM ()) -> ColExpM ()

Set data-dependent document label. For example,

collection "w00t" $ do
  ...
  document $ \doc ->  do
    readers ==> 'unrestricted'
    writers ==> "Alice" \/ (("name" `at`doc) :: String)

states that every document in the collection is readable by anybody, and only Alice or the principal named by the name value in the document can modify or insert such data.

Creating field policies

field :: FieldName -> ColFieldExpM () -> ColExpM ()

Set field policy. A field can be declared to be a searchable key or a labeled value.

Declaring a field to be a searchable key is straight forward:

collection "w00t" $ do
  ...
  field "name" searchable

The labeled field declaration is similar to the document policy, but sets the label of a specific field. For example

collection "w00t" $ do
  ...
  field "password" $ labeled $ \doc -> do
    let user = "name" `at` doc :: String
    readers ==> user
    writers ==> user

states that every password field in the is readable and writable only by or the principal named by the name value of the document can modify or insert such data.

searchable :: ColFieldExpM ()

Set the underlying field to be a searchable key.

  field "name" searchable

key :: ColFieldExpM ()

Synonym for searchable

labeled :: (HsonDocument -> ColLabFieldExpM ()) -> ColFieldExpM ()

Set data-dependent document label

  field "password" $ labeled $ \doc -> do
    readers ==> (("name" `at`doc) :: String)
    writers ==> (("name" `at`doc) :: String)