# FROST

The FROST language with associated tooling and documentation.

## Getting Started

This project contains a reference implementation of FROST, consisting of a domain-specific language (DSL) for authoring access control policies. This DSL is embedded in Haskell, which is assumed to be installed e.g. via Stack.

See the Yellow Paper to learn more about FROST. Developer-friendly documentation will also be available in due course.

## Writing Policies

Policies come in several forms, though typically they will be rules like “grant if the following condition holds…”. The Demo policy script contains an illustrative example of such a condition:

cond =  subj =:= name "courier"  And
(obj  =:= name "vehicle") And
(act  =:= name "getLocation" Or (act =:= name "openTrunk"  And
(t >:= name "startTime") And
(t <:= name "endTime")))
where
t = name "currentTime"


In fact, this is a conjunction of sub-conditions:

• the subject matches "courier"
• the object they request access to is some known "vehicle"
• the action they request to perform on it is either "getLocation" or, if it is instead "openTrunk", that the "currentTime" is between some known "startTime" and "endTime".

The string literals "courier", "vehicle", etc. are tagged with name to declare them as names of domain-specific entities that can be resolved to actual values. The terms subject, object and action are so common that they deserve a certain special status, denoted simply as subj, obj and act respectively.

While FROST is a small language at its core, it is nevertheless extended with convenient syntactic constructions from its host language Haskell, by virtue of being an embedded DSL. In particular, expressions may be bound to named variables e.g. in the above, the variable cond names the condition just described in the right hand side of the =. Note also that the entity "currentTime" is bound, though the where clause ensures this variable t has scope local only to cond.

### Policy Idioms

Now to express cond as the “body” of a grant-if rule policy, we can use grantIf0:

pol = grantIf0 cond


This returns a policy (called pol here) that grants whenever the condition cond is satisfied. Note the 0 in grantIf0 is a mnemonic for a zero-obligation policy, which suffices for simple cases. There is also a dual denyIf0 rule.

A common idiom is to take an existing policy and “wrap” it such that any decision from it other than grant would be treated conservatively as deny. Indeed, this pattern is common enough to deserve its own combinator function denyByDefault. For example,

pol' = denyByDefault pol


wraps the policy pol in the way described. In practice this enriches pol in the following way: if cond cannot be satisfied then pol' denies! Another important idiom join takes two policies and “merges” their information content. Other idioms can be defined with policy combinators in a similar way.

## Compiling Policies

Any FROST policy can be expressed in a canonical join normal form that is completely determined by a pair of Boolean circuits, expressed in the same language as conditions. The rationale for such circuits as a lower-level language is two-fold: they can be evaluated in a standard, predictable way - potentially even on devices with limited capacity - and they also form a basis for static analyses of policies.

Use compile0 to translate a policy into a lower-level circuit-pair. Internally, it uses the compilation functions goc and doc to generate the circuits. Furthermore, circuits are serialisable into a JSON form, by using one of the encode functions. For example,

encodeFilePretty "my-policy.json" (compile0 pol)


encodes the circuits from compile0 pol into a pretty-printed byte string that is written to the supplied file path.

## Testing

The Proptest module contains a suite of property-based tests (using QuickCheck, a standard test library). At present, they validate a core subset of the FROST language equipped with an evaluator evalP that defines the basic semantics of (zero-obligation) policies, given an environment of values assigned to named entities.

The properties themselves express some of the equational laws of FROST policies. As a simple example, join is idempotent i.e. merging a policy with itself leaves it unchanged:

prop_idemJoin p env =
evalP p env == evalP (p join p) env


This property holds if for every randomly generated policy p and environment env, both p and the join of p with itself evaluate (with respect to env) to the same decision.

Another property validates the compilation functions:

prop_joinNormalForm p env =
evalP p env == evalP (grantIf0 (goc p) join
denyIf0  (doc p)) env


This captures the join normal form law mentioned above: any policy is faithfully represented by its compilation expressed in canonical form.