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 = Text Source

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 -> DCLabel Source

Collection label

colClearance :: Collection -> DCLabel Source

Collection clearance

colPolicy :: Collection -> CollectionPolicy Source

Collection labeling policies


type DatabaseName = Text Source

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 -> DCLabel Source

Label of database

databaseCollections :: Database -> CollectionSet Source

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.

withDBContext :: String -> DBAction a -> DBAction a Source

Execute a database action with a "stack" context.

class Monad m => MonadDB m where Source

Arbitrary monad that can perform database actions.


liftDB :: DBAction a -> m a Source

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 a Source

Execute a database action returning the final result.

getDatabase :: DBAction Database Source

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 Database Source

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.