ccs.tex

\section{ACKNOWLEDGEMENTS}
I thank my supervisor Timo Hynninen for his advice at the start of the process. Additionally, I am grateful for William Byrd for spending time answering my questions during the course of writing. The idea for the topic of this thesis is largely thanks to him.

\section{CONCLUSION}
\ifthesis
The goal of this thesis was to find a way to write conditionals in miniKanren. This resulted in the following contributions:
\begin{enumerate}
\item A technique of using pseudo-functions to express conditionals in miniKanren.
\item The implementation of a miniKanren variant, staticKanren, to help extract certain modes of programs.
\item A way of reformatting staticKanren's answers to a more human-like style.
\end{enumerate}

We learned along the way the important fact that while conditionals can be easily expressed with \code{condo}, the behavior of existing programs are almost impossible to preserve. The best solution, as presented in this thesis, is to specify a more compact, Scheme-like version with \code{condo}, run it through staticKanren for normalization and then manually modify the generated result, if needed, for the final version.

While this solution is not ideal due to the additional framework in staticKanren, I believe that it is a necessary price to pay for the mechanization of negation while retaining user flexibility. An alternative approach is to use constructive negation (\cite{chan}) but due to the workload required it is not suitable for a Bachelor thesis. Besides, creating yet another version of miniKanren would dilute the already diluted attention of newcomers since there are so many versions available at the moment.

There is another interesting use case of staticKanren to be explored in future work. With the help of \code{condo}, it is simple to rewrite any Scheme program to staticKanren and extract its various modes for verification and analysis. Additionally, the idea of pseudo-functions might be useful for exploring many other functional programming features, the most obvious instance of which being function composition.







\else
This thesis presented the following contributions:
\begin{enumerate}
\item A simple modeling of network firewalls.
\item The implementation of a minimal firewall analysis assistant in miniKanren.
\end{enumerate}

Out of these two, the first is the most important because it is useful for educational purpose. Being quite short, the firewall analyzer still lacks useful properties of a useful firewall analyzer such as the ability to convert ACL to logical statements or many standard pre-made queries. Also, the simplified model does not deal with changes very easily because each change has to be converted to be compatible with the model.

For future works, it would be nice to incorporate actual IPv4 addresses for use in conjunction with the hierarchical topology. Modifications have to be made concerning the validity of actual networking packets (such the "ICMP established flag" example we saw above). Ultimately, the program should have the ability to do actual firewall synthesis, with or without help from users. In my opinion, this goal is quite far-fetched because it is quite hard for a purely logical program to understand what is meant by a "common sense" firewall (i.e. to limit the search space to firewalls that are relevant). A puzzling firewall that does what it is supposed to is still useless. Indeed, there may be commercial firewall designers available on the market that adhere to a common sense standard, but I still wonder if the two methods can be combined.
\fi