The Margrave Tool for Policy Analysis

1 Getting Started

Welcome to Margrave!

Margrave is part of an ongoing research project. We appreciate your feedback and suggestions (including feature requests).

1.1 Installing Margrave

• Make sure that you have a recent version of Java installed. Margrave requires Java 6 or later. You can download the latest version of Java at

  http://www.java.com/en/download/.

• Download and install Racket from

  http://racket-lang.org/download/

• Open DrRacket (the graphical development environment for Racket) and select the File|Install .plt file menu option. Enter this URL in the Web tab:

  http://www.cs.wpi.edu/~tn/temp/margrave-dev-1106a.plt

  Alternatively, download the .plt file linked above and enter its location in the File tab.

Your Margrave install directory depends on your username and the version of Racket you have installed. Every time you run Margrave, it will tell you where it is installed. For instance:

Searching for java executable ... 
    Using the java executable in: /usr/bin/java 
    -------------------------------------------------- 
    Starting Margrave's Java engine... 
     Margrave path was: /users/tn/Racket/5.0.1/collects/margrave 
   

would tell you that Margrave is installed in /users/tn/Racket/5.0.1/collects/margrave.

1.2 Running Margrave

Margrave runs in the DrRacket programming environment. To begin, first open DrRacket.

If this is your first time running DrRacket, you will see a message about choosing a language. Go to the Language|Choose Language menu and select “Use the language declared in the source”, then click Ok.

1.2.1 Tutorial: The Command Prompt

Margrave will automatically detect where your Java installation is located, start its Java engine, and display a Margrave prompt on the bottom half of the screen.

>

Margrave runs queries against policies, so let’s start by loading a policy. Click after the prompt in the bottom window, type:

> LOAD POLICY "*MARGRAVE*/tests/conference1.p";

and press the enter key. Margrave will reply with:

ConferencePolicy1

When loading policies, if you start a file path with *MARGRAVE*, the *MARGRAVE* will be replaced with Margrave’s installation directory. Once the policy is loaded, Margrave prints the policy’s name for use in queries. Here the policy’s name is ConferencePolicy1.

Ask questions using the EXPLORE command and get answers with the SHOW ONE/NEXT/ALL commands. For instance, to ask when the policy we just loaded yields a permit decision:

SHOW ONE tells Margrave to print a single scenario (in no particular order).

Commands in Margrave are case-insensitive. Entering Show One will do the same thing as entering SHOW ONE.

To get additional scenarios, use SHOW NEXT:

If Margrave finds no more solutions, it will say so.

You can display all the scenarios in the result with the SHOW ALL command:

> SHOW ALL;

(Results omitted.)

SHOW commands always display results for the most recent EXPLORE command.

You can write more refined queries using AND, OR, NOT, IMPLIES, and IFF, as well as parentheses. This query asks for scenarios where a request is both permitted and denied:

Queries can involve multiple policies. Let’s load a second policy and try asking how the permit different requests:

Since queries like this one completely describe how new and old versions of a policy disagree, we call them change-impact queries.

It can be cumbersome to manually write change-impact queries for policies with many decisions, so we provide a shortcut with the COMPARE command:

Margrave commands are case-insensitive. The following queries are equivalent:

> EXPLORE conferencepolicy1:permit(s, a, r); 
   

> explore ConferencePolicy1:Permit(s, a, r); 
   

1.2.2 Tutorial: Margrave Scripts

Of course, re-entering commands at the prompt can be tedious. You can avoid re-entering commands by using a script instead. A Margrave script is a sequence of semicolon-terminated Margrave commands preceded by #lang margrave.

Open a new DrRacket editor and change the first line to #lang margrave. Instead of clicking Run right away, add the following lines just under the #lang margrave line:

LOAD POLICY "*MARGRAVE*/tests/conference1.p"; 
    LOAD POLICY "*MARGRAVE*/tests/conference2.p"; 
    EXPLORE conferencepolicy1:permit(s, a, r); 
    SHOW ONE; 
   

Then click Run. In the previous tutorial, you created and ran an empty script to get to the prompt immediately. In this case, however, Margrave executes those four commands before giving you a prompt:

