1 \documentclass[dvipsnames,14pt,t, xelatex]{beamer}

     2 \usepackage{slides}

     3 \usepackage{graph}

     4 

     5 

     6 % beamer stuff 

     7 \renewcommand{\slidecaption}{SEN 09, King's College London}

     8 \newcommand{\bl}[1]{\textcolor{blue}{#1}}

     9 

    10 \begin{document}

    11 

    12 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    13 \begin{frame}[t]

    14 \frametitle{%

    15   \begin{tabular}{@ {}c@ {}}

    16   \\

    17   \LARGE Security Engineering (9)\\[-3mm] 

    18   \end{tabular}}\bigskip\bigskip\bigskip

    19 

    20   \normalsize

    21   \begin{center}

    22   \begin{tabular}{ll}

    23   Email:  & christian.urban at kcl.ac.uk\\

    24   Office: & S1.27 (1st floor Strand Building)\\

    25   Slides: & KEATS (also homework is there)\\

    26   \end{tabular}

    27   \end{center}

    28 

    29 \end{frame}

    30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    31 

    32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    33   \begin{frame}[c]

    34 

    35   \begin{center}

    36   \includegraphics[scale=0.6]{pics/bridge-limits.png}

    37   \end{center}

    38 

    39   \end{frame}

    40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    41 

    42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    43   \begin{frame}[c]

    44   \frametitle{Old-Fashioned Eng.~vs.~CS}

    45   

    46   \begin{center}

    47   \begin{tabular}{@{}cc@{}}

    48   \begin{tabular}{@{}p{5.2cm}} 

    49   \includegraphics[scale=0.058]{pics/towerbridge.jpg}\\ 

    50   {\bf bridges}: \\

    51   \raggedright\small

    52   engineers can ``look'' at a bridge and have a pretty good

    53   intuition about whether it will hold up or not\\ 

    54   (redundancy; predictive theory)

    55   \end{tabular} &

    56   \begin{tabular}{p{5cm}} 

    57   \includegraphics[scale=0.265]{pics/code.jpg}\\

    58   \raggedright

    59   {\bf code}: \\

    60   \raggedright\small

    61   programmers have very little intuition about their code; 

    62   often it is too expensive to have redundancy;

    63   not ``continuous'' 

    64   \end{tabular}

    65   \end{tabular}

    66   \end{center}

    67 

    68   \end{frame}

    69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    70 

    71 

    72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    73 \begin{frame}[c]

    74 \frametitle{Trusting Computing Base}

    75   

    76 When considering whether a system meets some security

    77 objectives, it is important to consider which parts of that

    78 system are trusted in order to meet that objective (TCB).

    79 \bigskip\pause

    80 

    81 The smaller the TCB, the less effort it takes to get

    82 some confidence that it is trustworthy, by doing a code 

    83 review or by performing some (penetration) testing.

    84 \bigskip

    85 

    86 \footnotesize

    87 CPU, compiler, libraries, OS, NP $\not=$ P,

    88 random number generator, \ldots

    89 \end{frame}

    90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    91 

    92 

    93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    94   \begin{frame}[c]

    95   \frametitle{Dijkstra on Testing}

    96   

    97   \begin{bubble}[10cm]

    98   ``Program testing can be a very effective way to show the

    99   presence of bugs, but it is hopelessly inadequate for showing

   100   their absence.''

   101   \end{bubble}\bigskip

   102   

   103   unfortunately attackers exploit bugs (Satan's computer vs 

   104   Murphy's)

   105 

   106   \end{frame}

   107 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   108 

   109 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   110 \begin{frame}[c]

   111 \frametitle{\Large Proving Programs to be Correct}

   112 

   113 \begin{bubble}[10cm]

   114 \small

   115 {\bf Theorem:} There are infinitely many prime 

   116 numbers.\medskip\\

   117 

   118 {\bf Proof} \ldots\\

   119 \end{bubble}\bigskip

   120 

   121 

   122 similarly\bigskip

   123 

   124 \begin{bubble}[10cm]

   125 \small

   126 {\bf Theorem:} The program is doing what 

   127 it is supposed to be doing.\medskip

   128 

   129 {\bf Long, long proof} \ldots\\

   130 \end{bubble}\bigskip\medskip

   131 

   132 \small This can be a gigantic proof. The only hope is to have

   133 help from the computer. `Program' is here to be understood to be

   134 quite general (protocols, OS, \ldots).

   135 

   136 \end{frame}

   137 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   138 

   139 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   140   \begin{frame}[c]

   141   \frametitle{\Large{}Mars Pathfinder Mission 1997}

   142 

   143   \begin{center}

   144   %\includegraphics[scale=0.15]{../pics/marspath1.png}

   145   %\includegraphics[scale=0.16]{../pics/marspath3.png}

   146   %\includegraphics[scale=0.3]{../pics/marsrover.png}

   147   \end{center}

   148   

   149   \begin{itemize}

   150   \item despite NASA's famous testing procedures, the lander crashed frequently on Mars

   151   \item a scheduling algorithm was not used in the OS

   152   \end{itemize}

   153 

   154   \end{frame}

   155 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   156 

   157 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   158   \begin{frame}[c]

   159   

   160 

   161   \begin{textblock}{11}(1,3)

   162   \begin{tabular}{@{\hspace{-10mm}}l}

   163   \begin{tikzpicture}[scale=1.1]

   164   \node at (-2.5,-1.5) {\textcolor{white}{a}};

   165   \node at (8,4) {\textcolor{white}{a}};

   166   

   167     

   168 

   169   \only<1>{

   170    \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   171   }

   172   \only<2>{

   173    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   174    \draw[fill, blue!50] (3,0) rectangle (5,0.6);

   175    \draw[fill, blue!100] (2,3) rectangle (3,3.6);

   176   }

   177   \only<3>{

   178    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   179    \draw[fill, blue!50] (3,0) rectangle (4.5,0.6);

   180    \draw[fill, blue!50] (5.5,0) rectangle (6,0.6);

   181    \draw[fill, blue!100] (2,3) rectangle (3,3.6);

   182    \draw[fill, blue!100] (4.5,3) rectangle (5.5,3.6);

   183   }

   184   \only<4>{

   185    \node at (2.5,0.9) {\small locked a resource};

   186    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   187    \draw[blue!50, very thick] (2,0) rectangle (4,0.6);

   188    \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);

   189    \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);

   190   }

   191   \only<5>{

   192    \node at (2.5,0.9) {\small locked a resource};

   193    \draw[fill, blue!50] (1,0) rectangle (4,0.6);

   194    \draw[blue!100, fill] (4,3) rectangle (5, 3.6);

   195   }

   196   \only<6>{

   197    \node at (2.5,0.9) {\small locked a resource};

   198    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   199    \draw[blue!50, very thick] (2,0) rectangle (4,0.6);

   200    \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);

   201    \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);

   202   }

   203   \only<7>{

   204    \node at (2.5,0.9) {\small locked a resource};

   205    \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);

   206    \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);

   207    \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);

   208    \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);

   209   }

   210   \only<8>{

   211    \node at (2.5,0.9) {\small locked a resource}; 

   212    \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);

   213    \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);

   214    \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);

   215    \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);

   216    \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);

   217    \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);

   218   }

   219   \only<9>{

   220    \node at (2.5,0.9) {\small locked a resource}; 

   221    \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);

   222    \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);

   223    \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);

   224    \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);

   225    \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);

   226   }

   227   \only<10>{

   228    \node at (2.5,0.9) {\small locked a resource}; 

   229    \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);

   230    \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);

   231    \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);

   232    \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);

   233    \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);

   234    \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);

   235   }

   236   \only<11>{

   237    \node at (2.5,0.9) {\small locked a resource};

   238    \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);

   239    \draw[blue!50, very thick] (4.5,0) rectangle (6,0.6);

   240    \draw[blue!100, very thick] (4.5,3) rectangle (5.5, 3.6);

   241    \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);

   242    \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);

   243    \draw[red, <-, line width = 2mm] (4.5,-0.1) -- (4.5, -1);

   244   }

   245   \only<12>{

   246    \node at (2.5,0.9) {\small locked a resource}; 

   247    \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);

   248    \draw[blue!50, very thick] (5.5,0) rectangle (7,0.6);

   249    \draw[blue!100, very thick] (5.5,3) rectangle (6.5, 3.6);

   250    \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);

   251    \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);

   252    \draw[red, fill] (4.55,1.5) rectangle (5.5,2.1);

   253    \draw[red, <-, line width = 2mm] (5.5,-0.1) -- (5.5, -1);

   254    \node [anchor=base] at (6.3, 1.8) {\Large\ldots};

   255   }

   256   \only<13>{

   257    \node at (2.5,0.9) {\small locked a resource}; 

   258    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   259    \draw[blue!50, very thick] (2,0) rectangle (4,0.6);

   260    \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);

   261    \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);

   262   }

   263   \only<14>{

   264    \node at (2.5,3.9) {\small locked a resource}; 

   265    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   266    \draw[blue!50, fill] (2,3) rectangle (4,3.6);

   267    \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);

   268    \draw[blue!50, ->, line width = 2mm] (2,1) -- (2, 2.5);

   269    \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);

   270   }

   271   \only<15>{

   272    \node at (2.5,3.9) {\small locked a resource};  

   273    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   274    \draw[blue!50, fill] (2,3) rectangle (4,3.6);

   275    \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);

   276    \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);

   277    \draw[red, very thick] (2.5,1.5) rectangle (3.5,2.1); 

   278   }

   279 

   280 

   281   \draw[very thick,->](0,0) -- (8,0);

   282   \node [anchor=base] at (8, -0.3) {\scriptsize time};

   283   \node [anchor=base] at (0, -0.3) {\scriptsize 0};

   284   \node [anchor=base] at (-1.2, 0.2) {\small low priority};

   285   \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}

   286   \only<8->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}

   287 

   288   \end{tikzpicture}

   289   \end{tabular}

   290   \end{textblock}

   291 

   292   \begin{textblock}{0}(2.5,13)%

   293   \small

   294   \onslide<3->{

   295   \begin{bubble}[8cm]%

   296   Scheduling: You want to avoid that a high 

   297   priority process is starved indefinitely.

   298   \end{bubble}}

   299   \end{textblock}

   300 

   301   \end{frame}

   302 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   303   

   304 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   305   \begin{frame}[c]

   306   \frametitle{\Large Priority Inheritance Scheduling}

   307 

   308   \begin{itemize}

   309   \item Let a low priority process $L$ temporarily inherit 

   310     the high priority of $H$ until $L$ leaves the critical 

   311     section unlocking the resource.\bigskip

   312   \item Once the resource is unlocked $L$ returns to its original 

   313     priority level.

   314   \end{itemize}

   315 

   316   \end{frame}

   317 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   318   

   319 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   320   \begin{frame}[c]

   321   

   322   \begin{textblock}{11}(1,3)

   323   \begin{tabular}{@{\hspace{-10mm}}l}

   324   \begin{tikzpicture}[scale=1.1]

   325   \node at (-2.5,-1.5) {\textcolor{white}{a}};

   326   \node at (8,4) {\textcolor{white}{a}};

   327   

   328   \only<1>{

   329     \draw[fill, blue!50] (1,0) rectangle (6,0.6);

   330     \node at (1.5,0.9) {\small $A_L$};

   331     \node at (2.0,0.9) {\small $B_L$};

   332     \node at (3.5,0.9) {\small $A_R$};

   333     \node at (5.7,0.9) {\small $B_R$};

   334     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   335     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   336     \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);

   337     \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);

   338   }

   339   \only<2>{

   340     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   341     \draw[very thick, blue!50] (3,0) rectangle (6,0.6);

   342     \node at (1.5,0.9) {\small $A_L$};

   343     \node at (2.0,0.9) {\small $B_L$};

   344     \node at (3.5,0.9) {\small $A_R$};

   345     \node at (5.7,0.9) {\small $B_R$};

   346     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   347     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   348     \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);

   349     \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);

   350   }

   351   \only<3>{

   352     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   353     \draw[very thick, blue!50] (3,0) rectangle (6,0.6);

   354     \node at (1.5,0.9) {\small $A_L$};

   355     \node at (2.0,0.9) {\small $B_L$};

   356     \node at (3.5,0.9) {\small $A_R$};

   357     \node at (5.7,0.9) {\small $B_R$};

   358     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   359     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   360     \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);

   361     \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);

   362     \draw[very thick,blue!100] (3,3) rectangle (4,3.6);

   363     \node at (3.5,3.3) {\small $A$};

   364   }

   365   \only<4>{

   366     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   367     \draw[very thick, blue!50] (3,0) rectangle (6,0.6);

   368     \node at (1.5,0.9) {\small $A_L$};

   369     \node at (2.0,0.9) {\small $B_L$};

   370     \node at (3.5,0.9) {\small $A_R$};

   371     \node at (5.7,0.9) {\small $B_R$};

   372     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   373     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   374     \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);

   375     \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);

   376     \draw[very thick,blue!100] (3,3) rectangle (4,3.6);

   377     \node at (3.5,3.3) {\small $A$};

   378     \draw[very thick,blue!100] (4,3) rectangle (5,3.6);

   379     \node at (4.5,3.3) {\small $B$};

   380   }

   381   \only<5>{

   382     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   383     \draw[very thick, blue!50] (3,3) rectangle (6,3.6);

   384     \node at (1.5,0.9) {\small $A_L$};

   385     \node at (2.0,0.9) {\small $B_L$};

   386     \node at (3.5,3.9) {\small $A_R$};

   387     \node at (5.7,3.9) {\small $B_R$};

   388     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   389     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   390     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   391     \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);

   392     \draw[very thick,blue!100] (6,3) rectangle (7,3.6);

   393     \node at (6.5,3.3) {\small $A$};

   394     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   395     \node at (7.5,3.3) {\small $B$};

   396     \draw[blue!50, ->, line width = 2mm] (3,1) -- (3, 2.5);

   397   }

   398   \only<6>{

   399     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   400     \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);

   401     \draw[very thick, blue!50] (3.5,3) rectangle (6,3.6);

   402     \node at (1.5,0.9) {\small $A_L$};

   403     \node at (2.0,0.9) {\small $B_L$};

   404     \node at (3.5,3.9) {\small $A_R$};

   405     \node at (5.7,3.9) {\small $B_R$};

   406     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   407     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   408     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   409     \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);

   410     \draw[very thick,blue!100] (6,3) rectangle (7,3.6);

   411     \node at (6.5,3.3) {\small $A$};

   412     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   413     \node at (7.5,3.3) {\small $B$}; 

   414   }

   415   \only<7>{

   416    \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   417     \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);

   418     \draw[very thick, blue!50] (3.5,0) rectangle (6,0.6);

   419     \node at (1.5,0.9) {\small $A_L$};

   420     \node at (2.0,0.9) {\small $B_L$};

   421     \node at (3.5,3.9) {\small $A_R$};

   422     \node at (5.7,0.9) {\small $B_R$};

   423     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   424     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   425     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   426     \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);

   427     \draw[very thick,blue!100] (6,3) rectangle (7,3.6);

   428     \node at (6.5,3.3) {\small $A$};

   429     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   430     \node at (7.5,3.3) {\small $B$};  

   431     \draw[blue!50, <-, line width = 2mm] (3.5,1) -- (3.5, 2.5);

   432     \draw[blue!50, <-, line width = 2mm] (4,3.3) -- (5.5,3.3);

   433   }

   434   \only<8>{

   435     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   436     \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);

   437     \draw[very thick, blue!50] (4.5,0) rectangle (7,0.6);

   438     \node at (1.5,0.9) {\small $A_L$};

   439     \node at (2.0,0.9) {\small $B_L$};

   440     \node at (3.5,3.9) {\small $A_R$};

   441     \node at (6.7,0.9) {\small $B_R$};

   442     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   443     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   444     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   445     \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);

   446     \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);

   447     \node at (4,3.3) {\small $A$};

   448     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   449     \node at (7.5,3.3) {\small $B$};  

   450   }

   451   \only<9>{

   452     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   453     \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);

   454     \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);

   455     \draw[very thick, blue!50] (5,0) rectangle (7,0.6);

   456     \node at (1.5,0.9) {\small $A_L$};

   457     \node at (2.0,0.9) {\small $B_L$};

   458     \node at (3.5,3.9) {\small $A_R$};

   459     \node at (6.7,0.9) {\small $B_R$};

   460     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   461     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   462     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   463     \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);

   464     \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);

   465     \node at (4,3.3) {\small $A$};

   466     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   467     \node at (7.5,3.3) {\small $B$};  

   468   }

   469   \only<10>{

   470     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   471     \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);

   472     \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);

   473     \draw[very thick, blue!50] (5,0) rectangle (7,0.6);

   474     \node at (1.5,0.9) {\small $A_L$};

   475     \node at (2.0,0.9) {\small $B_L$};

   476     \node at (3.5,3.9) {\small $A_R$};

   477     \node at (6.7,0.9) {\small $B_R$};

   478     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   479     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   480     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   481     \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);

   482     \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);

   483     \node at (4,3.3) {\small $A$};

   484     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   485     \node at (7.5,3.3) {\small $B$};  

   486     \draw[red, fill] (5,1.5) rectangle (6,2.1);

   487     \draw[red, fill] (6.05,1.5) rectangle (7,2.1);

   488   }

   489   \only<11>{

   490    \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   491     \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);

   492     \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);

   493     \draw[very thick, blue!50] (5,0) rectangle (7,0.6);

   494     \node at (1.5,0.9) {\small $A_L$};

   495     \node at (2.0,0.9) {\small $B_L$};

   496     \node at (3.5,3.9) {\small $A_R$};

   497     \node at (6.7,0.9) {\small $B_R$};

   498     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   499     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   500     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   501     \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);

   502     \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);

   503     \node at (4,3.3) {\small $A$};

   504     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   505     \node at (7.5,3.3) {\small $B$};  

   506     \draw[red, fill] (5,1.5) rectangle (6,2.1);

   507     \draw[red, fill] (6.05,1.5) rectangle (7,2.1);

   508     \draw[blue!50, ->, line width = 2mm] (7.1,0.4) -- (8, 0.4);

   509     \draw[blue!50, ->, line width = 2mm] (7.1,4) -- (8,4);

   510   }

   511 

   512   \draw[very thick,->](0,0) -- (8,0);

   513   \node [anchor=base] at (8, -0.3) {\scriptsize time};

   514   \node [anchor=base] at (0, -0.3) {\scriptsize 0};

   515   \node [anchor=base] at (-1.2, 0.2) {\small low priority};

   516   \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}

   517   \only<10->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}

   518 

   519   \end{tikzpicture}

   520   \end{tabular}

   521   \end{textblock}

   522   

   523   \begin{textblock}{0}(2.5,13)%

   524   \small

   525   \onslide<11>{

   526   \begin{bubble}[8cm]%

   527   Scheduling: You want to avoid that a high 

   528   priority process is staved indefinitely.

   529   \end{bubble}}

   530   \end{textblock}

   531 

   532 

   533   \end{frame}

   534 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   535   

   536 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   537   \begin{frame}[c]

   538   \frametitle{\Large Priority Inheritance Scheduling}

   539 

   540   \begin{itemize}

   541   \item Let a low priority process $L$ temporarily inherit 

   542     the high priority of $H$ until $L$ leaves the critical 

   543     section unlocking the resource.\bigskip

   544   \item Once the resource is unlocked $L$ returns to its original 

   545     priority level. \alert{\bf BOGUS}\pause\bigskip

   546   \item \ldots $L$ needs to switch to the highest 

   547     \alert{remaining} priority of the threads that it blocks.

   548   \end{itemize}\bigskip

   549 

   550   \small this error is already known since around 1999

   551 

   552   \end{frame}

   553 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   554 

   555 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   556   \begin{frame}[c]

   557 

   558   \begin{center}

   559   \includegraphics[scale=0.25]{pics/p3.jpg}

   560   \end{center}

   561 

   562    \begin{itemize}

   563   \item by Rajkumar, 1991

   564   \item \it ``it resumes the priority it had at the point of entry into the critical 

   565   section''

   566   \end{itemize}

   567 

   568   \end{frame}

   569 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   570      

   571 

   572 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   573   \begin{frame}[c]

   574 

   575   \begin{center}

   576   \includegraphics[scale=0.25]{pics/p2.jpg}

   577   \end{center}

   578 

   579    \begin{itemize}

   580   \item by Jane Liu, 2000

   581   \item {\it ``The job $J_l$ executes at its inherited 

   582     priority until it releases $R$; at that time, the 

   583     priority of $J_l$ returns to its priority 

   584     at the time when it acquires the resource $R$.''}\medskip

   585   \item \small gives pseudo code and totally bogus data structures  

   586   \item \small interesting part ``{\it left as an exercise}''

   587   \end{itemize}

   588 

   589   \end{frame}

   590 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   591      

   592 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   593   \begin{frame}[c]

   594 

   595   \begin{center}

   596   \includegraphics[scale=0.15]{pics/p1.pdf}

   597   \end{center}

   598 

   599   \begin{itemize}

   600   \item by Laplante and Ovaska, 2011 (\$113.76)

   601   \item \it ``when $[$the task$]$ exits the critical section that

   602         caused the block, it reverts to the priority it had

   603         when it entered that section'' 

   604   \end{itemize}

   605 

   606   \end{frame}

   607 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   608   

   609 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   610   \begin{frame}[c]

   611 

   612   \begin{center}

   613   \includegraphics[scale=0.25]{pics/p4.jpg}

   614   \end{center}

   615 

   616   \begin{itemize}

   617   \item by Silberschatz, Galvin, and Gagne, 2013 (OS-bible)

   618   \item \it ``Upon releasing the lock, the 

   619   $[$low-priority$]$ thread will revert to 

   620   its original priority.''

   621   \end{itemize}

   622 

   623   \end{frame}

   624 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   625    

   626   

   627 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   628   \begin{frame}[c]

   629   \frametitle{Priority Scheduling}

   630 

   631   \begin{itemize}

   632   \item a scheduling algorithm that is widely used in real-time operating systems

   633   \item has been ``proved'' correct by hand in a paper in 1983

   634   \item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause

   635   

   636   \item we corrected the algorithm and then {\bf really} proved that it is correct	

   637   \item we implemented this algorithm in a small OS called PINTOS (used for teaching at Stanford)

   638   \item our implementation was much more efficient than their reference implementation

   639   \end{itemize}

   640 

   641   \end{frame}

   642 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   643    

   644    

   645 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   646   \begin{frame}[c]

   647   \frametitle{Design of AC-Policies}

   648 

   649   Imagine you set up an access policy (root, lpd, users, staff, etc)

   650   \bigskip\pause

   651 

   652   \Large

   653   \begin{quote}

   654   ``what you specify is what you get but not necessarily what you want\ldots''

   655   \end{quote}\bigskip\bigskip\bigskip

   656   

   657   \normalsize main work by Chunhan Wu (a PhD-student in Nanjing)

   658 

   659   \end{frame}

   660 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   661 

   662 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   663   \begin{frame}[c]

   664   \frametitle{Testing Policies}

   665 

   666   \begin{center}

   667   \begin{tikzpicture}[scale=1]

   668   %\draw[black!10,step=2mm] (-5,-3) grid (5,4);

   669   %\draw[black!10,thick,step=10mm] (-5,-3) grid (5,4);

   670   \draw[white,thick,step=10mm] (-5,-3) grid (5,4);

   671 

   672   \draw [black!20, line width=1mm] (0,0) circle (1cm);

   673   \draw [line width=1mm] (0,0) circle (3cm);

   674   \node [black!20] at (0,0) {\begin{tabular}{c}core\\[-1mm] system\end{tabular}};

   675   

   676   \draw [red, line width=2mm, <-] (-2.1,2.1) -- (-3.5,3.2);

   677   \node at (-3.5,3.6) {your system};

   678   \node at (-4.8,0) {\Large policy $+$};

   679 

   680   

   681   \only<2>{

   682   \draw [black, fill=red, line width=0.5mm] (2,1) circle (3mm);

   683   \draw [red, line width=2mm, <-] (2.3,1.2) -- (3.5,2);

   684   \node at (3.8,2.6) {\begin{tabular}{l}a seed\\[-1mm] \footnotesize virus, Trojan\end{tabular}};}

   685 

   686   \only<3>{

   687   \draw [black, fill=red, line width=0.5mm] (2,1) circle (7mm);

   688   \node[white] at (2,1) {\small tainted};}

   689 

   690   \only<4>{

   691   \begin{scope}

   692   \draw [clip] (0,0) circle (2.955cm);

   693   \draw [black, fill=red, line width=0.5mm] (2,1) circle (9mm);

   694   \node[white] at (2,1) {\small tainted};

   695   \end{scope}}

   696 

   697   \only<5->{

   698   \begin{scope}

   699   \draw [clip] (0,0) circle (2.955cm);

   700   \draw [black, fill=red, line width=0.5mm] (2,1) circle (13mm);

   701   \node[white] at (2,1) {\small tainted};

   702   \end{scope}}

   703 

   704   \only<6->{

   705   \draw[fill=white, line width=1mm] (1.265,2.665) arc (-35:183:5mm);

   706   \draw[fill=white, line width=1mm] (1.25,3.25) arc (-35:183:3mm);

   707   \node[black, rotate=10] at (1.9,3.6) {\LARGE\ldots};

   708   }

   709 

   710   \end{tikzpicture}

   711   \end{center}

   712   

   713   \only<7->{

   714   \begin{textblock}{4}(1,12)

   715   \small

   716   reduced the problem to a finite problem; gave a proof

   717   \end{textblock}} 

   718 

   719   \end{frame}

   720 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   721 

   722 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   723 \begin{frame}[c]

   724 \frametitle{Fuzzy Testing C-Compilers}

   725 

   726 \begin{itemize}

   727 \item tested GCC, LLVM and others by randomly generating 

   728 C-programs

   729 \item found more than 300 bugs in GCC and also

   730 many in LLVM (some of them highest-level critical)\bigskip

   731 \item about CompCert:

   732 

   733 \begin{bubble}[10cm]\small ``The striking thing about our CompCert

   734 results is that the middle-end bugs we found in all other

   735 compilers are absent. As of early 2011, the under-development

   736 version of CompCert is the only compiler we have tested for

   737 which Csmith cannot find wrong-code errors. This is not for

   738 lack of trying: we have devoted about six CPU-years to the

   739 task.'' 

   740 \end{bubble} 

   741 \end{itemize}

   742 

   743 \end{frame}

   744 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   745 

   746 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   747 \begin{frame}[c]

   748 \frametitle{Big Proofs in CS (2)}

   749 

   750 \begin{itemize}

   751 \item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)

   752   \begin{itemize}

   753   \item used in helicopters and mobile phones

   754   \item 200k loc of proof

   755   \item 25 - 30 person years

   756   \item found 160 bugs in the C code (144 by the proof)

   757   \end{itemize}

   758 \end{itemize}

   759 

   760 \begin{bubble}[10cm]\small

   761 ``Real-world operating-system kernel with an end-to-end proof

   762 of implementation correctness and security enforcement''

   763 \end{bubble}\bigskip\pause

   764 

   765 unhackable kernel (New Scientists, September 2015)

   766 \end{frame}

   767 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   768 

   769 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   770 \begin{frame}[c]

   771 \frametitle{Big Proofs in CS (3)}

   772 

   773 \begin{itemize}

   774 \item verified TLS implementation\medskip

   775 \item verified compilers (CompCert, CakeML)\medskip

   776 \item verified distributed systems (Verdi)\medskip

   777 \item verified OSes or OS components\\

   778 (seL4, CertiKOS, Ironclad Apps, \ldots)\medskip

   779 \item verified cryptography

   780 \end{itemize}

   781 

   782 \end{frame}

   783 

   784 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   785 \begin{frame}[c]

   786 \frametitle{How Did This Happen?}

   787 

   788 Lots of ways!

   789 

   790 \begin{itemize}

   791 \item better programming languages

   792   \begin{itemize}

   793   \item basic safety guarantees built in

   794   \item powerful mechanisms for abstraction and modularity

   795   \end{itemize}

   796 \item better software development methodology

   797 \item stable platforms and frameworks

   798 \item better use of specifications\medskip\\

   799   \small If you want to build software that works or is secure, 

   800     it is helpful to know what you mean by ``works'' and by ``is secure''!

   801 \end{itemize}

   802 

   803 \end{frame}

   804 

   805 

   806 

   807 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   808 \begin{frame}[c]

   809 \frametitle{Goal}

   810 

   811 Remember the Bridges example?

   812 

   813 \begin{itemize}

   814 \item Can we look at our programs and somehow ensure

   815 they are secure/bug free/correct?\pause\bigskip

   816 

   817 \item Very hard: Anything interesting about programs is equivalent

   818 to halting problem, which is undecidable.\pause\bigskip

   819 

   820 \item \alert{Solution:} We avoid this ``minor'' obstacle by

   821       being as close as possible of deciding the halting

   822       problem, without actually deciding the halting problem.

   823       \small$\quad\Rightarrow$ yes, no, don't know (static analysis)

   824 \end{itemize}

   825 

   826 \end{frame}

   827 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   828 

   829 

   830 \end{document}

   831 

   832 

   833 %%% Local Variables:  

   834 %%% mode: latex

   835 %%% TeX-master: t

   836 %%% End: 

   837