194 lines
7.4 KiB
TeX
194 lines
7.4 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\ - \fstar}
|
||
\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}
|
||
|
||
Note: The previously defined measure is written as \texttt{|cs|}, where
|
||
\texttt{cs} is a call stack.
|
||
|
||
To prove \texttt{order\_decreases} it needs to be shown that from \texttt{nsteps
|
||
n te cs == cs'} and $n > 0$ follows \texttt{|cs'| << |cs|} for all
|
||
$n\in\mathbb{N}$. The proof is by induction on \texttt{n}. For \texttt{n = 1},
|
||
\texttt{nsteps 1 te cs} is equal to \texttt{step\_simp te cs}. Similarly to
|
||
Exercise 2.2 it follows that the hypothesis holds, because \texttt{cs} is not a
|
||
final state. After that, the induction step is \texttt{nsteps (n+1) te cs ==
|
||
cs'}, which can be rewritten as \texttt{nsteps n te (step\_simp te cs) == cs'}
|
||
(definition of \texttt{nsteps}). With the reasoning from the base case where
|
||
\texttt{n = 1}, it follows that \texttt{|step\_simp te cs| << |cs|}. Now there
|
||
are two cases: either the call stack \texttt{|step\_simp te cs} is final or not.
|
||
For the first case, the lemma \texttt{nsteps\_stop} can be used to derive
|
||
\texttt{step\_simp te cs == cs'} from \texttt{nsteps n te (step\_simp te cs) ==
|
||
cs'}, where \texttt{|step\_simp te cs| << |cs|} holds. For the second case, we
|
||
simply take the induction hypothesis to conclude that the induction holds.
|
||
|
||
Taking the previous proof, for \texttt{callstacks\_unique} it is evident that
|
||
\texttt{|cs'| << |cs|} holds. It follows that \texttt{cs'} $\neq$ \texttt{cs} by
|
||
proof of contradiction: Assuming that \texttt{cs' == cs} and \texttt{|cs'| <<
|
||
|cs|} is true, it would require that the top constant in both lists
|
||
\texttt{LexTop} satisfies \texttt{LexTop << LexTop}. Since this is impossible,
|
||
it contradicts the assumption and therefore it follows that \texttt{cs'} $\neq$
|
||
\texttt{cs}.
|
||
|
||
\section{Exception Propagation}
|
||
|
||
\paragraph{Paper proof}
|
||
|
||
Proof by induction:
|
||
|
||
\begin{verbatim}
|
||
length ps = 0
|
||
|
||
nsteps (2 * (length [])) te (Ter ExcState []) == (Ter ExcState [])
|
||
nsteps 0 te (Ter ExcState []) == (Ter ExcState [])
|
||
(Ter ExcState []) == (Ter ExcState [])
|
||
\end{verbatim}
|
||
|
||
\begin{verbatim}
|
||
length ps to (length ps) + 1
|
||
|
||
nsteps (2 * (length ps)) te (Ter ExcState ps) == (Ter ExcState [])
|
||
nsteps ((2 * (length ps)) - 1) te (step simp (Ter ExcState ps)) == (Ter ExcState [])
|
||
nsteps ((2 * (length ps)) - 1) te (Exec (apply returneffects ts s)::ps’) == (Ter ExcState [])
|
||
nsteps ((2 * (length ps)) - 1) te (Exec s’::ps’) == (Ter ExcState [])
|
||
nsteps ((2 * (length ps)) - 2) te (step simp (Exec s’::ps’)) == (Ter ExcState [])
|
||
nsteps ((2 * (length ps)) - 2) te (Ter (ExcState ps’)) == (Ter ExcState [])
|
||
nsteps (2 * ((length ps) - 1)) te (Ter (ExcState ps’)) == (Ter ExcState [])
|
||
nsteps (2 * (length ps’)) te (Ter (ExcState ps’)) == (Ter ExcState [])
|
||
\end{verbatim}
|
||
|
||
\end{document}
|
||
|