The FROST language with associated tooling and documentation.
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.
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
- the object they request access to is some known
- the action they request to perform on it is either
"getLocation"or, if it is instead
"openTrunk", that the
"currentTime"is between some known
The string literals
"vehicle", etc. are tagged with
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
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
"currentTime" is bound, though the
where clause ensures this variable
t has scope local only to
Now to express
cond as the “body” of a grant-if rule policy, we can
pol = grantIf0 cond
This returns a policy (called
pol here) that grants whenever the condition
is satisfied. Note the
grantIf0 is a mnemonic for a zero-obligation
policy, which suffices for simple cases. There is also a dual
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
the following way: if
cond cannot be satisfied then
pol' denies! Another
join takes two policies and “merges” their information
content. Other idioms can be defined with policy combinators in a similar way.
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.
compile0 to translate a policy into a lower-level circuit-pair.
Internally, it uses the compilation functions
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.
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
The properties themselves express some of the equational laws of FROST policies. As a
join is idempotent i.e. merging a policy with itself leaves it
prop_idemJoin p env = evalP p env == evalP (p `join` p) env
This property holds if for every randomly generated policy
p and environment
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.