hails- Multi-app web platform framework

Safe HaskellTrustworthy




A policy module is a library with access to the privileges of a dedicated principal (conceptually, the author of the library) and associated with a dedicated database. The job of the policy module is to specify what sort of data may be stored in this database, and what access-control policies should be applied to it. However, because Hails uses information flow control (IFC) to enforce policies, a policy specified by a policy module on a piece of data is enforce even when an app gets a hold of the data.

IFC lets apps and policy modules productively use other policy modules despite mutual distrust. Moreover, IFC prevents malicious apps from violating any of the policies specified by a policy module. As a consequence, users need not place as much trust in apps. Rather, they need to trust or verify the policies specified by policy modules.

This moule exports the class which every policy module must be an instance of. Though simple, the class allows a policy module to create collections with a set of policies and associate them with the policy module's underlying database.


Creating policy modules

class Typeable pm => PolicyModule pm where Source

A policy module is specified as an instance of the PolicyModule class. The role of this class is to define an entry point for policy modules. The policy module author should set up the database labels and create all the database collections in initPolicyModule. It is these collections and corresponding policies that apps and other policy modules use when interacting with the policy module's database using withPolicyModule.

The Hails runtime system relies on the policy module's type pm to load the corresponding initPolicyModule when some code "invokes" the policy module using withPolicyModule. In fact when a piece of code wishes to execute a database action on the policy module, withPolicyModule first executes the policy module's initPolicyModule and passes the result (of type pm) to the invoking code.

Observe that initPolicyModule has access to the policy module's privileges, which are passed in as an argument. This allows the policy module to encapsulate its privileges in its pm type and allow code it trusts to use its privileges when executing a database action using withPolicyModule. Of course, untrusted code (which is usually the case) should not be allow to inspect values of type pm to get the encapsulated privileges.

Consider the example below:

 module My.Policy ( MyPolicyModule ) where

 import LIO
 import LIO.DCLabel
 import Data.Typeable
 import Hails.PolicyModule

 -- | Handle to policy module, not exporting @MyPolicyModuleTCB@
 data MyPolicyModule = MyPolicyModuleTCB DCPriv deriving Typeable

 instance PolicyModule MyPolicyModule where
   initPolicyModule priv = do
         -- Get the policy module principal:
     let this = privDesc priv
         -- Create label:
         l    = dcLabel dcTrue -- Everybody can read
                        this   -- Only policy module can modify
     -- Label database and collection-set:
     labelDatabaseP priv l l
     -- Create collections:
     createCollectionP priv "collection1" ...
     createCollectionP priv "collection2" ...
     createCollectionP priv "collectionN" ...
     -- Return the policy module:
     return (MyPolicyModuleTCB priv)

Here the policy module labels the database, labels the list of collections and finally creates N collections. The computation returns a value of type MyPolicyModule which wraps the policy module's privileges. As a consequence, trustworthy code that has access to the value constructor can use the policy module's privileges:

-- Trustworthy code within the same module (My.Policy)

alwaysInsert doc = withPolicyModule $ \(MyPolicyModuleTCB priv) ->
 insertP priv "collection1" doc

Here alwaysInsert uses the policy module's privileges to insert a document into collection "collection1". As such, if doc is well-formed the function always succeeds. (Of course, such functions should not be exported.)

Untrusted code in a different module cannot, however use the policy module's privilege:

-- Untrusted code in a separate module
import My.Policy

maybeInsertIntoDB appPriv doc = withPolicyModule $ (_ :: MyPolicyModule) ->
 insertP appPriv "collection1" doc

Depending on the privileges passed to maybeInsertIntoDB, and set policies, the insertion may or may not succeed.


initPolicyModule :: DCPriv -> PMAction pm Source

Entry point for policy module. Before executing the entry function, the current clearance is "raised" to the greatest lower bound of the current clearance and the label <"Policy module principal", |True>, as to allow the policy module to read data labeled with its principal.

data PMAction a Source

A policy module action (PMAction) is simply a wrapper for database action (DBAction). The wrapper is used to restrict app code from specifying policies; only policy module may execute PMActions, and thus create collections, set a label on their databases, etc.