ConferencePolicy1 
    ConferencePolicy2 
    Query created successfully. 
    ********* SOLUTION FOUND at size = 3 ****************** 
    s: author reviewer  
    a: readpaper  
    r: paper  
    conflicted = {} 
    assigned = {[s, r]} 
     
    STATISTICS:  
    Margrave computed that 3 would be a sufficient size ceiling. 
    No ceiling explicitly provided in the query's CEILING clause. 
    Used size ceiling: 3 
    ******************************************************** 
    >  
   

You can create scripts in DrRacket and save them via the File|Save Definitions As menu option. To open a saved Margrave script, use DrRacket’s File|Open menu option. The script will execute when you click Run, and its results will appear in the bottom half of the window, followed by a Margrave prompt.

1.2.3 Moving On

For help understanding scenario output and a primer on Margrave’s intermediate policy language, go to General Policies in Margrave.

For help using Margrave on IOS configurations, go to IOS in Margrave.

If you would rather jump right to more complex examples, see the scripts in the examples/scripts sub-directory of your Margrave installation.

1.3 IOS in Margrave

Margrave supports a core subset of the IOS language involving standard and most extended ACLs, static NAT, ACL-based and map-based dynamic NAT, static routing, and policy-based routing. Support for filtering based on TCP flags is available for named, extended ACLs via the match-all and match-any keywords (rather than the deprecated established keyword). At the moment, our support for state is limited to reflexive access-lists.

To parse and load an IOS policy into Margrave, use:

LOAD IOS <config-file-name>

where <config-file-name> is the file name of the IOS configuration saved as a text file.

Margrave will produce several intermediate policy files (discussed in Section 4 of [nbdfk10]) in the same path as <config-file-name> and load them. For instance, if you have a configuration saved to a file config.txt in the directory /myfiles/Margrave/IOS, you should invoke:

> LOAD IOS "/myfiles/Margrave/IOS/config.txt"; 
   

If the configuration contains unsupported IOS commands, Margrave will skip the line in question and print a warning.

For detailed examples of running queries in IOS, see the ios-demo.rkt script in the examples/scripts sub-directory of your Margrave installation. If you would like to experiment with a small IOS configuration, we suggest using examples/policies/ios-demo/initial/demo.txt.

1.3.1 Understanding IOS Scenarios

The SHOW ALL, SHOW ONE, and SHOW NEXT commands format query results and display them in a concise format. A SHOW ONE command for an IOS query will produce output in this style:

********* SOLUTION FOUND at size = 16 ****************** 
    message: icmpmessage  
    protocol: prot-tcp  
    src-port-out: port  
    dest-port-out: port  
    next-hop: ipaddress  
    entry-interface: fe0  
    length: length  
    dest-addr-in: 192.168.5.11  
    src-addr-in: ipaddress  
    dest-addr-out: ipaddress  
    src-port-in: port  
    exit-interface: interface  
    hostname: hostname-router  
    flags: tcpflags  
    dest-port-in: port-25  
    src-addr-out: ipaddress  
     
    STATISTICS:  
    Margrave computed that 1 would be a sufficient size ceiling. 
    No ceiling explicitly provided in the query's CEILING clause. 
    Used size ceiling: 1 
    ******************************************************** 
   

On the first line, Size = 16 says that this scenario involves 16 atoms, where each atom is an IP address, port, interface, etc.

The scenario itself says that the query can be satisfied when the packet is a TCP request to the host 192.168.5.11 on port 25, entering the firewall at the fe0 interface. There are no restrictions on the source fields of the packet header in this scenario: “IPAddress” represents some IP address not explicitly mentioned in the IOS configuration. Similarly for “port” and “interface”.

The message binding is only applicable for ICMP packets, and can be ignored in this scenario. The length binding is not yet used. The -out bindings give information about NAT effects on the packet; there are none in this scenario. Similarly the flags binding gives information about the packet’s TCP flags, which are not important in this scenario. The STATISTICS section gives technical information about Margrave’s scenario-finding process.

