\section*{Synthesis}

\subsection*{General context}

This internship stands in the field of logic and programming languages.
The proof carrying authorization architecture is an efficient way to
control access to resources and has already been successfully used
in some applications. It is for instance used by the Grey project at CMU 
%  65 office doors are equipped for access control using smart phones,and are used by 150 people
\cite{bauer+:grey}.
This system uses a resource monitor to protect ressources,
proofs have to be submitted to this resource monitor when one wants
to have access to the resource.
The aim of this research is a programming language  in which we
can easily write these proofs and in which the type system makes
sure that these proofs are correct before even submitting them to 
the resource monitor. Such a type system would make a resource
monitor redundant, as when we are executing a well-typed program
we know that every access attempt will succeed.
\nocite{Tse05designinga,Abadi93acalculus}

\subsection*{Problem Studied}
  
One of the goal of the Manifest Security project \cite{Crary07projectsummary},
is to develop a programming language, in which the fact that
a given program respects some policies is made explicit by type checking.

The problem we are addressing here is authorization, we do so
by using a proof carrying authorization architecture.

ML5 is a distributed language in which location where the code
is executed is explicit in the type system.
I have studied a way to add proof carrying authorization into this 
language.

It is a first step towards a manifestly secure language.


\subsection*{Proposed contribution}

We extend ML5 with proof carrying authorization.
Taking this distributed programming language as a basis, 
we added a way to represent propositions and proofs 
of an authorization logic into the language.
Our goal is to eliminate incorrect authorization proofs by
typechecking proof terms written in the language.

The basic idea was to introduce proposition and truth term 
at the same level than types in the language.
We thought about what primitives a programmer will need,
how they would be integrated to the language and then
really added them to the implementation of the compiler we had.

Our implementation for this language consists of a compiler and a runtime
system incorporated in a HTTP server.

We also tried to implement some applications using this programming language.
 

\subsection*{Validity arguments}

We are developing a compiler for our language and hoping
to have applications programmed with it shortly.

%Our work is based on ML5 and we have kept basically the same terms, 
%additions were made on a higher level. %, for this reason correct terms in ML5 stays correct in PCML5.
Our work is based on ML5, we added proof terms at 
the same level than types in the language.
It gives a way to extend existing languages with an authorization policy,
in an elegant way. What we have done here, can easily be extended or adapted
for other logics.


\subsection*{Achievements and Prospects}

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.

This idea can be generalized to other languages, and also 
to other logics and not only authorization logics.

By now the language allows us to write some useful and secure applications, 
but there is several additions we would like to make.

%% but for instance logic reasoning with information flow properties.

