
\section{ML5 with Proof Carrying Authorization}

\subsection{Introduction}

Starting from the ML5 programming language we now want
to integrate a logic into the language.

Classically in a functional programming language, 
we distinguish two levels : terms and types.
Types classify terms.

Here, we would like to add propositions for example, at the same level than types.
But we have to keep a distinction between the two, 
to do so we need a third level.
We now have three levels :
\begin{itemize*}
\item terms
\item constructors , including types, which classify terms
\item kinds , which would classify constructors
\end{itemize*}

The ML5 language basically consists of two kinds : $\textsc{type}$ and $\textsc{world}$,
on the level of constructors we have type constructors,type variables and world variable,
and finally on the level of terms we have the terms which have been described in 
section \ref{ml5}.

The idea will be to add propositions of the logic on
the level of constructors, on this level we will also
have proof terms and therefore judgments will be on 
the level of kinds as they classify proofs.
We don't add anything on the level of terms except for
the $\textsc{acquire\_cert}$ primitive.

As there is nothing yet in the language that allow us
to manipulate constructors, it requires us to add
an explicit polymorphism instantiation for the kinds we added.

We are going to discuss all these points one by one.


\subsection{Architecture}

Lets first describe the architecture we are focusing on.

We have two worlds : server and client. 
The program is compiled to a continuation-passing-style language,
and from here, two different kinds of code are generated.
On the client side Javascript is executed and on the server side
we execute a bytecode language called B5.

The resource we are trying to protect is a database on the server side,
it is protected by a ressource monitor that requires proofs of access.

\begin{figure}[htp]
\centering
\input{architecture_picture.tex}
\label{PCML5 architecture}
\end{figure}



\subsection{Authorization logic}

The authorization logic we are using is quite simple.
It only has two predicates : $\textit {mayrd}$ and  $\textit {maywt}$.

\begin{table}[h]
\begin{tabular}{l c l}
  $A$ & $ ::= $ & $ \textup {mayrd} (R , K) $ $|$ $ \textup{maywt} (R , K) $ \\
  & $|$ &  $\langle K \rangle A$ $|$ $A \supset A $ $|$ $\forall_p A$ $|$ $\forall_r A$ \\
\end{tabular}
  \caption{Syntax for propositions}
\end{table}

We don't give here the rules for this logic, as it is really close
to the one described in \ref{author_log}. 
The difference is that we distinguish resources and principals so
we have two universal quantifications.
We will give inference rules for proof terms in subsection \ref{syntax}.

\subsection{Syntax of the language}
\label{syntax}
We give in the next table the details of the syntax of our language.

\begin{table}[H]
  \begin{tabular}{l l c l}
    Kinds & $ L $ & $::= $ & $\textsc{type}$ $|$ $\textsc{world}$ $|$ $\textsc{database}$ $|$ $\textsc{principal}$ \\
    & & $ | $ & $\textsc{prop}$ $|$ $\textsc{true(A)}$ $|$ $\textsc{aff(K,A)}$ \\% $|$ $\Pi \alpha :: K . K$ \\
    \\
    Constructors & $N$ & $ ::= $ & $\alpha$ $|$ $K$ $|$ $W$ $|$ $A \rightarrow A$ $|$ $A \wedge A$ $|$ $A \vee A $ \\
    & & $ | $ & $\Box A$ $|$ $\Diamond A $ $|$ $A @ W$ \\
   % & & $ | $ & $(N A)$ \\
    & & $ | $ & handle $(A)$ $|$ identity $(K)$ \\
    (Propositions) & & $ | $ &  mayrd$(A,K)$ $|$ maywt$(A,K)$ \\
    & & $ | $ & $ \langle K \rangle A$  $|$ $A \supset A$ $|$ $\forall_p \alpha A$ $|$ $\forall_r \alpha A$ \\
    (Proof terms) & & $ | $ & truaff$(A,K,A)$ $|$ saysI$(K,A,A)$ $|$ saysE$(A,A,A)$ \\
    & & $|$ & impI$(A,A,A)$ $|$ impE$(A,A)$ $|$ \\
    & & $|$ & allpI$(A,A)$ $|$ allpE$(A,A)$ $|$ allrI$(A,A)$ $|$ allrE$(A,A)$ \\
    \\
    Normal constructors & $A$ & $ ::= $ & $ N$ $|$ $\forall \alpha :: L . A$
    \\
    Terms & $M$ & $::=$ & $x$ $|$ $\lambda x : A . M$ $|$ $M_1 M_2$ $|$ $\langle M_1 , M_2 \rangle$ \\
    & & $|$ & $\#_1 M $ $|$ $\#_2 M $ $|$ inl $M$ $|$ inr $M$ $|$ 
    case $M$ $ \{ x . M_1 | x . M_2 \}$ \\
    & & $|$ & hold $(M)$ $|$ leta $x$ = $M$ in $M$ $|$ box $\alpha$ . $M$ $|$ unbox $M$\\
    & & $|$ & here $(M)$ $|$ letd $x,\alpha$ = $M$ in $M$ $|$ get [$A$] $M$ \\
%    & & $|$ & read [$A$,$A$,$A$] $|$ write [$A$,$A$,$A$] ($M$) \\
    & & $|$ & $(M N)$ \\
    & & $|$ & $\textup{acquire\_cert}$ [$A$] $\{ \alpha . M  | M \}$
  \end{tabular}
  \caption{Syntax}
\end{table}



We describe how types, proposition and proof terms are formed.
% should we put this in an annexe ?


We added to ML5 syntax new kinds : databases, principals,
propositions, and judgments of the form $ \textsc{true(A)} $ and $\textsc{aff(K,A)}$
where $K$ is a principal and $A$ a proposition.
This judgment kinds will be used to classify proof terms according
to the statement they are proving.

\begin{figure}[h]
\caption{Kinds}

$$
\inferrule{ } { \Delta \vdash \textsc{type} \, \textup{kind}}
\hspace{4em}
\inferrule{ } { \Delta \vdash \textsc{world} \,\textup{kind}}
$$

$$
\inferrule{ } { \Delta \vdash \textsc{database}\, \textup{kind}}
\hspace{4em}
\inferrule{ } { \Delta \vdash \textsc{principal} \,\textup{kind}}
\hspace{4em}
\inferrule{ } { \Delta \vdash \textsc{proposition} \,\textup{kind}}
$$

$$
\inferrule{  \Delta \vdash A :: \textsc{proposition} } { \Delta \vdash \textsc{true} (A) \,\textup{kind}}
\hspace{4em}
\inferrule{  \Delta \vdash A :: \textsc{proposition} \\  \Delta \vdash K :: \textsc{principal} }
          { \Delta \vdash \textsc{aff}(K,A) \, \textup{kind}}
$$
\end{figure}


We add two new types : $identity$ and $handle$,
terms of this types can be considered as the equivalent of principals
and database but at the level of terms.
The difference is that we don't want terms to appear in proof terms,
because proof terms have to be checked by a resource monitor.
The resource monitor is not an interpreter, it is not able to execute 
terms.

The other types are similar to ML5.

\begin{figure}[h]
\caption{Types}

$$
\inferrule{ \Delta \vdash P :: \textsc{principal}}
{ \Delta \vdash \textup{identity}(P) :: \textsc{type} }
\hspace{4em}
\inferrule{ \Delta \vdash D :: \textsc{database}}
{ \Delta \vdash \textup{handle}(D) :: \textsc{type} }
$$

$$
\inferrule{\Delta \vdash A :: \textsc{type} \\ \Delta \vdash B :: \textsc{type}}
          {\Delta \vdash A \rightarrow B :: \textsc{type}}
$$

$$
\inferrule{\Delta \vdash A :: \textsc{type} \\ \Delta \vdash B :: \textsc{type}}
          {\Delta \vdash A \wedge B :: \textsc{type}}
