\documentclass[dvipsnames,14pt,t]{beamer}\usepackage{../slides}\usepackage{../langs}\usepackage{../graphics}\usepackage{../grammar}\usepackage{soul}% beamer stuff \renewcommand{\slidecaption}{SEN 09, King's College London}\newcommand{\bl}[1]{\textcolor{blue}{#1}}\begin{document}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[t]\frametitle{% \begin{tabular}{@ {}c@ {}} \\ \LARGE Security Engineering (9)\\[-3mm] \end{tabular}}\bigskip\bigskip\bigskip \normalsize \begin{center} \begin{tabular}{ll} Email: & christian.urban at kcl.ac.uk\\ Office: & S1.27 (1st floor Strand Building)\\ Slides: & KEATS (also homework is there)\\ \end{tabular} \end{center}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \begin{center} \includegraphics[scale=0.6]{../pics/bridge-limits.png} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{Old-Fashioned Eng.~vs.~CS} \begin{center} \begin{tabular}{@{}cc@{}} \begin{tabular}{@{}p{5.2cm}} \includegraphics[scale=0.058]{../pics/towerbridge.jpg}\\ {\bf bridges}: \\ \raggedright\small engineers can ``look'' at a bridge and have a pretty good intuition about whether it will hold up or not\\ (redundancy; predictive theory) \end{tabular} & \begin{tabular}{p{5cm}} \includegraphics[scale=0.265]{../pics/code.jpg}\\ \raggedright {\bf code}: \\ \raggedright\small programmers have very little intuition about their code; often it is too expensive to have redundancy; not ``continuous'' \end{tabular} \end{tabular} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c]\frametitle{Trusting Computing Base}When considering whether a system meets some securityobjectives, it is important to consider which parts of thatsystem are trusted in order to meet that objective (TCB).\bigskip\pauseThe smaller the TCB, the less effort it takes to getsome confidence that it is trustworthy, by doing a code review or by performing some (penetration) testing.\bigskip\footnotesizeCPU, compiler, libraries, OS, NP $\not=$ P,random number generator, \ldots\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{Dijkstra on Testing} \begin{bubble}[10cm] ``Program testing can be a very effective way to show the presence of bugs, but it is hopelessly inadequate for showing their absence.'' \end{bubble}\bigskip unfortunately attackers exploit bugs (Satan's computer vs Murphy's) \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c]\frametitle{\Large Proving Programs to be Correct}\begin{bubble}[10cm]\small{\bf Theorem:} There are infinitely many prime numbers.\medskip\\{\bf Proof} \ldots\\\end{bubble}\bigskipsimilarly\bigskip\begin{bubble}[10cm]\small{\bf Theorem:} The program is doing what 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 havehelp from the computer. `Program' is here to be understood to bequite general (protocols, OS, \ldots).\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{\Large{}Mars Pathfinder Mission 1997} \begin{center} \includegraphics[scale=0.15]{../pics/marspath1.png} \includegraphics[scale=0.16]{../pics/marspath3.png} \includegraphics[scale=0.3]{../pics/marsrover.png} \end{center} \begin{itemize} \item despite NASA's famous testing procedures, the lander crashed frequently on Mars \item a scheduling algorithm was not used in the OS \end{itemize} \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 (3,0.6); } \only<2>{ \draw[fill, blue!50] (1,0) rectangle (2,0.6); \draw[fill, blue!50] (3,0) rectangle (5,0.6); \draw[fill, blue!100] (2,3) rectangle (3,3.6); } \only<3>{ \draw[fill, blue!50] (1,0) rectangle (2,0.6); \draw[fill, blue!50] (3,0) rectangle (4.5,0.6); \draw[fill, blue!50] (5.5,0) rectangle (6,0.6); \draw[fill, blue!100] (2,3) rectangle (3,3.6); \draw[fill, blue!100] (4.5,3) rectangle (5.5,3.6); } \only<4>{ \node at (2.5,0.9) {\small locked a resource}; \draw[fill, blue!50] (1,0) rectangle (2,0.6); \draw[blue!50, very thick] (2,0) rectangle (4,0.6); \draw[blue!100, very thick] (2,3) rectangle (3, 3.6); \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1); } \only<5>{ \node at (2.5,0.9) {\small locked a resource}; \draw[fill, blue!50] (1,0) rectangle (4,0.6); \draw[blue!100, fill] (4,3) rectangle (5, 3.6); } \only<6>{ \node at (2.5,0.9) {\small locked a resource}; \draw[fill, blue!50] (1,0) rectangle (2,0.6); \draw[blue!50, very thick] (2,0) rectangle (4,0.6); \draw[blue!100, very thick] (2,3) rectangle (3, 3.6); \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1); } \only<7>{ \node at (2.5,0.9) {\small locked a resource}; \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6); \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6); \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1); } \only<8>{ \node at (2.5,0.9) {\small locked a resource}; \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6); \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6); \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6); \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1); } \only<9>{ \node at (2.5,0.9) {\small locked a resource}; \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6); \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6); \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1); } \only<10>{ \node at (2.5,0.9) {\small locked a resource}; \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6); \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6); \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1); \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1); } \only<11>{ \node at (2.5,0.9) {\small locked a resource}; \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); \draw[blue!50, very thick] (4.5,0) rectangle (6,0.6); \draw[blue!100, very thick] (4.5,3) rectangle (5.5, 3.6); \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1); \draw[red, <-, line width = 2mm] (4.5,-0.1) -- (4.5, -1); } \only<12>{ \node at (2.5,0.9) {\small locked a resource}; \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); \draw[blue!50, very thick] (5.5,0) rectangle (7,0.6); \draw[blue!100, very thick] (5.5,3) rectangle (6.5, 3.6); \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1); \draw[red, fill] (4.55,1.5) rectangle (5.5,2.1); \draw[red, <-, line width = 2mm] (5.5,-0.1) -- (5.5, -1); \node [anchor=base] at (6.3, 1.8) {\Large\ldots}; } \only<13>{ \node at (2.5,0.9) {\small locked a resource}; \draw[fill, blue!50] (1,0) rectangle (2,0.6); \draw[blue!50, very thick] (2,0) rectangle (4,0.6); \draw[blue!100, very thick] (2,3) rectangle (3, 3.6); \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1); } \only<14>{ \node at (2.5,3.9) {\small locked a resource}; \draw[fill, blue!50] (1,0) rectangle (2,0.6); \draw[blue!50, fill] (2,3) rectangle (4,3.6); \draw[blue!100, very thick] (4,3) rectangle (5, 3.6); \draw[blue!50, ->, line width = 2mm] (2,1) -- (2, 2.5); \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1); } \only<15>{ \node at (2.5,3.9) {\small locked a resource}; \draw[fill, blue!50] (1,0) rectangle (2,0.6); \draw[blue!50, fill] (2,3) rectangle (4,3.6); \draw[blue!100, very thick] (4,3) rectangle (5, 3.6); \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1); \draw[red, very thick] (2.5,1.5) rectangle (3.5,2.1); } \draw[very thick,->](0,0) -- (8,0); \node [anchor=base] at (8, -0.3) {\scriptsize time}; \node [anchor=base] at (0, -0.3) {\scriptsize 0}; \node [anchor=base] at (-1.2, 0.2) {\small low priority}; \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};} \only<8->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};} \end{tikzpicture} \end{tabular} \end{textblock} \begin{textblock}{0}(2.5,13)% \small \onslide<3->{ \begin{bubble}[8cm]% Scheduling: You want to avoid that a high priority process is starved indefinitely. \end{bubble}} \end{textblock} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{\Large Priority Inheritance Scheduling} \begin{itemize} \item Let a low priority process $L$ temporarily inherit the high priority of $H$ until $L$ leaves the critical section unlocking the resource.\bigskip \item Once the resource is unlocked $L$ returns to its original priority level. \end{itemize} \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$}; \node at (5.7,0.9) {\small $B_R$}; \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6); \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); } \only<2>{ \draw[fill, blue!50] (1,0) rectangle (3,0.6); \draw[very thick, blue!50] (3,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$}; \node at (5.7,0.9) {\small $B_R$}; \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6); \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); } \only<3>{ \draw[fill, blue!50] (1,0) rectangle (3,0.6); \draw[very thick, blue!50] (3,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$}; \node at (5.7,0.9) {\small $B_R$}; \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6); \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); \draw[very thick,blue!100] (3,3) rectangle (4,3.6); \node at (3.5,3.3) {\small $A$}; } \only<4>{ \draw[fill, blue!50] (1,0) rectangle (3,0.6); \draw[very thick, blue!50] (3,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$}; \node at (5.7,0.9) {\small $B_R$}; \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6); \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); \draw[very thick,blue!100] (3,3) rectangle (4,3.6); \node at (3.5,3.3) {\small $A$}; \draw[very thick,blue!100] (4,3) rectangle (5,3.6); \node at (4.5,3.3) {\small $B$}; } \only<5>{ \draw[fill, blue!50] (1,0) rectangle (3,0.6); \draw[very thick, blue!50] (3,3) rectangle (6,3.6); \node at (1.5,0.9) {\small $A_L$}; \node at (2.0,0.9) {\small $B_L$}; \node at (3.5,3.9) {\small $A_R$}; \node at (5.7,3.9) {\small $B_R$}; \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6); \draw[very thick,blue!100] (6,3) rectangle (7,3.6); \node at (6.5,3.3) {\small $A$}; \draw[very thick,blue!100] (7,3) rectangle (8,3.6); \node at (7.5,3.3) {\small $B$}; \draw[blue!50, ->, line width = 2mm] (3,1) -- (3, 2.5); } \only<6>{ \draw[fill, blue!50] (1,0) rectangle (3,0.6); \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); \draw[very thick, blue!50] (3.5,3) rectangle (6,3.6); \node at (1.5,0.9) {\small $A_L$}; \node at (2.0,0.9) {\small $B_L$}; \node at (3.5,3.9) {\small $A_R$}; \node at (5.7,3.9) {\small $B_R$}; \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6); \draw[very thick,blue!100] (6,3) rectangle (7,3.6); \node at (6.5,3.3) {\small $A$}; \draw[very thick,blue!100] (7,3) rectangle (8,3.6); \node at (7.5,3.3) {\small $B$}; } \only<7>{ \draw[fill, blue!50] (1,0) rectangle (3,0.6); \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); \draw[very thick, blue!50] (3.5,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,3.9) {\small $A_R$}; \node at (5.7,0.9) {\small $B_R$}; \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); \draw[very thick,blue!100] (6,3) rectangle (7,3.6); \node at (6.5,3.3) {\small $A$}; \draw[very thick,blue!100] (7,3) rectangle (8,3.6); \node at (7.5,3.3) {\small $B$}; \draw[blue!50, <-, line width = 2mm] (3.5,1) -- (3.5, 2.5); \draw[blue!50, <-, line width = 2mm] (4,3.3) -- (5.5,3.3); } \only<8>{ \draw[fill, blue!50] (1,0) rectangle (3,0.6); \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); \draw[very thick, blue!50] (4.5,0) rectangle (7,0.6); \node at (1.5,0.9) {\small $A_L$}; \node at (2.0,0.9) {\small $B_L$}; \node at (3.5,3.9) {\small $A_R$}; \node at (6.7,0.9) {\small $B_R$}; \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6); \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6); \node at (4,3.3) {\small $A$}; \draw[very thick,blue!100] (7,3) rectangle (8,3.6); \node at (7.5,3.3) {\small $B$}; } \only<9>{ \draw[fill, blue!50] (1,0) rectangle (3,0.6); \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); \draw[fill, blue!50] (4.5,0) rectangle (5,0.6); \draw[very thick, blue!50] (5,0) rectangle (7,0.6); \node at (1.5,0.9) {\small $A_L$}; \node at (2.0,0.9) {\small $B_L$}; \node at (3.5,3.9) {\small $A_R$}; \node at (6.7,0.9) {\small $B_R$}; \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6); \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6); \node at (4,3.3) {\small $A$}; \draw[very thick,blue!100] (7,3) rectangle (8,3.6); \node at (7.5,3.3) {\small $B$}; } \only<10>{ \draw[fill, blue!50] (1,0) rectangle (3,0.6); \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); \draw[fill, blue!50] (4.5,0) rectangle (5,0.6); \draw[very thick, blue!50] (5,0) rectangle (7,0.6); \node at (1.5,0.9) {\small $A_L$}; \node at (2.0,0.9) {\small $B_L$}; \node at (3.5,3.9) {\small $A_R$}; \node at (6.7,0.9) {\small $B_R$}; \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6); \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6); \node at (4,3.3) {\small $A$}; \draw[very thick,blue!100] (7,3) rectangle (8,3.6); \node at (7.5,3.3) {\small $B$}; \draw[red, fill] (5,1.5) rectangle (6,2.1); \draw[red, fill] (6.05,1.5) rectangle (7,2.1); } \only<11>{ \draw[fill, blue!50] (1,0) rectangle (3,0.6); \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); \draw[fill, blue!50] (4.5,0) rectangle (5,0.6); \draw[very thick, blue!50] (5,0) rectangle (7,0.6); \node at (1.5,0.9) {\small $A_L$}; \node at (2.0,0.9) {\small $B_L$}; \node at (3.5,3.9) {\small $A_R$}; \node at (6.7,0.9) {\small $B_R$}; \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6); \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6); \node at (4,3.3) {\small $A$}; \draw[very thick,blue!100] (7,3) rectangle (8,3.6); \node at (7.5,3.3) {\small $B$}; \draw[red, fill] (5,1.5) rectangle (6,2.1); \draw[red, fill] (6.05,1.5) rectangle (7,2.1); \draw[blue!50, ->, line width = 2mm] (7.1,0.4) -- (8, 0.4); \draw[blue!50, ->, line width = 2mm] (7.1,4) -- (8,4); } \draw[very thick,->](0,0) -- (8,0); \node [anchor=base] at (8, -0.3) {\scriptsize time}; \node [anchor=base] at (0, -0.3) {\scriptsize 0}; \node [anchor=base] at (-1.2, 0.2) {\small low priority}; \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};} \only<10->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};} \end{tikzpicture} \end{tabular} \end{textblock} \begin{textblock}{0}(2.5,13)% \small \onslide<11>{ \begin{bubble}[8cm]% Scheduling: You want to avoid that a high priority process is staved indefinitely. \end{bubble}} \end{textblock} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{\Large Priority Inheritance Scheduling} \begin{itemize} \item Let a low priority process $L$ temporarily inherit the high priority of $H$ until $L$ leaves the critical section unlocking the resource.\bigskip \item Once the resource is unlocked $L$ returns to its original priority level. \alert{\bf BOGUS}\pause\bigskip \item \ldots $L$ needs to switch to the highest \alert{remaining} priority of the threads that it blocks. \end{itemize}\bigskip \small this error is already known since around 1999 \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \begin{center} \includegraphics[scale=0.25]{../pics/p3.jpg} \end{center} \begin{itemize} \item by Rajkumar, 1991 \item \it ``it resumes the priority it had at the point of entry into the critical section'' \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \begin{center} \includegraphics[scale=0.25]{../pics/p2.jpg} \end{center} \begin{itemize} \item by Jane Liu, 2000 \item {\it ``The job $J_l$ executes at its inherited priority until it releases $R$; at that time, the priority of $J_l$ returns to its priority at the time when it acquires the resource $R$.''}\medskip \item \small gives pseudo code and totally bogus data structures \item \small interesting part ``{\it left as an exercise}'' \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \begin{center} \includegraphics[scale=0.15]{../pics/p1.pdf} \end{center} \begin{itemize} \item by Laplante and Ovaska, 2011 (\$113.76) \item \it ``when $[$the task$]$ exits the critical section that caused the block, it reverts to the priority it had when it entered that section'' \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \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} \item a scheduling algorithm that is widely used in real-time operating systems \item has been ``proved'' correct by hand in a paper in 1983 \item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause \item we corrected the algorithm and then {\bf really} proved that it is correct \item we implemented this algorithm in a small OS called PINTOS (used for teaching at Stanford) \item our implementation was much more efficient than their reference implementation \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \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'' \end{quote}\bigskip\bigskip\bigskip \normalsize main work by Chunhan Wu (a PhD-student in Nanjing) \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{Testing Policies} \begin{center} \begin{tikzpicture}[scale=1] %\draw[black!10,step=2mm] (-5,-3) grid (5,4); %\draw[black!10,thick,step=10mm] (-5,-3) grid (5,4); \draw[white,thick,step=10mm] (-5,-3) grid (5,4); \draw [black!20, line width=1mm] (0,0) circle (1cm); \draw [line width=1mm] (0,0) circle (3cm); \node [black!20] at (0,0) {\begin{tabular}{c}core\\[-1mm] system\end{tabular}}; \draw [red, line width=2mm, <-] (-2.1,2.1) -- (-3.5,3.2); \node at (-3.5,3.6) {your system}; \node at (-4.8,0) {\Large policy $+$}; \only<2>{ \draw [black, fill=red, line width=0.5mm] (2,1) circle (3mm); \draw [red, line width=2mm, <-] (2.3,1.2) -- (3.5,2); \node at (3.8,2.6) {\begin{tabular}{l}a seed\\[-1mm] \footnotesize virus, Trojan\end{tabular}};} \only<3>{ \draw [black, fill=red, line width=0.5mm] (2,1) circle (7mm); \node[white] at (2,1) {\small tainted};} \only<4>{ \begin{scope} \draw [clip] (0,0) circle (2.955cm); \draw [black, fill=red, line width=0.5mm] (2,1) circle (9mm); \node[white] at (2,1) {\small tainted}; \end{scope}} \only<5->{ \begin{scope} \draw [clip] (0,0) circle (2.955cm); \draw [black, fill=red, line width=0.5mm] (2,1) circle (13mm); \node[white] at (2,1) {\small tainted}; \end{scope}} \only<6->{ \draw[fill=white, line width=1mm] (1.265,2.665) arc (-35:183:5mm); \draw[fill=white, line width=1mm] (1.25,3.25) arc (-35:183:3mm); \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{Big Proofs in CS (1)}Formal proofs in CS sound like science fiction? Completelyirrelevant! Lecturer gone mad?\pause\begin{itemize}\item in 2008, verification of a small C-compiler\begin{itemize}\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}\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 tested GCC, LLVM and others by randomly generating C-programs\item found more than 300 bugs in GCC and alsomany in LLVM (some of them highest-level critical)\bigskip\item about CompCert:\begin{bubble}[10cm]\small ``The striking thing about our CompCertresults is that the middle-end bugs we found in all othercompilers are absent. As of early 2011, the under-developmentversion of CompCert is the only compiler we have tested forwhich Csmith cannot find wrong-code errors. This is not forlack of trying: we have devoted about six CPU-years to thetask.'' \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 proofof implementation correctness and security enforcement''\end{bubble}\bigskip\pauseunhackable 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 ``works'' and by ``is secure''!\end{itemize}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c]\frametitle{Goal}Remember the Bridges example?\begin{itemize}\item Can we look at our programs and somehow ensurethey are secure/bug free/correct?\pause\bigskip\item Very hard: Anything interesting about programs is equivalentto 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, don't know (static analysis)\end{itemize}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state.png} \end{center} \begin{itemize} \item depending on some initial input, a program (behaviour) will ``develop'' over time. \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state2.png} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state3.jpg} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state4.jpg} \end{center} \begin{itemize} \item to be avoided \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state5.png} \end{center} \begin{itemize} \item this needs more work \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \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}\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} | \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)\small\begin{bubble}[5.6cm]\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language={},xleftmargin=3mm] a := 1 n := 5 top: jmp? n = 0 done a := a * n n := n + -1 goto top done:\end{lstlisting}\end{bubble}\end{textblock}\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} | \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)\small\begin{bubble}[5.6cm]\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language={},xleftmargin=3mm] n := 6 m1 := 0 m2 := 1top: jmp? n = 0 done tmp := m2 m2 := m1 + m2 m1 := tmp n := n + -1 goto topdone:\end{lstlisting}\end{bubble}\end{textblock}\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} | \pcode{jmp?} \meta{Exp} \meta{label} | \pcode{goto} \meta{label}\\: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\\end{plstx}}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\frametitle{Eval: An Interpreter}\mbox{}\\[-14mm]\mbox{}\small\begin{center}\bl{\begin{tabular}{lcl}$[n]_{env}$ & $\dn$ & $n$\\$[x]_{env}$ & $\dn$ & $env(x)$\\$[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} + [e_2]_{env}$\\$[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} * [e_2]_{env}$\\$[e_1 = e_2]_{env}$ & $\dn$ & $\begin{cases}1 & \text{if}\quad[e_1]_{env} = [e_2]_{env}\\0 & \text{otherwise}\end{cases}$\\\end{tabular}}\end{center}\footnotesize\begin{lstlisting}[numbers=none,xleftmargin=-5mm]def eval_exp(e: Exp, env: Env) : Int = e match { case Num(n) => n case Var(x) => env(x) case Plus(e1, e2) => eval_exp(e1, env) + eval_exp(e2, env) case Times(e1, e2) => eval_exp(e1, env) * eval_exp(e2, env) case Equ(e1, e2) => if (eval_exp(e1, env) == eval_exp(e2, env)) 1 else 0}\end{lstlisting}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\smallA program\begin{bubble}[6cm]\footnotesize\begin{lstlisting}[numbers=none, language={}, basicstyle=\ttfamily, xleftmargin=1mm] a := 1 n := 5 top: jmp? n = 0 done a := a * n n := n + -1 goto top done:\end{lstlisting}\end{bubble}The \emph{snippets} of the program:\footnotesize\begin{columns}\begin{column}[t]{5cm}\begin{bubble}[4.5cm]\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language={},xleftmargin=1mm]"" a := 1 n := 5 top: jmp? n = 0 done a := a * n n := n + -1 goto top done:\end{lstlisting}\end{bubble}\end{column}\begin{column}[t]{5cm}\begin{bubble}[4.5cm]\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language={},xleftmargin=1mm]top: jmp? n = 0 done a := a * n n := n + -1 goto top done:\end{lstlisting}\end{bubble}\end{column}\begin{column}[t]{2cm}\begin{bubble}[1.1cm]\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language={},xleftmargin=1mm]done:\end{lstlisting}\end{bubble}\end{column}\end{columns}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\frametitle{Eval for Stmts}\mbox{}\\[-12mm]\mbox{}Let \bl{$sn$} be the snippets of a program\small\begin{center}\bl{\begin{tabular}{lcl}$[\texttt{nil}]_{env}$ & $\dn$ & $env$\medskip\\$[\texttt{Label}(l:)::rest]_{env}$ & $\dn$ & $[rest]_{env}$\medskip\\$[x \,\texttt{:=}\, e::rest]_{env}$ & $\dn$ & $[rest]_{(env[x:= [e]_{env}])}$\medskip\\$[\texttt{jmp?}\;e\;l::rest]_{env}$ & $\dn$ & $\begin{cases}[sn(l)]_{env} & \text{if}\quad[e]_{env} = 1\\[rest]_{env} & \text{otherwise}\end{cases}$\medskip\\$[\texttt{goto}\;l::rest]_{env}$ & $\dn$ & $[sn(l)]_{env}$\\\end{tabular}}\end{center}\bigskipStart with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\frametitle{Eval in Code}\footnotesize\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]def eval(sn: Snips) : Env = { def eval_stmts(sts: Stmts, env: Env) : Env = sts match { case Nil => env case Label(l)::rest => eval_stmts(rest, env) case Assign(x, e)::rest => eval_stmts(rest, env + (x -> eval_exp(e, env))) case Jmp(b, l)::rest => if (eval_exp(b, env) == 1) eval_stmts(sn(l), env) else eval_stmts(rest, env) case Goto(l)::rest => eval_stmts(sn(l), env) } eval_stmts(sn(""), Map())}\end{lstlisting}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\frametitle{The Idea of Static Analysis}\small\mbox{}\bigskip\\\begin{columns}\begin{column}{5cm}\begin{bubble}[4.5cm]\footnotesize\begin{lstlisting}[numbers=none, language={}, basicstyle=\ttfamily, xleftmargin=1mm] a := 1 n := 5 top: jmp? n = 0 done a := a * n n := n + -1 goto top done:\end{lstlisting}\end{bubble}\end{column}\begin{column}{1cm}\raisebox{-20mm}{\LARGE\bf$\Rightarrow$}\end{column}\begin{column}{6cm}\begin{bubble}[4.7cm]\footnotesize\begin{lstlisting}[numbers=none, language={}, basicstyle=\ttfamily, xleftmargin=1mm, escapeinside={(*}{*)}] a := (*\hl{'+'}*) n := (*\hl{'+'}*) top: jmp? n = (*\hl{'0'}*) done a := a * n n := n + (*\hl{'-'}*) goto top done:\end{lstlisting}\end{bubble}\end{column}\end{columns}\bigskip\bigskipReplace all constants and variables by either \pcode{+}, \pcode{-} or \pcode{0}. What we want to find outis what the sign of \texttt{a} and \texttt{n} is (they should always positive).\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{Sign Analysis?} \begin{columns} \begin{column}{3cm} \begin{tabular}{cc|l} $e_1$ & $e_2$ & $e_1 + e_2$\\\hline{} - & - & -\\ - & 0 & -\\ - & + & -, 0, +\\ 0 & $x$ & $x$\\ + & - & -, 0, +\\ + & 0 & +\\ + & + & +\\ \end{tabular} \end{column} \begin{column}{3cm} \begin{tabular}{cc|l} $e_1$ & $e_2$ & $e_1 * e_2$\\\hline{} - & - & +\\ - & 0 & 0\\ - & + & -\\ 0 & $x$ & 0\\ + & - & -\\ + & 0 & 0\\ + & + & +\\ \end{tabular} \end{column} \end{columns} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\mbox{}\\[-13mm]\mbox{}\small\begin{center}\bl{\begin{tabular}{lcl}$[n]_{aenv}$ & $\dn$ & $\begin{cases}\{+\} & \text{if}\; n > 0\\\{-\} & \text{if}\; n < 0\\\{0\} & \text{if}\; n = 0\end{cases}$\\$[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}\scriptsize\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]def aeval_exp(e: Exp, aenv: AEnv) : Set[Abst] = e match { case Num(0) => Set(Zero) case Num(n) if (n < 0) => Set(Neg) case Num(n) if (n > 0) => Set(Pos) case Var(x) => aenv(x) case Plus(e1, e2) => aplus(aeval_exp(e1, aenv), aeval_exp(e2, aenv)) case Times(e1, e2) => atimes(aeval_exp(e1, aenv), aeval_exp(e2, aenv)) case Equ(e1, e2) => Set(Zero, Pos)}\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}\bigskipStart 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{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). 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}%%% Local Variables: %%% mode: latex%%% TeX-master: t%%% End: