hails- Multi-app web platform framework

Safe HaskellTrustworthy




This module exports labeled documents and the databse monad (DBAction). The database monad is used by apps and policy modules to execute database actions against a policy module's databse (see Hails.PolicyModule). The Hails database model and interface is documented in Hails.Database.



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.

colLabel :: Collection -> DCLabelSource

Collection label

colClearance :: Collection -> DCLabelSource

Collection clearance

colPolicy :: Collection -> CollectionPolicySource

Collection labeling policies


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.

databaseLabel :: Database -> DCLabelSource

Label of database

databaseCollections :: Database -> CollectionSetSource

Collections associated with databsae

Labeled documents

Hails DB monad

data 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.

class Monad m => MonadDB m whereSource

Arbitrary monad that can perform database actions.


liftDB :: DBAction a -> m aSource

Lift a database action into the database monad.

runDBAction :: DBAction a -> DBActionState -> DC (a, DBActionState)Source

Execute a database action returning the final result and state. In general, code should instead use evalDBAction. This function is primarily used by trusted code to initialize a policy module which may have modified the underlying database.

evalDBAction :: DBAction a -> DBActionState -> DC aSource

Execute a database action returning the final result.

getDatabase :: DBAction DatabaseSource

Get the underlying database. Must be able to read from the database as enforced by applying taint to the database label. This is required because the database label protects the label on collections which can be projected given a Database value.

getDatabaseP :: DCPriv -> DBAction DatabaseSource

Same as getDatabase, but uses privileges when raising the current label.

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.