\documentclass[twoside,11pt]{article}

\usepackage[margin=1.25in]{geometry}
\usepackage{amsmath,amsfonts,amsthm,amssymb,graphicx}
\usepackage{lmodern}
\usepackage{enumerate}
\usepackage{courier}
\usepackage{mathpartir}

\newcommand{\pred}[1]{\ensuremath{{\sf #1}}}
\newcommand{\rname}[1]{\mbox{\small #1}}
\newtheorem{theorem}{Theorem}
\newtheorem{definition}{Definition}
\setlength{\parindent}{0 in}

\newcounter{lecnum}
\renewcommand{\thepage}{\thelecnum-\arabic{page}}

\newcounter{pbcounter}
\newcommand{\problem}[1]{\stepcounter{pbcounter}\vspace{12pt}{\Large\bf Problem \thelecnum-\arabic{pbcounter} (#1 points)}\\[3pt]}

\newcommand{\jcmd}{\; \mathsf{cmd}}

\newcommand{\lecture}[3]{
\pagestyle{myheadings}
\thispagestyle{plain}
\newpage
\setcounter{lecnum}{#1}
\setcounter{page}{1}
\noindent
\begin{center}
	\textbf{\large Logics in Security} \hfill \textbf{\large Winter 2014}\\[9pt]
	{\LARGE Homework for Module #1}\\[9pt]
	Instructor: Deepak Garg \hfill TA: Iulia Bolo\c steanu\\
	\texttt{dg@mpi-sws.org} \hfill \texttt{iulia\_mb@mpi-sws.org}\\[-6pt]
	\rule{\textwidth}{0.2mm}\\
	{\it Release date: #2 \hfill Due date: #3}\\[-6pt]
	\rule{\textwidth}{0.2mm}
\end{center}

\vspace{-18pt}

\paragraph{General instructions:}
Attempt all questions. Submit your homework via email to both the
instructor and the TA before midnight on the due date. The {\LaTeX}
source for this homework will be provided to help you typeset. You can
also typeset using any other means, including simple ASCII.

\paragraph{Homework instructions:}
This homework is divided into two sections. Section~1 tests your
understanding of programming language semantics, typing and
type-safety, as taught in class. Section~2 tests your understanding of
the type system for information flow from the paper of Volpano, Smith
and Irvine.}

\begin{document}
\lecture{4}{02.02.2015}{14.02.2015}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Operational Semantics and Types}

For this section, refer to the operational semantics in Appendix~A and
the typing rules in Appendix~B. Appendix~C is \textbf{not} to be
referred for this section.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\problem{5} {\bf Expression determinism lemma.}
%
A key lemma in the proof of type-safety that we discussed in class is
determinism of expression evaluation. Prove that lemma here: If $\mu,
e \Downarrow v_1$ and $\mu, e \Downarrow v_2$ then $v_1 = v_2$.

State clearly what you are are inducting on. Independent of what you
induct on, you only need to write the induction cases corresponding to
the following forms of $e$: $v$, $l$, and $e_1 + e_2$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\problem{5} {\bf Progress theorem.}  The progress theorem says that a
well-typed program that is not $\mathsf{skip}$ must always reduce
further. Formally, if $\lambda \vdash p$ and $\lambda \vdash \mu$ and
$p \not= \mathsf{skip}$, then there exist $\mu', p'$ such that $\mu, p
\rightarrow \mu', p'$. 

The proof proceeds by induction on the
derivation of $\lambda \vdash p$. In class, we covered all cases of
the proof except $p =\mathsf{while}~e ~\mathsf{do}~p'$. Show that case
of the proof.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\problem{5} {\bf Type-safety.} Consider the program $p = (\ell :=
\mathsf{true}; \mathsf{if} ~\ell~ \mathsf{then}~ \ell :=
\mathsf{false} ~\mathsf{else}~ \ell := 1)$. Assuming the typing context is
$\lambda = \{\ell: \texttt{int}\}$, answer the following questions:
%
\begin{enumerate}
\item Is $p$ well-typed, i.e., is $\lambda \vdash p$ provable? Justify your answer.
\item Is $p$ unsafe, i.e., can $p$ reach a stuck (bad) state by
  reduction starting from any memory $\mu$? (Recall that a program is
  bad/stuck when it is not $\mathsf{skip}$ and no reduction is
  possible.)
\end{enumerate}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Types for information flow control}

For this section, refer to the operational semantics in Appendix~A and
the typing rules in Appendix~C. Appendix~B is \textbf{not} to be
referred for this section.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\problem{10}{\bf Lattices.}  The following exercise is designed to help
you better understand the structure of lattices.

\begin{definition}(Complete lattice)
A partially ordered set $(S, \sqsubseteq)$ is called a \emph{complete
  lattice} if every subset $M$ of $S$ has a least upper bound and a
greatest lower bound in $(S, \sqsubseteq)$.
\end{definition}

The least upper bound (also called lub or join) of two elements $a, b
\in L$ is written $a \sqcup b$. The greatest lower bound (glb or meet)
of two elements $a,b \in L$ is written $a \sqcap b$.
%
\begin{enumerate}
\item On natural numbers other than $0$, consider the following order:
  $a \sqsubseteq b$ if and only if $a$ divides $b$, i.e., $b \text{
  mod } a = 0$. For each of the following sets $S$, is $(S, \sqsubseteq)$ a complete lattice? Justify your answers.
%
  \begin{enumerate}
  \item $S = \mathbb{N} \backslash 0$ (all positive natural numbers).
  \item $S = \{1, 2, 3, 4, 12, 24, 36, 48\}$.
  \item $S = \{k ~|~ k \text{ divides } n\}$ where $n$ is a fixed
    integer.
  \item $S = \{k ~|~ n \text{ divides } k\}$ where $n$ is a fixed
    integer.
  \end{enumerate}

\item Consider the lattice defined in 1(b) above. Calculate the
  following joins and meets: $2 \sqcup 3$, $12 \sqcup 24$, $2 \sqcap
  3$, $24 \sqcup 36$, $48 \sqcap 36$, $12 \sqcap 3$.
\end{enumerate}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\problem{7}{\bf Information flow.}  Let $\lambda$ be a typing context
--- an assignment of lattice elements to memory locations. Recall that
a program $p$ is non-interfering (secure in the sense that it does not
have any bad information flows) if the following hold for all $\tau,
\mu_1,\mu_2,\mu_1',\mu_2'$: If for all $l$ such that $\lambda (l)
\sqsubseteq \tau$, $\mu_1(l) = \mu_2(l)$ and, additionally, $\mu_1, p
\Rightarrow \mu_1'$ and $\mu_2, p \Rightarrow \mu_2'$, then for all
$l$ such that $\lambda(l) \sqsubseteq \tau$, $\mu_1'(l) = \mu_2'(l)$.

\begin{enumerate}
\item Let the lattice be $L \sqsubseteq H$ and let $\lambda = \{x : L,
  y : H, z: H\}$. Consider the following program:
%
\begin{center}
\begin{tabular}{cl}
 & $\mathsf{if}~ (y = 1)~ \mathsf{then}~ \{$ \\
	& \quad $x := 1;$\\
        & $\}$\\
	& $\mathsf{else}~ \{$\\
	& \quad $z := y + 1;$\\
        & $\}$\\
 & $x := 1;$
\end{tabular}
\end{center}
%
\begin{enumerate}[a.]
\item Assuming the initial memory is $\mu = \{ x \mapsto 5, y \mapsto
  1, z \mapsto 2 \}$, what is the final memory $\mu'$ after the
  execution of the program?

\item Using the type system of Appendix~C, derive a type of the form
  $\tau \jcmd$ for the program. If no type can be derived, explain
  where the derivation fails and why the program cannot be typed.

\item Is this program non-interfering? Justify your answer.
\end{enumerate}

\item Let the lattice be $\mathcal{L} = \{L \sqsubseteq M_1, L
  \sqsubseteq M_2, M_1 \sqsubseteq H, M_2 \sqsubseteq H\}$ and let
  $\lambda = \{a:L, b:M_1, c:M_2, d:H \}$. Consider the following program:
%
\begin{center}
\begin{tabular}{cl}
 & $\mathsf{while}~ (a > 0)~ \mathsf{do}~\{$ \\
	& \quad $b := b + a;$\\
	& \quad $a := a - 1;$\\
& \} \\	
& $\mathsf{if}~ (b + 2 == 0)~ \mathsf{then}$\\
	& \quad $d := d + b;$\\
& $\mathsf{else}$\\
	& \quad $d := d + c;$
\end{tabular}
\end{center}
%
\begin{enumerate}[a.]
\item Using the type system of Appendix~C, derive a type of the form
  $\tau \jcmd$ for the program. If no type can be derived, explain
  where the derivation fails and why the program cannot be typed.

\item Is this program non-interfering? Justify your answer.
\end{enumerate}
\end{enumerate}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\appendix

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Syntax and Operational Semantics}

Syntax:

\[\begin{array}{llll}
\mbox{Values} & v & ::= & 0 \mid 1 \mid 2 \ldots \mid \mathsf{true}
\mid \mathsf{false}\\

\mbox{Expressions} & e & ::= & v \mid \ell \mid e_1 + e_2 \mid e_1 -
e_2 \mid e_1 == e_2 \mid e_1 > e_2\\

\mbox{Commands} & p & ::= & \mathsf{skip} \mid \ell := e \mid p_1;p_2
\mid \mathsf{if}~ (e)~ \mathsf{then}~ p_1~ \mathsf{else}~ p_2 \mid
\mathsf{while}~ (e)~ \mathsf{do}~p \\

\mbox{Memory} & \mu & ::= & \ell_1 \mapsto v_1, \ldots, \ell_n \mapsto v_n

\end{array} \]

\medskip

Semantic rules for expressions:\\

{\bf Note:} For any connective $o$ in $\{+, -, ==, >\}$, $\hat{o}$
denotes the underlying arithmetic operator.
%
\begin{mathpar}
\inferrule{ }{\mu, v \Downarrow v}

\inferrule{ }{\mu, \ell \Downarrow \mu(\ell)}

\inferrule{\mu, e_1 \Downarrow v_1 \and \mu, e_2 \Downarrow v_2 \and
  v_1 \hat{+} v_2 = v}{\mu, e_1 + e_2 \Downarrow \mu, v}

\inferrule{\mu, e_1 \Downarrow v_1 \and \mu, e_2 \Downarrow v_2 \and
  v_1 \hat{-} v_2 = v}{\mu, e_1 - e_2 \Downarrow \mu, v}

\inferrule{\mu, e_1 \Downarrow v_1 \and \mu, e_2 \Downarrow v_2 \and
  (v_1 \hat{==} v_2) = v}{\mu, e_1 == e_2 \Downarrow \mu, v}

\inferrule{\mu, e_1 \Downarrow v_1 \and \mu, e_2 \Downarrow v_2 \and
  (v_1 \hat{>} v_2) = v}{\mu, e_1 > e_2 \Downarrow \mu, v}
\end{mathpar}

\medskip

Small-step or reduction semantics for commands:
%
\begin{mathpar}
\inferrule{\mu, e \Downarrow v }{\mu, \ell := e \rightarrow \mu[\ell \mapsto v], \mathsf{skip}}

\inferrule{\mu, p_1 \rightarrow \mu', p'_1}{\mu, p_1; p_2 \rightarrow \mu', p_1';p_2}

\inferrule{ }{\mu, (\mathsf{skip}; p) \rightarrow \mu, p}

\inferrule{\mu, e \Downarrow \mathsf{true}}{\mu, \mathsf{if}~ (e)~ \mathsf{then}~ p_1 ~\mathsf{else}~ p_2 \rightarrow \mu, p_1} 

\inferrule{\mu, e \Downarrow \mathsf{false}}{\mu, \mathsf{if}~ (e)~ \mathsf{then}~ p_1 ~\mathsf{else}~ p_2 \rightarrow \mu, p_2}

\inferrule{\mu, e \Downarrow \mathsf{true}}{\mu, \mathsf{while}~ (e)~ \mathsf{do}~ p \rightarrow \mu, p; \mathsf{while}~ (e)~ \mathsf{do}~ p}

\inferrule{\mu, e \Downarrow \mathsf{false}}{\mu, \mathsf{while}~ (e)~ \mathsf{do}~ p \rightarrow \mu, \mathsf{skip}}
\end{mathpar}

\medskip

Big-step semantics for commands:
%
\begin{mathpar}

\inferrule{ }{\mu, \mathsf{skip} \Rightarrow \mathsf{skip}}

\inferrule{\mu, e \Downarrow v}{\mu, \ell := e \Rightarrow \mu[\ell
    \mapsto v]}

\inferrule{\mu, p_1 \Rightarrow \mu' \\ \mu' , p_2 \Rightarrow
  \mu''}{\mu, (p_1; p_2) \Rightarrow \mu''}

\inferrule{\mu, e \Downarrow \mathsf{true} \\ \mu, p_1 \Rightarrow
  \mu'}{\mu, \mathsf{if}~e~\mathsf{then}~p_1~\mathsf{else}~p_2
  \Rightarrow \mu'}

\inferrule{\mu, e \Downarrow \mathsf{false} \\ \mu, p_2 \Rightarrow
  \mu'}{\mu, \mathsf{if}~e~\mathsf{then}~p_1~\mathsf{else}~p_2
  \Rightarrow \mu'}

\inferrule{\mu, e \Downarrow \mathsf{true} \\ \mu, (p;
  \mathsf{while}~e~\mathsf{do}~p) \Rightarrow \mu'}{\mu,
  \mathsf{while}~e~\mathsf{do}~p \Rightarrow \mu'}

\inferrule{\mu, e \Downarrow \mathsf{false}}{\mu,
  \mathsf{while}~e~\mathsf{do}~p \Rightarrow \mu}

\end{mathpar}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Typing rules}

\[\begin{array}{llll}
\mbox{Types} & \tau & ::= & \texttt{int} \mid \texttt{bool}\\

\mbox{Type context} & \lambda & ::= & \ell_1 : \tau_1, \ldots, \ell_n
: \tau_n
%
\end{array} \]

\medskip

Typing rules for expressions:
%
\begin{mathpar}

\inferrule{n \in \{0,1,2,\ldots\}}{\lambda \vdash n: \texttt{int}}

\inferrule{b \in \{\mathsf{true}, \mathsf{false}\}}{\lambda \vdash b: \texttt{bool}}

\inferrule{\ell : \tau \in \lambda}{\lambda \vdash \ell: \tau}

\inferrule{\lambda \vdash e_1: \texttt{int} \\ \lambda \vdash e_2:
  \texttt{int}}{\lambda \vdash e_1 + e_2: \texttt{int}}

\inferrule{\lambda \vdash e_1: \texttt{int} \\ \lambda \vdash e_2:
  \texttt{int}}{\lambda \vdash e_1 - e_2: \texttt{int}}

\inferrule{\lambda \vdash e_1: \texttt{int} \\ \lambda \vdash e_2:
  \texttt{int}}{\lambda \vdash e_1 == e_2: \texttt{bool}}

\inferrule{\lambda \vdash e_1: \texttt{int} \\ \lambda \vdash e_2:
  \texttt{int}}{\lambda \vdash e_1 > e_2: \texttt{bool}}
%
\end{mathpar}

\medskip

Typing rules for commands:
%
\begin{mathpar}

\inferrule{ }{\lambda \vdash \mathsf{skip}}

\inferrule{\ell :\tau \in \lambda \\ \lambda \vdash e: \tau}{\lambda \vdash \ell := e}

\inferrule{\lambda \vdash p_1 \\ \lambda \vdash p_2}{\lambda \vdash p_1 ; p_2}

\inferrule{\lambda \vdash e: \texttt{bool} \\ \lambda \vdash p_1
  \\ \lambda \vdash p_2}{\lambda \vdash
  \mathsf{if}~e~\mathsf{then}~p_1~\mathsf{else}~p_2}

\inferrule{\lambda \vdash e: \texttt{bool} \\ \lambda \vdash
  p}{\lambda \vdash \textsf{while}~e~\text{do}~p}
\end{mathpar}

\medskip

Typing rule for memories:
%
\begin{mathpar}
\inferrule{\lambda \vdash v_1: \lambda(\ell_1) \\ \ldots
  \\ \lambda \vdash v_n: \lambda(\ell_n)}{\lambda \vdash \ell_1
  \mapsto v_1, \ldots, \ell_n \mapsto v_n}

\end{mathpar}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Types for Information Flow Control}

For information flow control, types $\tau$ are elements of a lattice
$(S, \sqsubseteq)$. A type context $\lambda$ assigns types to memory
locations. This is written $\lambda ~::=~ \ell_1: \tau_1,\ldots,
\ell_n:\tau_n$.

\medskip 

Typing rules for expressions:
%
\begin{mathpar}

\inferrule{ }{\lambda \vdash v: \tau}

\inferrule{\ell : \tau \in \lambda}{\lambda
  \vdash \ell: \tau}

\inferrule{\lambda \vdash e_1: \tau_1 \\ \lambda \vdash e_2: \tau_2
  \\ \circ \in \{+,-,==,>\}}{\lambda \vdash e_1 \circ e_2: \tau_1
  \sqcup \tau_2}


\inferrule{\lambda \vdash e: \tau \\ \tau \sqsubseteq \tau'}{\lambda
  \vdash e: \tau'}
\end{mathpar}


\medskip

Typing rules for commands:
%
\begin{mathpar}

\inferrule{ } {\lambda \vdash \mathsf{skip}: \tau \jcmd}

\inferrule{\ell: \tau \in \lambda \\ \lambda \vdash e: \tau}{\lambda
  \vdash \ell := e : \tau \jcmd}

\inferrule{\lambda \vdash p_1: \tau \jcmd \\ \lambda \vdash p_2: \tau
  \jcmd}{\lambda \vdash p_1;p_2: \tau \jcmd}

\inferrule{\lambda \vdash e: \tau \\ \lambda \vdash p_1: \tau \jcmd
  \\ \lambda \vdash p_2: \tau \jcmd}{\lambda \vdash
  \mathsf{if}~e~\mathsf{then}~p_1~\mathsf{else}~p_2: \tau \jcmd}

\inferrule{\lambda \vdash e: \tau \\ \lambda \vdash p: \tau
  \jcmd}{\lambda \vdash \mathsf{while}~e~\mathsf{do}~p: \tau \jcmd}

\inferrule{\lambda \vdash p: \tau \jcmd \\ \tau' \sqsubseteq
  \tau}{\lambda \vdash p: \tau' \jcmd}
\end{mathpar}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\end{document}





