# HG changeset patch # User Christian Urban # Date 1455569337 -3600 # Node ID ffe5d850df62705171c6669ade26d92a8f07705c # Parent 7f589bfecffadb1ef359a3efae9d5bc941a6a9e8 added some slides diff -r 7f589bfecffa -r ffe5d850df62 Slides/graph.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/graph.sty Mon Feb 15 21:48:57 2016 +0100 @@ -0,0 +1,16 @@ +\usepackage{tikz} +\usepackage{pgf} +\usetikzlibrary{positioning} +\usetikzlibrary{calc} +\usetikzlibrary{fit} +\usepackage{graphicx} +\usepackage{pgfplots} + + +\newenvironment{bubble}[1][]{% +\addtolength{\leftmargini}{4mm}% +\begin{tikzpicture}[baseline=(current bounding box.north)]% +\draw (0,0) node[inner sep=2mm,fill=cream,ultra thick,draw=red,rounded corners=2mm]% +\bgroup\begin{minipage}{#1}\raggedright{}} +{\end{minipage}\egroup;% +\end{tikzpicture}\bigskip} diff -r 7f589bfecffa -r ffe5d850df62 Slides/slides.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/slides.sty Mon Feb 15 21:48:57 2016 +0100 @@ -0,0 +1,86 @@ +\usepackage[absolute,overlay]{textpos} +\usepackage{xcolor} +\usepackage{fontspec} +\usepackage[sc]{mathpazo} +\usefonttheme{serif} +\defaultfontfeatures{Ligatures=TeX} +\defaultfontfeatures{Mapping=tex-text} +\setromanfont{Hoefler Text} +\setmonofont[Scale=.88]{Consolas} +\newfontfamily{\consolas}{Consolas} + + +\definecolor{darkblue}{rgb}{0,0,0.6} +\hypersetup{colorlinks=true} +\hypersetup{linkcolor=darkblue} +\hypersetup{urlcolor=darkblue} + + + +\newcommand{\tttext}[1]{{\consolas{#1}}} + +\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% +\newcommand{\slidecaption}{} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Frametitles + +\setbeamerfont{frametitle}{size={\LARGE}} +\setbeamerfont{frametitle}{family={\fontspec{Hoefler Text Black}}} +\setbeamercolor{frametitle}{fg=ProcessBlue,bg=white} + +\setbeamertemplate{frametitle}{% +\vskip 2mm % distance from the top margin +\hskip -3mm % distance from left margin +\vbox{% +\begin{minipage}{1.05\textwidth}% +\centering% +\begin{tabular}{@{}c@{}}% +\insertframetitle% +\end{tabular}% +\end{minipage}\vspace{-10pt}}% +} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Foot +% +\setbeamertemplate{navigation symbols}{} +\usefoottemplate{% +\vbox{% + \tinyline{% + \tiny\hfill\textcolor{gray!50}{\slidecaption{} -- + p.~\insertframenumber/\inserttotalframenumber}}}% +} + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\beamertemplateballitem +\setlength\leftmargini{2mm} +\setlength\leftmarginii{0.6cm} +\setlength\leftmarginiii{1.5cm} +\setbeamertemplate{itemize/enumerate body end}{\vspace{-2mm}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% blocks +%\definecolor{cream}{rgb}{1,1,.65} +\definecolor{cream}{rgb}{1,1,.8} +\setbeamerfont{block title}{size=\normalsize} +\setbeamercolor{block title}{fg=black,bg=cream} +\setbeamercolor{block body}{fg=black,bg=cream} + +\setbeamertemplate{blocks}[rounded][shadow=true] + +\setbeamercolor{boxcolor}{fg=black,bg=cream} + +\mode + + + + + + + diff -r 7f589bfecffa -r ffe5d850df62 Slides/slides01.pdf Binary file Slides/slides01.pdf has changed diff -r 7f589bfecffa -r ffe5d850df62 Slides/slides01.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/slides01.tex Mon Feb 15 21:48:57 2016 +0100 @@ -0,0 +1,836 @@ +\documentclass[dvipsnames,14pt,t, xelatex]{beamer} +\usepackage{slides} +\usepackage{graph} + + +% 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 security +objectives, it is important to consider which parts of that +system are trusted in order to meet that objective (TCB). +\bigskip\pause + +The smaller the TCB, the less effort it takes to get +some confidence that it is trustworthy, by doing a code +review or by performing some (penetration) testing. +\bigskip + +\footnotesize +CPU, 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}\bigskip + + +similarly\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 have +help from the computer. `Program' is here to be understood to be +quite 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{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 also +many in LLVM (some of them highest-level critical)\bigskip +\item about CompCert: + +\begin{bubble}[10cm]\small ``The striking thing about our CompCert +results is that the middle-end bugs we found in all other +compilers are absent. As of early 2011, the under-development +version of CompCert is the only compiler we have tested for +which Csmith cannot find wrong-code errors. This is not for +lack of trying: we have devoted about six CPU-years to the +task.'' +\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 proof +of implementation correctness and security enforcement'' +\end{bubble}\bigskip\pause + +unhackable 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 ensure +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, don't know (static analysis) +\end{itemize} + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +\end{document} + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: + diff -r 7f589bfecffa -r ffe5d850df62 thys/Paper/Paper.thy --- a/thys/Paper/Paper.thy Sat Feb 13 02:00:09 2016 +0000 +++ b/thys/Paper/Paper.thy Mon Feb 15 21:48:57 2016 +0100 @@ -320,8 +320,7 @@ \noindent which holds because @{term "(c # s\<^sub>1) @ s\<^sub>3 \ L r\<^sub>1 "} implies @{term "s\<^sub>1 @ s\<^sub>3 \ L (der c r\<^sub>1) "} - \item[(2)] This case is similar except that in the last step we have to - instantiate the existential quantifier with @{term "Seq (projval r\<^sub>1 c v) v'"} + \item[(2)] This case is similar. \end{itemize} \noindent diff -r 7f589bfecffa -r ffe5d850df62 thys/ReStar.thy --- a/thys/ReStar.thy Sat Feb 13 02:00:09 2016 +0000 +++ b/thys/ReStar.thy Mon Feb 15 21:48:57 2016 +0100 @@ -1456,17 +1456,8 @@ apply metis apply metis apply(auto)[1] -apply(simp add: L_flat_NPrf) +apply(simp add: der_correctness Der_def) apply(auto)[1] -apply(frule_tac c="c" in v3_proj) -apply metis -apply(drule_tac x="s\<^sub>3" in spec) -apply(drule mp) -apply(rule_tac x="projval r1 c v" in exI) -apply(rule conjI) -apply (metis v4_proj2) -apply (metis NPrf_imp_Prf) -apply metis (* nullable case *) apply(erule PMatch.cases) apply(simp_all)[7] diff -r 7f589bfecffa -r ffe5d850df62 thys/paper.pdf Binary file thys/paper.pdf has changed