
\documentclass[a4paper,10pt]{article}

\let\bfseriesbis=\bfseries \def\bfseries{\sffamily\bfseriesbis}


\newenvironment{point}[1]%
{\subsection*{#1}}%
{}

\setlength{\parskip}{0.3\baselineskip}

\begin{document}

\title{Proof carrying authorization in ML5}

\author{Brenguier Romain, Frank Pfenning, Carnegie Mellon University}

\date{April - August 2008}

\maketitle

\pagestyle{empty} %
\thispagestyle{empty}

%% Attention: pas plus d'un recto-verso!


\begin{point}{General context}

This internship stand in the field of manifest security.

The goal of the manifest security project is to be able
to build manifestly secure pieces of software.

By first specifying a logic in which we can express security policies,
and develop programming languages whose type system enforce this policies.



%%  De quoi s'agit-il? D'o� vient la question? Quels sont les travaux
%%  d�j� accomplis dans ce domaine dans le monde?

\end{point}

\begin{point}{Study}
  
I study a way to implement a programming language incorporating
properties and proofs comming from an authorization logic.


%%  Quelle est la question que vous avez r�solue? Pourquoi est-elle
%%  importante, � quoi cela sert-il d'y r�pondre?  Pourquoi �tes-vous
%%  le premier chercheur de l'univers � l'avoir pos�e?

\end{point}

\begin{point}{Proposed contribution}

%%  Qu'avez vous propos� comme solution � cette question? Attention, pas
%%  de technique, seulement les grandes id�es! Soignez particuli�rement
%%  la description de la d�marche \emph{scientifique}.

We extend a distributed programming language (ML5) with proof carrying authorization.

Taking ML5 as a basis, we added a way to represent propositions and proofs 
of an authorization logic into the language.

We also added runtime primitives to inforce policies specified in this logic.
 
\end{point}

\begin{point}{Validity arguments}

We implemented extended the existing compiler for ML5 to compile our language.
I also developed some application in this language to show its usability.

%%  Qu'est-ce qui montre que cette solution est une bonne solution? Des
%%  exp�riences, des corollaires? Commentez la \emph{stabilit�} de votre
%%  proposition: comment la validit� de la solution d�pend-elle des
%%  hypoth�ses de travail?

\end{point}


\begin{point}{Achievements and Prospects}
  
This give us a programming language in which manifestly secure 
application can be developped, 
but it remains to build more application to illustrate its usefullness.
Some improvement could be made in the way we treat certificates, 
removals and adds of them are not yet part of the language.

%%  Et aprzs? En quoi votre approche est-elle g�n�rale? Qu'est-ce que
%%  votre contribution a apport� au domaine? Que faudrait-il faire
%%  maintenant? Quelle est la bonne \emph{prochaine} question?

\end{point}


\end{document}



