
\chapter{AIR Reasoner}

\section{Introduction}
Justifications are required to explain reasoning results and usually
include the knowledge and rules used to infer these results. For
policy reasoners, this justification becomes especially important
because it provides important 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 them 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 integrated justification support where policy
administrators are not required to handle or manipulate these
dependencies or justifications. We use a production rule system as a
reasoner and a Truth Maintenance System (TMS) 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 portions of explanations in order to
prevent the user from being overwhelmed by irrelevant data and
rules. As explanations are usually in the form of proof trees, we have
developed a graphical justification user interface, 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.

Based on this approach, we propose a new policy language
\comment{amenable to efficient reasoning with dependency tracking in
  order to} 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.

\section{Overview}

\subsection{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 \emph{Truth Maintenance System} (TMS) \cite{doyle79} 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 A dependency-tracking mechanism that tracks derivation
    structure 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.

  \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.

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.  To see how this is done, we first need to define some
terms.

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.

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.

Our reasoner is not quite so simple.  It has additional features, such
as goal direction, for which the correct dependency structure is not
always inferrable from the rule.  To handle such situations, we
provide a means to write explicit justifications.  In practice, this
is used only occasionally, and has little impact on the overall
readability of a policy description.

Finally, one problem with this 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 the statement ``Bob has a sister named Alice'' is
believed and that some rule has a pattern ``?X has a brother named
?Y''.  A rule can be written to deduce ``Alice has a brother named
Bob'' so the pattern can match, but that deduction step won't be very
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
\emph{hidden}, 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.

Let's reconsider our example to see how this works.  Assign the
following names:

\begin{itemize}
  \item{\(A\):} ``Bob has a sister named Alice''
  \item{\(B\):} ``Alice has a brother named Bob''
  \item{\(R_1\):} rule with pattern ``?X has a brother named ?Y''
  \item{\(R_2\):} rule that deduces \(B\) from \(A\)
\end{itemize}

In the absence of any hiding, the result of rule \(R_1\) will be shown
as derived from \(B\), and \(B\) in turn will be shown as derived from
\(A\) via \(R_2\).  However, if \(R_2\) is marked \emph{hidden}, then
the result of rule \(R_1\) will be shown as derived directly from
\(A\), while \(B\) won't be shown at all.  A person reading the
explanation will see that \(R_1\) was triggered by \(A\), which is
semantically obvious even though syntactically incorrect.

\subsection{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\@.  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 outlining the derivation of the result
from the inputs.

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=4in}}
  \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.  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.)

\begin{verbatim}
:DIGPolicy a air:Policy;
   air:variable :REQ, :REQUESTER,
           :RESOURCE, :MEMBERLIST;
   air:rule :rule1, :rule2.

:rule1 a air:Belief-rule;
   air:variable :MEMBER.

:rule2 a air:Belief-rule;
   air:variable :MEMBER, :FOAF-REQ.
\end{verbatim}

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 pattern, a matched-graph variable, a
justification, a label, and zero or more actions.  The matched-graph
variable, justification, and label are optional.  Omitting the
matched-graph variable means there's no direct reference for the
matched graph, which often isn't needed.  Omitting the justification
means a default justification is used, also the usual case.  For
example, the following belief rule declares a variable and has a
label and a pattern.

\begin{verbatim}
:rule1 a air:Belief-Rule;
   air:variable :MEMBER;
   air:label "Member access";
   air:pattern {
     :MEMBER air:in :MEMBERLIST.
     :MEMBER a foaf:Person;
     foaf:openid :REQUESTER.
   }.
\end{verbatim}

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{ruleB} 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's
also a member of the containing class \lqname{V2}".

\begin{verbatim}
:ruleB 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{verbatim}

The purpose of the goal rule r1 is to limit the deductions made by the
system. If \lqname{ruleB} 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{verbatim}
:ruleB 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{verbatim}

The action of a rule consists of a set of assertions and sub-rules.  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.

\begin{verbatim}
: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{verbatim}

An assertion appearing in the action of a rule can be either a belief
or a goal. If it is a belief, the asserted
statement 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, a belief assertion is associated with
\lqname{rule2}, so when the rule's pattern matches, the statement is asserted
as a belief.  Variables \lqname{MEMBERLIST}, \lqname{REQUESTER}, and
\lqname{DIG} are bound before the rule is invoked.

\begin{verbatim}
:rule2 a air:Belief-rule;
   air:variable :MEMBER;
   air:label "Member access";
   air:pattern {
     :MEMBER air:in :MEMBERLIST.
     :MEMBER a foaf:Person;
       foaf:openid :REQUESTER.
   };
   air:assert {
     :MEMBER foaf:member :DIG
   } .
\end{verbatim}

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 has a single rule, which when matched
asserts that the request is compliant with the policy.

\begin{verbatim}
:rule6 a air:Belief-Rule;
   air:variable :MEMBER, :FOAF-REQ;
   air:label "Member referral access";
   air:pattern {
     :MEMBER air:in :MEMBERLIST.
     :MEMBER foaf:knows :FOAF-REQ.
     :FOAF-REQ foaf:openid :REQUESTER.
   };
   air:assert {
     :REQ air:compliant-with :DIGPolicy
   } .
\end{verbatim}


\section{RETE AIR Reasoner}

\section{TREAT AIR Reasoner}

\section{TMS}

\section{Proof Generation}


\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.

\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.pdf?'', 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 \cite{owl}.

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

\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 incompliance, (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{Justification UI}

As explanations are usually in the form of proof trees, which 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 \cite{berners08n3}, 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 a screen shot of
the explanation provided for the DIG policy scenario for a request
made by \textit{Alice}, a friend of one of DIG members for a protected
resource, \textit{http://dig.csail.mit.edu/proposal/nsf.tex}. The
different buttons {\bf Because} and {\bf Justify} provide a way for
the user to step through the proof starting from the most relevant
information (in this case facts that Alice is a friend of RRS who is a
member of the DIG group) and working backwards. We are still working
on improving the user interface to make it more intuitive to users.

\end{itemize}
}

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

The explanation framework in \cite{bonatti06advanced} provides natural
language explanations for questions about policy decisions including
explanations for failed results. 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 the proof language in the proof are then
substituted with natural language structures. Abductive reasoning is
known to produce incorrect results and as the proof generation process
is different from the query process it could infer an explanation that
is different from that 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, the proof generation happens
along with the inference and is not a separate process. We track 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, it is possible to
provide explanations for failed (or incompliant) policy decisions
without revealing all unmatched rules.

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 written in PML
a user could Inference Web (IW) is 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{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.
}

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.


\comment{\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.  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.
}
