70 \end{frame} |
70 \end{frame} |
71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
72 |
72 |
73 |
73 |
74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
75 \begin{frame}[c] |
|
76 \frametitle{Trusting Computing Base} |
|
77 |
|
78 When considering whether a system meets some security |
|
79 objectives, it is important to consider which parts of that |
|
80 system are trusted in order to meet that objective (TCB). |
|
81 \bigskip\pause |
|
82 |
|
83 The smaller the TCB, the less effort it takes to get |
|
84 some confidence that it is trustworthy, by doing a code |
|
85 review or by performing some (penetration) testing. |
|
86 \bigskip |
|
87 |
|
88 \footnotesize |
|
89 CPU, compiler, libraries, OS, NP $\not=$ P, |
|
90 random number generator, \ldots |
|
91 \end{frame} |
|
92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
93 |
|
94 |
|
95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
75 \begin{frame}[c] |
96 \begin{frame}[c] |
76 \frametitle{Dijkstra on Testing} |
97 \frametitle{Dijkstra on Testing} |
77 |
98 |
78 \begin{bubble}[10cm] |
99 \begin{bubble}[10cm] |
79 ``Program testing can be a very effective way to show the |
100 ``Program testing can be a very effective way to show the |
679 \end{center} |
713 \end{center} |
680 |
714 |
681 \end{frame} |
715 \end{frame} |
682 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
716 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
683 |
717 |
684 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
685 \begin{frame}[c] |
|
686 \frametitle{A Sound and Complete Test} |
|
687 |
|
688 \begin{itemize} |
|
689 \item working purely in the \emph{dynamic world} does not work -\!-\!- infinite state space\bigskip |
|
690 |
|
691 \item working purely on \emph{static} policies also does not\\ work -\!-\!- because of over approximation |
|
692 \smallskip |
|
693 \begin{itemize} |
|
694 \item sup+e a tainted file has type \emph{bin} and |
|
695 \item there is a role \bl{$r$} which can both read and write \emph{bin}-files\pause |
|
696 \item then we would conclude that this tainted file can spread\medskip\pause |
|
697 \item but if there is no process with role \bl{$r$} and it will never been |
|
698 created, then the file actually does not spread |
|
699 \end{itemize}\bigskip\pause |
|
700 |
|
701 \item \alert{our solution:} take a middle ground and record precisely the information |
|
702 of the initial state, but be less precise about every newly created object. |
|
703 \end{itemize} |
|
704 |
|
705 \end{frame} |
|
706 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
718 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
707 |
719 |
708 \begin{frame}[c] |
720 \begin{frame}[c] |
709 \frametitle{Big Proofs in CS} |
721 \frametitle{Big Proofs in CS (1)} |
710 |
722 |
711 Formal proofs in CS sound like science fiction? Completely irrelevant! |
723 Formal proofs in CS sound like science fiction? Completely |
712 Lecturer gone mad?\pause |
724 irrelevant! Lecturer gone mad?\pause |
713 |
725 |
714 \begin{itemize} |
726 \begin{itemize} |
715 \item in 2008, verification of a small C-compiler |
727 \item in 2008, verification of a small C-compiler |
716 \begin{itemize} |
728 \begin{itemize} |
717 \item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour'' |
729 \item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour'' |
718 \item is as good as \texttt{gcc -O1}, but much less buggy |
730 \item is as good as \texttt{gcc -O1}, but much less buggy |
719 \end{itemize} |
731 \end{itemize} |
720 \medskip |
732 \end{itemize} |
|
733 |
|
734 \begin{center} |
|
735 \includegraphics[scale=0.12]{../pics/compcert.png} |
|
736 \end{center} |
|
737 |
|
738 \end{frame} |
|
739 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
740 |
|
741 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
742 \begin{frame}[c] |
|
743 \frametitle{Fuzzy Testing C-Compilers} |
|
744 |
|
745 \begin{itemize} |
|
746 \item tested GCC, LLVM, others by randomly generating |
|
747 C-programs |
|
748 \item found more than 300 bugs in GCC and also |
|
749 many in LLVM (some of them highest-level critical)\bigskip |
|
750 \item about CompCert: |
|
751 |
|
752 \begin{bubble}[10cm]\small ``The striking thing about our CompCert |
|
753 results is that the middle-end bugs we found in all other |
|
754 compilers are absent. As of early 2011, the under-development |
|
755 version of CompCert is the only compiler we have tested for |
|
756 which Csmith cannot find wrong-code errors. This is not for |
|
757 lack of trying: we have devoted about six CPU-years to the |
|
758 task.'' |
|
759 \end{bubble} |
|
760 \end{itemize} |
|
761 |
|
762 \end{frame} |
|
763 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
764 |
|
765 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
766 \begin{frame}[c] |
|
767 \frametitle{Big Proofs in CS (2)} |
|
768 |
|
769 \begin{itemize} |
721 \item in 2010, verification of a micro-kernel operating system (approximately 8700 loc) |
770 \item in 2010, verification of a micro-kernel operating system (approximately 8700 loc) |
|
771 \begin{itemize} |
|
772 \item used in helicopters and mobile phones |
|
773 \item 200k loc of proof |
|
774 \item 25 - 30 person years |
|
775 \item found 160 bugs in the C code (144 by the proof) |
|
776 \end{itemize} |
|
777 \end{itemize} |
|
778 |
|
779 \begin{bubble}[10cm]\small |
|
780 ``Real-world operating-system kernel with an end-to-end proof |
|
781 of implementation correctness and security enforcement'' |
|
782 \end{bubble}\bigskip\pause |
|
783 |
|
784 unhackable kernel (New Scientists, September 2015) |
|
785 \end{frame} |
|
786 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
787 |
|
788 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
789 \begin{frame}[c] |
|
790 \frametitle{Big Proofs in CS (3)} |
|
791 |
722 \begin{itemize} |
792 \begin{itemize} |
723 \item 200k loc of proof |
793 \item verified TLS implementation\medskip |
724 \item 25 - 30 person years |
794 \item verified compilers (CompCert, CakeML)\medskip |
725 \item found 160 bugs in the C code (144 by the proof) |
795 \item verified distributed systems (Verdi)\medskip |
|
796 \item verified OSes or OS components\\ |
|
797 (seL4, CertiKOS, Ironclad Apps, \ldots)\medskip |
|
798 \item verified cryptography |
726 \end{itemize} |
799 \end{itemize} |
|
800 |
|
801 \end{frame} |
|
802 |
|
803 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
804 \begin{frame}[c] |
|
805 \frametitle{How Did This Happen?} |
|
806 |
|
807 Lots of ways! |
|
808 |
|
809 \begin{itemize} |
|
810 \item better programming languages |
|
811 \begin{itemize} |
|
812 \item basic safety guarantees built in |
|
813 \item powerful mechanisms for abstraction and modularity |
|
814 \end{itemize} |
|
815 \item better software development methodology |
|
816 \item stable platforms and frameworks |
|
817 \item better use of specifications\medskip\\ |
|
818 \small If you want to build software that works or is secure, |
|
819 it is helpful to know what you mean by ``work'' and by ``secure''! |
727 \end{itemize} |
820 \end{itemize} |
728 |
821 |
729 \end{frame} |
822 \end{frame} |
|
823 |
|
824 |
730 |
825 |
731 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
826 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
732 \begin{frame}[c] |
827 \begin{frame}[c] |
733 \frametitle{Goal} |
828 \frametitle{Goal} |
734 |
829 |
735 Remember the Bridges example? |
830 Remember the Bridges example? |
736 |
831 |
737 \begin{itemize} |
832 \begin{itemize} |
738 \item Can we look at our programs and somehow ensure |
833 \item Can we look at our programs and somehow ensure |
739 they are secure/bug free/correct?\pause\bigskip |
834 they are secure/bug free/correct/secure?\pause\bigskip |
740 |
835 |
741 \item Very hard: Anything interesting about programs is equivalent |
836 \item Very hard: Anything interesting about programs is equivalent |
742 to halting problem, which is undecidable.\pause\bigskip |
837 to halting problem, which is undecidable.\pause\bigskip |
743 |
838 |
744 \item \alert{Solution:} We avoid this ``minor'' obstacle by |
839 \item \alert{Solution:} We avoid this ``minor'' obstacle by |
745 being as close as +sible of deciding the halting |
840 being as close as possible of deciding the halting |
746 problem, without actually deciding the halting problem. |
841 problem, without actually deciding the halting problem. |
747 $\quad\Rightarrow$ static analysis |
842 \small$\quad\Rightarrow$ yes, no, do not know (static analysis) |
748 \end{itemize} |
843 \end{itemize} |
749 |
844 |
750 \end{frame} |
845 \end{frame} |
751 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
846 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
752 |
847 |
842 | \meta{var}\\ |
940 | \meta{var}\\ |
843 : \meta{Stmt} ::= \meta{label} : |
941 : \meta{Stmt} ::= \meta{label} : |
844 | \meta{var} := \meta{Exp} |
942 | \meta{var} := \meta{Exp} |
845 | jmp? \meta{Exp} \meta{label} |
943 | jmp? \meta{Exp} \meta{label} |
846 | goto \meta{label}\\ |
944 | goto \meta{label}\\ |
847 : \meta{Prog} ::= \meta{Stmt} \ldots\\ |
945 : \meta{Prog} ::= \meta{Stmt} \ldots \meta{Stmt}\\ |
848 \end{plstx}} |
|
849 |
|
850 \end{frame} |
|
851 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
852 |
|
853 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
854 \begin{frame}[fragile] |
|
855 \frametitle{\large Concrete Example: Sign-Analysis} |
|
856 \mbox{}\\[-20mm]\mbox{} |
|
857 |
|
858 \bl{\begin{plstx}[rhs style=,one per line] |
|
859 : \meta{Exp} ::= \meta{Exp} + \meta{Exp} |
|
860 | \meta{Exp} * \meta{Exp} |
|
861 | \meta{Exp} = \meta{Exp} |
|
862 | \meta{num} |
|
863 | \meta{var}\\ |
|
864 : \meta{Stmt} ::= \meta{label} : |
|
865 | \meta{var} := \meta{Exp} |
|
866 | jmp? \meta{Exp} \meta{label} |
|
867 | goto \meta{label}\\ |
|
868 : \meta{Prog} ::= \meta{Stmt} \ldots\\ |
|
869 \end{plstx}} |
946 \end{plstx}} |
870 |
947 |
871 \begin{textblock}{0}(7.8,2.5) |
948 \begin{textblock}{0}(7.8,2.5) |
872 \small |
949 \small |
873 \begin{bubble}[5.6cm] |
950 \begin{bubble}[5.6cm] |
929 \end{frame} |
1006 \end{frame} |
930 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1007 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
931 |
1008 |
932 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1009 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
933 \begin{frame}[fragile] |
1010 \begin{frame}[fragile] |
|
1011 \frametitle{\large Concrete Example: Sign-Analysis} |
|
1012 \mbox{}\\[-20mm]\mbox{} |
|
1013 |
|
1014 \bl{\begin{plstx}[rhs style=,one per line] |
|
1015 : \meta{Exp} ::= \meta{Exp} + \meta{Exp} |
|
1016 | \meta{Exp} * \meta{Exp} |
|
1017 | \meta{Exp} = \meta{Exp} |
|
1018 | \meta{num} |
|
1019 | \meta{var}\\ |
|
1020 : \meta{Stmt} ::= \meta{label} : |
|
1021 | \meta{var} := \meta{Exp} |
|
1022 | jmp? \meta{Exp} \meta{label} |
|
1023 | goto \meta{label}\\ |
|
1024 : \meta{Prog} ::= \meta{Stmt} \ldots \meta{Stmt}\\ |
|
1025 \end{plstx}} |
|
1026 |
|
1027 \end{frame} |
|
1028 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1029 |
|
1030 |
|
1031 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1032 \begin{frame}[fragile] |
934 \frametitle{Eval} |
1033 \frametitle{Eval} |
935 \mbox{}\\[-18mm]\mbox{} |
1034 \mbox{}\\[-14mm]\mbox{} |
936 |
1035 |
937 \small |
1036 \small |
938 \begin{center} |
1037 \begin{center} |
939 \bl{\begin{tabular}{lcl} |
1038 \bl{\begin{tabular}{lcl} |
940 $[n]_{env}$ & $\dn$ & $n$\\ |
1039 $[n]_{env}$ & $\dn$ & $n$\\ |