Polar Rules Syntax
Polar is Oso's configuration language. It is a declarative, logic-based language that is optimized for handling the ambiguity inherent in writing authorization policies. Most folks can learn the basics in an hour. This guide is a brief description of the core syntax of Polar.
Each Polar file defines a set of rules. When a Polar file is loaded into the authorization engine, all rules are added to the engine's knowledge base, which can then be queried for authorization decisions.
Integer
Polar parses a sequence of numeric characters, optionally prefixed with a +
or -
,
as a value of type Integer
. Polar integers are 64-bit signed integers.
@current_unix_time
The @current_unix_time
keyword can be used to refer to the unix time
(the number of seconds that have elapsed since January 1, 1970 at midnight UTC)
at the time of a query. For example, if you have a fact
expires_at(File:foo, 1670280790)
indicating the time that the "foo" file expires,
you could use this for time-based access:
has_permission(_: Actor, "read", file: File) if expires_at(file, time) and @current_unix_time < time;
Boolean
Polar parses the keywords true
and false
as boolean values.
String
Polar supports double-quoted ("
) strings, which can be used to represent any
textual data. Quotes within strings can be escaped with a single backslash
("\""
). Two strings are considered equal if they have the same length and
each of their corresponding characters are equal.
The string type can be referenced as String
for use as a
specializer or with the matches
operator:
is_string(_s: String);is_string(s) if s matches String;
Object Literal
Polar supports object literals that have the format specializer
{string
}.
Object literals can limit rules to a unique instance of an application type.
The value of an object literal is always a string.
For example, the following rule states that an actor is an internal user if
they are a member of the acme
Organization:
is_internal_user(actor: Actor) if has_role(actor, "member", Organization{"acme"});
Integers, booleans, and strings can also be expressed as object literals;
i.e., Boolean{true} = true
succeeds. These object literals only accept
values that are of compatible types.
Rules
Rules are logical statements that may be conditional ("if this then that").
The simplest rule is the statement of a fact, such as:
is_bear("Yogi");
This rule is unconditional: it states that Yogi is a bear.
However, a rule can also be conditional. Consider the following:
is_person(x) if is_bear(x);
This rule states that x
is a person if x
is a bear. Given a policy
consisting of the above pair of rules, Oso Cloud can infer that Yogi is a
person because we've told it that Yogi is a bear and that if something is a
bear then it is a person. Bears are people, too, y'know.
Variables
In Polar, a variable does not need a separate declaration; it is initialized
the first time it is referenced in a rule. The following are all variables:
foo
, BAR
, myVar123
.
If a variable is unbound and unified with a value, the variable will be bound to that value for the remainder of the rule. If two bound variables are unified, their values will be unified. For example:
# Bind variable `x` -> "hello"x = "hello"# With `x` still bound to "hello", unifying it again with "hello" succeeds…"hello" = x# …but unifying `x` with "world" fails:x = "world"# With `x` still bound to "hello", binding `y` to "world" and then unifying `x`# and `y` failsy = "world" and x = y
Singletons
If a variable occurs only once, then its value can't be used for anything. Such variables are called singletons, and Polar will warn you if they occur in a rule. For example, if you try to load the rule…
user(first, last) if person("George", last);
…you'll see the following message:
Singleton variable first is unused or undefined001: user(first, last) if person("George", last); ^
The reason these warnings are important is that, as in this case, they usually
indicate logical errors. Here, the error is forgetting to use the first
variable, and instead using a literal string ("George"
) in the call to the
person
rule.
Singleton variables can be seen as wildcards: their values depend on nothing
else in the expression and therefore can be anything. In the example above,
first
matches any value as long as person("George", last)
results in a
match.
If you wish to keep an unused parameter in a rule, you can suppress the
singleton variable warning by starting your variable's name with an _
(underscore), e.g., change first
to _first
in the example above. The
underscore makes explicit that the variable can match any value.
A variable named just _
(a single underscore) is called an anonymous
variable, and it is always a singleton but will never generate a warning.
Each occurrence is translated into a fresh variable, guaranteed not to match
any other variable. You may therefore have as many anonymous variables in a
rule as you like and each will be unique. It's up to you whether to use an
anonymous variable or an underscore-prefixed singleton with a more descriptive
name.
Operators
Operators are used to combine terms in rule bodies into expressions.
Unification
Unification is the basic matching operation in Polar. Two values are said to unify if they are equal or if there is a consistent set of variable bindings that makes them equal. Unification is defined recursively over lists: two lists unify if all of their corresponding elements unify.
The unification operator (=
) checks if its left and right operands unify; for
example, "a" = "a"
, x = "a"
, or ["a", "b"] = [x, "b"]
where the variable
x
is either bound to "a"
or unbound.
Conjunction (and)
The and
operator is used to state that a pair of conditions in a rule's body
must both hold. For example, the rule…
oso_employee(first, last) if is_user(first, last) and is_employee("Oso", first, last);
…will be satisfied if the person is a user and an Oso employee.
Disjunction (or)
The or
operator will be true if either its left or its right operand is
true. Disjunctions can always be replaced by multiple rules with identical
heads but different bodies, but the or
operator may help simplify writing
rules with alternatives. For example:
is_user(first, last) if oso_employee(first, last) or is_guest(first, last);# The `or` can be rewritten as a pair of rules:is_user(first, last) if oso_employee(first, last);is_user(first, last) if is_guest(first, last);
List membership (in)
The in
operator can be used to iterate over lists of strings. An in
operation looks like this:
x in ["a", "b", "c"]
The left operand, x
, is a variable that will be
unified with each element in the list. If the right operand is
not a list of strings, the in
operation will fail.
In the following example, the variable x
will be bound to "a"
, "b"
, and
"c"
, in turn, and then the x = "a"
check will evaluate. This expression
will only succeed for the first item in the list, "a"
.
x in ["a", "b", "c"] and x = "a"
The left operand does not need to be a variable. For example, the following
expression will succeed twice since "a"
is in the first and fourth
positions in the list:
"a" in ["a", "b", "c", "a"]
Integer comparisons
The <
, <=
, >
, and >=
operators compare integer values.
For example, if you have a fact expires_at(File:foo, 1670280790)
indicating the time that the "foo" file expires:
expires_after_y2k38(resource) if expires_at(resource, time) and time > 2147483647
Patterns and Matching
Polar has powerful pattern matching facilities that can control which rules execute and act as type guards within rule bodies.
Specialization
Rule heads (the part of the rule before the if
keyword) can contain
specializers. A specializer is usually an application type, but there are also
a couple built-in specializers. When Polar
evaluates a query to see if it matches a rule head, the query will only match
if the types of the query's arguments match the specializers in the rule head.
For example, given the rule…
is_person(_person: Person);
…the lone argument in a query for is_person
must be of type Person
.
Multiple rules with the same name can be written with different specializers:
is_person(_person: Person);is_person(_user: User);
Now, the is_person
rule will match if the argument is a User
or a Person
.
matches
operator
The matches
operator can be used anywhere within a rule body to assert that a
variable has a certain type. The semantics are identical to
specialization; x matches Person
will succeed if x
is of
type Person
and fail otherwise.
Actor and Resource Specializers
Oso provides built-in specializers that will match any application type that has been declared via an actor or resource block.
The Actor
specializer will match any application type that has been declared
via an actor
block, and Resource
will match types declared via actor
and
resource
blocks.
For example, the following is a valid head for an allow
rule:
allow(actor: Actor, action, resource: Resource) if ...
The Actor
and Resource
specializers are used by Oso's
resource blocks to simplify policies.
Fact type inference
Alongside your policy, Oso uses small pieces of authorization data called facts to make authorization decisions. Facts are concrete pieces of authorization-relevant information about the entities in your application, such as role assignments for specific users. Your application is responsible for providing these facts to Oso. You can learn more about facts here.
Oso infers type information about facts based on how the facts are used in your policy. For example, with a policy like this:
has_permission(user: User, "pet", dog: Dog) if are_friends(user, dog);
Oso infers that it should only accept are_friends
facts with two arguments,
where the first argument is a User
and the second is a Dog
.
Oso uses these inferred fact types to prevent you from inserting invalid facts.
For example, with the above policy, if you attempted to tell
Oso the fact are_friends(User:alice, Rabbit:peter)
, Oso would reject the
fact, because your policy doesn't use facts with the type
are_friends(User, Rabbit)
. Additionally, Oso prevents you from accidentally
omitting an argument – Oso will reject are_friends(User:alice)
, because the
second Dog
argument is missing.
Oso also uses these inferred types to prevent you from inserting facts that it
doesn't know about. This makes it impossible to accidentally insert a fact with
a misspelled predicate, like ar_frens(User:alice, Dog:fido)
.
Overriding inferred types
What if you want Oso Cloud to store a fact that isn't used anywhere in your policy? For
instance, maybe you want to tag users by inserting has_tag
facts into Oso,
anticipating that you might use tags in your policy someday. Or maybe you
already tag users and use those in your policy, but you want to start tagging
organizations, too.
In these cases, you can use the declare
statement to force Oso to accept a certain fact type:
declare has_tag(User, Tag);
This will make Oso accept facts like has_tag(User:alice, Tag:is-cool)
, even
if your policy doesn't currently use facts like this.
You can have multiple declare
statements for a given fact predicate:
declare has_tag(User, Tag);declare has_tag(Dog, Tag);declare has_tag(Tag, Tag, Tag); # I heard you like tags.
These declare
statements form a union type-- as long as a fact matches
one of the declared or inferred types, Oso will accept it.
You never need to use a declare
statement for fact types that are used in
your policy. declare
statements are only for making Oso accept fact types
that your policy never uses. Most policies will not use declare
statements.
Talk to an Oso Engineer
If you'd like to learn more about using Oso Cloud in your app or have any questions about this guide, connect with us on Slack. We're happy to help.