When printing, only the most specific applicable information will be shown. You will never see:

src-addr-in: 10.0.0.0/255.0.0.0 10.100.100.100 
   

since the host 10.100.100.100 is always contained in the network 10.0.0.0/255.0.0.0. Instead, you would see

src-addr-in: 10.100.100.100 
   

1.4 General Policies in Margrave

Margrave’s intermediate language can capture many different kinds of policies. In this section, we discuss how to use the intermediate language to express policies for analysis.

First, we’ll quickly overview what a Margrave policy looks like.

A policy’s form depends on its vocabulary. A vocabulary dictates what a policy request is, what decisions a policy renders, and so on.

Here is one of Margrave’s built-in example policies, a fragment of an access-control policy for a conference management system. Its vocabulary and policy files are respectively conference1.v and conference1.p in your installation’s tests directory.

The vocabulary file contains:

(PolicyVocab ConferencePolicy

(Types

(Subject : Author Reviewer)

(Action : SubmitPaper ReadPaper SubmitReview)

(Resource : Paper Review))

(Decisions

Permit

Deny)

(Predicates

(Conflicted : Reviewer Paper)

(Assigned : Reviewer Paper))

(ReqVariables (s : Subject)

(a : Action)

(r : Resource))

(OthVariables)

(Constraints

(disjoint-all Resource)

(disjoint-all Action)

(atmostone-all Action)

(abstract Subject)

(abstract Action)

(abstract Resource)

(nonempty Subject)

(nonempty Resource)))

The section “Elements of a Vocabulary” contains details about this language. For now, note that this particular vocabulary gives the following:

• the notion of “subjects”, “actions”, and “resources” and some sub-types for each;

• “permit” and “deny” as valid decisions; and

• the fact that each request contains a subject, an action, and a resource (given by the ReqVariables construct).

The policy for this example is:

(Policy ConferencePolicy1 uses conferencepolicy

(Target)

(Rules

(PaperNoConflict = (Permit s a r) :-

(!Conflicted s r) (ReadPaper a) (Paper r))

(PaperAssigned = (Permit s a r) :-

(Assigned s r) (ReadPaper a) (Paper r))

(PaperConflict = (Deny s a r) :-

(Conflicted s r) (ReadPaper a) (Paper r)))

(RComb FAC)

(PComb FAC)

(Children))

This policy uses the above vocabulary, and contains three rules that each map certain requests to decisions. For instance, the first rule, named PaperNoConflict, causes the policy to permit requests to read papers, provided the subject is not known to be conflicted on the paper. (For details, see the section “Elements of a Policy”.)

1.4.1 Tutorial: Understanding Scenarios

Paste the following script into DrRacket:

#lang margrave 
    LOAD POLICY "*MARGRAVE*/tests/conference1.p"; 
    EXPLORE ConferencePolicy1:Deny(s, a, r) AND  
     reviewer(s) AND paper(r) AND readpaper(a); 
   

and click Run. At the command prompt, enter:

> SHOW ALL; 
   

One of the two scenarios printed will be this one:

********* SOLUTION FOUND at size = 3 ****************** 
    s: author reviewer  
    a: readpaper  
    r: paper  
    conflicted = {[s, r]} 
    assigned = {} 
     
    STATISTICS:  
    Margrave computed that 3 would be a sufficient size ceiling. 
    No ceiling explicitly provided in the query's CEILING clause. 
    Used size ceiling: 3 
    ******************************************************** 
   

This text represents a scenario where the query is satisfied. The SHOW ALL, SHOW ONE, and SHOW NEXT commands format query results and display them in this concise format. The scenario above says: “The query is satisfied when the subject is both a reviewer and an author, the resource is a paper, and the action is readpaper (i.e. reading the paper), provided that the subject is conflicted on the paper but not assigned to it.”

Here, s, a, and r correspond to the variables that appear in the query. Size = 3 means that in this scenario, there were 3 objects. In this case, one is both an author and a reviewer. Another is a paper. The third represents the action readpaper.

Conflicted and assigned are binary predicates mentioned in the policy. Any such facts will be printed after information about individual variables.

