\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}