diff -r f8dc3dbdaa5c -r 0c62ec6dc691 slides/slides10.tex --- 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{ \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{ \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{ +\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{ +\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{ -\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{ +\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{ +\begin{frame}[c] +\frametitle{\begin{tabular}{c}6th Lecture:\\ Privacy\end{tabular}} + + + + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \end{document}