hails- Multi-app web platform framework

Safe HaskellUnsafe




This module exports the basic database types and constructors. See Hails.Database for a description of the Hails database system.



type CollectionName = TextSource

The name of a collection.

data Collection Source

A Collection is a MongoDB collection name with an associated label, clearance and labeling policy. Access to the collection is restricted according to the collection label. Data inserted-to and retrieved-from the collection will be labeled according to the collection policy, with the guarantee that no data more sensitive than the collection clearance can be inserted into the collection.




colName :: CollectionName

Collection name

colLabel :: DCLabel

Collection label

colClearance :: DCLabel

Collection clearance

colPolicy :: CollectionPolicy

Collection labeling policies



:: CollectionName

Collection name

-> DCLabel

Collection label

-> DCLabel

Collection clearance

-> CollectionPolicy

Collection policy

-> Collection 

Create a Collection, ignoring any IFC restrictions.


type DatabaseName = TextSource

The name of a database.

data Database Source

A Database is a MongoDB database with an associated label and set of collections. The label is used to restrict access to the database. Since collection policies are specified by policy modules, every collection must always be associated with some database (and thereby, policy module); a policy module is not allowed to create a collection (and specify policies on it) in an arbitrary database. We allow for the existance of a collection to be secrect, and thus protect the set of collections with a label.




databaseName :: DatabaseName

Database name

databaseLabel :: DCLabel

Label of database

databaseCollections :: CollectionSet

Collections associated with databsae


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.

Hails DB monad

newtype DBAction a Source

A DBAction is the monad within which database actions can be executed, and policy modules are defined. The monad is simply a state monad with DC as monad as the underlying monad with access to a database system configuration (Pipe, AccessMode, and Database). The value constructor is part of the TCB as to disallow untrusted code from modifying the access mode.



data DBActionState Source

The database system state threaded within a Hails computation.




dbActionPipe :: Pipe

Pipe to underlying database system

dbActionMode :: AccessMode

Types of reads/write to perform

dbActionDB :: Database

Database computation is currently executing against

dbActionPriv :: DCPriv

Privilege of the policy module related to the DB

getActionStateTCB :: DBAction DBActionStateSource

Get the underlying state.

putActionStateTCB :: DBActionState -> DBAction ()Source

Get the underlying state.

updateActionStateTCB :: (DBActionState -> DBActionState) -> DBAction ()Source

Update the underlying state using the supplied function.

makeDBActionStateTCB :: DCPriv -> DatabaseName -> Pipe -> AccessMode -> DBActionStateSource

Given a policy module's privileges, database name, pipe and access mode create the initial state for a DBAction. The underlying database is labeled with the supplied privileges: both components of the label (secrecy and integrity) are set to the privilege description. In other words, only code that owns the policy module's privileges can modify the database configuration. Policy modules can use setDatabaseLabelP to change the label of their database, and setCollectionMapLabelP to change the label of the collection map.

setDatabaseLabelTCB :: DCLabel -> DBAction ()Source

Set the label of the underlying database to the supplied label, ignoring IFC.

setCollectionSetLabelTCB :: DCLabel -> DBAction ()Source

Set the label of the underlying database to the supplied label, ignoring IFC.



:: Collection

New collection

-> DBAction () 

Associate a collection with underlying database, ignoring IFC.

Database system configuration

type Pipe = Pipeline Response Message

Thread-safe TCP connection with pipelined requests

data AccessMode

Type of reads and writes to perform



Read-only action, reading stale data from a slave is OK.


Read-write action, slave not OK, every write is fire & forget.

ConfirmWrites GetLastError

Read-write action, slave not OK, every write is confirmed with getLastError.


Exception thrown by failed database actions

data DBError Source

Exceptions thrown by invalid database queries.



Collection does not exist


Policy module not found

ExecFailure Failure

Execution of action failed

Lifting Database.MongoDB actions

execMongoActionTCB :: Action IO a -> DBAction aSource

Lift a mongoDB action into the DBAction monad. This function always executes the action with Database.MongoDB's access. If the database action fails an exception of type Failure is thrown.