From 361e794829accf80898763cd8492ad111febc4ed Mon Sep 17 00:00:00 2001 From: Caesar Date: Wed, 5 Oct 2016 21:20:46 +0200 Subject: [PATCH] Organize the two OpenFlow pdfs into one for the AFP --- .gitignore | 3 +- .../Examples/OF_conv_test/OF_conv_test.thy | 4 +-- thy/OpenFlow/Examples/RFC2544/RFC2544.thy | 4 +-- thy/OpenFlow/OpenFlowDoc.thy | 33 ++++-------------- thy/OpenFlow/ROOT | 28 +++++++-------- thy/OpenFlow/Semantics_OpenFlow.thy | 2 +- thy/OpenFlow/document/root.bib | 12 +++++++ thy/OpenFlow/document/root.tex | 34 +++++++++++++++++-- 8 files changed, 67 insertions(+), 53 deletions(-) diff --git a/.gitignore b/.gitignore index 387751cf..5ef9594a 100644 --- a/.gitignore +++ b/.gitignore @@ -23,5 +23,4 @@ cabal.sandbox.config thy/Examples/generated_code # generated OpenFlow files… -thy/OpenFlow/of_doc -thy/OpenFlow/of_outp +thy/OpenFlow/output diff --git a/thy/OpenFlow/Examples/OF_conv_test/OF_conv_test.thy b/thy/OpenFlow/Examples/OF_conv_test/OF_conv_test.thy index adc3a131..f45c3535 100644 --- a/thy/OpenFlow/Examples/OF_conv_test/OF_conv_test.thy +++ b/thy/OpenFlow/Examples/OF_conv_test/OF_conv_test.thy @@ -7,7 +7,7 @@ imports "../../OpenFlowSerialize" begin -section\Example: Simple Test for Translation to OpenFlow\ +(*section\Example: Simple Test for Translation to OpenFlow\*) parse_iptables_save SQRL_fw="iptables-save" @@ -51,7 +51,7 @@ definition "SQRL_fw_simple \ remdups_rev (to_simple_firewall (upper_closu value[code] "SQRL_fw_simple" lemma "simple_fw_valid SQRL_fw_simple" by eval -section\Example: SQRL RTBL\ +(*section\Example: SQRL RTBL\*) parse_ip_route SQRL_rtbl_main = "ip-route" value SQRL_rtbl_main diff --git a/thy/OpenFlow/Examples/RFC2544/RFC2544.thy b/thy/OpenFlow/Examples/RFC2544/RFC2544.thy index 89e54a27..ccbe09e1 100644 --- a/thy/OpenFlow/Examples/RFC2544/RFC2544.thy +++ b/thy/OpenFlow/Examples/RFC2544/RFC2544.thy @@ -6,7 +6,7 @@ imports "../../OpenFlowSerialize" begin -section\Example: Simple Test for Translation to OpenFlow\ +(*section\Example: Simple Test for Translation to OpenFlow\*) parse_iptables_save SQRL_fw="iptables-save" @@ -46,8 +46,6 @@ definition "SQRL_fw_simple \ remdups_rev (to_simple_firewall (upper_closu value[code] "SQRL_fw_simple" lemma "simple_fw_valid SQRL_fw_simple" by eval -section\Example: SQRL RTBL\ - parse_ip_route SQRL_rtbl_main = "ip-route" value SQRL_rtbl_main lemma "SQRL_rtbl_main = [\routing_match = PrefixMatch 0xC6120100 24, metric = 0, routing_action = \output_iface = ''ip1'', next_hop = None\\, diff --git a/thy/OpenFlow/OpenFlowDoc.thy b/thy/OpenFlow/OpenFlowDoc.thy index d6aac81e..4e5a6b3f 100644 --- a/thy/OpenFlow/OpenFlowDoc.thy +++ b/thy/OpenFlow/OpenFlowDoc.thy @@ -1,22 +1,10 @@ text_raw\ -\normalfont -\title{Verified Migration of Linux Firewalls to SDN} -\author{Julius Michaelis and Cornelius Diekmann} -\maketitle - -\begin{abstract} - We present a system that transforms the main routing table and \texttt{FORWARD} chain of iptables of a Linux-based firewall into a set of static OpenFlow rules. - Our implementation is verified against a model of a simplified Linux-based router and we can directly show how much of the original functionality is preserved. -\end{abstract} - -%\tableofcontents - -% sane default for proof documents -\parindent 0pt\parskip 0.5ex - -\input{chap1} +\twocolumn +\columnsep 2pc % Space between columns +\textwidth 42pc % Width of text line. +\part{Documentation} +\label{part2} \ - section\Configuration Translation\ text_raw\\label{sec:conv}\ text\ @@ -158,7 +146,7 @@ text\If no matching entry is found, the behavior is undefined.\ subsubsection\iptables Firewall\ text_raw\\label{sec:lfwfw}\ text\The firewall subsystem in a linux router is not any less complex than any of the of the other systems. -Fortunately, this complexity has been dealt with in~\cite{diekmann2016verified} already and we can directly use the result.\ +Fortunately, this complexity has been dealt with in~\cite{diekmann2016verified,Iptables_Semantics-AFP} already and we can directly use the result.\ text\In short, one of the results is that a complex \emph{iptables} configuration can be simplified to be represented by a single list of matches that only support the following match conditions: \begin{itemize} \item (String) prefix matches on the input and output interfaces. @@ -535,12 +523,3 @@ There are some fundamental differences between Exodus and our work: (*<*) end (*>*) - -text_raw\ - -\input{chap3} - -\bibliographystyle{abbrv} -\bibliography{root} -\ -(*\embedfile{OpenFlowDoc.tex}*) diff --git a/thy/OpenFlow/ROOT b/thy/OpenFlow/ROOT index d216a0ae..784fa5a7 100644 --- a/thy/OpenFlow/ROOT +++ b/thy/OpenFlow/ROOT @@ -1,25 +1,13 @@ chapter OpenFlow -session "OpenFlow_Documentation" = OpenFlow + - options [document_output = "of_doc"] - theories - OpenFlowDoc - document_files - "root.tex" - "chap1.tex" - "chap3.tex" - "root.bib" - "moeptikz.sty" - "fig/ofts.pdf" - "fig/pipeline.pdf" - "fig/rtr.pdf" - "bench.csv" session "OpenFlow" = Iptables_Semantics + - options [document_output = "of_outp"] + options[document_output = "output"] + theories[document=false] - "CaesarTheories" (* just some helper lemmas *) + CaesarTheories (* just some helper lemmas *) List_Group Sort_Descending + theories OpenFlowAction OpenFlowMatches @@ -29,8 +17,16 @@ session "OpenFlow" = Iptables_Semantics + LinuxRouterOpenFlowTranslation "Examples/OF_conv_test/OF_conv_test" "Examples/RFC2544/RFC2544" + OpenFlowDoc document_files "root.tex" + "chap1.tex" + "chap3.tex" + "root.bib" "moeptikz.sty" + "fig/ofts.pdf" + "fig/pipeline.pdf" + "fig/rtr.pdf" + "bench.csv" diff --git a/thy/OpenFlow/Semantics_OpenFlow.thy b/thy/OpenFlow/Semantics_OpenFlow.thy index fb8731a3..6eb34abe 100644 --- a/thy/OpenFlow/Semantics_OpenFlow.thy +++ b/thy/OpenFlow/Semantics_OpenFlow.thy @@ -9,7 +9,7 @@ datatype 'a flowtable_behavior = Action 'a | NoAction | Undefined definition "option_to_ftb b \ case b of Some a \ Action a | None \ NoAction" definition "ftb_to_option b \ case b of Action a \ Some a | NoAction \ None" -section\OpenFlow\ +(*section\OpenFlow\*) (*https://www.opennetworking.org/images/stories/downloads/sdn-resources/onf-specifications/openflow/openflow-switch-v1.5.0.pdf*) diff --git a/thy/OpenFlow/document/root.bib b/thy/OpenFlow/document/root.bib index 188f5196..5d2c4426 100644 --- a/thy/OpenFlow/document/root.bib +++ b/thy/OpenFlow/document/root.bib @@ -361,6 +361,7 @@ @inproceedings{michaelis2016middlebox title={Middlebox Models in Network Verification Research}, booktitle={Proceedings of the Seminars Future Internet (FI) and Innovative Internet Technologies and Mobile Communications (IITM), Winter Semester 2015/2016}, year={2016}, + volume={17}, } @article{barras1997coq, title={The Coq proof assistant reference manual: Version 6.1}, @@ -401,3 +402,14 @@ @inproceedings{lantz2010network year={2010}, organization={ACM} } + +@article{Iptables_Semantics-AFP, + author = {Cornelius Diekmann and Lars Hupel}, + title = {{I}ptables {S}emantics}, + journal = {Archive of Formal Proofs}, + month = sep, + year = 2016, + note = {\url{http://isa-afp.org/entries/Iptables_Semantics.shtml}, + Formal proof development}, + ISSN = {2150-914x}, +} diff --git a/thy/OpenFlow/document/root.tex b/thy/OpenFlow/document/root.tex index 7a9551db..ae373818 100644 --- a/thy/OpenFlow/document/root.tex +++ b/thy/OpenFlow/document/root.tex @@ -51,7 +51,6 @@ \usepackage{listings} \lstset{breaklines=true,numbers=left,numberstyle=\tiny\color{gray},basicstyle=\footnotesize\ttfamily} \usepackage{pgfplots} -\twocolumn \columnsep 2pc % Space between columns \textwidth 42pc % Width of text line. \oddsidemargin 4.5pc @@ -60,7 +59,7 @@ \advance\evensidemargin by -1in % Correct for LaTeX gratuitousness \marginparwidth 0pt % Margin pars are not allowed. \marginparsep 11pt % Horizontal space between outer margin and -\emergencystretch=3cm +\emergencystretch=10cm % this should be the last package used @@ -77,9 +76,39 @@ % for \frqq (whatever that actually is) \begin{document} +\title{Verified Migration of Linux Firewalls to SDN} +\author{Julius Michaelis and Cornelius Diekmann} +\maketitle + +\begin{abstract} + We present a system that transforms the main routing table and \texttt{FORWARD} chain of iptables of a Linux-based firewall into a set of static OpenFlow rules. + Our implementation is verified against a model of a simplified Linux-based router and we can directly show how much of the original functionality is preserved. +\end{abstract} +\vspace{1em} + +Please note that this document is organized in two distinct parts. +The first part contains the necessary definitions, helper lemmas and proofs in all their technicality as made in the theory code. +The second part reiterates the most important definitions and proofs in a manner that is more suitable for human readers and enriches them with detailed explanations in natural language. +Any interested reader should start from there. + +Many of the considerations that have led to the definitions made here have been explained in \cite{michaelis2016middlebox}. + +\tableofcontents + +\newpage + +\part{Code} + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex \input{session} +\input{chap3} + +\bibliographystyle{abbrv} +\bibliography{root} + % optional bibliography %\bibliographystyle{abbrv} %\bibliography{root} @@ -90,3 +119,4 @@ %%% mode: latex %%% TeX-master: t %%% End: +