Grammar

The specification bellow is HAPI's full grammar defined in ANTLR's notation:

grammar Hapi;

program
  : library 
  | executable 
  ;

library: exportStmt (stmt ';')+ ;

executable: (stmt ';')+ ;

stmt
  : letStmt
  | dataStmt
  | importStmt
  ;

exportStmt: EXPORT ID WHERE ;

importStmt: IMPORT ID ;

dataStmt: DATA ID '=' dataElem (',' dataElem)* ;

letStmt: ID '=' policyExpr ;

policyExpr
  : allowExpr
  | denyExpr
  | allowAllExceptExpr
  | denyAllExceptExpr
  ;

denyExpr
  : DENY attributeExpr
  | denyExceptExpr
  | literalExpr
  ;

denyExceptExpr: DENY attributeExpr EXCEPT '{' allowExpr+ '}';
denyAllExceptExpr: DENY EXCEPT '{' allowExpr+ '}';

allowExpr
  : ALLOW attributeExpr
  | allowExceptExpr
  | literalExpr
  ;
  
allowExceptExpr: ALLOW attributeExpr EXCEPT '{' denyExpr+ '}';
allowAllExceptExpr: ALLOW EXCEPT '{' denyExpr+ '}';

attributeExpr: '{' attribute+ '}' ;

literalExpr: ID ('::' ID)? ;

attribute
  : ID
  | ID ':' value (',' value)*
  ;

dataElem
  : ID
  | ID '(' value (',' value)* ')'
  ;

value: ID;

DENY: 'DENY' ;
EXCEPT: 'EXCEPT' ;
ALLOW: 'ALLOW' ;
IMPORT: 'import' ;
EXPORT: 'export' ;
WHERE: 'where' ;
DATA: 'data' ;
ID:    [a-zA-Z0-9]+ ;

SKIP_
  : ( NL | SPACES | COMMENT ) -> skip
  ;

fragment NL
  : ( '\r'? '\n' ) SPACES?
  ;

fragment SPACES
  : [ \t]+
  ;

fragment COMMENT
  : '//' ~[\r\n\f]*
  ;

A program's entry point is the program rule which define either a library or an executable specification. These two keywords distinguish the programs that are executable from programs that just exports policies to be used somewhere else. The former contains a main clause to start the evaluation, whereas the latter contains an export statement at the top level.

Examples

This section provides examples of Hapi specifications that illustrate how the language's syntactic constructs work in practice.

Basic Syntax

The program below is supposed to illustrate a simple policy that denies all accesses but allows for a specific group called Analyst to perform Reads in the Email and IP resources.

main =  
  DENY
  EXCEPT
    ALLOW {
      Actors: Analyst
      Resources: Email, IP
      Actions: Reads
    }

Exporting and Importing

The next example demonstrates how we can export policies in a file and then incorporate them in another.

// Main.lgl

import Privacy

main =  
  DENY
  EXCEPT
    ALLOW Privacy::analystActions


// Privacy.lgl

export Privacy where

analystActions =
  ALLOW {
      Actors: Analyst
      Resources
      Actions
    }

Each file defines a namespace. If a file doesn't export a module it is then declared (implicitly) as the Main module. On the other hand, if it is marked as export ... where statement, then it export a module defining a namespace. File names must be the same as module names. Also, they must be in the same folder of the file that imports them. So, in the example above we have two files ("Main.lgl" and "Privacy.lgl") and they must be in the same folder (say "src" for instance).

Unicity and Totality

These are two important properties to our language. They will be better explained in the verification section, but here we intend to give a general intuition on how these properties are guaranteed by the syntax of our language.

  • Totality: For each vector of sets of lattice elements T , and policy clause C, C allows T or C denies T.
  • Unicity: For each vector of sets of lattice elements T , and policy clause C, C allows T and C denies T , are not both true.

The first one is guaranteed by the restriction that every main clause must have a "default" policy clause at the top.

// example 1
main =  
  DENY
  EXCEPT
    ...

// example 2
main =  
  ALLOW
  EXCEPT
    ...

This policy tells us that by default everything is denied (example 1) or allowed (example 2). And then we can specify further rules in the EXCEPT clause.

As for unicity, suppose we have two policies denyAnalyst and allowAnalyst. These policies alone does not really mean anything, we need to combine them in the program's main execution. So we define a main clause to be our entry point.

denyAnalyst = DENY {
                Actors: Analyst
                Resources
                Actions
              }

allowAnalyst = ALLOW {
                Actors: Analyst
                Resources
                Actions
              }

main= ALLOW
      EXCEPT {
        DENY denyAnalyst
      }
      EXCEPT {
        DENY denyAnalyst
        EXCEPT {
          ALLOW allowAnalyst
        }
      }

In this example I chose (without loss of generality) it to be a default ALLOW clause. Its semantics says that its conditions must be valid and all of its EXCEPT DENY clauses are valid as well (this will be better explained in the semantics section). There's only one way for the policy EXCEPT DENY denyAnalyst to be valid and that is by denying all Analyst's access. You might now wonder "What about the other one? Isn't it supposed to be valid as well?". In this case, it will be valid because of the semantics of the DENY clause. This is going to be further discussed in the semantics section, but for now, all we need to know is that this structure of nested verification ensures unicity by construction (for a formal proof see verification section).

As you may have noticed, these examples are simple, yet an explanatory way to describe HAPI's grammar. In the next section we're going to dive into the semantics of the language together with the implementation details.