The STATISTICS section gives technical information about Margrave’s scenario-finding process.

Note: When printing, only the most specific applicable information will be shown. E.g., you will never see s: reviewer subject because a reviewer is always a subject in this policy.

1.5 Creating Your Own Policies

You can create your own policies in the same style as the examples above. The sections “Elements of a Policy” and “Elements of a Vocabulary” contain more details on the policy language. Place the vocabulary in a text-file with the .v extension, and the policy in a text-file with the .p extension. Make sure that you refer to the correct vocabulary name in the policy file. For instance, if your vocabulary is in the file myvocab.v, make sure that the vocabulary is named myvocab and the policy uses myvocab.

2 Margrave’s Command Language

There are three kinds of Margrave commands: queries, presentation commands, and system commands.

2.1 The Query Sub-Language

2.1.1 EXPLORE

Explore statements instruct Margrave to look for scenarios that satisfy the statement’s conditions. For instance, in:

EXPLORE ConferencePolicy1:Deny(s, a, r) AND  
     reviewer(s) AND paper(r) AND readpaper(a); 
   

When querying a policy, first use an EXPLORE statement to define the scenarios of interest, and then use a presentation command to get the results.

EXPLORE statements have the following form:

EXPLORE <condition>
[UNDER <policy-name>, ...]
[PUBLISH <variable-name>, ...]
[TUPLING]
[INCLUDE <id>, ...]
[CEILING <number>]

Clauses enclosed in [] are optional, and can appear in any order.

A vocabulary predicate is the name of either a type or other predicate in the query’s vocabulary context. Every vocabulary predicate has an arity no less than 1. If a vocabulary predicate is the name of a type, its arity is 1, and it is called a unary predicate.

A variable vector is one of:

• x, where x is a variable symbol;

• <id:req>, where id is the name of a policy or saved query;

• A comma-delimited sequence of variable vectors.

The variable vector of the form <id:req> is equivalent to explicitly stating the request vector of the vocabulary associated with id.

Each variable vector has an associated arity. A single variable x has arity 1. A <id:req> reference has the same arity as id’s request vector. A comma-delimited sequence of vectors has arity equal to the sum of its sub-vectors’ arities.

A <condition> is a boolean combination (via AND, OR, IFF, IMPLIES, NOT, and parentheses) of atomic formulas.

An atomic formula is one of:

• an atomic vocabulary formula, which is one of:

  • predname(X), where X is a variable vector and predname is a vocabulary predicate of the same arity;

  • x IN predname, where x is a variable symbol and predname is a unary vocabulary predicate;

  • (X) IN predname, where X is a variable vector and predname is a vocabulary predicate of the same arity;

  • x = typename, where x is a variable symbol and typename is the name of an at-most-one or singleton constrained type in the statement’s vocabulary context

• an atomic IDB formula, which is one of:

  • policyid:idbname(X), where policyid is an identifier for a policy with a k-ary request vector, idbname is a valid IDB in that policy), and X is a variable vector of arity k;

  • savedquery(X), where savedquery is an identifier for a k-ary saved query and X is a variable vector of arity k;

• or a variable equality formula: x = y, where x and y are variable symbols.

The saved query identifier last always refers to the last successful EXPLORE statement.

Every EXPLORE statement has a vocabulary context: the set of vocabularies across all policies mentioned in the query’s <condition> and its UNDER clause, if any. If the policies have incompatable vocabularies (for example, if they both define the same predicate name, but with a different arity) the query will produce an error.

The term IDB is taken from the database field. Each policy provides a set of IDBs that represent policy decisions, rule applicability, and more. For details, see Section 2 of [nbdfk10].

The UNDER clause adds policies to the query’s vocabulary context that do not appear in the query <condition>. If the <condition> does not explicitly refer to a policy, the query must include an UNDER clause.

The PUBLISH clause dictates which variables in the query condition are published for use in later queries.

The TUPLING clause activates the optional tupling optimization. In order to qualify for tupling, all of the query’s saved-query predicates (if any) must refer to saved queries that PUBLISHed all of their variables.