withPMContext :: String -> PMAction a -> PMAction a Source

Execute a database action with a "stack" context.

Database and collection-set

The main role of a policy module is to provide a data model and security policies on said data. To this end and as previously mentioned, every policy module has access to a underlying MongoDB database. Each database, in turn, has an associated collection-set: a set of collections and their security policies.

At the coarsest level, the policy module can restrict access to the database by labeling it with setDatabaseLabel. By default, only the policy module itself may access the database. Whenever an app or another policy module accesses the database it is "tainted" by this label. Strictly speaking, the database label is the label on the database collection-set label. Hence, changing or observing the collection-set label is directed by the database label. Any meaningful database action (e.g., insert, update, etc.) involves a collection, and to observe the existence of collection in the database requires reading the collection-set. As already noted, the collection-set itself is protected by a label, which a policy module sets with setCollectionSetLabel, which is used to taint code that names collections of the database. Since the database label and collection-set labels are closely related Hails allows policy modules to set them using a single function labelDatabaseP.

labelDatabaseP Source


:: DCPriv

Policy module privilges

-> DCLabel

Database label

-> DCLabel

Collections label

-> PMAction () 

This is the first action that any policy module should execute. It is simply a wrapper for setDatabaseLabelP and setCollectionSetLabelP. Given the policy module's privilges, label for the database, and label for the collection-set labelDatabaseP accordingly sets the labels.

setDatabaseLabel :: DCLabel -> PMAction () Source

Set the label of the underlying database. The supplied label must be bounded by the current label and clearance as enforced by guardAlloc. Moreover the current computation mut write to the database, as enforce by applying guardWrite to the current database label. The latter requirement suggests that every policy module use setDatabaseLabelP when first changing the label.

setDatabaseLabelP Source


:: DCPriv

Set of privileges

-> DCLabel

New database label

-> PMAction () 

Same as setDatabaseLabel, but uses privileges when performing label comparisons. If a policy module wishes to allow other policy modules or apps to access the underlying databse it must use setDatabaseLabelP to "downgrade" the database label, which by default only allows the policy module itself to access any of the contents (including collection-set).

setCollectionSetLabel :: DCLabel -> PMAction () Source

The collections label protects the collection-set of the database. It is used to restrict who can name a collection in the database and who can modify the underlying collection-set (e.g., by creating a new collection). The policy module may change the default collections label, which limits access to the policy module alone, using setCollectionSetLabel.

The new label must be bounded by the current label and clearance as checked by guardAlloc. Additionally, the current label must flow to the label of the database which protects the label of the colleciton set. In most cases code should use setCollectionSetLabelP.

setCollectionSetLabelP Source


:: DCPriv

Set of privileges

-> DCLabel

New collections label

-> PMAction () 

Same as setCollectionSetLabel, but uses the supplied privileges when performing label comparisons.


As noted above a database consists of a set of collections. Each Hails collection is a MongoDB collection with a set of labels and policies. The main database "work units" are HsDocuments, which are stored and retrieved from collections (see Hails.Database).

Each collection has:

  • A collection name, which is simply a string that can be used to name the collection. These names are protected by the collection-set label. Hence when performing insert "myCollection" doc, the name "myCollection" is always checked to actually be part of the databsae.
  • A collection label. The collection label imposes a restriction on who can read and write to the collection.
  • A collection clearance. The collection clearance imposes an upper bound on the sensitivity of data that can be stored in the collection.
  • A collection policy (of type CollectionPolicy). The collection policy specifies how collection documents and internal fields should be labeled . Specifically, a collection policy can be used to assign labeling policies to specific fields (PolicyLabeled), declares fields as SearchableFields (effectively readable by anybody that can read from the collection), and at a coarser level assign a label to each document.

The creation of collections, similar to setting database and collection-set labels, is restricted to policy modules. Concretely, a policy module may use createCollection to create collections.

createCollection Source


:: CollectionName

Collection name

-> DCLabel

Collection label

-> DCLabel

Collection clearance

-> CollectionPolicy

Collection policy

-> PMAction () 

