--- a/slides/slides09.tex Mon Nov 16 13:35:30 2015 +0000
+++ b/slides/slides09.tex Thu Nov 19 03:27:04 2015 +0000
@@ -72,6 +72,27 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Trusting Computing Base}
+
+When considering whether a system meets some security
+objectives, it is important to consider which parts of that
+system are trusted in order to meet that objective (TCB).
+\bigskip\pause
+
+The smaller the TCB, the less effort it takes to get
+some confidence that it is trustworthy, by doing a code
+review or by performing some (penetration) testing.
+\bigskip
+
+\footnotesize
+CPU, compiler, libraries, OS, NP $\not=$ P,
+random number generator, \ldots
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Dijkstra on Testing}
@@ -84,11 +105,6 @@
unfortunately attackers exploit bugs (Satan's computer vs
Murphy's)
- \vfill
- \small
- Dijkstra: shortest path algorithm,
- dining philosophers problem,
- semaphores
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -110,14 +126,14 @@
\begin{bubble}[10cm]
\small
{\bf Theorem:} The program is doing what
-it is sup+ed to be doing.\medskip
+it is supposed to be doing.\medskip
{\bf Long, long proof} \ldots\\
\end{bubble}\bigskip\medskip
\small This can be a gigantic proof. The only hope is to have
help from the computer. `Program' is here to be understood to be
-quite general (protocol, OS,\ldots).
+quite general (protocols, OS, \ldots).
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -597,6 +613,24 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
+
+ \begin{center}
+ \includegraphics[scale=0.25]{../pics/p4.jpg}
+ \end{center}
+
+ \begin{itemize}
+ \item by Silberschatz, Galvin, and Gagne, 2013 (OS-bible)
+ \item \it ``Upon releasing the lock, the
+ $[$low-priority$]$ thread will revert to
+ its original priority.''
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
\frametitle{Priority Scheduling}
\begin{itemize}
@@ -681,35 +715,13 @@
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \begin{frame}[c]
- \frametitle{A Sound and Complete Test}
-
- \begin{itemize}
- \item working purely in the \emph{dynamic world} does not work -\!-\!- infinite state space\bigskip
-
- \item working purely on \emph{static} policies also does not\\ work -\!-\!- because of over approximation
- \smallskip
- \begin{itemize}
- \item sup+e a tainted file has type \emph{bin} and
- \item there is a role \bl{$r$} which can both read and write \emph{bin}-files\pause
- \item then we would conclude that this tainted file can spread\medskip\pause
- \item but if there is no process with role \bl{$r$} and it will never been
- created, then the file actually does not spread
- \end{itemize}\bigskip\pause
-
- \item \alert{our solution:} take a middle ground and record precisely the information
- of the initial state, but be less precise about every newly created object.
- \end{itemize}
-
- \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
-\frametitle{Big Proofs in CS}
+\frametitle{Big Proofs in CS (1)}
-Formal proofs in CS sound like science fiction? Completely irrelevant!
-Lecturer gone mad?\pause
+Formal proofs in CS sound like science fiction? Completely
+irrelevant! Lecturer gone mad?\pause
\begin{itemize}
\item in 2008, verification of a small C-compiler
@@ -717,16 +729,98 @@
\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''
\item is as good as \texttt{gcc -O1}, but much less buggy
\end{itemize}
-\medskip
-\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)
+\end{itemize}
+
+\begin{center}
+ \includegraphics[scale=0.12]{../pics/compcert.png}
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Fuzzy Testing C-Compilers}
+
\begin{itemize}
-\item 200k loc of proof
-\item 25 - 30 person years
-\item found 160 bugs in the C code (144 by the proof)
-\end{itemize}
+\item tested GCC, LLVM, others by randomly generating
+C-programs
+\item found more than 300 bugs in GCC and also
+many in LLVM (some of them highest-level critical)\bigskip
+\item about CompCert:
+
+\begin{bubble}[10cm]\small ``The striking thing about our CompCert
+results is that the middle-end bugs we found in all other
+compilers are absent. As of early 2011, the under-development
+version of CompCert is the only compiler we have tested for
+which Csmith cannot find wrong-code errors. This is not for
+lack of trying: we have devoted about six CPU-years to the
+task.''
+\end{bubble}
\end{itemize}
\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Big Proofs in CS (2)}
+
+\begin{itemize}
+\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)
+ \begin{itemize}
+ \item used in helicopters and mobile phones
+ \item 200k loc of proof
+ \item 25 - 30 person years
+ \item found 160 bugs in the C code (144 by the proof)
+ \end{itemize}
+\end{itemize}
+
+\begin{bubble}[10cm]\small
+``Real-world operating-system kernel with an end-to-end proof
+of implementation correctness and security enforcement''
+\end{bubble}\bigskip\pause
+
+unhackable kernel (New Scientists, September 2015)
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Big Proofs in CS (3)}
+
+\begin{itemize}
+\item verified TLS implementation\medskip
+\item verified compilers (CompCert, CakeML)\medskip
+\item verified distributed systems (Verdi)\medskip
+\item verified OSes or OS components\\
+(seL4, CertiKOS, Ironclad Apps, \ldots)\medskip
+\item verified cryptography
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{How Did This Happen?}
+
+Lots of ways!
+
+\begin{itemize}
+\item better programming languages
+ \begin{itemize}
+ \item basic safety guarantees built in
\item powerful mechanisms for abstraction and modularity
+ \end{itemize}
+\item better software development methodology
+\item stable platforms and frameworks
+\item better use of specifications\medskip\\
+ \small If you want to build software that works or is secure,
+ it is helpful to know what you mean by ``work'' and by ``secure''!
+\end{itemize}
+
+\end{frame}
+
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
@@ -736,15 +830,15 @@
\begin{itemize}
\item Can we look at our programs and somehow ensure
-they are secure/bug free/correct?\pause\bigskip
+they are secure/bug free/correct/secure?\pause\bigskip
\item Very hard: Anything interesting about programs is equivalent
to halting problem, which is undecidable.\pause\bigskip
\item \alert{Solution:} We avoid this ``minor'' obstacle by
- being as close as +sible of deciding the halting
+ being as close as possible of deciding the halting
problem, without actually deciding the halting problem.
- $\quad\Rightarrow$ static analysis
+ \small$\quad\Rightarrow$ yes, no, do not know (static analysis)
\end{itemize}
\end{frame}
@@ -825,10 +919,13 @@
\begin{center}
\includegraphics[scale=0.4]{../pics/state6.png}
\end{center}
+
+ for example no key is leaked
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{\large Concrete Example: Sign-Analysis}
@@ -843,27 +940,7 @@
| \meta{var} := \meta{Exp}
| jmp? \meta{Exp} \meta{label}
| goto \meta{label}\\
-: \meta{Prog} ::= \meta{Stmt} \ldots\\
-\end{plstx}}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[fragile]
-\frametitle{\large Concrete Example: Sign-Analysis}
-\mbox{}\\[-20mm]\mbox{}
-
-\bl{\begin{plstx}[rhs style=,one per line]
: \meta{Exp} ::= \meta{Exp} + \meta{Exp}
- | \meta{Exp} * \meta{Exp}
- | \meta{Exp} = \meta{Exp}
- | \meta{num}
- | \meta{var}\\
-: \meta{Stmt} ::= \meta{label} :
- | \meta{var} := \meta{Exp}
- | jmp? \meta{Exp} \meta{label}
- | goto \meta{label}\\
-: \meta{Prog} ::= \meta{Stmt} \ldots\\
+: \meta{Prog} ::= \meta{Stmt} \ldots \meta{Stmt}\\
\end{plstx}}
\begin{textblock}{0}(7.8,2.5)
@@ -900,7 +977,7 @@
| \meta{var} := \meta{Exp}
| jmp? \meta{Exp} \meta{label}
| goto \meta{label}\\
-: \meta{Prog} ::= \meta{Stmt} \ldots\\
+: \meta{Prog} ::= \meta{Stmt} \ldots \meta{Stmt}\\
\end{plstx}}
\begin{textblock}{0}(7.8,3.5)
@@ -928,8 +1005,29 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
+\frametitle{\large Concrete Example: Sign-Analysis}
+\mbox{}\\[-20mm]\mbox{}
+
+\bl{\begin{plstx}[rhs style=,one per line]
: \meta{Exp} ::= \meta{Exp} + \meta{Exp}
+ | \meta{Exp} * \meta{Exp}
+ | \meta{Exp} = \meta{Exp}
+ | \meta{num}
+ | \meta{var}\\
+: \meta{Stmt} ::= \meta{label} :
+ | \meta{var} := \meta{Exp}
+ | jmp? \meta{Exp} \meta{label}
+ | goto \meta{label}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots \meta{Stmt}\\
+\end{plstx}}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
\frametitle{Eval}
-\mbox{}\\[-18mm]\mbox{}
+\mbox{}\\[-14mm]\mbox{}
\small
\begin{center}