The syntax of the INCLUDE clause differs depending on whether tupling has been enabled.

• If TUPLING is not enabled, then the INCLUDE clause contains a nonempty list of policy IDB predicates whose instantiations are to be included in the scenario output.

  Example: INCLUDE mypolicy:permit will cause each output scenario to include the requests that mypolicy permits.

• If TUPLING is enabled, then the INCLUDE clause may contain a nonempty list of IDB and/or vocabulary predicates; however a tuple of arguments must be supplied to each predicate. Variable names shared between INCLUDE and the <condition> are assumed to refer to the same variable.

  Examples: INCLUDE mypolicy:permit(r, a, s) causes each scenario to report if the request (r, a, s) is permitted by mypol.

  INCLUDE mypolicy:permit(s, a, r), mypolicy:permit(r, a, s) sets the watch on both (s, a, r) and (r, a, s).

The CEILING clause provides a limit on the scenario-sizes Margrave will check. In most cases, Margrave can infer its own sufficient ceiling (see the Margrave firewall paper [nbdfk10]). If not, Margrave uses the user-provided ceiling (or 6, if none is provided).

2.1.2 COMPARE

Margrave provides shorthand for change-impact queries in the form of the COMPARE command. The syntax of COMPARE is:

COMPARE <policy> <policy>
[TUPLING]
[CEILING <number>]

Running COMPARE on a pair of policies is equivalent to writing an EXPLORE statement that produces the scenarios in which the two policies render different decisions.

2.2 The Presentation Sub-Language

The presentation sub-language is concerned with getting the results of the previous query.

IS POSSIBLE?: If you just want to know if any scenarios exist to satisfy a query, follow it up with the IS POSSIBLE? command.

To get concrete scenarios, use:

SHOW ONE: Returns a string containing a single satisfying scenario that Margrave finds (in no particular order), pretty-printed for human consumption.

GET ONE, GET NEXT, GET ALL: Same as above, except returns an XML object that represents the scenario and can be used in programs.

If the TUPLING optimization is enabled, the following commands also become available:

SHOW (UN)REALIZED <atom>, ...: Given a list (“candidates”) of atomic IDB formulas, atomic predicate formulas, and atomic type formulas, returns the subset of the atomic formualas given that can be true (are never true) in a satisfying scenario. All candidates must be declared in the INCLUDE clause.

For example:

> EXPLORE mypolicy:permit(s, a, r)  
    INCLUDE mypolicy:rule10_matches(s, a, r) 
    TUPLING;  
    SHOW REALIZED mypolicy:rule10_matches(s, a, r); 
   

SHOW (UN)REALIZED <atom>, ... FOR CASES <atom>, ...: Given two lists (“candidates” and “cases”) of atomic IDB formulas, atomic predicate formulas, and atomic type formulas, returns a map taking each case to a separate SHOW (UN)REALIZED list where the case was included in the <condition>.

The Margrave paper [nbdfk10] contains more information on the subtleties of the SHOW REALIZED command, and the example files contain sample uses. SHOW REALIZED is especially useful when reasoning about interactions between rules.

2.3 The Command Sub-Language

The rest of Margrave’s language comprises system commands.

2.3.1 Loading Policies

To load a policy in Margrave’s intermediate language use the LOAD POLICY command:

If the filename path begins with *MARGRAVE*, the *MARGRAVE* will be replaced with Margrave’s installation directory.

> LOAD POLICY <filename> 
   

To load a Cisco IOS configuration (that uses the subset of IOS we support; see IOS in Margrave) use the LOAD IOS command:

> LOAD IOS <filename> 
   

This command will create several new policies in Margrave: InboundACL, OutboundACL, LocalSwitching, NetworkSwitching, StaticRoute, PolicyRoute, and DefaultPolicyRoute, each representing a part of the configuration. (For details, see the Margrave paper [nbdfk10].)

> LOAD IOS <filename> WITH <prefix> <suffix> 
   

also creates the above 7 policies, but renames them with the given <prefix> and <suffix>. For instance, given the command:

