Hails.Database

This module exports the database interface used by apps and policy modules to carry out database queries. The Hails data model is similar to that of MongoDB. Below we highlight some similarities and difference. We refer the interested reader to the documentation in Hails.PolicyModule for more details on the role of labels in Hails.

At the coarsest level code can execute database actions (DBAction) against the Database of a policy module using withPolicyModule. Different from MongoDB's notion of a database, Hails databases have an associated Label which is used to restrict who can access the database.

Each Database is composed of a set of Collections. The existence of a collection is protected by a collection-set label, which is, intern, protected by the database label. A collection is an approach to organizing and grouping elements of the same model. For example, collection "users" may contain elements (documents) corresponding to users of the system. Each collection has a label, clearance, and associated collection policy. The label of a collection serves the same role as the database label, but at a finer grain: it protects who can read and write to the collection. The collection clearance is also a label, but its role is to set an upper bound on the sensitivity of data that is and can be stored in the collection. For example, the collection "user" may set a clearance such that the system's private keys cannot be stored in the collection (by accident or malice). The collection policy specifies how elements of the collection are to be labeled when retrieved from the database.

The aforementioned elements of a collection are documents of type HsonDocument. Documents are the basic storage units composed of a fields (of type HsonField), which are effectively key-value pairs. The first part of the collection policy is to specify how such documents are labeled upon retrieval from the database. Namely, by providing a function from the document to a label. Keys, or field names, have type FieldName while values have type HsonValue. Hails values are a subset of MongoDB's BSON specification. The second part of the collection policy is used to specify if a field value is publicly-searchable (i.e., readable by anybody that can read from the collection) or labeled according to a function that may depend on the data contained within the document itself. Hence, different form MongoDB's documents, Hails documents are typically labeled and thus protect the potentially-sensitive data contained within.

This module is analogous to Database.MongoDB and uses MongoDB as the backed. Since the interfaces are similar we recommend glancing at their documentation as well.

Hails database monad

data DBAction a

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.

Instances

Monad DBAction

Functor DBAction

Applicative DBAction

MonadDB DBAction

MonadLIO DCLabel DBAction

class Monad m => MonadDB m where

Arbitrary monad that can perform database actions.

Methods

liftDB :: DBAction a -> m a

Lift a database action into the database monad.

Instances

MonadDB DBAction

MonadDB PMAction

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

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

getDatabase :: DBAction Database

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

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

Exception thrown by failed database actions

data DBError

Exceptions thrown by invalid database queries.

Constructors

UnknownCollection

Collection does not exist

UnknownPolicyModule

Policy module not found

ExecFailure Failure

Execution of action failed

Instances

Show DBError

Typeable DBError

Exception DBError

Database layers

Database

type DatabaseName = Text

The name of a database.

data Database

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 :: Database -> DatabaseName

Database name

databaseLabel :: Database -> DCLabel

Label of database

databaseCollections :: Database -> CollectionSet

Collections associated with databsae

Collection

type CollectionName = Text

The name of a collection.

type CollectionSet = DCLabeled (Set Collection)

A labeled Collection set.

data Collection

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.

Instances

Eq Collection

Ord Collection

colName :: Collection -> CollectionName

Collection name

colLabel :: Collection -> DCLabel

Collection label

colClearance :: Collection -> DCLabel

Collection clearance

colPolicy :: Collection -> CollectionPolicy

Collection labeling policies

Policy errors

data PolicyError

A document policy error.

Constructors

TypeError String

Document is not "well-typed"

PolicyViolation

Policy has been violated

Instances

Show PolicyError

Typeable PolicyError

Exception PolicyError

Documents

module Hails.Data.Hson

type LabeledHsonDocument = DCLabeled HsonDocument

A labeled HsonDocument.

Database queries

Write (insert/save)

class InsertLike doc where

Class used to generalize insertion and saving of documents. Specifically, it permits reusing function names when inserting/saving both already-labeled and unlabeled documents. Minimal definition: insertP and saveP.

Methods

insert :: CollectionName -> doc -> DBAction ObjectId

Insert document into collection and return its _id value. When performing an insert it is required that the computation be able to write to both the database and collection. To this end, insert internally applies guardWrite on the database label and collection label. Of course, the computation must be able to name the collection in the database, and thus must be able to read the database collection map as verified by applying taint to the collections label.

When inserting an unlabeled document, all policies must be succesfully applied using applyCollectionPolicyP and the document must be "well-typed" (see applyCollectionPolicyP).

When inserting an already-labeled document, the labels on fields and the document itself are compared against the policy-generated labels. Note that this approach allows an untrusted piece of code to insert a document it could not label according to the policy module.

insert_ :: CollectionName -> doc -> DBAction ()

Same as insert except it does not return _id

insertP :: DCPriv -> CollectionName -> doc -> DBAction ObjectId

Same as insert, but uses privileges when applying the policies and performing label comparisons.

insertP_ :: DCPriv -> CollectionName -> doc -> DBAction ()

Same as insertP except it does not return the _id.

save :: CollectionName -> doc -> DBAction ()

Update a document according to its _id value. The IFC requirements subsume those of insert. Specifically, in addition to being able to apply all the policies and requiring that the current label flow to the label of the collection and database, save requires that the current label flow to the label of the existing database record (i.e, the existing document can be overwritten).

saveP :: DCPriv -> CollectionName -> doc -> DBAction ()

Same as save, but uses privileges when applying the policies and performing label comparisons. Note that a find is performed if the provided document contains an _id field. This lookup does _not_ leak timing information since the _id field is always searchable and thus solely protected by the collection label (which the computation is tainted by).

