--- 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}