> LOAD IOS "myconfig.txt" WITH "pre" "suff" 
   

instead of a policy named InboundACL, one named preInboundACLsuff will be created. To avoid naming conflicts, use this variant command when loading multiple IOS configurations in the same Margrave session.

To load multiple router configurations at once, use

> LOAD IOS <filename1>, <filename2>,... IN <directory> 
   

or

> LOAD IOS <filename1>, <filename2>,... IN <directory> WITH <prefix> <suffix> 
   

For instance:

> LOAD IOS "inner-router.txt", "outer-router.txt" IN "user/tn/myconfigs" 
   

will include both configurations in the same Margrave policies. (For an example of this, see Section 6.2 of the Margrave firewall paper [nbdfk10].)

A relative path will be interpreted relative to the location of the script file. If the file is unsaved, or if you are working at the prompt, do not use a relative path.

2.3.2 Renaming Prior Queries

To rename a query or policy, use the RENAME command:

RENAME <old-identifier> <new-identifier>

For example, suppose you want to compare two different versions of the same policy, which have the same name by default. You can load the first version, then

RENAME policy policy_orig

then load the new version and

RENAME policy policy_new

Now you can write a single query that refers to both policies, such as this partial change-impact query:

EXPLORE policy_old:deny(x) AND policy_new:permit(x)

You can also use the RENAME command to save the last query created under a unique name:

RENAME last otherquery

2.3.3 Getting INFO

To get general information about the Margrave engine, including memory use and other statistics, use the INFO command:

INFO

To get information about a specific policy, vocabulary, or saved query, append the policy, vocabulary, or query identifier:

INFO mypolicy

2.3.4 Comments

Lines beginning with // are comments and will be ignored by Margrave.

3 Representing Policies

Policies map requests to decisions. Each policy is associated with exactly one vocabulary. In this section, we demonstrate the elements of policies and vocabularies using the conference policy presented in General Policies in Margrave.

3.1 Elements of a Policy

The Example Policy

(Policy ConferencePolicy1 uses conferencepolicy

(Target)

(Rules

(PaperNoConflict = (Permit s a r) :-

(!Conflicted s r) (ReadPaper a) (Paper r))

(PaperAssigned = (Permit s a r) :-

(Assigned s r) (ReadPaper a) (Paper r))

(PaperConflict = (Deny s a r) :-

(Conflicted s r) (ReadPaper a) (Paper r)))

(RComb FAC)

(PComb FAC)

(Children))

• ConferencePolicy1 is the policy name. Use the policy name to reference the policy in Margrave queries.

• conferencepolicy is the policy’s vocabulary name. Every policy has a single vocabulary that dictates what kind of request it handles and which decisions it renders.

• (Target ) is the policy’s target. The target specifies a guard on the policy’s applicability. In order for any rule in the policy to apply, the policy’s target condition must also apply. For instance, (Target (Reviewer s)) would mean that the policy applies only to subjects who are reviewers.

  An empty target, as shown above, means that the policy always applies.

• The (Rules ...) construct gives the policy’s rule set. Each rule has a name, a decision, and a set of conditions. Each condition must be the use of a type or predicate in the policy’s vocabulary. A "!" before a type or predicate name means that the type or predicate does not apply.

  The first rule in the example policy:

  (PaperNoConflict = (Permit s a r) :- (!Conflicted s r) (ReadPaper a) (Paper r))

  is named PaperNoConflict, renders the Permit decision, and applies when the subject is trying to read a paper on which he or she is not conflicted.

  The variable names that appear after the decision name (e.g. Permit s a r) must exactly match the names of the request variables declared in the policy’s vocabulary. New variables can be introduced on the right hand side of the rule, in which case they are interpreted existentially.

  For instance, in a policy for vehicle access, this rule would apply for any subject who owns some car, regardless of the action and resource involved:

  (PermitIfOwnsCar = (Permit s a r) :- (Owns s c) (Car c))