\hspace{4em}
\inferrule{\Delta \vdash A :: \textsc{type} \\ \Delta \vdash B :: \textsc{type}}
          {\Delta \vdash A \vee B :: \textsc{type}}
$$

$$
\inferrule{\Delta \vdash A :: \textsc{type} }
          {\Delta \vdash \Box A :: \textsc{type}}
\hspace{4em}
\inferrule{\Delta \vdash A :: \textsc{type} }
          {\Delta \vdash \Diamond A :: \textsc{type}}
\hspace{4em}
\inferrule{\Delta \vdash A :: \textsc{type} \\ \Delta \vdash W :: \textsc{world}}
          {\Delta \vdash A @ W :: \textsc{type}}
$$
\end{figure}


Propositions are just the internalization of propositions
of the logic in the language as constructors.

\begin{figure}[H]
\caption{Propositions}
$$
\inferrule{\Delta \vdash D :: \textsc{database} \\ \Delta \vdash K :: \textsc{principal}}
          {\Delta \vdash \textup{mayrd}(D,K) :: \textsc{proposition}}
$$

$$
\inferrule{\Delta \vdash D :: \textsc{database} \\ \Delta \vdash K :: \textsc{principal}}
          {\Delta \vdash \textup{maywt}(D,K) :: \textsc{proposition}}
$$

$$
\inferrule{\Delta \vdash K :: \textsc{principal} \\ \Delta \vdash P :: \textsc{proposition}}
          {\Delta \vdash \langle K \rangle P :: \textsc{proposition}}
$$

$$
\inferrule{\Delta \vdash A :: \textsc{proposition} \\ \Delta \vdash B :: \textsc{proposition}}
          {\Delta \vdash A \supset B :: \textsc{proposition}}
$$

$$
\inferrule{ \Delta , x :: \textsc{principal} \vdash A :: \textsc{proposition} }
          { \Delta \vdash \forall_p x \, A :: \textsc{proposition}}
\hspace{4em}
\inferrule{ \Delta , x :: \textsc{database} \vdash A :: \textsc{proposition} }
          { \Delta \vdash \forall_r x \, A :: \textsc{proposition}}
$$
\end{figure}

Proof terms are somehow more interesting because 
their kinds reflect the proposition they are a proof of.
These proofs are checked at compile time so that we are
sure that compiled code contains only correct proofs.
Thanks to that programs cannot fail in the execution because
the ressource monitor refused access being submitted an 
incorrect proof. 
However the ressource monitor remains necessary as we
do not have control on what is executed at other worlds 
and some malicious computers could execute ill-typed code.

\begin{figure}[h]

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

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

$$
\inferrule*[Left=allpI]
{ \Delta \vdash y :: \textsc {true} (A)}
{ \Delta \vdash \textsc{allpI} (x, y) :: \textsc {true} (\forall_p x . A)}
\hspace {4em}
\inferrule*[Left=allpE]
{ \Delta \vdash y :: \textsc {true} (\forall_p x . A) \\ \Delta \vdash K :: \textsc {principal} }
{ \Delta \vdash \textsc{allpE} (y,K) :: \textsc {true} (A[x \leftarrow_p K])}
$$

$$
\inferrule*[Left=allrI]
{ \Delta \vdash y :: \textsc {true} (A) }
{ \Delta \vdash \textsc{allrI} (x, y) :: \textsc {true} (\forall_r x . A)}
\hspace {4em}
\inferrule*[Left=allrE]
{ \Delta \vdash y :: \textsc {true} (\forall_p x  . A) \\ \Delta \vdash D :: \textsc{database} }
{ \Delta \vdash \textsc{allrE} (y ,\alpha) :: \textsc {true} ( A[x \leftarrow_r D]) }
$$

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

$$
\inferrule*[Left=truaff]
{ \Delta \vdash x ::  \textsc{true} (A)}
{ \Delta \vdash \textsc{truaff} (A ,K, x) :: \textsc{aff} (K, A) }
$$

