%  $Author: lkagal $
%  $Date: 2008-04-04 14:22:41 -0400 (Fri, 04 Apr 2008) $
%  $Revision: 18565 $
%

\documentclass[times, 10pt,twocolumn]{article}
\usepackage{latex8}
\usepackage{times}

\usepackage{epsfig, url}
\usepackage{fancyvrb,relsize,url,graphicx}
\DefineVerbatimEnvironment%
   {VerbatimN3}%
   {Verbatim}%
   {fontsize=\scriptsize, xleftmargin=0.25in}
\DefineVerbatimEnvironment%
   {VerbatimScript}%
   {Verbatim}%
   {fontsize=\scriptsize}

\long\def\comment#1{\relax}

% Put remarks in the paper easily located by ``bigodot'' in margin
% Usage: \todo{twf: we need a better example here.}
\newcommand{\todo}[1]{%
\mbox{}\marginpar[\hfill$\bigodot$]{$\bigodot$\hfill}
{\sc#1}}

% RDF qnames:
\newcommand{\qname}[1]{\texttt{#1}}
\newcommand{\airname}[1]{\qname{#1}}
\newcommand{\lqname}[1]{\qname{:#1}}

% hyphen with allowed line break:
\newcommand{\dash}{-\linebreak[0]}

%\documentstyle[times,art10,twocolumn,latex8]{article}

\pagestyle{empty}

\begin{document}

\title{Using Dependency Tracking to Provide Explanations for Policy Management}

\author{Lalana Kagal, Chris Hanson, and Daniel Weitzner \\
Decentralized Information Group \\
MIT Computer Science and Artificial Intelligence Lab\\
\{lkagal, cph, djweitzner\}@csail.mit.edu\\
}
% For a paper whose authors are all at the same institution,
% omit the following lines up until the closing ``}''.
% Additional authors and addresses can be added with ``\and'',
% just like the second author.
%\and
%Next author\\
%second instituition\\
%email\\
%}

\maketitle
\thispagestyle{empty}

\begin{abstract}

Explanations for decisions made by a policy framework allow end users
to understand how the results were obtained, increase trust in the
policy decision and enforcement process, and enable policy
administrators to ensure the correctness of the policy.  In our
framework, an explanation for any statement including a policy
decision is a representation of the list of reasons (known as
dependencies) associated with its derivation.  Dependency tracking
involves maintaining the list of reasons (statements and rules) for
the derivation of a new statement.  In this paper, we describe our
policy approach that (i) provides explanations for policy decisions,
\comment{(ii) supports hypothetical reasoning that can be used for
  policy and data analysis, and} (ii) provides more efficient and
expressive reasoning through the use of nested sub-rules and goal
direction, and (iii) is grounded in Semantic Web technologies. We
discuss the characteristics of our approach and provide a brief
overview of the AIR policy language that implements it.  We also
discuss how relevant explanation information is identified and
presented to end users and describe our preliminary graphical user
interface. \comment{We then illustrate the advantages of our approach
  through several examples.  }

\end{abstract}

\comment{

1. does dependency tracking that helps with justification and
hypotheticals. provides a simple way to write down computations that
keep track of explanations/ justifications. If you were write down a
policy in a regular language you would ahve to manage the
justifications on your own.

3. certain level of abstraction as you don't have to handle
dependencies or justifications

4. Work with hypotheticals - for policy analysis, under a certain set
of circumstances, will this access be granted or will this policy be
violated. can also be used for scenario analysis, so if the reasoner
cannot come up with a result, then you can incrementally adjust the
record to try to understand what is required to make the reasoner move
forward. These hypotheticals can be retracted later.

5. Addressing shortcomings of rule languages: w/o goal direction there
is no way to control how much forward chaining/inferencing the engine
will do. sub-rules give you expressive power.

Focussed on explanations - very important to end user. screen shot of
Oshani's tabulator plugin

}

\section{Introduction}

An explanation is a reason that justifies certain results or
decisions. For policy frameworks, this justification becomes
especially important because it provides insights into the policy
development and enforcement process. Policy administrators use these
justifications to confirm the correctness of the policy and to check
that the result is as expected. Users, on the other hand, mainly
utilize justifications to check that the policy enforcement process
works as it should and, in the case of failed queries, to figure out
what additional information is required to get the correct result.

Our policy approach tracks dependencies during the reasoning process
in order to provide automated justification support so that policy
administrators are not required to handle or manipulate these
dependencies or justifications. We use a production rule
system~\cite{waterman78pattern} as a reasoner and a \emph{Truth
  Maintenance System} (TMS)~\cite{doyle79} as the dependency-tracking
mechanism. Our reasoner has additional features for improved reasoning
efficiency such as goal direction, which controls how much inferencing
the reasoner does. The reasoner also supports the extraction of
relevant portions of explanations in order to prevent the user from
being overwhelmed by irrelevant data and rules. As justifications
provided by the TMS are usually in the form of proof trees that may
not be useful for end users, we have developed a user interface to
interpret these results into a graphical user-friendly layout.

\comment{which presents the explanation either in a Semantic Web rule
  language or in a graphical layout that highlights the result of the
  reasoning and allows the explanation to be explored.}

The AIR policy language, based on this approach,\comment{amenable to
  efficient reasoning with dependency tracking in order to} is aimed
at meeting policy compliance requirements of open, decentralized
information infrastructures such as the World Wide Web and large
enterprise systems. \comment{Such environments have two unique
  requirements.  First, given the complexity of information usage
  rules, it is not always possible to completely evaluate rule
  compliance at the time an individual resource is accessed.  Rather,
  rule compliance can only be fully assessed by looking back over a
  chain of transactions.  Second, compliance may not be provable by an
  automated process, but only satisfied by the application of human
  judgment.  Hence, our system must be able to present a partial chain
  of justifications for a given action for evaluation by a human
  decision maker.  Finally, a mix of open and closed world reasoning
  is required.  Such challenging environments require a mix of open
  and closed world reasoning.}  The policy reasoner must be able to
search over a knowledge base as open as the Semantic Web, but must
also be able to assert closure over some set of facts in order to
reach a useful result.  These open environments point to the need for
flexible dependency tracking that gives users and administrators the
most complete possible view of the inference as well as efficient ways
of reasoning.

The paper is structured as follows: we start by discussing details of
our dependency tracking approach in section \ref{dependency-tracking}
and then describe our motivating scenario in section \ref{scenario}.
In section \ref{air}, we discuss the AIR policy language and its
constructs. The next two sections deal with how we generate and
display explanations. We compare our research with other work in
policy explanations in section \ref{related-work} and conclude the
paper with a discussion of our results and our future work in section
\ref{future-work}.



\section{Dependency Tracking}
\label{dependency-tracking}

A deductive reasoning system derives conclusions from previous
deductions or premises by the application of deductive rules.  For any
given conclusion, it is useful to know the specific set of premises
that it was derived from; this set is called the \emph{set of
  dependencies} for the conclusion.  \emph{Dependency tracking} is the
process of maintaining dependency sets for derived conclusions.

Some dependency-tracking mechanisms provide additional features.  For
example, a Truth Maintenance System (TMS) keeps track of the logical
structure of a derivation, which is an effective explanation of the
corresponding conclusion.  Another useful feature, also provided by a
TMS, is the ability to assume and retract hypothetical premises.

There are several reasons why dependency tracking is useful for policy
systems:

\begin{itemize}
  \item The dependency set for a result provides a natural focus when
    trying to solve policy compliance problems.
  \item It can provide a concise explanation for a result.  This is
    essential for confirming that a policy is correctly modeled.  It
    can also help identify situations where a policy is having
    unanticipated or undesirable consequences.
\comment{ \item A dependency-tracking mechanism that supports
  hypothetical premises can simplify analysis and design of policies.
  It can be used to test the response of a policy to a hypothetical
  situation.  Or it can be used to construct an argument based on a
  supposed but as-yet unsupported belief.}

\end{itemize}

We have chosen to use a TMS as the dependency-tracking mechanism for
our project.  The TMS provides considerable power in a very simple
mechanism; its primary cost is the memory required to record the
structure of a derivation.  Although the TMS technology was invented
in the 1970s, it is not well known outside the artificial intelligence
community, and consequently there are no uses of this technology in
policy systems of which we are aware.

\comment{One possible complaint about dependency tracking is that its
  use might clutter the description of a policy, obscuring its
  meaning.  In practice, this is not usually a problem since most of
  the information needed to support dependency tracking can be
  inferred from the policy description.}

Our reasoner is a kind of \emph{production-rule system} in which the
\emph{condition} of a rule is a pattern to be matched against a set of
believed statements.  When the pattern matches, the rule's
\emph{action} is performed.  Typically the action asserts new beliefs,
causing them to be added to the set of believed statements.

When something is added to the belief set, it is associated with a
\emph{justification} for its belief.  In the case of a simple
statement of fact, there is a trivial justification that the statement
is an assumption.  A derived statement has a justification based on
the inputs used to make the derivation.

In such a simple rule system, all of the dependency information is
implied by the rules themselves.  If a new belief is asserted by a rule's
action, then its justification is the set of statements that matched
the rule's pattern.  More precisely, we believe the asserted statement
if and only if we believe every one of the matched statements.
Additionally, the justification records an identifier for the rule;
this identifier together with the matched statements provide all the
relevant information about the particular deduction step just
performed.  Typically these deduction steps build on one another,
resulting in a tree-like justification structure for any given belief,
in which the belief is the trunk of the tree and the assumptions are
the leaves.  This tree structure is a complete explanation of the
support for the belief.

\section{Motivating Scenario: Decentralized Access Control}
\label{scenario}

The DIG group has several online resources including pictures, papers,
presentations, and proposals that are only accessible to members of
the group and to people that members trust. The group has a webpage
that lists its members using N3~\cite{berners08n3}, a representation
of RDF (Resource Description Framework)~\cite{klyne04rdf}. An example
of this group listing is provided below.

\begin{figure}[!h]
  \centerline{\epsfig{file=images/dig-member-list.pdf, height=2.8in}}
  \caption{DIG member description in Turtle}
  \label{fig-group}
\end{figure}


The page identifies members by their Friend Of A Friend
(FOAF)~\cite{foaf} pages.  FOAF is a vocabulary for describing people,
their email and physical addresses, projects they are working on,
people they know etc. Authentication in this scenario is via
OpenID~\cite{openid}. OpenID is a decentralized authentication
mechanism that associates users with URIs (Uniform Resource
Identifiers) that they own and can modify. If users can prove that
they own the URI, they are successfully authenticated. DIG members
provide their OpenID URI (usually the same as their work homepages) in
their FOAF pages.

\comment{
\begin{figure}[!h]
  \centerline{\epsfig{file=images/foaf-example.pdf, height=1in}}
  \caption{FOAF file example}
  \label{fig-foaf}
\end{figure}
}

When a user makes a request for a DIG resource, she specifies her
OpenID URI\@. The OpenID component on the DIG web server authenticates
the user and obtains this OpenID URI\@. The policy reasoner then
checks whether the authenticated OpenID URI belongs to one of the
members of the group or to anyone who is known (specified via
\qname{foaf:knows} on the member's FOAF pages) to any DIG member.  The
former is checked by extracting the FOAF pages of members from the DIG
page and seeing if any of them state that their OpenID URI is the same
as the requester.  The latter is checked by reading in the FOAF pages
of the members and then reading the FOAF pages of people they know and
checking if any of them have the same OpenID URI as that of the
requester. If the OpenID URI matches, the user is given access and the
resource is returned. If not, the user is denied access. The reasoner
is able to provide a justification for why someone was given or denied
access to a certain document.

This entire example can be accessed at the following URI
\begin{VerbatimScript}
http://dig.csail.mit.edu/2008/Papers/IEEE%20Policy/ex/
\end{VerbatimScript}

\section{AIR Policy Language}
\label{air}

AIR ({\bf A}ccountability {\bf I}n {\bf R}DF) is a policy language
that exploits our dependency tracking approach. The policies are
represented in Turtle~\cite{beckett04turtle}, which is a human
readable syntax for RDF, and include the quoting feature of
N3Logic~\cite{berners08n3}. AIR constructs allow policy writers to
explicitly control how the reasoning happens by invoking rules
according to pattern matches and are based on AMORD constructs
\cite{kleer77amord}.  AMORD is a production-rule system that features
pattern matching, dependency tracking, nesting of rules, and goal
direction.  The combination of these features provides expressive
power (pattern matching and rule nesting), efficient execution (goal
direction), and integrated explanations (dependency tracking).

AIR consists of an ontology and a reasoner, which when given a set of
policies and data in Turtle, attempts to compute compliance of the
data with respect to the policies.  Each computed compliance result
has an associated explanation in Turtle outlining the derivation of
the result from the inputs.

\subsection{Language Overview}

The AIR ontology comprises several classes and properties that are
used to define rule-based policies. Please refer to Figure
\ref{fig-air-ont} for an overview of the AIR classes, properties, and
their relationships.

\begin{figure}[tb]
  \centerline{\epsfig{file=images/air-ont.pdf, height=3.2in}}
  \caption{AIR ontology}
  \label{fig-air-ont}
\end{figure}

There are two top-level classes in AIR:
\airname{Abstract\dash{}action} and
\airname{Abstract\dash{}container}.  \airname{Policy} is a subclass of
\airname{Abstract\dash{}container}.  The
\airname{Abstract\dash{}container} class has properties for defining
variables, belief rules, goal rules, belief assertions, and goal
assertions that \airname{Policy} inherits.  Variables are scoped to
the container they appear in.

\comment{For example, in the following declaration the scope of
  variable \lqname{REQ} is within \lqname{DIGPolicy} and the rules it
  contains including \lqname{rule1} and \lqname{rule2}.  The scope of
  variable \lqname{MEMBER} declared in \lqname{rule1} is
  \lqname{rule1} and the scope of variable \lqname{MEMBER} and
  \lqname{FOAF-REQ} declared in \lqname{rule2} is \lqname{rule2}.  If
  \lqname{REQ} is bound before \lqname{rule1} or \lqname{rule2} are
  invoked then it is passed as a value and not as a variable.
  (Variables do not have to be uppercase.)}

The following is an example of a policy, \lqname{DecAccessPolicy},
which has 2 properties, \airname{variable} and \airname{rule}. The
policy has three variables, \lqname{REQ}, \lqname{REQUESTER},
\lqname{RESOURCE}, and consists of one rule, \lqname{DAP-1}. The scope
of the variables declared in \lqname{DecAccessPolicy} is within the
policy and the rules it contains. The scope of the variables declared
in \lqname{DAP-1} is \lqname{DAP-1} itself. If a variable is bound
before a rule is invoked, then it is passed as a value and not as a
variable. (Variables do not have to be uppercase, it is just a
convention we use)

\begin{VerbatimN3}
:DecAccessPolicy a air:Policy;
   air:variable :REQ, :REQUESTER, :RESOURCE;
   air:rule :DAP-1.

:DAP-1 a air:Belief-rule;
   air:variable :MEMBERLIST, :MEMBER.
\end{VerbatimN3}

An \airname{Abstract\dash{}rule} is a subclass of both
\airname{Abstract\dash{}container} and \airname{Abstract\dash{}action}
and its subclasses are \airname{Goal\dash{}rule} and
\airname{Belief\dash{}rule}.  Instances of \airname{Goal\dash{}rule}
match statements that are asserted as goals, and are used sparingly in
typical applications.  The \airname{rule} property applies to all
\airname{Abstract\dash{}containers} and is used to attach rules to
policies as shown in the example above.

A rule consists of a \airname{pattern}, a \airname{matched-graph}
variable, a \airname{justification}, a \airname{label}, and zero or
more actions. The atomic formulas in the RDF abstract syntax are
called \emph{triples} and they are analogous to one 3-place {\it
  holds(s, p, o)} predicate. A pattern is a set of triples containing
variables in any one of the 3 places and matches a set of triples in
an RDF graph. The \airname{matched-graph} variable is bound to that
set of triples at run-time. The matched-graph variable, justification,
and label are optional.  (More information about
\airname{matched-graph} and \airname{justification} properties is
provided in Section~\ref{explicit-just}.) If \airname{justification}
is omitted means the default justification is used.

 For example, the following belief rule \lqname{DAP-2} has two
 variables, a label titled ``Decentralized Access Control Rule2'', a
 pattern, and an assertion. The pattern consists of 4 triples, where
 the last two triples have the same subject \lqname{MEMBER}. The
 assertion is a single triple stating that the request is compliant
 with the the policy.

\begin{VerbatimN3}
:DAP-2 a air:BeliefRule;
       air:label "Decentralized Access Control Rule2";
       air:variable :MEMBERLIST, :MEMBER;
       air:pattern {
          :DIG foaf:member :MEMBERLIST.
          :MEMBER air:in :MEMBERLIST.
          :MEMBER a foaf:Person;
             foaf:openid :REQUESTER.
       };
       air:assert { :REQ air:compliant-with :DIGPolicy }.
\end{VerbatimN3}

Belief rules implement forward-chaining deduction, while goal rules
provide a means to limit the application of rules (and consequently
the amount of computation performed).  In the following example, a
belief rule \lqname{RuleA} has a nested goal rule \texttt{r1} that
controls the introduction of sub-class type inference. The outer rule
fires whenever a sub-class relationship is believed, causing
\texttt{r1} to be enabled.  \texttt{R1} is applied when there is a
goal to show that some resource is a member of the class \lqname{V2},
enabling the belief rule \texttt{r2}.  \texttt{R2} implements the
implication "if a resource is a member of a subclass \lqname{V3}, it
is also a member of the containing class \lqname{V2}".

\begin{VerbatimN3}
:RuleA a air:Belief-rule;
   air:variable :V1, :V2, :V3, :V4;
   air:label "sub-class implication";
   air:pattern {
      :V3 rdfs:subClassOf :V2.
   };
   air:goal-rule [       # sub-rule r1
      air:pattern { :V1 a :V2. };
      air:rule [         # sub-rule r2
         air:pattern { :V1 a :V3. };
         air:assert { :V1 a :V2. };
      ];
   ].
\end{VerbatimN3}

The purpose of the goal rule \texttt{r1} is to limit the deductions
made by the system and provide \emph{goal direction}. On the other
hand, if \lqname{RuleA} were rewritten as a belief rule, as below, it
would make all possible deductions of this kind, whether they were
needed or not. The use of a goal rule instead limits the deductions to
those actually asked for (specified as goals) rather than for every
possible deduction.

\begin{VerbatimN3}
:RuleA a air:Belief-rule;
   air:variable :V1, :V2, :V3;
   air:label "sub-class implication";
   air:pattern {
      :V3 rdfs:subClassOf :V2.
      :V1 a :V3.
   };
   air:assert { :V1 a :V2. }.
\end{VerbatimN3}

The action of a rule consists of a set of assertions, sub-rules, and
alternatives.  When the pattern of a rule matches, its assertions get
fired and its sub-rules became \emph{active}. A sub-rule appearing in
the action of a containing rule is initially \emph{inactive}, meaning
it is not eligible for matching.  When the containing rule's pattern
matches and its action is performed, the sub-rule becomes
\emph{active} and its pattern will be matched as needed.

In the following example, \lqname{sub-rule} only becomes active after
the pattern of \lqname{containing-rule} has been matched and similarly
\lqname{sub-sub-rule} only becomes active after the pattern of
\lqname{sub-rule} has been matched.

\begin{VerbatimN3}
:SomePolicy a air:Policy;
  air:rule [
    air:label "containing-rule";
    air:pattern { ... };
    air:rule [
      air:label "sub-rule";
      air:pattern  { ... };
      air:assert { ... };
      air:rule [
        air:label "sub-sub-rule";
        air:pattern { ... };
        air:assert { ... }
      ]
    ]
  ] .
\end{VerbatimN3}

An alternative is a rule that becomes active if the pattern of the
containing rule fails. This \airname{alt} property is used to assert
closure over some set of facts. Consider the following example. If the
pattern of \lqname{RuleB} matches, then the assertion fires, otherwise
the alternative, \lqname{RuleC} becomes active.

\begin{VerbatimN3}
:RuleB a air:Belief-rule;
   air:variable :MEMBER;
   air:pattern {
     :MEMBER air:in :MEMBERLIST.
   };
   air:assert { :MEMBER foaf:member :DIG };
   air:alt [ air:rule :RuleC ].

:RuleC a air:Belief-rule;
  ...
\end{VerbatimN3}

An assertion appearing in the action of a rule consists of a set of
triples containing variables and literals. It is similar in appearance
to a \airname{pattern}. When the pattern of the rule is matched, the
assertion statement with bound variable values is added to the set of
beliefs.

\comment{or a goal. If it is a belief, the asserted statement is added
  to the set of beliefs and can be matched against belief rules and if
  it is a goal, the asserted statement can be matched against goal
  rules. }

In the following example, an assertion is associated with
\lqname{RuleD}. When the rule's pattern matches, the statement is
asserted as a belief.  The variables \lqname{MEMBERLIST} and
\lqname{DIG} are bound before the rule is invoked. 

\begin{VerbatimN3}
:RuleD a air:Belief-rule;
   air:variable :MEMBER;
   air:pattern {
     :MEMBER air:in :MEMBERLIST.
   };
   air:assert { :MEMBER foaf:member :DIG } .
\end{VerbatimN3}


After the pattern of the above rule matches, assume that
\lqname{MEMBER} is bound to
\textit{http://people.apache.org/\~{}oshani/foaf.rdf} and \lqname{DIG} is
bound to \textit{http://dig.csail.mit.edu/data\#DIG}, then the triple
that is asserted is

\begin{VerbatimScript}
<http://people.apache.org/~oshani/foaf.rdf> foaf:member 
<http://dig.csail.mit.edu/data#DIG>
\end{VerbatimScript}


AIR provides a small library that implements some simple
RDFS~\cite{rdfs} and OWL~\cite{owl} deduction rules.  For example, if
a relation \(R\) is declared to be transitive, and the belief set
contains \(xRy\) and \(yRz\), the library can deduce \(xRz\).  The
library provides a number of generally useful deductions, and will be
augmented with new rules as the need arises.
  
The properties dealing with policy compliance are
\airname{compliant\dash{}with} and
\airname{non\dash{}compliant\dash{}with}; they specify that the
subject is or is not compliant with the object policy.  For example,
the following policy, \lqname{DecAccessPolicy} has a rule,
\lqname{DAP-3}, which when matched, asserts that the request is
compliant with the policy. If the pattern does not match, then the
alternative rule, \lqname{DAP-4} becomes active.

\begin{VerbatimN3}
:DecAccessPolicy a air:Policy;
   air:variable :REQ, :REQUESTER, :RESOURCE;
   air:rule :DAP-1,:DAP-3.

:DAP-3 a air:BeliefRule;
    air:variable :MEMBER, :FOAF-REQ;
    air:pattern {
        :MEMBER air:in :MEMBERLIST.
        :MEMBER foaf:knows :FOAF-REQ.
        :FOAF-REQ foaf:openid :REQUESTER.
    };
    air:assert { :REQ air:compliant-with :DIGPolicy };
    air:alt [ air:rule :DAP-4 ].
\end{VerbatimN3}


\section{Explanation Generation}

Our reasoner provides three ways in which to identify and extract
relevant information from justification trees generated by the TMS;
(i) hidden rules, (ii) explicit justifications, and (iii) rule
descriptions.

\subsection{Hidden rules}
One problem with the dependency-tracking mechanism is that it can
record \emph{too much} information.  It has no way to distinguish
between deductions that are interesting and that should appear as part
of an explanation, and those that should be omitted.  For example,
suppose there is a rule that says ``Students have access to group
resources'' and the statement ``GradStudents is a subclass of
students'' is believed. Then while proving that a student has access
to some resource, there will be a rule to deduce the sub-class
relationship, but it won't be interesting for most end users.

Our system provides a simple means for policy authors to elide
uninteresting deduction steps from explanations.  When writing a rule
that makes such a deduction step, the author declares it as
\airname{Hidden-rule}, and any deduction made by that rule will not
appear in the resulting explanation.  This distinction is under the
control of the policy author, so the consequent hiding can be tailored
to the users in the policy domain.

For example, if we wanted to hide the sub-class rule and its
justification from the overall justification trace generated, would
simply declare it to be of type \emph{Hidden-rule}

\begin{VerbatimN3}
:Sub-Class-Implication a air:Hidden-rule.
\end{VerbatimN3}

\begin{figure*}[!t]
  \centerline{\epsfig{file=images/proof-tree.pdf, height=2.8in}}
  \caption{Proof tree generated by TMS}
  \label{fig-prooftree}
\end{figure*}

\subsection{Explicit Justifications}
\label{explicit-just}
The TMS provides a tree-like justification structure for every belief
(asserted or inferred) in our policy reasoner. In certain cases, such
as goal direction, the correct dependency structure is not always
inferable from the rule.  In other cases, we might want to modify the
dependency structure to provide customized justifications. To handle
such situations, we provide a means to write explicit justifications
and to override the default justification provided by the TMS. This is
done by using the \airname{assertion} property associated with
rules. This property is composed of two components,
\airname{statement}, which is the set of triples being asserted, and
\airname{justification}, which is the explicit justification that
needs to be associated with the statement. The value of the
\airname{justification} property has to be an instance of the
\airname{Justification} class. The \airname{Justification} class
consists of two properties \airname{rule-id} and
\airname{antecedent}. The \airname{rule-id} can be set to the name of
the \airname{rule} that the assertion is to be attributed to and the
\airname{antecedent} is a list of matched graphs that would act as the
premises. It is possible to obtain the matched graphs of rules by
using the \airname{matched-graph} property of \airname{Rules} with a
variable.

Consider the example below. A rule, \lqname{DAP-1}, has a nested rule,
\lqname{DAP-2}, inside it. The default justification for the assertion
of \lqname{DAP-2} would be both the rules and their matched graphs.

\begin{VerbatimN3}
:DAP-1 a air:BeliefRule;
       air:variable :REQ, :REQUESTER, :RESOURCE, :MEMBER, 
                    :MEMBERLIST;
       air:pattern {
          :REQ a air:Request;
             foaf:openid :REQUESTER;
             air:resource :RESOURCE.
          :DIG data:owns :RESOURCE.
       };
       air:rule :DAP-2.

:DAP-2 a air:BeliefRule;
       air:pattern {
          :DIG foaf:member :MEMBERLIST.
          :MEMBER list:in :MEMBERLIST.
          :MEMBER a foaf:Person;
             foaf:openid :REQUESTER.
           };
        air:assert{ :MEMBER permitted :RESOURCE }.
\end{VerbatimN3}

In order to change this justification structure and show that a
completely different rule, \lqname{SomeOtherRule} is used, the
matched-graph, \lqname{G1}, for the new rule is obtained. This
matched-graph is used as the \airname{antecedent} and the rule name,
\lqname{SomeOtherRule}, is used as the \airname{rule-id} in the
assertion of \lqname{DAP-2}. This overwrites the original
justification tree of assertion of ``:MEMBER permitted :RESOURCE''.

\begin{VerbatimN3}
:SomeOtherRule a air:BeliefRule;
       air:matched-graph :G1;
       air:pattern { A X C };
       air:assert { B A C}.

:DAP-2 a air:BeliefRule;
       air:pattern {
          :DIG foaf:member :MEMBERLIST.
          :MEMBER list:in :MEMBERLIST.
          :MEMBER a foaf:Person;
             foaf:openid :REQUESTER.
           };
        air:assertion [
           air:statement { :MEMBER permitted :RESOURCE };
           air:justification [
              air:rule-id :SomeOtherRule;
              air:antecedent :G1
            ]
         ]. 
\end{VerbatimN3}



\subsection{Rule Descriptions}
The earlier mechanisms cause the default justification tree to be
modified and the justification to be customized. Though knowing the
rules and facts from which a conclusion is derived is useful, it does
not describe what the rule was attempting to do. In order to provide
natural language like explanations, we allow descriptions to be added
to rules. These descriptions are English sentences and can contain
variable values. The \airname{description} is an optional property of
rules and is a list instance, where list items are enclosed in
brackets and separated by commas. Each list item can either be a
string enclosed in quotes or a variable. During the reasoning process,
each variable is replaced by its current value and inserted into the
description string.

Consider the rule below, \lqname{DAP-3}. It has a description
containing four list items - two strings and two variables,
\lqname{REQUESTER} and \lqname{MEMBER}

\begin{VerbatimN3}
:DAP-3 a air:BeliefRule;
   air:variable :MEMBERLIST, :MEMBER, :FOAF-REQ;
   air:pattern {
       :MEMBER air:in :MEMBERLIST.
       :MEMBER foaf:knows :FOAF-REQ.
       :FOAF-REQ foaf:openid :REQUESTER.
   };
   air:description ("The requester, whose openid URI 
                  is" :REQUESTER ", is known by a 
                  DIG member, " :MEMBER);
   air:assert { :REQ air:compliant-with :DIGPolicy }
\end{VerbatimN3}

If the \lqname{REQUESTER} variable is bound to
\textit{http://auth.mit.edu/syosi} and the \lqname{MEMBER} variable is
bound to \textit{http://dig.sail.mit.edu/People/RRS}, then the
description of the rule generated at run-time is

\begin{VerbatimScript}
The requester, whose openid URI is http://auth.mit.edu/syosi, 
is known by a DIG member, http://dig.sail.mit.edu/People/RRS
\end{VerbatimScript}

\comment{prooftree image}

\begin{figure*}[!t]
  \centerline{\epsfig{file=images/screen-shot1.pdf, height=2.8in}}
  \caption{Justification UI}
  \label{fig-ui}
\end{figure*}




\comment{\section{Scenario Discussion}
\label{scenario-discussion}

The AIR rules that make up the DIG policy are defined in Figure
\ref{fig-digpolicy}.  The first rule called ``DIG Policy'' has a
pattern that tries to match the attributes of the request such as the
OpenID URI and the resource and binds values to variables REQ,
REQUESTER, and RESOURCE.  The ``DIG Policy'' rule does not have an
assertion but consists of two nested rules, ``Member Access'' and
``Referral Access''.  The first rule has a pattern that tries to match
a member of the DIG group with the same OpenID URI as the
authenticated URI\@. If the pattern matches, the request is asserted to
be compliant with the policy.  The second rule, ``Referral Access''
checks if the authenticated URI belongs to one of the people known to
one of the members of the DIG group.
}

\comment{\section{Contributions}
\label{contributions}

Perhaps the most important aspect of this work is the assumptions
underlying its design.  First, that the complexity of modern data
systems, as typified by the web, requires the ability to do effective
reasoning in the presence of \emph{both} incompleteness and
inconsistency---and, as if that wasn't enough, to scale over many
orders of magnitude.  And second, that the widespread dissemination of
information is making access control decreasingly effective, requiring
the development of new complementary strategies.

Even so, our system brings some significant technical strengths to the
policy domain:

\begin{itemize}

\item{Explanations}

AIR is able to produce a concise explanation for \emph{any} result it
computes.  It is hard to overstate the importance of explanations: in
many cases, the explanation for a result is more important than the
result itself.  For example, to someone being arrested by a police
officer, an explanation is likely to be very important.  And later, a
detailed justification for the arrest may be crucial.

Good explanations are just one consequence of AIR's
dependency-tracking mechanism.  And because dependency tracking is
integrated into the language, it has little or no effect on the form
or expression of policies.

\item{Improved reasoning efficiency}

Conventional forward-chaining production rule systems suffer poor
efficiency and scalability.  AIR's goal direction mechanism provides
significantly better performance by restricting rules to make
deductions that support a specific goal, rather than making every
possible deduction over a set of beliefs.

This can make a huge difference in performance.  For example, consider
trying to determine whether objects \(a\) and \(b\) are related by a
transitive relation \(R\).  A conventional rule system answers this
question by computing the transitive closure of \(R\), which can
require deducing \(n^2\) statements from \(n\) initial references to
\(R\).  However, in AIR one can specify \(aRb\) as a goal, and the
appropriate goal rule then tries to deduce this statement, which at
most requires computing those parts of \(R\) that lie between \(a\)
and \(b\).  Typically this computation doesn't depend on the size of
\(R\), but only on the distance between \(a\) and \(b\), so in
addition to doing less work, it scales much better.

\comment{
\item{Default reasoning}

Although our present implementation doesn't support default reasoning,
it is trivially added and we are in the process of doing so.  We are
introducing an optional \airname{alt} keyword to our rules, which
specifies a set of actions to be performed when the rule is unable to
find a match.  Any result computed by these alternative actions will
implicitly depend on there being no other way to match the rule.  In
other words, the result depends on a closed-world assumption, bounded
by the set of rules and beliefs being reasoned over.

The need for default reasoning is common in policy domains.  For
example, privacy policies often deny use of data in the absence of
specific permission.  If the privacy policy is later extended to
include additional permissions, or if new facts come to light, results
depending on the earlier closure are automatically invalidated and
will be recomputed to reflect the changes.  This is yet another
benefit of using a general dependency-tracking mechanism.
}

\item{Working with hypotheticals}

It is straightforward to add hypothetical reasoning ability to the
reasoner.  Hypothetical reasoning is very useful for policy and data
analysis and can be used to answer questions such as ``Under this set
of conditions, will John have access to nsf.tex?'', or ``By modifying
the input data, will the policy be violated?''.  These hypotheticals
can be retracted later and all consequences depending on them are also
retracted.  This reasoning can also used for policy development.  If
the reasoner does not come up with the required result, the data can
be incrementally adjusted to try to understand what changes are
required to the policy and data in order to obtain the required
result.

\item{Semantic Web technologies}

The AIR language and reasoner are grounded in Semantic Web
technologies so AIR policies can use and extract information from Web
resources and can be easily integrated with common vocabularies such
as FOAF, and OWL.

\comment{w/o handling closure, reasoning is tough but good because you
  can integrate existing sw technologies such as FOAF, and use URIs}

\comment{
\item{Support for accountability reasoning}

Information Accountability is an alternative to using access
restrictions and privacy-preserving algorithms for information
privacy. It emphasizes maintaining explicit logs of data usage in
order to check policy compliance when misuse of data leads to adverse
consequences. This approach does not prevent privacy leakage but
allows violators of applicable privacy policies to be identified and
held accountable.

Our approach supports accountability reasoning through (i)
explanations for policy compliance and non-compliance, (ii) use of
Semantic Web techniques to enable progressively larger overlapping
communities to develop shared vocabularies in a step-by-step,
bottom-up fashion, and (iii) handling of class expressions to
calculate appropriate data usage as data is passed from one entity to
another \cite{hanson07dpa}.  }

\item{Explanation Generation}

TMS, dependency tracking, rule description, output as proof tree
example
\end{itemize}
}

\section{Justification User Interface}

The AIR reasoner produces explanations in the form of proof trees in
Turtle. Please refer to Figure~\ref{fig-prooftree} for a justification
generated by the reasoner for the DIG policy scenario. The
justification is for a request, \lqname{Req2}, made by \textit{Yosi},
a friend of one of DIG members for a protected resource,
\textit{http://dig.csail.mit.edu/proposal/nsf.tex}. The reasoner finds
that \lqname{Req2} is compliant with the DIG policy because the
requester is known to one of the DIG members,
\textit{http://dig.sail.mit.edu/People/RRS}. The conclusion in the
proof is outlined by a box.

As these proof trees might be incomprehensible to end users, we have
developed a graphical justification user interface in
Tabulator~\cite{berners06tabulator}, a Semantic Web browser. This
allows users to view the explanation provided by the reasoner in
different ways: (i) in a simple rule language, N3, and (ii) in a
graphical layout that highlights the result of the reasoning and
allows the explanation to be explored.  Please refer to Figure
\ref{fig-ui} for the graphical view of the explanation in
Figure~\ref{fig-prooftree}. The {\bf More Information} button provides
a way for the user to step through the proof starting from the most
relevant information (in this case facts that Yosi is a friend of RRS
who is a member of the DIG group) and working backwards to the top of
the tree (a request was made for a DIG resource). The top bar contains
the \airname{description} of the rule that generated the assertion and
the bar below contains premises (matched-graph) of that rule. We are
still working on improving the user interface to make it more
intuitive to users.


\section{Related Work}
\label{related-work}

\noindent
{\bf Policy Languages}

\noindent
In recent years there have been several efforts to develop expressive
policy languages using Semantic Web technologies for a variety of
application domains including network management, Web services, and
privacy.  These include languages such as
KAoS~\cite{bradshaw03representation} and
Rei~\cite{kagal03policy}. KAoS policies are OWL descriptions of
actions that are permitted (or not) or obligated (or not).  This
limits the expressive power, but allows the classification of policy
statements, enabling conflicts to be discovered from the rules
themselves.  Another advantage that KAoS has is that if policy
descriptions stay within OWL-Lite or OWL-DL, then the computation is
decidable and has well understood complexity results.  On the other
hand, languages such as Rei and AIR allow for rules to be defined over
attributes of classes in the domain including users, resources, and
the context. Though they are expressive, they lack well defined
semantics.

AIR is more expressive than either KAoS or Rei. However, Rei includes
tools for policy analysis and speech acts for dynamic policy
modification, both of which AIR lacks. Conversely, AIR is focused on
generating explanations for policy decisions, which neither KAoS nor
Rei are capable of.

\noindent
{\bf Explanation Generators \& Languages}

\noindent
The explanation framework in \cite{bonatti06advanced} provides natural
language explanations for questions about policy decisions including
explanations for failed results. In their framework, the explanation
generation process is separate from the regular query process and uses
abductive reasoning, a method of inferring which hypothesis best
explains the facts, to obtain a proof. Parts of their proof language
in the proof are then substituted with natural language
structures. One problem with this approach is that abductive reasoning
is known to produce logically invalid results that can be confirmed
inductively~\cite{fischer01abductive} and as the proof generation
process is different from the query process, it could infer an
explanation that is different from that was inferred by the query
process. Another problem is that the explanation for failed policy
results (e.g. why-not) ends up being the list of all rules that the
user did not match. This means that the user has to sort through a lot
of potentially irrelevant information and the disclosure of these
additional policy rules could also be a privacy risk. In our approach,
however, the proof generation happens along with the inference and is
not a separate process so our reasoner tracks the rules and statements
that were actually used to infer the statement (policy
decision). Also, by explicitly handling failed results or unmatched
cases using the \airname{alt} construct, our reasoner is able to
provide explanations for failed (or incompliant) policy decisions
without revealing all possible unmatched rules.

Both WhyNot~\cite{chalupsky02whynot} and the Know
system~\cite{kapadia04know} focus explicitly on failed queries and try
to suggest changes to the knowledge base that will cause these queries
to succeed.  Our justification approach is more general and allows
failures to be captured in policies so explanations can be provided
for both successful and failed policy decisions.

Our proofs could be easily converted to generic proof representation
formats such as PML for display and analysis. PML is a general proof
language or "proof interlingua" that is used to describe proof steps
generated by different kinds of reasoning engines. Once our proofs are
converted to PML a user could manipulate them in Inference Web (IW), a
framework for displaying and manipulating proofs defined in Proof
Markup Language (PML)~\cite{mcguinness04iw}.  IW concentrates on
displaying proofs whereas our approach is mainly about generating
these proofs.


\comment{
\todo{argumentation} 

Another approach to generating possible reasons for a belief is to use
argumentation logic frameworks such as
\cite{kakas99argumentation}. This

Argumentation is an approach for reasoning with inconsistent
information and conflicting objectives. Classically, argumentation has
been mainly concerned with theoretical reasoning to check beliefs
veracity

\comment{veracity~\cite{dung95acceptability,amgoud2002reasoning,bench-capon02value}.
}
}


\comment{Inference Web (IW) is a framework for displaying and
  manipulating proofs defined in Proof Markup Language (PML)
  \cite{mcguinness04iw}.  PML is a general proof language or ``proof
  interlingua'' that is used to describe proof steps generated by
  different kinds of reasoning engines. IW concentrates on displaying
  proofs whereas our approach is mainly about generating these
  proofs. Our proofs could be easily converted to PML so that we can
  use the IW set of tools.  }

\section{Conclusion and Future Work}
\label{future-work}

Having prototyped a number of different scenarios with AIR, we believe
that the language is expressive enough to support policy compliance in
a variety of environments. In the future, we plan to address the
engineering challenges of scalable, efficient reasoning over large,
distributed knowledge bases. We also see a number of UI and
HCI-related research challenges to be met including a higher-level
representation of the language to make authoring easier and UI designs
to help with rules authoring and presentation of dependency
relationships.  \comment{One of the benefits of the Semantic Web is
  the open world assumption. Through our prototypes we have learned
  that some subcultures, such as reasoning for legal adjudication,
  require the ability to check when a certain premise does not exist,
  which is impossible under open world semantics.  In future work, we
  will look at mechanisms for creating closed world structures to
  derive conclusions for discrete issues in those environments.}
Finally, we will integrate policy aware capabilities into Semantic Web
data browsers.

\section{Acknowledgements}
This work was sponsored by NSF Cybertrust Award \#0524481 and DTO
NICECAP Award \#FA8750-07-2-0031.  We would like to thank our
colleagues Hal Abelson, Tim Berners-Lee, Jim Hendler, Deborah
McGuinness, Oshani Seneviratne, Yosi Scharf, Gerry Sussman, and
K. Krasnow Waterman for their participation in this project and their
comments on the paper.

\nocite{kakas99argumentation}
\bibliographystyle{latex8}
\bibliography{air-overview}

\end{document}
