sen-material: comparison slides/slides09.tex

equal deleted inserted replaced

-:b1272782f902
+:73e6076b9225
 \begin{textblock}{0}(2.5,13)%
 \small
 \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}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \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$};
 \node at (2.0,0.9) {\small $B_L$};
 \node at (3.5,0.9) {\small $A_R$};
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \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}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \node[black, rotate=10] at (1.9,3.6) {\LARGE\ldots};
 }
 \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}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \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
 \item about CompCert:
 \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''!
+it is helpful to know what you mean by ``works'' and by ``is secure''!
 \end{itemize}
 \end{frame}
 Remember the Bridges example?
 \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
 \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}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 | \meta{Exp} = \meta{Exp}
 | \meta{num}
 | \meta{var}\\
 : \meta{Stmt} ::= \meta{label} :
 | \meta{var} := \meta{Exp}
-| jmp? \meta{Exp} \meta{label}
+| \pcode{jmp?} \meta{Exp} \meta{label}
-| goto \meta{label}\\
+| \pcode{goto} \meta{label}\\
-: \meta{Prog} ::= \meta{Stmt} \ldots \meta{Stmt}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
 \end{plstx}}
 \begin{textblock}{0}(7.8,2.5)
 \small
 \begin{bubble}[5.6cm]
 | \meta{Exp} = \meta{Exp}
 | \meta{num}
 | \meta{var}\\
 : \meta{Stmt} ::= \meta{label} :
 | \meta{var} := \meta{Exp}
-| jmp? \meta{Exp} \meta{label}
+| \pcode{jmp?} \meta{Exp} \meta{label}
-| goto \meta{label}\\
+| \pcode{goto} \meta{label}\\
-: \meta{Prog} ::= \meta{Stmt} \ldots \meta{Stmt}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
 \end{plstx}}
 \begin{textblock}{0}(7.8,3.5)
 \small
 \begin{bubble}[5.6cm]
 | \meta{Exp} = \meta{Exp}
 | \meta{num}
 | \meta{var}\\
 : \meta{Stmt} ::= \meta{label} :
 | \meta{var} := \meta{Exp}
-| jmp? \meta{Exp} \meta{label}
+| \pcode{jmp?} \meta{Exp} \meta{label}
-| goto \meta{label}\\
+| \pcode{goto} \meta{label}\\
-: \meta{Prog} ::= \meta{Stmt} \ldots \meta{Stmt}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
 \end{plstx}}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[fragile]
-\frametitle{Eval}
+\frametitle{Eval: An Interpreter}
 \mbox{}\\[-14mm]\mbox{}
 \small
 \begin{center}
 \bl{\begin{tabular}{lcl}
 goto top
 done:
 \end{lstlisting}
 \end{bubble}
-Some snippets
+The \emph{snippets} of the program:
 \footnotesize
 \begin{columns}
 \begin{column}[t]{5cm}
 \begin{bubble}[4.5cm]
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[fragile]
-\frametitle{The Idea}
+\frametitle{The Idea of Static Analysis}
 \small
 \mbox{}\bigskip\\
 \begin{columns}
 \begin{column}{5cm}
 \mbox{}\\[-13mm]\mbox{}
 \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)$\\
+$[x]_{aenv}$ & $\dn$ & $aenv(x)$\\
-$[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} \oplus [e_2]_{env}$\\
+$[e_1 + e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \oplus [e_2]_{aenv}$\\
-$[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} \otimes [e_2]_{env}$\\
+$[e_1 * e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \otimes [e_2]_{aenv}$\\
-$[e_1 = e_2]_{env}$ & $\dn$ & $\{0, +\}$\\
+$[e_1 = e_2]_{aenv}$ & $\dn$ & $\{0, +\}$\\
 \end{tabular}}
 \end{center}
 \scriptsize
 \begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]
 \end{lstlisting}
 \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}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \frametitle{Sign Analysis}
 \begin{itemize}
 \item We want to find out whether \texttt{a} and \texttt{n}
 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
 \end{itemize}\bigskip
 \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}

changeset 434	73e6076b9225
parent 433	b1272782f902
child 518	e1fcfba63a31