\documentclass[a4paper,11pt]{article}
\usepackage {a4wide}
\usepackage {mathpartir}
\usepackage {amssymb}
\usepackage {float}
\usepackage {graphicx}
\usepackage[usenames]{color}
\usepackage {hyperref}
\usepackage{gastex}
\usepackage{mdwlist}
\title{Proof carrying authorization in ML5}
\author{Romain Brenguier \\ Internship report \\ Supervisor : Frank Pfenning \\ Carnegie Mellon University}
\date{April - August 2008}

\begin{document}

\maketitle
\tableofcontents

\include{synth}

\section{Introduction}
 
The goal of this report will be to show how we 
added proof carrying authorization into the ML5 language.
Proof carrying authorization is a technique used for
access control, based on an authorization logic.
We will start by presenting it and its advantages.


We will then describe the ML5 language and its type system.
This language was our starting point, 
it is a distributed language and incorporate the notion of location in
its type system.
I find it necessary to present it before going into the changes
we made to it.

The language we have designed integrates an authorization
logic in its type system, and we will go through a complete
description of it.

And finally I will discuss the implementation of
our compiler and runtime system for the language
and the applications we are thinking about.

\input{proof_carrying_authorization}
\input{ml5}
\input{pcml5}
\input{application}

\section{Conclusion}

Thanks to our work, we now have a distributed language in which 
proof of authorization can directly be expressed, and checked
at compile time, preventing the use of wrong proofs at run time.
We will have to build more applications in this language to illustrate
how it can be used and why is type system is useful in practice.
Their is also several points that we would like to think about.

It could be a good allow arbitrary predicates, for instance in
the sheet grade application, it would be more convenient to have a
\emph{student} predicate.
More generally, we could be using more expressive logic, for instance
with consumable credentials \cite{Bauer06consumablecredentials,Garg06alinear} or
a notion of time \cite{deyoung-garg-pfenning08:eta}.

We could have primitives in the language to manage certificates, 
because their is no easy way yet to add certificates or to revoke them,
the \textsc{Aura} programming language \cite{aura} for instance has a
primitive for certificate signature.

We can notice that the checking of proofs by the ressource monitor is useless
for well typed programs.
We could think of getting rid of it.
For a distributed language this is not so evident because we
do not know if parts of the program that are executed on other
world are well typed, but at least on the server
side we know that proofs constructed at our worlds are correct
so we can allow access to our database without checking these proofs
but just looking at their kinds.

Adding existential types could also be useful, for instance
in the type of the \textup{checksig} function, it could prevent
some runtime errors.

\appendix
%\include{lambda5}

%\nocite{*}
\bibliographystyle{alpha}
\bibliography{biblio}


\end{document}          
