diff -r 1c3d38cc34a9 -r b1272782f902 slides/slides09.tex
--- 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}