diff -r b1272782f902 -r 73e6076b9225 slides/slides09.tex
--- a/slides/slides09.tex	Thu Nov 19 03:27:04 2015 +0000
+++ b/slides/slides09.tex	Thu Nov 19 20:59:24 2015 +0000
@@ -296,7 +296,7 @@
   \onslide<3->{
   \begin{bubble}[8cm]%
   Scheduling: You want to avoid that a high 
-  priority process is staved indefinitely.
+  priority process is starved indefinitely.
   \end{bubble}}
   \end{textblock}
 
@@ -321,15 +321,12 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \begin{frame}[c]
   
-
   \begin{textblock}{11}(1,3)
   \begin{tabular}{@{\hspace{-10mm}}l}
   \begin{tikzpicture}[scale=1.1]
   \node at (-2.5,-1.5) {\textcolor{white}{a}};
   \node at (8,4) {\textcolor{white}{a}};
   
-    
-
   \only<1>{
     \draw[fill, blue!50] (1,0) rectangle (6,0.6);
     \node at (1.5,0.9) {\small $A_L$};
@@ -651,12 +648,15 @@
   \begin{frame}[c]
   \frametitle{Design of AC-Policies}
 
+  Imagine you set up an access policy (root, lpd, users, staff, etc)
+  \bigskip\pause
+
   \Large
   \begin{quote}
-  ''what you specify is what you get but not necessarily what you want\ldots''
+  ``what you specify is what you get but not necessarily what you want\ldots''
   \end{quote}\bigskip\bigskip\bigskip
   
-  \normalsize main work by Chunhan Wu (PhD-student)
+  \normalsize main work by Chunhan Wu (a PhD-student in Nanjing)
 
   \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -711,6 +711,12 @@
 
   \end{tikzpicture}
   \end{center}
+  
+  \only<7->{
+  \begin{textblock}{4}(1,12)
+  \small
+  reduced the problem to a finite problem; gave a proof
+  \end{textblock}} 
 
   \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
@@ -743,7 +749,7 @@
 \frametitle{Fuzzy Testing C-Compilers}
 
 \begin{itemize}
-\item tested GCC, LLVM, others by randomly generating 
+\item tested GCC, LLVM and 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
@@ -815,7 +821,7 @@
 \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''!
+    it is helpful to know what you mean by ``works'' and by ``is secure''!
 \end{itemize}
 
 \end{frame}
@@ -830,7 +836,7 @@
 
 \begin{itemize}
 \item Can we look at our programs and somehow ensure
-they are secure/bug free/correct/secure?\pause\bigskip
+they are secure/bug free/correct?\pause\bigskip
 
 \item Very hard: Anything interesting about programs is equivalent
 to halting problem, which is undecidable.\pause\bigskip
@@ -838,7 +844,7 @@
 \item \alert{Solution:} We avoid this ``minor'' obstacle by
       being as close as possible of deciding the halting
       problem, without actually deciding the halting problem.
-      \small$\quad\Rightarrow$ yes, no, do not know (static analysis)
+      \small$\quad\Rightarrow$ yes, no, don't know (static analysis)
 \end{itemize}
 
 \end{frame}
@@ -938,9 +944,9 @@
          | \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}\\
+         | \pcode{jmp?} \meta{Exp} \meta{label}
+         | \pcode{goto} \meta{label}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
 \end{plstx}}
 
 \begin{textblock}{0}(7.8,2.5)
@@ -975,9 +981,9 @@
          | \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}\\
+         | \pcode{jmp?} \meta{Exp} \meta{label}
+         | \pcode{goto} \meta{label}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
 \end{plstx}}
 
 \begin{textblock}{0}(7.8,3.5)
@@ -1015,9 +1021,9 @@
          | \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}\\
+         | \pcode{jmp?} \meta{Exp} \meta{label}
+         | \pcode{goto} \meta{label}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
 \end{plstx}}
 
 \end{frame}
