\section{Proof carrying authorization}


\subsection{Access control}

The problem we are addressing is access control.
We want to restrict access to resources to specific users.
This can be for instance a file on a local filesystem or
a database on a distant computer.
To enforce access control we generally have a 
\textit {reference monitor} that verifies that a request
is performed by a user who has the permission to do so.
The set of rules determining who should be granted access is 
called the \textit {policy}.

Specifying policies will be done by writing proposition
in an authorization logic and access to a resource by
a specific user will be allowed when a proof in this logic
has for conclusion that this user can access the resource.
 
We will start by presenting an authorization logic,
and giving an example of proof in this logic.
And we then introduce proof carrying authorization 
architecture.

%a more complete introduction to proof carrying authorization can be found in ??

\subsection{Authorization logic}
\label{author_log}

An authorization logic \cite{Garg06csfw,Pfenning99ajudgmental} allows us to specify clearly
what the policies concerning access to a ressource are.
We give here the syntax of formulas for a simple authorization logic.


\begin{figure}[h]

$$
A ::=   P | A \supset A | \forall K \, A | K \textup{says} A
$$
\caption{Syntax of formulas, P denotes an arbitrary atomic formula}
\end{figure}


We reason with this formulas by constructing proofs.
Proofs are constructed by using the inference rules
given in figure \ref{inf_rules}.

\begin{figure}[h]
\label{inf_rules}

$$
\inferrule* [Left=use]
{ }
{ \Gamma , \textsc{true} (A) \vdash \textsc{true} (A)}
$$

$$
\inferrule* [Left=impI]
{ \Gamma , \textsc{true} (A) \vdash \textsc{true} (B)}
{ \Gamma \vdash \textsc{true} (A \supset B)}
\hspace {4em}
\inferrule* [Left=impE]
  { \Gamma \vdash \textsc{true} (A \supset B) \\ \Gamma \vdash \textsc{true} (A) }
  { \Gamma \vdash \textsc{true} (B)}
$$

$$
\inferrule* [Left=allpI]
{ \Gamma \vdash \textsc{true} (A)}
{\Gamma \vdash \textsc{true} (\forall x A)}
\hspace {4em}
\inferrule* [Left=allpE]
{ \Gamma \vdash \textsc{true} (\forall x A)}
{ \Gamma \vdash \textsc{true} (A[x \leftarrow K])}
$$

$$\inferrule* [Left=saysI]
{ \Gamma \vdash \textsc{aff} (K, A)}
{ \Gamma \vdash \textsc{true} ( K \textup{says} A) }
$$

$$
\inferrule* [Left=truaff]
{ \Gamma \vdash \textsc{true} (A)}
{ \Gamma \vdash \textsc{aff} (K, A) }
\hspace {4em}
\inferrule* [Left=saysE]
{ \Gamma \vdash \textsc{true} (K \textup{says} A) \\ \Gamma, A \vdash \textsc{aff} (K,B)}
{ \Gamma \vdash \textsc{aff} (K, B) }
$$
\caption{Inference rules}
\end{figure}

The first rule is the use of a hypothesis,
$\textsc{impI}$ and $\textsc{impE}$ are 
introduction and elimination rules for the implication construct $\supset$ ,
and $\textsc{allpI}$ and $\textsc{allpE}$ for the universal quantification $\forall$,
we will not detail them as they are commonly used in natural deduction.

The last three rules are the most interesting.
$\textsc {truaff}$ states that if a proposition is 
true, then anybody affirms it.
$\textsc {saysI}$ is the rule that internalizes the affirmation
judgment as a proposition.
$\textsc {saysE}$ states that if the truth of a proposition $A$ makes $K$ believe in $B$,
then it is enough that $K$ says $A$ to make $K$ affirm $B$, 
it implies that when reasoning from the point of view of $K$, it is the same
 if something is true or if we think it is.


\subsubsection*{Example}
\label{example}
We give the example of a grade sheet, a teacher use to publish grades for his students.
He wants to be able access them in order to write them and read them and he want
his students to be able to read them. 
Policies would be :

$$ p1 : Alice \, \textup{says} \, \textsc {maywt} ( Sheet, Alice ) $$
$$ p2 : Alice \, \textup{says} \, \textsc {mayrd} ( Sheet, Alice ) $$
$$ p3 : Alice \, \textup{says} \, \forall x  ( \textsc {student} ( x , Alice)  \supset \textsc {mayrd} (Sheet, x) ) $$

The three predicate we have here are $\textsc {maywt} (Sheet, K)$ meaning that the principal K
may write on the sheet, $\textsc {mayrd} (Sheet, K)$ meaning that K may read it and
$\textsc {student} ( B , A)$ meaning that B is a student of A.