$$
\inferrule*[Left=saysE]
{ \Delta \vdash x :: \textsc{true} (K \textup{says} A) \\ \Delta, \alpha :: A \vdash y :: \textsc{aff} (K,B)}
{ \Delta \vdash \textsc{saysE} (\alpha, x ,y) :: \textsc{aff} (K, B) }
$$
\caption{Proof terms}
\end{figure}



\subsection{Explicit polymorphism}

Proofs need to be passed to some functions, so 
that they can verify the proofs and, for instance,
allow the access to a database.
This is similar to polymorphism, since 
such functions will takes constructors as argument.
For instance we would like to be able to declare 
something like this
$$
\textup{read} \, : \, \forall p :: \textsc {principal} . \forall x :: \textsc{true} (mayrd (db,p)) . 
\textup {identity} (p) \rightarrow \textup {string}
$$
In the same way we could represent a polymorphic type
$$
\textup{id} \, : \,\forall a :: \textsc {type} . a \rightarrow a
$$

The difference with polymorphism over types is
that we already have type inference, making
explicit instantiation unnecessary. 
In the case of proofs we want the programmer 
to manually write them, as their is no way to automatically
infer them.

The typing rules for this instantiation follow in figure \ref{fig:instantiation}.

\begin{figure}[H]
\caption{Instantiation rules}
\label{fig:instantiation}

$$
\inferrule
{ \Delta \vdash M : \forall x :: \textsc {database} . T \\ \Delta \vdash D :: \textsc {database} }
{ \Delta \vdash (M D) : T }
$$

$$
\inferrule
{ \Delta \vdash M : \forall x :: \textsc {principal} . T \\ \Delta \vdash P :: \textsc {principal} }
{ \Delta \vdash (M P) : T }
$$

$$
\inferrule
{ \Delta \vdash M : \forall x :: \textsc {proposition} . T \\ \Delta \vdash P :: \textsc {proposition} }
{ \Delta \vdash (M P) : T }
$$

$$
\inferrule
{ \Delta \vdash M : \forall x :: \textsc {true}(A) . T \\ \Delta \vdash P :: \textsc {true}(A) }
{ \Delta \vdash (M P) : T }
$$

$$
\inferrule
{ \Delta \vdash M : \forall x :: \textsc {aff}(K,A) . T \\ \Delta \vdash P :: \textsc {aff}(K,A) }
{ \Delta \vdash (M P) : T }
$$
\end{figure}

We have an application of polymorphic terms to kinds, but we choose not to have
a corresponding abstraction.
Consequently, only values declared as externals can introduce 
this kind of polymorphism.
Read and write are two examples of these functions.

\subsubsection*{Read and Write}

With polymorphism we can now express that a function needs a
proof, directly in its type.
A principal can read a resource only if he can prove that
the principal controlling this resource, says he may read it.
This can directly be expressed in our language through the
type of the read function.

\begin{eqnarray*}
\textup{read} : \forall d :: \textsc{database} \, \forall p :: \textsc {principal} \,
\forall t :: \textsc{true} (\textsc{mayrd} (d,p) ) \,\\ 
\textup{handle}(d)  \rightarrow \textup{identity}(p)
 \rightarrow \textup{string}
\end{eqnarray*}

and the write function is similar 

\begin{eqnarray*}
\textup{write} : \forall d :: \textsc{database} \, \forall p :: \textsc {principal} \,
\forall t :: \textsc{true} (\textsc{maywt} (d,p) ) \, \\
\textup{handle}(d)  \rightarrow \textup{identity}(p)
 \rightarrow \textup{string} \rightarrow \textup{unit}
\end{eqnarray*}

Here is the actual declaration of this function in the language :
\begin{verbatim}
extern val (d:database , p:principal ,  prf : TRUE mayrd d p) read : 
      d dbhandle -> p identity -> string @ server

