The high-level policy language is designed to allow you to specify policies for your application in a succinct, readable manner.

A policy is like a security checklist for your code. It describes what should happen (or not happen) in your application. The analyzer reads your code, traces how data moves around, and checks if your rules are being followed.

Policies reason about privacy and security in terms of dependencies. This lets you restrict how data is processed and how it flows through your application. For example you could express that "sensitive user data should never go to analytics servers" or "credit card numbers must always be encrypted before storage". Paralegal can then check these rules on your code automatically. You connect rules to actual code by adding simple annotations (Markers and Annotations) to functions and data in your source code.

Basic structure of a policy

Every policy has three parts:

Scope: Where should this rule apply?

Definitions: (Optional) Shortcuts for complex patterns

Policy: The actual rules to check

We will now explore each of these parts in opposite order, starting with the policy, the “actual rules”. After that it will be easier to understand what the “definitions” and “scope” are for.

Policy: The actual rules

Policies are logical expressions. You may think of it also as a conditional which, if it evaluates to false for your program, means that there is an issue in your program. In the actual evaluation of a policy Paralegal however not only produces a boolean but keeps around tracing information to give you a better error message (see Error Messages).

There are several components you will see in a policy

Variable References
Variable Introductions (also called quantifiers)
- with an optional constraint
Logical Connectives
Markers, and
Primitive Relations

In the next sections we’ll explore each of these in detail, but let me first show you a policy where I’ve marked one of each of these components so you can connect them to something concrete. The referenced component in each case is underlined.

Policy:
1. For each "temporary_data" ← Introduction of variable "temporary_data"
		   marked temp_storage: ← Marker
    A. There is a "expiry_check" 
			    marked expiration_validator ← Constraint on the introduction of "expiry_check"
			    where:
        a. "current_time" goes to "expiry_check"
        and ← Logical Connective
        b. "temporary_data" ← Reference of Variable "temporary_data"
			        goes to ← Primitive Relation
			      "expiry_check" 
        and
        c. "expiry_check" affects whether "temporary_data" happens

You may notice that there are a lot of “bullets”, such as “1.” and “A.”. This is an enforced structure whereby all nesting in the policy must be preceded by a matching bullet. The bullets is how Paralegal (and a reader) can unambiguously tell which clauses of the policy relate to one another. For example, all lowercase letter bullets in this example belong to the sequence of “and” conjunctions.

The sequence of permissible bullets is fixed and as follows:

Number followed by .