Here we suppose that $Alice$ is the principal controlling the ressource that means that
$$\forall x (Alice \, \textup{says} \, \textsc {maywt} ( Sheet, x )) \supset \textsc {maywt} (Sheet, x) $$
and 
$$\forall x (Alice \, \textup{says} \, \textsc {mayrd} ( Sheet, x )) \supset \textsc {mayrd} (Sheet, x) $$.

We also have to specify in the policy who the students are, for instance :
$$
p4 : \textsc {student} (Bob, Alice)
$$

Now, we can see that $Bob$ should be able to read the sheet, 
for that we give a proof of $ Alice \, \textup{says} \, \textsc {mayrd} (Sheet, Bob)$.
Let $\Gamma$ be the policies, this would be the hypothesis for our proof.

We first begin by proving $Alice \,\textup{says}\, \textsc {mayrd} (Sheet, Bob)$ under
the hypothesis 
$$\Gamma' = \Gamma, \textsc{true} (\textsc {student} (Bob, Alice) \supset \textsc {mayrd} (Sheet, Bob))$$.
We will refer to this proof as $\Pi _1$.

$$
\inferrule* 
    [Left=truaff]
    { 
      \inferrule* 
          [Left=impE]
          { \inferrule*[Left=use,rightskip=2em,vdots=2em]{ }
            {\Gamma' \vdash \textsc{true} ( \textsc {student} (Bob, Alice) \supset \textsc {mayrd} (Sheet, Bob))}
            \\
            \inferrule*[Right=use,leftskip=2em]{ }
                       {\Gamma' \vdash \textsc{true} ( \textsc {student} (Bob, Alice))}
          }
          {\Gamma' \vdash \textsc{true} ( \textsc {mayrd} (Sheet, Bob) )}
    }
    {\Gamma' \vdash \textsc{aff} (Alice, \textsc {mayrd} (Sheet, Bob))}
    $$
    
We then prove $\textsc {student} (Bob, Alice) \supset \textsc {mayrd} (Sheet, Bob) $
under the hypothesis 
$\Gamma '' = \Gamma , 
\textsc{true} (\forall x  ( \textsc {student} ( x , Alice)  \supset \textsc {mayrd} (Sheet, x) )) $.

$$
\inferrule* 
    [Left=allpE]
    {\inferrule* [Left=use]{ }
      {\Gamma ''  \vdash \textsc{true} (
        \forall x  ( \textsc {student} ( x , Alice)  \supset \textsc {mayrd} (Sheet, x) )) }
    }
    { \Gamma '' \vdash \textsc{true} ( 
      \textsc {student} (Bob, Alice) \supset \textsc {mayrd} (Sheet, Bob) )}
    $$

And we conclude by using the rule $saysE$ on the to preceding proofs.
$$
\inferrule* [Left=trueaff]
{
\inferrule* [Left=saysE]
{
\inferrule* [Left=saysI] % ,leftskip=2em,rightskip=2em,vdots=1.5em]
{
\inferrule*
    [Left=saysE]
    { \inferrule*[Left=use] { }{\Gamma \vdash p3}
      \\ 
      \inferrule*[Right=trueaff] 
                 {\Pi_2}
                 { \Gamma'' \vdash \textsc{aff} (Alice, \textsc {student} (Bob, Alice) \supset \textsc {mayrd} (Sheet, Bob)) }
    }
    { \Gamma \vdash \textsc{aff} (Alice, \textsc {student} (Bob, Alice) \supset \textsc {mayrd} (Sheet, Bob)) }
}
{ \Gamma \vdash \textsc{true} ( Alice \,\textup {says} \,\textsc {student} (Bob, Alice) \supset \textsc {mayrd} (Sheet, Bob) ) }
  \\ \Pi_1
}
{ \Gamma \vdash \textsc{aff} (Alice, \textsc {mayrd} (Sheet, Bob))}
}
{  \Gamma \vdash \textsc{true} (Alice \,\textup{says}\, \textsc {mayrd} (Sheet, Bob))}
$$

\subsection{Proof carrying authorization architecture}

In general looking for a proof is a difficult problem, 
undecidable in the logic we consider.
Therefore it is not a good idea to rely on the ressource
monitor to automatically find a proof of authorization.
On the other hand the user making the request is more
likely to know why the access should be alloweded to him.
In the preceding example $Bob$ would know that he have access
because he is a student.

It is a better idea to rely on the user to construct a proof of authorization,
so that the ressource monitor only have to check the proof, which
is a much simpler task.
This is the proof carrying authorization architecture that we
want to setup in the context of the ML5 programming language.
%This kind of architecture as already been used in previous works [...].
