The Margrave Tool for Policy Analysis
1 Getting Started
1.1 Installing Margrave
1.2 Running Margrave
1.2.1 Tutorial:   The Command Prompt
1.2.2 Tutorial:   Margrave Scripts
1.2.3 Moving On
1.3 IOS in Margrave
1.3.1 Understanding IOS Scenarios
1.4 General Policies in Margrave
1.4.1 Tutorial:   Understanding Scenarios
1.5 Creating Your Own Policies
2 Margrave’s Command Language
2.1 The Query Sub-Language
2.1.1 EXPLORE
2.1.2 COMPARE
2.2 The Presentation Sub-Language
2.3 The Command Sub-Language
2.3.1 Loading Policies
2.3.2 Renaming Prior Queries
2.3.3 Getting INFO
2.3.4 Comments
3 Representing Policies
3.1 Elements of a Policy
3.2 Elements of a Vocabulary
Bibliography
8.12

The Margrave Tool for Policy Analysis🔗ℹ

Tim Nelson <tn@cs.wpi.edu>,
Christopher Barratt,
Daniel J. Dougherty,
Kathi Fisler,
Shriram Krishnamurthi,
and Varun Singh

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🔗ℹ

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🔗ℹ

Run DrRacket and open a new editor via the File|New menu option. Change the first line in the file to #lang margrave, then click Run.

When you click Run, Margrave will always print out its current install location.

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:

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

Query created successfully.

> SHOW ONE;

********* SOLUTION FOUND at size = 3 ****************** 
    s: author reviewer  
    a: readpaper  
    r: paper  
    conflicted = {}  
    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 
    ******************************************************** 
   

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:

> SHOW NEXT;

********* SOLUTION FOUND at size = 3 ****************** 
    s: author reviewer  
    a: readpaper  
    r: paper  
    conflicted = {[s, r]} 
    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 
    ******************************************************** 
   

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:

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

Query created successfully.

> SHOW ONE;

---> No more solutions! <--- 
     
    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 
   

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

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

ConferencePolicy2

> EXPLORE (ConferencePolicy1:permit(s,a,r)  
      AND NOT ConferencePolicy2:permit(s,a,r)) 
          OR (ConferencePolicy2:permit(s,a,r) 
      AND NOT ConferencePolicy1:permit(s,a,r)); 
   

Query created successfully.

> SHOW ONE;

********* SOLUTION FOUND at size = 3 ****************** 
    s: author reviewer  
    a: readpaper  
    r: paper  
    conflicted = {[s, r]} 
    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 
    ******************************************************** 
   

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:

> COMPARE ConferencePolicy1 ConferencePolicy2; 
   

Query created successfully.

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 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); 
   

reviewer(s), paper(r) and readpaper(a) signify properties about the request: The subject is a reviewer, etc. The term ConferencePolicy:Deny(s, a, r) states that the policy renders the “Deny” decision for the request.

Rendering deny is not the same as failing to render permit!

The EXPLORE statement as a whole instructs Margrave to find scenarios that meet all of those conditions.

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:

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:

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.

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 ALL: Returns a string containing all satisfying scenarios, pretty-printed for human consumption.

Beware casual use of the SHOW ALL and GET ALL commands, as some queries can have enormous numbers of satisfying scenarios.

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

SHOW NEXT: Returns a string containing a different satisfying scenario, if one exists. Each successive use of SHOW NEXT will produce a different scenario until all have been given. Using SHOW ONE or defining a new query with EXPLORE will cause Margrave to forget which scenarios it has already printed.

Without a preceding SHOW ONE, the first SHOW NEXT will behave like SHOW ONE.

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))

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:

Bibliography🔗ℹ

[nbdfk10] Timothy Nelson and Christopher Barratt and Daniel J. Dougherty and Kathi Fisler and Shriram Krishnamurthi, “The Margrave Tool for Firewall Analysis,” Proceedings of the 24th USENIX Large Installation System Administration Conference (LISA 2010), 2010. http://web.cs.wpi.edu/~tn/publications/index.html#nbdfk10