152 lines
5.0 KiB
TeX
152 lines
5.0 KiB
TeX
\documentclass[12pt,a4paper]{article}
|
|
|
|
\usepackage[cm]{fullpage}
|
|
\usepackage{amsthm}
|
|
\usepackage{amsmath}
|
|
\usepackage{amsfonts}
|
|
\usepackage{amssymb}
|
|
\usepackage{xspace}
|
|
\usepackage[english]{babel}
|
|
\usepackage{fancyhdr}
|
|
\usepackage{titling}
|
|
\renewcommand{\thesection}{Exercise \projnumber.\arabic{section}:}
|
|
|
|
\newcommand{\groupnumber}{5}
|
|
\newcommand{\name}{Tobias Eidelpes}
|
|
\newcommand{\matriculation}{01527193}
|
|
|
|
\newcommand\fstar{F$^\star$\xspace}
|
|
\newcommand{\projnumber}{2}
|
|
\newcommand{\Title}{\fstar}
|
|
\setlength{\headheight}{15.2pt}
|
|
\setlength{\headsep}{20pt}
|
|
\setlength{\textheight}{680pt}
|
|
\pagestyle{fancy}
|
|
\fancyhf{}
|
|
\fancyhead[L]{Formal Methods for Security and Privacy \projnumber\ - ProVerif}
|
|
\fancyhead[C]{}
|
|
\fancyhead[R]{Group \groupnumber}
|
|
\renewcommand{\headrulewidth}{0.4pt}
|
|
\fancyfoot[C]{\thepage}
|
|
|
|
|
|
\begin{document}
|
|
\thispagestyle{empty}
|
|
\noindent\framebox[\linewidth]{%
|
|
\begin{minipage}{\linewidth}%
|
|
\hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2021)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\
|
|
|
|
\begin{center}
|
|
{\bf\Large Project \projnumber~-- \Title}
|
|
\end{center}
|
|
|
|
\vspace*{5pt}\hspace*{5pt} \hfill TU Wien \hspace*{5pt}
|
|
\end{minipage}%
|
|
}
|
|
\vspace{0.5cm}
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
|
|
\section*{Group \groupnumber}
|
|
Our group consists of the following members:
|
|
\begin{center}
|
|
\textbf{\name}
|
|
|
|
\matriculation
|
|
\end{center}
|
|
|
|
\section{Small-step semantics}
|
|
|
|
\textit{Notes on semantics. Not mandatory.}
|
|
|
|
\section{Termination}
|
|
|
|
\paragraph{Explanation of the used measure}
|
|
|
|
The measure consists of a list of size three. The entries are:
|
|
|
|
\begin{enumerate}
|
|
\item The amount of gas in the execution state.
|
|
\item The size of the call stack.
|
|
\item If the call stack is constructed with \texttt{Exec}, the third element
|
|
is the natural number 1 and if the call stack is constructed with
|
|
\texttt{Ter}, the third element is the natural number 0.
|
|
\end{enumerate}
|
|
|
|
For the amount of gas, there are three different possibilities:
|
|
|
|
\begin{enumerate}
|
|
\item The call stack is a plain call stack.
|
|
\item If the call stack is in a halting state, gas specifies the amount of
|
|
remaining gas.
|
|
\item If there is an exception state, the amount of gas is set to 0.
|
|
\end{enumerate}
|
|
|
|
Additionally, there are three match clauses in the \texttt{step} function. The
|
|
first case matches a termination state with an empty call stack. If the state
|
|
before that was an exception, the first elements are equal but the size of the
|
|
call stack before the application of the \texttt{step} function was greater.
|
|
This means that the measure decreases. If there was no exception but of type
|
|
\texttt{Exec} with a positive amount of gas, the measure also decreases.
|
|
|
|
In the second match clause, a termination state with a non-empty call stack is
|
|
handled. The amount of gas decreases if there is a termination state of
|
|
\texttt{ExcState}, because it is set to 0. If the termination state is
|
|
\texttt{HaltState}, the amount of gas also decreases.
|
|
|
|
The third match clause handles execution of a plain call stack. If a
|
|
\texttt{HaltState} is reached, the amount of gas reduces by 1. Again, if there
|
|
occurs an exception, looking at the third element of the list gives a value
|
|
change from 1 to 0.
|
|
|
|
\section{Final states}
|
|
|
|
\paragraph{Paper proofs}
|
|
|
|
To prove \texttt{nsteps\_stop}, induction over the amount of executed steps $n$
|
|
is used. The base case starts with $n = 0$. This case is trivial since
|
|
\texttt{nsteps 0 te cs == cs}. The induction hypothesis is \texttt{nsteps (n-1)
|
|
te cs == cs} and it is assumed that $n > 0$. The induction then goes as follows:
|
|
\begin{verbatim}
|
|
nsteps n te cs = nsteps (n-1) te (step_simp te cs)
|
|
= nsteps (n-1) te cs
|
|
= cs
|
|
\end{verbatim}
|
|
It is allowed to reduce \texttt{step\_simp te cs} to \texttt{cs}, because
|
|
\texttt{cs} is already final.
|
|
|
|
Now it is possible to prove the lemma \texttt{progress}: \texttt{cs ==
|
|
step\_simp te cs} $\rightarrow$ \texttt{isFinal cs}. Since, \texttt{step\_simp}
|
|
has the same value as the \texttt{step} function, when the outcome is
|
|
\texttt{Next}, the call stack is different from \texttt{cs}. This means that the
|
|
left side of the lemma does not hold and therefore the right side does not have
|
|
to hold to satisfy the implication. If the outcome is \texttt{Stop}, \texttt{cs}
|
|
can only equal \texttt{Ter ts []} and therefore the left side is satisfied. When
|
|
the left side is satisfied, \texttt{cs} is a final state and therefore it
|
|
follows that \texttt{isFinal cs} is also true.
|
|
|
|
\paragraph{Explanation on used equalities}
|
|
|
|
The lemma uses propositional equality, because \texttt{callstack} has the
|
|
keyword \texttt{noeq}, which means that the type does not satisfy decidable
|
|
equality. The usual equality only works with types that satisfy decidable
|
|
equality and therefore propositional equality is needed.
|
|
|
|
\section{Uniqueness of call stacks}
|
|
|
|
\paragraph{Paper proofs}
|
|
%TODO
|
|
|
|
\paragraph{Explanation on lemma \texttt{order\_ineq}}
|
|
|
|
\section{Exception Propagation}
|
|
|
|
\paragraph{Paper proof}
|
|
%TODO
|
|
|
|
\paragraph{Explanation on alternative formulations}
|
|
%TODO
|
|
|
|
\end{document}
|
|
|