--- a/slides/slides10.tex Tue Dec 03 20:00:03 2013 +0000
+++ b/slides/slides10.tex Tue Dec 10 04:15:57 2013 +0000
@@ -1,8 +1,6 @@
\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{proof}
-\usepackage{beamerthemeplainculight}
-\usepackage[T1]{fontenc}
-\usepackage[latin1]{inputenc}
+\usepackage{beamerthemeplaincu}
\usepackage{mathpartir}
\usepackage{isabelle}
\usepackage{isabellesym}
@@ -18,7 +16,8 @@
\usetikzlibrary{shapes}
\usetikzlibrary{shadows}
\usetikzlibrary{plotmarks}
-
+\setmonofont[Scale=MatchLowercase]{Consolas}
+\newfontfamily{\consolas}{Consolas}
\isabellestyle{rm}
\renewcommand{\isastyle}{\rm}%
@@ -41,7 +40,7 @@
\renewcommand{\isasymbullet}{\act}
% beamer stuff
-\renewcommand{\slidecaption}{APP 09, King's College London, 3 December 2013}
+\renewcommand{\slidecaption}{APP 09, King's College London, 10 December 2013}
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
@@ -65,7 +64,7 @@
\begin{center}
\begin{tabular}{ll}
Email: & christian.urban at kcl.ac.uk\\
- Of$\!$fice: & S1.27 (1st floor Strand Building)\\
+ Office: & S1.27 (1st floor Strand Building)\\
Slides: & KEATS (also homework is there)\\
\end{tabular}
\end{center}
@@ -77,27 +76,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
-\frametitle{Revision: Proofs}
-
-\begin{center}
-\includegraphics[scale=0.4]{pics/river-stones.jpg}
-\end{center}
-
-\begin{textblock}{5}(11.7,5)
-goal
-\end{textblock}
-
-\begin{textblock}{5}(11.7,14)
-start
-\end{textblock}
-
-\begin{textblock}{5}(0,7)
-\begin{center}
-\bl{\infer[\small\textcolor{black}{\text{axiom}}]{\quad\vdash\quad}{}}\\[8mm]
-\bl{\infer{\vdash}{\quad\vdash\quad}}\\[8mm]
-\bl{\infer{\vdash}{\quad\vdash\qquad\vdash\quad}}
-\end{center}
-\end{textblock}
+\frametitle{\mbox{}\\[20mm]\huge Revision}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -105,55 +84,380 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
-\frametitle{Proof Example Proof}
+\frametitle{1st Lecture}
+
+
+
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,t]
+\frametitle{\begin{tabular}{c}2nd Lecture:\\ E-Voting\end{tabular}}
+
+\begin{itemize}
+\item Integrity
+\item Ballot Secrecy
+\item Voter Authentication
+\item Enfranchisement
+\item Availability
+\end{itemize}
+
+
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,t]
+\frametitle{\begin{tabular}{c}2nd Lecture:\\ E-Voting\end{tabular}}
+
+Online Banking vs.~E-Voting
+
+\begin{itemize}
+\item online banking: if fraud occurred you try to identify who did what (somebody's account got zero)\bigskip
+\item e-voting: some parts can be done electronically, but not the actual voting (final year project: online voting)
+\end{itemize}
+
+
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\tikzset{alt/.code args={<#1>#2#3#4}{%
+ \alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}} % \pgfkeysalso doesn't change the path
+}}
+
+\mode<presentation>{
+\begin{frame}[t]
+\frametitle{\begin{tabular}{c}3rd Lecture:\\ Buffer Overflow Attacks\end{tabular}}
+
+\begin{itemize}
+\item the problem arises from the way C/C++ organises its function calls\\[-8mm]\mbox{}
+\end{itemize}
\begin{center}
-\bl{\infer{P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1}
- {\raisebox{2mm}{\text{\LARGE $?$}}}}
+\begin{tikzpicture}[scale=1]
+%\draw[black!10,step=2mm] (0,0) grid (9,4);
+%\draw[black!10,thick,step=10mm] (0,0) grid (9,4);
+
+\node at (0.5,4.5) {\small\begin{tabular}{l}main\\[-2mm] prog.\end{tabular}};
+\draw[line width=0mm, white, alt=<2->{fill=red}{fill=blue}] (0,2.5) rectangle (1,3.8);
+\draw[line width=0mm, white, alt=<9->{fill=red}{fill=blue}] (0,0.2) rectangle (1,0.5);
+\draw[line width=1mm, alt=<3->{fill=yellow}{fill=blue}] (0,2.0) rectangle (1,2.5);
+\draw[line width=1mm, alt=<6->{fill=red}{fill=blue}] (0,1.0) rectangle (1,2.0);
+\draw[line width=1mm, alt=<7->{fill=yellow}{fill=blue}] (0,0.5) rectangle (1,1.0);
+\draw[line width=1mm] (0,0) -- (0,4);
+\draw[line width=1mm] (1,0) -- (1,4);
+
+\node at (3.5,3.5) {\small\begin{tabular}{l}fact(n)\end{tabular}};
+\draw[line width=1mm, alt=<{4-5,8}>{fill=red}{fill=blue}] (3,1.0) rectangle (4,3.0);
+
+\onslide<3-4>{\draw[->, line width=1mm,red] (1,2.3) to node [above,sloped,midway] {n=4} (3,3);}
+\onslide<5>{\draw[<-, line width=1mm,red] (1,2.3) to node [above,sloped,midway] {res=24} (3,1);}
+
+\onslide<7-8>{\draw[->, line width=1mm,red] (1,0.8) to node [above,sloped,midway] {n=3} (3,3);}
+\onslide<9>{\draw[<-, line width=1mm,red] (1,0.8) to node [above,sloped,midway] {res=6} (3,1);}
+
+
+\node at (7.75,3.9) {\small\begin{tabular}{l}stack\end{tabular}};
+\draw[line width=1mm] (7,3.5) -- (7,0.5) -- (8.5,0.5) -- (8.5,3.5);
+
+\onslide<3,4,7,8>{
+\node at (7.75, 0.8) {ret};
+\draw[line width=1mm] (7,1.1) -- (8.5,1.1);
+}
+\onslide<3>{
+\node at (7.75, 1.4) {4};
+\draw[line width=1mm] (7,1.7) -- (8.5,1.7);
+}
+\onslide<7>{
+\node at (7.75, 1.4) {3};
+\draw[line width=1mm] (7,1.7) -- (8.5,1.7);
+}
+
+
+
+
+\end{tikzpicture}
\end{center}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+
+\begin{center}
+\begin{tikzpicture}[scale=1]
+%\draw[black!10,step=2mm] (0,0) grid (9,4);
+%\draw[black!10,thick,step=10mm] (0,0) grid (9,4);
+
+\node at (0.5,4.5) {\small\begin{tabular}{l}main\\[-2mm] prog.\end{tabular}};
+\draw[line width=0mm, white, alt=<2->{fill=red}{fill=blue}] (0,2.5) rectangle (1,3.8);
+\draw[line width=1mm, white, fill=blue] (0,1.0) rectangle (1,2.0);
+\draw[line width=1mm, alt=<3->{fill=yellow}{fill=blue}] (0,2.0) rectangle (1,2.5);
+\draw[line width=1mm] (0,0) -- (0,4);
+\draw[line width=1mm] (1,0) -- (1,4);
+
+\node at (3.5,3.5) {\small\begin{tabular}{l}fact(n)\end{tabular}};
+\draw[line width=0mm, alt=<{4-}>{red, fill=red}{blue, fill=blue}] (3,2.8) rectangle (4,3.0);
+\draw[line width=0mm, alt=<{5-}>{red, fill=red}{blue, fill=blue}] (3,2.8) rectangle (4,2.0);
+\draw[line width=0mm, alt=<{7-}>{red, fill=red}{blue, fill=blue}] (3,2.0) rectangle (4,1.0);
+\draw[line width=1mm] (3,1.0) rectangle (4,3.0);
+
+\onslide<3->{\draw[->, line width=1mm,red] (1,2.3) to node [above,sloped,midway] {n=4} (3,3);}
+\onslide<5->{\draw[<-, line width=2mm,red] (4,2) to node [above,sloped,midway]
+{\begin{tabular}{l}user\\[-1mm] input\end{tabular}} (6,2);}
+\onslide<8->{\draw[<-, line width=1mm,red] (1,-2) to (3,1);}
+
+\node at (7.75,3.9) {\small\begin{tabular}{l}stack\end{tabular}};
+\draw[line width=1mm] (7,3.5) -- (7,0.5) -- (8.5,0.5) -- (8.5,3.5);
+
+\onslide<3->{
+\draw[line width=1mm,alt=<6->{fill=red}{fill=white}] (7,0.5) rectangle (8.5,1.1);
+\node at (7.75, 0.8) {\alt<6->{@a\#}{ret}};
+\draw[line width=1mm,alt=<6->{fill=red}{fill=white}] (7,1.1) rectangle (8.5,1.7);
+\node at (7.75, 1.4) {\alt<6->{!?w;}4};
+}
+
+\onslide<4->{
+\draw[line width=1mm,fill=red] (7,1.7) rectangle (8.5,3.0);
+\node[white] at (7.75, 2.4) {buffer};
+}
+
+\end{tikzpicture}
+\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Proof Example Proof}
+\begin{frame}[t]
+\frametitle{\begin{tabular}{c}3rd Lecture:\\ Unix Access Control\end{tabular}}
-\begin{tabular}{@{\hspace{-6mm}}l}
-\begin{minipage}{1.1\textwidth}
-We have (by axiom)
+\begin{itemize}
+\item privileges are specified by file access permissions (``everything is a file'')
+\end{itemize}\medskip
\begin{center}
-\begin{tabular}{@{}ll@{}}
-(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2$}
+ \begin{tikzpicture}[scale=1]
+
+ \draw[line width=1mm] (-.3, 0) rectangle (1.5,2);
+ \draw (4.7,1) node {Internet};
+ \draw (-2.7,1.7) node {\footnotesize Application};
+ \draw (0.6,1.7) node {\footnotesize Interface};
+ \draw (0.6,-0.4) node {\footnotesize \begin{tabular}{c}unprivileged\\[-1mm] process\end{tabular}};
+ \draw (-2.7,-0.4) node {\footnotesize \begin{tabular}{c}privileged\\[-1mm] process\end{tabular}};
+
+ \draw[line width=1mm] (-1.8, 0) rectangle (-3.6,2);
+
+ \draw[white] (1.7,1) node (X) {};
+ \draw[white] (3.7,1) node (Y) {};
+ \draw[red, <->, line width = 2mm] (X) -- (Y);
+
+ \draw[red, <->, line width = 1mm] (-0.6,1) -- (-1.6,1);
+ \end{tikzpicture}
+\end{center}
+
+\begin{itemize}
+\item the idea is make the attack surface smaller and
+mitigate the consequences of an attack
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,t]
+\frametitle{\begin{tabular}{c}3rd Lecture:\\ Unix Access Control\end{tabular}}
+
+\begin{itemize}
+\item when a file with setuid is executed, the resulting process will assume the
+UID given to the owner of the file
+\end{itemize}
+
+\small\tt
+\begin{center}
+\begin{verbatim}
+$ ls -ld . * */*
+drwxr-xr-x 1 ping staff 32768 Apr 2 2010 .
+-rw----r-- 1 ping students 31359 Jul 24 2011 manual.txt
+-r--rw--w- 1 bob students 4359 Jul 24 2011 report.txt
+-rwsr--r-x 1 bob students 141359 Jun 1 2013 microedit
+dr--r-xr-x 1 bob staff 32768 Jul 23 2011 src
+-rw-r--r-- 1 bob staff 81359 Feb 28 2012 src/code.c
+-r--rw---- 1 emma students 959 Jan 23 2012 src/code.h
+\end{verbatim}
+\end{center}
+
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,t]
+\frametitle{\begin{tabular}{c}4th Lecture:\\ Security Levels\end{tabular}}
+
+Bell-LaPadula access model:
+
+ \begin{itemize}
+ \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if
+ \bl{$P$}'s security level is at least as high as \bl{$O$}'s.
+ \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if
+ \bl{$O$}'s security level is at least as high as \bl{$P$}'s.\medskip
+
+ \item Meta-Rule: All principals in a system should have a sufficiently high security level
+ in order to access an object.
+ \end{itemize}\bigskip
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,t]
+\frametitle{\begin{tabular}{c}4th Lecture:\\ Security Levels\end{tabular}}
+
+Biba (data integrity)
+
+ \begin{itemize}
+ \item Biba: {\bf `no read down'} - {\bf `no write up'}
+ \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if
+ \bl{$P$}'s security level is lower or equal than \bl{$O$}'s.
+ \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if
+ \bl{$O$}'s security level is lower or equal than \bl{$P$}'s.
+ \end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,t]
+\frametitle{\begin{tabular}{c}4th Lecture:\\ Protocols\end{tabular}}
+
+A mutual authentication protocol
+
+\begin{center}
+\begin{tabular}{ll}
+\bl{$A \rightarrow B$:} & \bl{$N_a$}\\
+\bl{$B \rightarrow A$:} & \bl{$\{N_a, N_b\}_{K_{ab}}$}\\
+\bl{$A \rightarrow B$:} & \bl{$N_b$}\\
\end{tabular}
\end{center}
-From (1) we get
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,t]
+\frametitle{\begin{tabular}{c}5th Lecture:\\ Access Control Logic\end{tabular}}
+
+
+\begin{itemize}
+\item formulas
+\item judgements
+\end{itemize}\pause
\begin{center}
-\begin{tabular}{@{}ll@{}}
-(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
-(3) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
-\end{tabular}
+ \begin{tikzpicture}[scale=1]
+
+ \draw[line width=1mm] (-.3, 0) rectangle (1.5,2);
+ \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}};
+ \draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}};
+ \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}};
+
+ \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1);
+ \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1);
+ \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2);
+
+ \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}};
+
+ \end{tikzpicture}
\end{center}
-From (3) and (2) we get
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,t]
+\frametitle{\begin{tabular}{c}5th Lecture:\\ Access Control Logic\end{tabular}}
\begin{center}
-\begin{tabular}{@{}ll@{}}
-\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}
-\end{tabular}
+\begin{tikzpicture}[scale=1]
+
+ \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}};
+ \onslide<1->{
+ \draw (-1,-0.3) node (X) {};
+ \draw (-2.0,-2.0) node (Y) {};
+ \draw (0.7,-3) node {\begin{tabular}{l}Gamma\\stands for a collection of formulas\\(``assumptions'')\end{tabular}};
+ \draw[red, ->, line width = 2mm] (Y) -- (X);
+
+ \draw (1.2,-0.1) node (X1) {};
+ \draw (2.8,-0.1) node (Y1) {};
+ \draw (4.5,-0.1) node {\begin{tabular}{l}a single formula\end{tabular}};
+ \draw[red, ->, line width = 2mm] (Y1) -- (X1);
+
+ \draw (-0.1,0.1) node (X2) {};
+ \draw (0.5,1.5) node (Y2) {};
+ \draw (1,1.8) node {\begin{tabular}{l}entails sign\end{tabular}};
+ \draw[red, ->, line width = 2mm] (Y2) -- (X2);}
+
+ \end{tikzpicture}
\end{center}
-Done.
-\end{minipage}
-\end{tabular}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{\begin{tabular}{c}5th Lecture:\\ Inference Rules\end{tabular}}
+
+
+\begin{center}
+\begin{tikzpicture}[scale=1]
+
+ \draw (0.0,0.0) node
+ {\Large\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}};
+
+ \draw (-0.1,-0.7) node (X) {};
+ \draw (-0.1,-1.9) node (Y) {};
+ \draw (-0.2,-2) node {\begin{tabular}{l}conclusion\end{tabular}};
+ \draw[red, ->, line width = 2mm] (Y) -- (X);
+
+ \draw (-1,0.6) node (X2) {};
+ \draw (0.0,1.6) node (Y2) {};
+ \draw (0,1.8) node {\begin{tabular}{l}premisses\end{tabular}};
+ \draw[red, ->, line width = 2mm] (Y2) -- (X2);
+ \draw (1,0.6) node (X3) {};
+ \draw (0.0,1.6) node (Y3) {};
+ \draw[red, ->, line width = 2mm] (Y3) -- (X3);
+ \end{tikzpicture}
+\end{center}
+
\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{\begin{tabular}{c}6th Lecture:\\ Privacy\end{tabular}}
+
+
+
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
\end{document}