extern val (d:database , p:principal , prf : TRUE maywt d p) write : 
      d dbhandle -> p identity -> string -> unit @ server
\end{verbatim}

\subsection{Certificates}

The proofs we construct need hypothesis, 
they would be the access policies.
When the reference monitor checks the proofs, 
he also need to verify that hypothesis are correct.
These hypothesis would take the form of digitally signed
certificates, this way the resource monitor can check them
by knowing the public key of a principal.


For instance we can use the hypothesis $ K \textup{says} P$ in a proof
if we have a certificate asserting the proposition $P$, signed by the principal $K$.

We need to dynamically access these certificates.
That is what provides the \emph{acquire\_cert} primitive.
Here is the typing rule associated with \emph{acquire\_cert}.

$$
\inferrule
{ \Delta , \alpha :: \textsc{true} (A) ; \Gamma \vdash M_1 : A' @ l \\ 
  \Delta ; \Gamma \vdash M_2 : A' @ l}
{ \Delta ; \Gamma \vdash \textup{acquire\_cert} [A] \{\alpha . M_1 | M_2\} : A' @ l }
$$

In this rule, $M_1$ represent the term that is to be executed if 
we succeed at runtime in finding a certificate for A.
In that case the variable $\alpha$ is bind and is of kind $\textsc{true}(A)$,
it can be used in access proof terms as a proof of $A$.

If we fail to get a certificate then $M_2$ is executed.

\section{Implementation}

\subsection{Runtime system}

Our implementation is based on the \textit {ml5pgh} compiler and the \textit{server5},
so the runtime system is almost similar.
The compiler is designed for web applications and produce Javascript and bytecode.
Both are kept on the server side. 

When someone use his web browser to access an application on the server,
he received the Javascript part of the program.
The browser should then starts the execution of the script it received,
and the server starts to execute the bytecode part of the program.


\subsection{Identity}
The terms of type $\textup{identity} (p)$, should in fact be
evidence that the principal executing the program is the principal $p$.
In our implementation it is represented by a certificate digitally
signed by an authentication authority. 
This certificate is checked by the runtime system along with proofs
and other certificates.

To provide a certificate of identity the server can trust we are using
the authentication system used by Carnegie Mellon University's websites.
This system is called pubcookie and is an implementation of WebISO, it's used
in several universities in the United States.
% sources
The goal is to provide an authentication server common for every web-applications
in the university, this way the users do not have to type their logins and passwords everytime
they access a new application, and they only do so when asked by the webiso login server, which
they can trust.

The application server side of pubcookie is written as an apache module, and 
as we are not using apache but our own server implementation (called server5) we
needed to reimplement some of the primitives provided by this module.

We provide this identification by functions declared as external, as it is
implemented in the server runtime.
This is the way we get an identity type.

Here are the actual declaration in our language.
\begin{verbatim}
val webiso : unit -> string @ home 

extern val (p:principal) checksig : string -> p identity option @ server
\end{verbatim}

The $\textup{webiso}$ function request that the user identify himself
to the webiso server, the string returned is a cookie generated by
this login server containing the login of the user, signed with
private key of the login server, and encrypted with a symmetric key
that webiso shares with our application server.
The checksig function converts this string to a identity if it
can verify its signature is valid.

The signature is conserved in the identity value, as it would have
to be checked by the resource monitor when we access a resource.

\subsection{Certificates}

Certificates are mainly managed by the server, 
there is no primitives in our language yet to 
dynamically add or remove certificates, so for now
they are read by the server in files. 

This certificates are propositions, along
with a digitally signed hash of the string
 representation of this propositions.


\subsection{Resources}

In our implementation resources are only on the server side.
So we implemented a simple database linked with the server side 
which uses a resource monitor, requiring a proof everytime
somebody want to access its data.

The way we obtain a handle value for a database is by using the
$\textup{gethandle}$ function.

\begin{verbatim}
extern val (d:database) gethandle : unit -> d handle
\end{verbatim}

