Grammar

The specification below 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 defines either a library or an executable specification. These two keywords distinguish the programs that are executable from programs that just export 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 one file and incorporate them in another.

// Main.hp

import Privacy;

main =  
  DENY
  EXCEPT {
    ALLOW Privacy::analystActions
  };


// Privacy.hp

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 is an exportation of 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.hp" and "Privacy.hp") and they must be in the same folder (say "src" for instance).

Unicity and Totality

These are two essential properties we must enforce, in order to make sure our policies are consistent. Here we intend to give a general intuition on how the language’s syntax guarantees their satisfaction by construction.

• 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 do 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 (without loss of generality), it is a default ALLOW clause. According to the language semantics, all these 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 access coming from Analyst. 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 structure of nested verification ensures unicity by construction.

As you may have noticed, these examples are a simple, yet an explanatory way to describe Hapi's grammar. In the next section, we dive into the semantics of the language and also highlight some implementation details.