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

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

     4 

     5 %\usepackage{grammar}

     6 \usepackage{soul}

     7 \usepackage{data}

     8 \usepackage{proof}

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

    11 \renewcommand{\slidecaption}{Canterbury, 22.2.2016}

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

    45   \Large POSIX Lexing with Derivatives\\[-1.5mm] 

    46   \Large of Regular Expressions\\[-1mm] 

    47   %\normalsize Or, How to Find Bugs with the\\[-5mm] 

    48   %\normalsize Isabelle Theorem Prover

    22   \begin{tabular}{ll}

    53   \begin{tabular}{c}

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

    54   \small Christian Urban\\

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

    55   \small King's College London\\

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

    56   \\

    57   \\

    58   Joint work with Fahad Ausaf and Roy Dyckhoff

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

    69   \includegraphics[scale=0.2]{isabelle.png}

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

    83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    43   \begin{frame}[c]

    84 \begin{frame}[c]

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

    85 \frametitle{Why Bother?}

    45   

    86 

    46   \begin{center}

    87 Surely regular expressions must have been implemented and 

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

    88 studied to death, no?

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

    89 

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

    90 \begin{center}

    50   {\bf bridges}: \\

    91 \begin{tikzpicture}

    51   \raggedright\small

    92 \begin{axis}[

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

    93     xlabel={{\tt a}s},

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

    94     ylabel={time in secs},

    54   (redundancy; predictive theory)

    95     enlargelimits=false,

    55   \end{tabular} &

    96     xtick={0,5,...,30},

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

    97     xmax=30,

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

    98     ymax=35,

    58   \raggedright

    99     ytick={0,5,...,30},

    59   {\bf code}: \\

   100     scaled ticks=false,

    60   \raggedright\small

   101     axis lines=left,

    61   programmers have very little intuition about their code; 

   102     width=8cm,

    62   often it is too expensive to have redundancy;

   103     height=6cm, 

    63   not ``continuous'' 

   104     legend entries={Python,Ruby},  

   105     legend pos=north west,

   106     legend cell align=left  

   107 ]

   108 \addplot[blue,mark=*, mark options={fill=white}] 

   109   table {re-python.data};

   110 \addplot[brown,mark=pentagon*, mark options={fill=white}] 

   111   table {re-ruby.data};  

   112 \end{axis}

   113 \end{tikzpicture}

   114 \end{center}

   115 

   116 evil regular expressions: \bl{$({\tt a}?)^n \cdot {\tt a}^n$}

   117 

   118 \end{frame}

   119 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   120 

   121 

   122 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   123 \begin{frame}[c]

   124 \frametitle{\Large Isabelle Theorem Prover}

   125 

   126 \begin{itemize}

   127 \item started to use Isabelle after my PhD (in 2000)

   128 

   129 \item the thesis included a rather complicated 

   130   ``pencil-and-paper'' proof for a 

   131   termination argument (sort of $\lambda$-calculus)\medskip

   132  

   133 \item me, my supervisor, the examiners did not find any problems\medskip 

   134  \begin{center}

   135   \begin{tabular}{@ {}c@ {}}

   136   \includegraphics[scale=0.38]{barendregt.jpg}\\[-2mm]

   137   \footnotesize Henk Barendregt

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

   395 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    70 

   396 

    71 

   397 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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

   398 %  \begin{frame}[c]

    73 \begin{frame}[c]

   399 %  \frametitle{\Large Lessons Learned}

    74 \frametitle{Trusting Computing Base}

   400 %

    75   

   401 %  \begin{itemize}

    76 When considering whether a system meets some security

   402 %  \item using a theorem prover we were able to keep a large 

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

   403 %  proof consistent with changes in the definitions\bigskip

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

   404 %  \item it took us some 10 days to get to the error\ldots

    79 \bigskip\pause

   405 %  probably the same time Harper and Pfenning needed to \LaTeX{}

    80 

   406 %  their paper\bigskip 

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

   407 %  \item once there, we ran circles around them

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

   408 %  \end{itemize}

    83 review or by performing some (penetration) testing.

   409 %

    84 \bigskip

   410 %  \end{frame}

    85 

   411 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

    86 \footnotesize

   412   

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

   413 

    88 random number generator, \ldots

   414 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    89 \end{frame}

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

    91 

    92 

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

    95   \frametitle{Dijkstra on Testing}

   416   \frametitle{Real-Time Scheduling} 

    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   

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

   441    \node at (2.5,0.9) {\small locks a resource};

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

   448    \node at (2.5,0.9) {\small locks a resource};

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

   453    \node at (2.5,0.9) {\small locks a resource};

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

   460    \node at (2.5,0.9) {\small locks a resource};

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

   467    \node at (2.5,0.9) {\small locks a resource}; 

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

   476    \node at (2.5,0.9) {\small locks a resource}; 

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

   484    \node at (2.5,0.9) {\small locks a resource}; 

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

   493    \node at (2.5,0.9) {\small locks a resource};

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

   502    \node at (2.5,0.9) {\small locks a resource}; 

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

   513    \node at (2.5,0.9) {\small locks a resource}; 

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

   520    \node at (2.5,3.9) {\small locks a resource}; 

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

   528    \node at (2.5,3.9) {\small locks a resource};  

   296   Scheduling: You want to avoid that a high 

   552   RT-Scheduling: You want to avoid that a 

   297   priority process is starved indefinitely.

   553   high-priority process is starved indefinitely.

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

   565   \item Let a low priority process \bl{$L$} temporarily inherit 

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

   566     the high priority of \bl{$H$} until \bl{$L$} leaves the critical 

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

   568   \item Once the resource is unlocked, \bl{$L$} ``returns to its original 

   313     priority level.

   569     priority level.''\\

   570     \mbox{}\hfill\footnotesize

   571     \begin{tabular}{p{6cm}@{}}

   572     L.~Sha, R.~Rajkumar, and J.~P.~Lehoczky. 

   573     {\it Priority Inheritance Protocols: An Approach to 

   574     Real-Time Synchronization}. IEEE Transactions on 

   575     Computers, 39(9):1175–1185, 1990

   576     \end{tabular}\bigskip\normalsize\pause

   577   

   578   \item Proved correct, reviewed in a respectable journal....what could possibly be wrong?

   579     

   321   

   587 

   528   priority process is staved indefinitely.

   794   priority process is starved indefinitely.

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

   807   \item Let a low priority process \bl{$L$} temporarily inherit 

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

   808     the high priority of \bl{$H$} until \bl{$L$} leaves the critical 

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

   810   \item Once the resource is unlocked, \bl{$L$} returns to its original 

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

   812   \item \ldots \bl{$L$} needs to switch to the highest 

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

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

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

   825   \includegraphics[scale=0.25]{p3.jpg}

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

   841   \includegraphics[scale=0.25]{p2.jpg}

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

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

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

   861   \includegraphics[scale=0.15]{p1.pdf}

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

   878   \includegraphics[scale=0.22]{p5.jpg}

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

   882   \item by Silberschatz, Galvin and Gagne (9th edition, 2013)

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

   883   \item \it ``Upon releasing the

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

   884   lock, the $[$low-priority$]$ thread will revert to its original

   620   its original priority.''

   885   priority.''

   886   \end{itemize}

   887 

   888   \end{frame}

   889 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   890     

   891   

   892 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   893   \begin{frame}[c]

   894   \frametitle{Priority Scheduling}

   895 

   896   \begin{itemize}

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

   898   \item has been ``proved'' correct by hand in a paper in 1990

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

   900   

   901   \item we (generalised) the algorithm and then {\bf really} proved that it is correct	

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

   903   \item our implementation was faster than their reference implementation

   626   

   909 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   910 %  \begin{frame}[c]

   911 %  \frametitle{\Large{}Mars Pathfinder Mission 1997}

   912 %

   913 %  \begin{center}

   914 %  \includegraphics[scale=0.15]{marspath1.png}

   915 %  \includegraphics[scale=0.16]{marspath3.png}

   916 %  \includegraphics[scale=0.3]{marsrover.png}

   917 %  \end{center}

   918 %  

   919 %  \begin{itemize}

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

   921 %  \item a scheduling algorithm was not used in the OS at the 

   922 %  beginning; PIP was enabled after the cause was identified

   923 %  \end{itemize}

   924 %

   925 %  \end{frame}

   926 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   927 

   629   \frametitle{Priority Scheduling}

   930   \frametitle{Lessons Learned}

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

   933   \item our proof-technique is adapted from security 

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

   934   protocols\bigskip

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

   935  

   635   

   936   \item do not venture outside your field of expertise 

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

   937   \includegraphics[scale=0.03]{smiley.jpg}

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

   938   \bigskip

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

   939 

   940   \item we solved the single-processor case; the multi-processor 

   941   case: no idea!

   643    

   946 

   644    

   947 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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

   948 \begin{frame}[c]

   949 \frametitle{Regular Expressions}

   950 

   951 

   952 \begin{textblock}{6}(2,5)

   953   \begin{tabular}{rrl@ {\hspace{13mm}}l}

   954   \bl{$r$} & \bl{$::=$}  & \bl{$\varnothing$}   & null\\

   955            & \bl{$\mid$} & \bl{$\epsilon$}      & empty string\\

   956            & \bl{$\mid$} & \bl{$c$}             & character\\

   957            & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\

   958            & \bl{$\mid$} & \bl{$r_1 + r_2$}     & alternative / choice\\

   959            & \bl{$\mid$} & \bl{$r^*$}           & star (zero or more)\\

   960   \end{tabular}

   961   \end{textblock}

   962   

   963 \end{frame}

   964 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   965 

   966 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   967 \begin{frame}[c]

   968 \frametitle{\begin{tabular}{c}The Derivative of a Rexp\end{tabular}}

   969 

   970 \large

   971 If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular 

   972 expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip

   973 

   974 \small

   975 \bl{$der\,c\,r$} gives the answer, Brzozowski (1964), Owens (2005)

   976 ``\ldots have been lost in the sands of time\ldots''

   977 \end{frame}

   978 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   979 

   980 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   981 \begin{frame}[c]

   982 \frametitle{}

   983 

   984 

   985 \ldots{}whether a regular expression can match the empty string:

   986 \begin{center}

   987 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}

   988 \bl{$nullable(\varnothing)$}      & \bl{$\dn$} & \bl{$false$}\\

   989 \bl{$nullable(\epsilon)$}           & \bl{$\dn$} &  \bl{$true$}\\

   990 \bl{$nullable (c)$}                    & \bl{$\dn$} &  \bl{$false$}\\

   991 \bl{$nullable (r_1 + r_2)$}       & \bl{$\dn$} &  \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 

   992 \bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} &  \bl{$nullable(r_1) \wedge nullable(r_2)$} \\

   993 \bl{$nullable (r^*)$}                 & \bl{$\dn$} & \bl{$true$} \\

   994 \end{tabular}

   995 \end{center}

   996 

   997 \end{frame}

   998 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   999 

  1000 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1001 \begin{frame}[c]

  1002 \frametitle{\begin{tabular}{c}The Derivative of a Rexp\end{tabular}}

  1003 

  1004 \begin{center}

  1005 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}

  1006   \bl{$der\, c\, (\varnothing)$}      & \bl{$\dn$} & \bl{$\varnothing$} & \\

  1007   \bl{$der\, c\, (\epsilon)$}           & \bl{$\dn$} & \bl{$\varnothing$} & \\

  1008   \bl{$der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\epsilon$ else $\varnothing$} & \\

  1009   \bl{$der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$der\, c\, r_1 + der\, c\, r_2$} & \\

  1010   \bl{$der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\

  1011   & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ 

  1012   & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\

  1013   \bl{$der\, c\, (r^*)$}          & \bl{$\dn$} & \bl{$(der\,c\,r) \cdot (r^*)$} &\medskip\\\pause

  1014 

  1015   \bl{$\textit{ders}\, []\, r$}     & \bl{$\dn$} & \bl{$r$} & \\

  1016   \bl{$\textit{ders}\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$\textit{ders}\,s\,(der\,c\,r)$} & \\

  1017   \end{tabular}

  1018 \end{center}

  1019 

  1020 \end{frame}

  1021 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

  1022 

  1023 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1024 \begin{frame}[c]

  1025 \frametitle{\begin{tabular}{c}\bl{$({\tt a}?)^n \cdot {\tt a}^n$}\end{tabular}}

  1026 

  1027 \begin{center}

  1028 \begin{tikzpicture}

  1029 \begin{axis}[

  1030     xlabel={\pcode{a}s},

  1031     ylabel={time in secs},

  1032     enlargelimits=false,

  1033     xtick={0,200,...,1000},

  1034     xmax=1000,

  1035     ytick={0,5,...,30},

  1036     scaled ticks=false,

  1037     axis lines=left,

  1038     width=9.5cm,

  1039     height=7cm, 

  1040     legend entries={Python,Ruby,Scala V1,Scala V2},  

  1041     legend pos=north west,

  1042     legend cell align=left  

  1043 ]

  1044 \addplot[blue,mark=*, mark options={fill=white}] 

  1045   table {re-python.data};

  1046 \addplot[brown,mark=pentagon*, mark options={fill=white}] 

  1047   table {re-ruby.data};  

  1048 \addplot[red,mark=triangle*,mark options={fill=white}] 

  1049   table {re1.data};  

  1050 \addplot[green,mark=square*,mark options={fill=white}] 

  1051   table {re2b.data};

  1052 \end{axis}

  1053 \end{tikzpicture}

  1054 \end{center}

  1055 

  1056 \end{frame}

  1057 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

  1058 

  1059 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1060 \begin{frame}[t]

  1061 \frametitle{\begin{tabular}{c}\bl{$({\tt a}?)^n \cdot {\tt a}^n$}\end{tabular}}

  1062 

  1063 \begin{center}

  1064 \begin{tikzpicture}

  1065 \begin{axis}[

  1066     xlabel={\pcode{a}s},

  1067     ylabel={time in secs},

  1068     enlargelimits=false,

  1069     xtick={0,3000,...,12000},

  1070     xmax=12000,

  1071     ymax=35,

  1072     ytick={0,5,...,30},

  1073     scaled ticks=false,

  1074     axis lines=left,

  1075     width=9cm,

  1076     height=7cm

  1077 ]

  1078 \addplot[green,mark=square*,mark options={fill=white}] table {re2b.data};

  1079 \addplot[black,mark=square*,mark options={fill=white}] table {re3.data};

  1080 \end{axis}

  1081 \end{tikzpicture}

  1082 \end{center}

  1083 

  1084 \end{frame}

  1085 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

  1086 

  1087 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1088 \begin{frame}[c]

  1089 \frametitle{Correctness}

  1090 

  1091 It is a relative easy exercise in a theorem prover:

  1092 

  1093 \begin{center}

  1094 \bl{$matches(r, s)$}  if and only if  \bl{$s \in L(r)$} 

  1095 \end{center}\bigskip

  1096 

  1097 \small

  1098 \bl{$matches(r, s) \dn nullable(ders(r, s))$}

  1099 

  1100 \end{frame}

  1101 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

  1102 

  1103 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1104 \begin{frame}[c]

  1105 \frametitle{POSIX Regex Matching}

  1106 

  1107 Two rules:

  1108 

  1109 \begin{itemize}

  1110 \item Longest match rule (``maximal munch rule''): The 

  1111 longest initial substring matched by any regular expression 

  1112 is taken as the next token.

  1113 

  1114 \begin{center}

  1115 \bl{$\texttt{\Grid{iffoo\VS bla}}$}

  1116 \end{center}\medskip

  1117 

  1118 \item Rule priority:

  1119 For a particular longest initial substring, the first regular

  1120 expression that can match determines the token.

  1121 

  1122 \begin{center}

  1123 \bl{$\texttt{\Grid{if\VS bla}}$}

  1124 \end{center}

  1125 \end{itemize}\bigskip\pause

  1126 

  1127 \small

  1128 \hfill Kuklewicz: most POSIX matchers are buggy\\

  1129 \footnotesize

  1130 \hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix}

  1131 

  1132 \end{frame}

  1133 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

  1134 

  1135 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1136 \begin{frame}[c]

  1137 \frametitle{POSIX Regex Matching}

  1138 

  1139 \begin{itemize}

  1140 

  1141 \item Sulzmann \& Lu came up with a beautiful

  1142 idea for how to extend the simple regular expression 

  1143 matcher to POSIX matching/lexing (FLOPS 2014)\bigskip\bigskip\bigskip

  1144 

  1145 \begin{tabular}{@{\hspace{4cm}}c@{}}

  1146   \includegraphics[scale=0.14]{sulzmann.jpg}\\[-2mm]

  1147   \hspace{0cm}\footnotesize Martin Sulzmann

  1148 \end{tabular}\bigskip\bigskip

  1149 

  1150 \item the idea: define an inverse operation to the derivatives

  1151 \end{itemize}

  1152 

  1153 

  1154 

  1155 \end{frame}

  1156 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

  1157 

  1158 

  1159 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1160 \begin{frame}[c]

  1161 \frametitle{Regexes and Values}

  1162 

  1163 Regular expressions and their corresponding values:

  1164 

  1165 \begin{center}

  1166 \begin{columns}

  1167 \begin{column}{3cm}

  1168 \begin{tabular}{@{}rrl@{}}

  1169   \bl{$r$} & \bl{$::=$}  & \bl{$\varnothing$}\\

  1170            & \bl{$\mid$} & \bl{$\epsilon$}   \\

  1171            & \bl{$\mid$} & \bl{$c$}          \\

  1172            & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\

  1173            & \bl{$\mid$} & \bl{$r_1 + r_2$}   \\

  1174   \\

  1175            & \bl{$\mid$} & \bl{$r^*$}         \\

  1176   \\

  1177   \end{tabular}

  1178 \end{column}

  1179 \begin{column}{3cm}

  1180 \begin{tabular}{@{\hspace{-7mm}}rrl@{}}

  1181   \bl{$v$} & \bl{$::=$}  & \\

  1182            &             & \bl{$Empty$}   \\

  1183            & \bl{$\mid$} & \bl{$Char(c)$}          \\

  1184            & \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\

  1185            & \bl{$\mid$} & \bl{$Left(v)$}   \\

  1186            & \bl{$\mid$} & \bl{$Right(v)$}  \\

  1187            & \bl{$\mid$} & \bl{$[]$}      \\

  1188            & \bl{$\mid$} & \bl{$[v_1,\ldots\,v_n]$} \\

  1189   \end{tabular}

  1190 \end{column}

  1191 \end{columns}

  1192 \end{center}\pause

  1193 

  1194 There is also a notion of a string behind a value: \bl{$|v|$}

  1195 

  1196 \end{frame}

  1197 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

  1198 

  1199 

  1200 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1201 \begin{frame}[c]

  1202 \frametitle{Sulzmann \& Lu Matcher}

  1203 

  1204 We want to match the string \bl{$abc$} using \bl{$r_1$}:

  1205 

  1206 \begin{center}

  1207 \begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]

  1208 \node (r1)  {\bl{$r_1$}};

  1209 \node (r2) [right=of r1] {\bl{$r_2$}};

  1210 \draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};\pause

  1211 \node (r3) [right=of r2] {\bl{$r_3$}};

  1212 \draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};\pause

  1213 \node (r4) [right=of r3] {\bl{$r_4$}};

  1214 \draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};\pause

  1215 \draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$\;\;nullable?$}}};\pause

  1216 \node (v4) [below=of r4] {\bl{$v_4$}};

  1217 \draw[->,line width=1mm]  (r4) -- (v4);\pause

  1218 \node (v3) [left=of v4] {\bl{$v_3$}};

  1219 \draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};\pause

  1220 \node (v2) [left=of v3] {\bl{$v_2$}};

  1221 \draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};\pause

  1222 \node (v1) [left=of v2] {\bl{$v_1$}};

  1223 \draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};\pause

  1224 \draw[->,line width=0.5mm]  (r3) -- (v3);

  1225 \draw[->,line width=0.5mm]  (r2) -- (v2);

  1226 \draw[->,line width=0.5mm]  (r1) -- (v1);

  1227 \draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};

  1228 \end{tikzpicture}

  1229 \end{center}

  1230 

  1231 \end{frame}

  1232 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

  1233 

  1234 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1235 \begin{frame}[t,squeeze]

  1236 \frametitle{Sulzmann \& Lu Paper}

  1237 

  1238 \begin{itemize}

  1239 \item I have no doubt the algorithm is correct --- 

  1240   the problem, I do not believe their proof.

  1241 

  1242   \begin{center}

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

  1244   ``How could I miss this? Well, I was rather careless when 

  1245   stating this Lemma :)\smallskip

  1246  

  1247   Great example how formal machine checked proofs (and 

  1248   proof assistants) can help to spot flawed reasoning steps.''

  1249   \end{bubble}

  1250   \end{center}\pause

  1251   

  1252   \begin{center}

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

  1254   ``Well, I don't think there's any flaw. The issue is how to 

  1255   come up with a mechanical proof. In my world mathematical 

  1256   proof $=$ mechanical proof doesn't necessarily hold.''

  1257   \end{bubble}

  1258   \end{center}\pause

  1259   

  1260 \end{itemize}

  1261 

  1262   \only<3>{%

  1263   \begin{textblock}{11}(1,4.4)

  1264   \begin{center}

  1265   \begin{bubble}[10.9cm]\small\centering

  1266   \includegraphics[scale=0.37]{msbug.png}

  1267   \end{bubble}

  1268   \end{center}

  1269   \end{textblock}}

  1270   

  1271 

  1272 \end{frame}

  1273 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

  1274 

  1275 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1276 \begin{frame}[c]

  1277 \frametitle{\begin{tabular}{c}The Proof Idea\\[-1mm] by Sulzmann \& Lu

  1278 \end{tabular}}

  1279 

  1280 \begin{itemize}

  1281 \item introduce an inductively defined ordering relation 

  1282 \bl{$v \succ_r v'$} which captures the idea of POSIX matching

  1283 

  1284 \item the algorithm returns the maximum of all possible

  1285  values that are possible for a regular expression.\pause

  1286  \bigskip\small

  1287