hails-0.11.2.1: Multi-app web platform framework

Safe HaskellTrustworthy
LanguageHaskell98

Hails.PolicyModule.DSL

Contents

Description

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.

Synopsis

Documentation

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

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 Source

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

secrecy :: Readers Source

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

writers :: Writers Source

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

integrity :: Writers Source

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

admins :: Admins Source

Synonym for Admins.

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

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 Source

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

Creating databases label policies

database :: DBExpM () -> PolicyExpM () Source

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 () Source

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 () Source

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 () Source

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 () Source

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 () Source

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 () Source

Set the underlying field to be a searchable key.

  field "name" searchable

key :: ColFieldExpM () Source

Synonym for searchable

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

Set data-dependent document label

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