• (RComb ...) denotes the policy’s rule-combination algorithm. This is used to resolve rule conflicts. Margrave currently supports first-applicable, overrides, and none combinators:

  • (RComb FAC): In first-applicable policies, rules apply in the order in which they appear.

  • (RComb O <decisions>): In overrides policies, the vocabulary gives an ordering on the decisions, and higher-priority decisions take precedence over lower-priority decisions. E.g., (RComb O CallPolice Deny Permit) means that the CallPolice decision overrides the Deny and Permit decisions, and the Deny decision overrides the Permit decision.

  • (RComb none): In none policies, multiple rules (indeed, multiple decisions) can apply to a single request.

• Margrave also supports hierarchical policies via (Children ...): A policy’s children are a list of sub-policies that together form the parent policy. A policy contains either rules (in which case it is a leaf policy) or children but never both. For example:

  (Policy Parentpolicy uses myvocab

  ...

  (Rules)

  (Children (Policy Child1 ...

  (Rules ...)

  (Children))

  (Policy Child2 ...

  (Rules ...)

  (Children))))

  Conflicts between sub-policies are resolved via a policy-combination algorithm, which is set with the (PComb ...) construct. The same options are available to policy combination as to rule combination.

3.2 Elements of a Vocabulary

The Example Vocabulary

(PolicyVocab ConferencePolicy

(Types

(Subject : Author Reviewer)

(Action : SubmitPaper ReadPaper SubmitReview)

(Resource : Paper Review))

(Decisions

Permit

Deny)

(Predicates

(Conflicted : Reviewer Paper)

(Assigned : Reviewer Paper))

(ReqVariables (s : Subject)

(a : Action)

(r : Resource))

(OthVariables)

(Constraints

(disjoint-all Resource)

(disjoint-all Action)

(atmostone-all Action)

(abstract Subject)

(abstract Action)

(abstract Resource)

(nonempty Subject)

(nonempty Resource)))

A policy for a door lock may take keys as requests, and decide whether or not the door opens. A phone company policy may take source and destination phone numbers and decide whether the call is denied, toll-free, or toll. Margrave allows users to specify these domain-specific details about a policy using vocabularies.

A vocabulary in Margrave contains the following:

• The (Types ...) construct defines a hierarchy of types (also called sorts) that elements of a request may belong to.

  Top-level types (Subject, Action, and Resource in the above example) are always pairwise disjoint.

• The (Predicates ...) construct defines a set of predicates that may hold of request properties in a scenario. For instance, the binary predicate Assigned contains reviewer-to-paper assignments in a given scenario.

• The (Decisions ...) construct gives a set of Decisions that policies using this vocabulary render. The usual decisions are permit and deny, but others can appear in more detailed policies.

• The (ReqVariables ...) construct defines the shape of a request in this vocabulary. The request variables are an ordered list of variable names and a type assignment for each. For instance, in the access-control domain, the request variables will often be (s, a, r), representing a single subject, action, and resource. In the firewall domain, the request variables will involve IP addresses, ports, etc.

• The (Constraints ...) construct gives domain-specific assertions about how types and predicates can be populated. Margrave will not consider scenarios that violate vocabulary constraints, ruling out non-sensical results.

  Valid constraint types are:

  • atmostone: If a type is at-most-one constrained, it can never contain more than one thing.

  • singleton: If a type is singleton constrained, it must contain exactly one thing.

  • nonempty: A nonempty type must never be empty.

  • abstract: An abstract type is fully covered by its children. For instance, consider a type Bit with child types ZeroBit and OneBit. If Bit is abstract, every Bit must be either a zero or a one.

  • partial-function, total-function: A binary predicate P: (A x B) can be constrained to behave as a total or partial function from A to B.

  • disjoint: Two types that are disjoint must never share an atom.

  • subset: Used to enforce subset constraints that cannot be captured in the type hierarchy. If type A is constrained to be a subset of B, every scenario will have A contained in B, even if B is not a super-type of A.

  The constraints disjoint, at-most-one, singleton, and nonempty can be applied to all subtypes of a type at once by using the -all suffix. For instance: Declaring that the IPAddress type is disjoint-all constrained forces all of its sub-types to be pairwise disjoint.

Bibliography