@@ -1026,7 +1032,7 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[fragile]
-\frametitle{Eval}
+\frametitle{Eval: An Interpreter}
 \mbox{}\\[-14mm]\mbox{}
 
 \small
@@ -1079,7 +1085,7 @@
 \end{lstlisting}
 \end{bubble}
 
-Some snippets
+The \emph{snippets} of the program:
 
 \footnotesize
 \begin{columns}
@@ -1182,7 +1188,7 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[fragile]
-\frametitle{The Idea}
+\frametitle{The Idea of Static Analysis}
 \small
 \mbox{}\bigskip\\
 
@@ -1277,16 +1283,16 @@
 \small
 \begin{center}
 \bl{\begin{tabular}{lcl}
-$[n]_{env}$ & $\dn$ & 
+$[n]_{aenv}$ & $\dn$ & 
 $\begin{cases}
 \{+\} & \text{if}\; n > 0\\
 \{-\} & \text{if}\; n < 0\\
 \{0\} & \text{if}\; n = 0
 \end{cases}$\\
-$[x]_{env}$ & $\dn$ & $env(x)$\\
-$[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} \oplus [e_2]_{env}$\\
-$[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} \otimes [e_2]_{env}$\\
-$[e_1 = e_2]_{env}$ & $\dn$ & $\{0, +\}$\\
+$[x]_{aenv}$ & $\dn$ & $aenv(x)$\\
+$[e_1 + e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \oplus [e_2]_{aenv}$\\
+$[e_1 * e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \otimes [e_2]_{aenv}$\\
+$[e_1 = e_2]_{aenv}$ & $\dn$ & $\{0, +\}$\\
 \end{tabular}}
 \end{center}
 
@@ -1308,6 +1314,33 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{AEval for Stmts}
+\mbox{}\\[-12mm]\mbox{}
+
+Let \bl{$sn$} be the snippets of a program
+
+\small
+\begin{center}
+\bl{\begin{tabular}{lcl}
+$[\texttt{nil}]_{aenv}$ & $\to$ & $(\texttt{nil},aenv)$\medskip\\
+$[\texttt{Label}(l:)::rest]_{aenv}$ & $\to$ & $(rest, aenv)$\medskip\\
+$[x \,\texttt{:=}\, e::rest]_{aenv}$ & $\to$ & 
+$(rest, aenv[x:= [e]_{aenv}])$\medskip\\
+$[\texttt{jmp?}\;e\;l::rest]_{aenv}$ & $\to$ & 
+$(sn(l),aenv)$ \textcolor{black}{and} $(rest, aenv)$\medskip\\
+$[\texttt{goto}\;l::rest]_{aenv}$ & $\to$ & $(sn(l), aenv)$\\
+\end{tabular}}
+\end{center}\bigskip
+
+Start with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}, try to 
+reach all \emph{states} you can find (until a fix point is reached).
+
+Check whether there are only $aenv$ in the final states that have 
+your property.
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1319,7 +1352,7 @@
   are always positive?\medskip
   \item After a few optimisations, we can indeed find this out.
   \begin{itemize}
-  \item \texttt{if} returns \texttt{+} or \texttt{0}
+  \item \texttt{equations} return \texttt{+} or \texttt{0}
   \item branch into only one dircection if you know
   \item if $x$ is \texttt{+}, then $x + \texttt{-1}$ 
   cannot be negative 
@@ -1327,12 +1360,28 @@
   
   \item What is this good for? Well, you do not need 
   underflow checks (in order to prevent buffer-overflow
-  attacks).
+  attacks). In general this technique is used to make sure 
+  keys stay secret.
   \end{itemize}
   
   \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
+  \frametitle{Take Home Points}
+
+  \begin{itemize}
+  \item While testing is important, it does not show the 
+    absence of bugs/vulnerabilities.\medskip
+  \item More and more we need (formal) proofs that show
+    a program is bug free.
+  \end{itemize}
+  
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
 
 \end{document}