Instances

InsertLike HsonDocument

InsertLike LabeledHsonDocument

Read

find :: Query -> DBAction Cursor

Fetch documents satisfying query. A labeled Cursor is returned, which can be used to retrieve the actual HsonDocuments. For this function to succeed the current computation must be able to read from the database and collection (implicilty the database's collection-set). This is satisfied by applying taint to the join join of the collection, database, and ccollection-set label. The curor label is labeled by the upperBound of the database and collection labels and must be used within the same withPolicyModule block.

Note that this function is quite permissive in the queries it accepts. Specifically, any non-SearchableFields used in sort, order, or hint are ignored (as opposed to throwing an exception).

findP :: DCPriv -> Query -> DBAction Cursor

Same as find, but uses privileges when reading from the collection and database.

next :: Cursor -> DBAction (Maybe LabeledHsonDocument)

Return next HsonDocument in the query result, or Nothing if finished. Note that the current computation must be able to read from the labeled Cursor. To enforce this, next uses taint to raise the current label to join of the current label and 'Cursor'\'s label. The returned document is labeled according to the underlying Collection policy.

nextP :: DCPriv -> Cursor -> DBAction (Maybe LabeledHsonDocument)

Same as next, but usess privileges when raising the current label.

findOne :: Query -> DBAction (Maybe LabeledHsonDocument)

Fetch the first document satisfying query, or Nothing if not documents matched the query.

findOneP :: DCPriv -> Query -> DBAction (Maybe LabeledHsonDocument)

Same as findOne, but uses privileges when performing label comparisons.

Cursor

data Cursor

A labeled cursor. The cursor is labeled with the join of the database and collection it reads from. The collection policies are "carried" along since they are applied on-demand.

curLabel :: Cursor -> DCLabel

Cursor label

Selection

class Select selectionOrQuery where

Class used to simplicy the creation of a 'Selection'/'Query'. Specifically, select can be used to create a Section in a straight foward manner, but similarly can be used to create a Query with a set of default options.

Methods

select :: Selector -> CollectionName -> selectionOrQuery

Given a selector and collection name create a Query. The resultant type depends on the use case, for example, in find select mySel myCol is a Query, but in delete it is a Selection.

Instances

Select Selection

Select Query

data Selection

A Section is a Selector query on a Collection. In other words, a Selection is the necessary information for performing a database query.

Constructors

Selection

Fields

selectionSelector :: Selector

Selection query.

selectionCollection :: CollectionName

Collection to perform query on.

Instances

Show Selection

Select Selection

type Selector = BsonDocument

Filter for a query, analogous to the WHERE clause in SQL. [] matches all documents in collection. For example, [x -: a, y -: b] is analogous to WHERE x = a AND y = b in SQL.

Note: only FieldNames of SearchableFields may be used in selections, and thus all other fields are ignored.

Query

data Query

Use select to create a basic query with defaults, then modify if desired. Example: (select sel col) {limit =: 10}. For simplicity, and since policies may be specified in terms of arbitrary fields, The selection and sort fields are restricted to SearchableFields, or the _id field that is implicitly a SearchableField.

Constructors

Query

Fields

options :: [QueryOption]

Query options, default [].

selection :: Selection

WHERE clause,default []. Non-SearchableFields ignored.

project :: [FieldName]

The fields to project. Default [] corresponds to all.

skip :: Word32

Number of documents to skip, default 0.

limit :: Limit

Max number of documents to return. Default, 0, means no limit.

sort :: [Order]

Sort result by given order, default []. Non-SearchableFields ignored.

batchSize :: BatchSize

The number of document to return in each batch response from the server. 0 means MongoDB default.

hint :: [FieldName]

Force mongoDB to use this index, default [], no hint. Non-SearchableFields ignored.

Instances

Select Query

data QueryOption

Constructors

TailableCursor

Tailable means cursor is not closed when the last data is retrieved. Rather, the cursor marks the final object's position. You can resume using the cursor later, from where it was located, if more data were received. Like any latent cursor, the cursor may become invalid at some point – for example if the final object it references were deleted. Thus, you should be prepared to requery on CursorNotFound exception.

NoCursorTimeout

The server normally times out idle cursors after 10 minutes to prevent a memory leak in case a client forgets to close a cursor. Set this option to allow a cursor to live forever until it is closed.

AwaitData

Use with TailableCursor. If we are at the end of the data, block for a while rather than returning no data. After a timeout period, we do return as normal. | Exhaust -- ^ Stream the data down full blast in multiple more packages, on the assumption that the client will fully read all data queried. Faster when you are pulling a lot of data and know you want to pull it all down. Note: the client is not allowed to not read all the data unless it closes the connection. Exhaust commented out because not compatible with current Pipeline implementation

Partial

Get partial results from a _mongos_ if some shards are down, instead of throwing an error.

Instances

Eq QueryOption

Show QueryOption

type Limit = Word32

Maximum number of documents to return, i.e. cursor will close after iterating over this number of documents. 0 means no limit.

type BatchSize = Word32

The number of document to return in each batch response from the server. 0 means use Mongo default.

data Order

Sorting fields in Ascending or Descending order.

Constructors

Asc FieldName

Ascending order

Desc FieldName

Descending order

Instances

Eq Order

Ord Order

Show Order

Delete

delete :: Selection -> DBAction ()

Delete documents according to the selection. It must be that the current computation can overwrite the existing documents. That is, the current label must flow to the label of each document that matches the selection.

deleteP :: DCPriv -> Selection -> DBAction ()

Same as delete, but uses privileges.