Create a Collection given a name, label, clearance, and policy. Several IFC rules must be respected for this function to succeed:

  1. The supplied collection label and clearance must be above the current label and below the current clearance as enforced by guardAlloc.
  2. The current computation must be able to read the database collection-set protected by the database label. The guard taint is used to guarantee this and raise the current label (to the join of the current label and database label) appropriately.
  3. The computation must be able to modify the database collection-set. The guard guardWrite is used to guarantee that the current label is essentially equal to the collection-set label.

Note: the collection policy is modified to make the _id field explicitly a SearchableField.

createCollectionP Source


:: DCPriv


-> CollectionName

Collection name

-> DCLabel

Collection label

-> DCLabel

Collection clearance

-> CollectionPolicy

Collection policy

-> PMAction () 

Same as createCollection, but uses privileges when performing IFC checks.

Collection policies

data CollectionPolicy Source

A collection policy contains the policy for labeling documents (documentLabelPolicy) at a coarse grained level, and a set of policies for labeling fields of a document (fieldLabelPolicies).

Specific fields can be associated with a FieldPolicy, which allows the policy module to either:

  • Explicitly make a field publicly readable to anyone who can access the collection by declaring the field to be a SearchableField, or
  • Label a field given the full documnet (see FieldPolicy).

Fields that do not have an associated policy are (conceputally) labeled with the document label (documentLabelPolicy). Similarly, the labels on the label of a policy-labeled field is the document label created with documentLabelPolicy. Note: the label on SearchableFields is solely the collection label.




documentLabelPolicy :: HsonDocument -> DCLabel

The label on documents of the collection.

fieldLabelPolicies :: Map FieldName FieldPolicy

The policies associated with specific fields.

data FieldPolicy Source

A FieldPolicy is a security policy associated with fields. SearchabelField specifies that the field can be referenced in the selection clause of a Query, and therefore only the collection label protects such fields. Conversely, FieldPolicy specifies a labeling policy for the field.



Unlabeled, searchable field.

FieldPolicy (HsonDocument -> DCLabel)

Policy labeled field.

isSearchableField :: FieldPolicy -> Bool Source

Returns True if the field policy is a SearchableField.

searchableFields :: CollectionPolicy -> [FieldName] Source

Get the list of names corresponding to SearchableFields.

Using policy module databases

Policy modules define a data model and security policies on the data. Hence, in Hails, apps solely focus on implementing controllers and viewers. Apps may use different policy modules to implement a rich experience without focusing on how to specify and enforce security policies. Moreover, Hails allows apps to use multiple policy modules that may be in mutual distrust while guaranteeing that the policies of each individual policy module are obeyed. Additionally, policy modules may themselves rely on other policy modules to implement their duties. A policy module's database is accessed using withPolicyModule.

withPolicyModule :: forall a pm. PolicyModule pm => (pm -> DBAction a) -> DC a Source

This function is the used to execute database queries on policy module databases. The function firstly invokes the policy module, determined from the type pm, and creates a pipe to the policy module's database. The supplied database query function is then applied to the policy module. In most cases, the value of type pm is opaque and the query is executed without additionally privileges.

withPolicyModule $ \(_ :: SomePolicyModule) -> do
 -- Perform database operations: insert, save, find, delete, etc.

Trustworthy code (as deemed by the policy module) may, however, be passed in additional privileges by encapsulating them in pm (see PolicyModule).


type TypeName = String Source

Policy type name. Has the form:

<Policy module package>:<Fully qualified module>.<Policy module type>

policyModuleTypeName :: PolicyModule pm => pm -> TypeName Source

Get the name of a policy module.

availablePolicyModules :: Map TypeName (Principal, DatabaseName, MVar (Maybe Pipe)) Source

This contains a map of all the policy modules. Specifically, it maps the policy moule types to a pair of the policy module principal and database name.

For the trusted programmer: The map itself is read from the file pointed to by the environment variable DATABASE_CONFIG_FILE. Each line in the file corresponds to a policy module. The format of a line is as follows

("<Policy module package>:<Fully qualified module>.<Policy module type>", "<Policy module database name>")

Example of valid line is:

("my-policy-", "my_db")

The principal used by Hails is the first projection with a "_" suffix. In the above, the principal assigned by Hails is: