% optimization

The optimal distribution model, starting from the traffic pattern analysis, understands what are the filtering points crossed by specific packets. The model allows the choice of the filtering control to configure to achieve the better performance, minimized delay and maximized bandwidth. This reduces the number of rules in each filtering point and to get a better use of the available resources.

The distribution model opens to a new security problem that rises the same anomalies listed in Section~\ref{subsec:policy_analysis}, because this model, from an equivalent firewall, builds a distributed firewall in which the same filtering point has a list of heterogeneous rules coming from different policies.
The Section~\ref{sec:policy_services} presents how the conflicts and are handled and removed, but in in this case the task is to find an ordered list of rules without any anomalies between them to place in a filtering point, avoiding any further policy refinement.

The optimization is due to two different aspect, the former is to enforce the same security level of the equivalent firewall with the minimum number of rules and the latter is to maximize the performance in terms of latency, bandwidth and resource consumptions.

The distribution is modelled as SAT problem (Boolean Satisfiability problem), which is the problem of determining if exists an interpretation that satisfies a given boolean expression. In other words, it try to set the variables of a boolean formula with the values \textit{true} or \textit{false} in such a way that the given expression is evaluated as \textit{true}, in this case the boolean formula is called satisfiable, otherwise \textit{false} if it is unsatisfiable.

This optimization model is made of a list of boolean expressions, each one has a distinct task.

\subsection{Propositional equation}

It expresses a boolean propositional equation that means it is composed by binary variables.

\begin{itemize}
	\item 
	vertical equation: it represents the choice to place a specific rule in a specific filtering point. This is done exploring the rules that could be enforced in this point.
	
	\begin{empheq}[box=\myBox]{equation*}
	\mathit{P}_{n,x}^{\alpha} = generalization() \; \land \; !precedingSuperSet() \; \land \; \mathit{S}_{n,x} 
	\end{empheq}
	
	\begin{itemize}
		\item 
		$\mathit{P}_{n,x}^{\alpha}$: it expresses the boolean variable which is true if the $n$-rule, with the $\alpha$ action, on the $x$ filtering point is present, otherwise false if is not enforced;
		
		\item
		$generalization()$: it is a boolean function that expresses if the $n$-rule falls under the Generalization anomaly (Figure \ref{fig:rule_anomalies}) that is not an error or a misconfiguration. 
		This is done searching a \textit{correlation anomaly} and, if it is found, making sure that there is no rules that falls under the \textit{redundancy anomaly} between the current rule and the ``correlated'' rule;
		
		\[ generalization(\mathit{P}_{n,x}^{\alpha}) = \bigvee_{i=n+1}^{R-1}\bigg[\mathit{P}_{i,x}^{!\alpha, \cap} \; \land \; !redundant(\mathit{P}_{n,x}^{\alpha})\bigg] \]
		
		\item
		$redundant()$: it is a boolean function that expresses if the $n$-rule falls under the\break Redundancy anomaly, if this expression return true, the rules must be not enforced.
		To check if the $n$-rule is redundant it is needed to search any rules, between the following rules and the current one, which is a super set or equivalent one and it has the same action to be performed.;	
		
		\[ redundant(\mathit{P}_{n,x}^{\alpha}) = \bigvee_{j=n+1}^{i-1} \bigg( \mathit{P}_{j,x}^{\alpha, \supseteq} \bigg) \]
		
		\item
		$precedingSuperSet()$: it is a boolean function that expresses if the $n$-rule falls under the shadowing anomaly (Figure \ref{fig:rule_anomalies}) and in this case the rule must deleted. This function search any rule, with any action, preceding the $n$-rule which is a superset or an equivalent set, if it is found at least one rule, the function return true;
		
		\[ precedingSuperSet(\mathit{P}_{n,x}^{\alpha}) = \bigvee_{k=0}^{n-1} \bigg( \mathit{P}_{k,x}^{\alpha, \supseteq} \bigg) \]
		
		\item
		$\mathit{S}_{n,x}$: it is a boolean variable that represents the freedom degree of the system.
	\end{itemize}
\end{itemize}

\subsection{Hard constraints}

The hard constraints express the clauses that must be satisfied by the model. 

\begin{itemize}
	\item 
	horizontal equation: it represents the choice to place a specific rule at maximum in one filtering point. This equation is built only for the rules whose action is \textit{deny}, independently from the default action.
	
	%\[\mathcal{D}_{n,p}^{\alpha} = setInOnePoint() \; \lor \; !necessary() = 1 \]
	
	\begin{empheq}[box=\myBox]{equation*}
	\mathcal{D}_{n,p}^{\alpha} = setInOnePoint() \; \lor \; !necessary() = True
	\end{empheq}
	
	\begin{itemize}
		\item 
		$\mathcal{D}_{n,p}^{\alpha}$: it is the name of the equation that represent the $n$-rule in the $p$ traffic path;
		
		\item
		$setInOnePoint()$: it is the boolean function that values true is the $n$-rule is placed in one filtering point, or false if it is placed in multiple instances or not placed at all;
		
		\[ setInOnePoint() = \bigvee_{i=0}^{M} \bigg[ \mathit{S}_{n,i} \; \land \; \mathit{P}_{n,i} \; \land \; noOtherPlaces() \bigg] \]
		
		\item
		$noOtherPlaces()$: it is the boolean function that checks if no other filtering point has the $n$-rule present variable set to true;		
		
		\[ noOtherPlaces() = \bigwedge_{j=0, j \neq i}^{M} \Big( !\mathit{S}_{n,j} \Big) \]
		
		\item
		$necessary()$: it is the boolean function that returns true if the $n$-rule is neither \textit{shadowed} or \textit{redundant} in at least one filtering point.
		
		\[ necessary() = \bigvee_{i=0}^{M} \Big( \mathit{P}_{n,i} \Big) \]
		
	\end{itemize}
	
	\item
	freedom degree equation: it represents a check on the degree of freedom that the model has, this equation adds a constrain such that limits this flexibility. It imposes that at least one $\mathcal{S}_{n,i}$ has to be set to true on the list of filtering points, otherwise the optimization engine puts all $\mathcal{S}_{n,i}$ to false.
	
	%	\[\mathcal{F}_{n,p}^{\alpha} = \bigvee_{i=0}^{M} \Big( \mathcal{S}_{n,i} \Big) = 1 \]
	\begin{empheq}[box=\myBox]{equation*}
	\mathcal{F}_{n,p}^{\alpha} = \bigvee_{i=0}^{M} \Big( \mathcal{S}_{n,i} \Big) = True
	\end{empheq}
	
	\begin{itemize}
		\item 
		$\mathcal{F}_{n,p}^{\alpha}$: it is the name of the equation that represent the $n$-rule in the $p$ traffic path;
		
		\item
		$\bigvee_{i=0}^{M}$: it builds an expression in which the boolean variables are placed in \textit{OR} condition with the others. This expression slides all the $M$ filtering points, given a specific $p$ traffic path.
	\end{itemize}
	
	\item
	number delimiter equation: it represents a check on the number of rules that a filtering point has enforced on itself, because some security controls has strictly performance requirements or implementation requirements that cannot allow more than a certain number of rules.
	
	%\[\sum_{n=0}^{R} countOneIfTrue(\mathit{P}_{n,i}) \leq  \mathcal{M}_{i}\]
	\begin{empheq}[box=\myBox]{equation*}
	\sum_{n=0}^{R} countOneIfTrue(\mathit{P}_{n,i}) \leq  \mathcal{M}_{i}
	\end{empheq}
	
	\begin{itemize}
		\item
		$\mathcal{M}_{i}$: is identifies the maximum value of number of rules that the $i$ filtering point can enforce that is give in input; 
		
		\item
		$countOneIfTrue(\mathit{P}_{n,i})$: it is the boolean function that returns the value 1 if the $n$-rule is enforced in this filtering point, otherwise returns 0;
		
		\[
		countOneIfTrue(\mathit{P}_{n,i}) = \Bigg\{ \begin{array}{lr}
		1, & \text{if } \mathit{P}_{n,i} = true\\
		0, & \text{if } \mathit{P}_{n,i} = false\\
		\end{array} \]
		
		\item
		$\sum_{n=0}^{R}$: it counts how many rules are settled in the filtering point.
	\end{itemize}
\end{itemize}

\subsection{Integer equation}

The integer equation made this model a SMT problem, because it takes advantages of, not only boolean logic, but others theories like integers or real numbers.
Moreover there is the clause that this value has to be minimize and this leads this problem to be classified as MaxSMT.

\begin{itemize}
	\item 
	cost equation: it represents the evaluation of the performance based on the number of rules injected for each filtering point. It sums all the costs of the $M$ points and it finds the minimal value.
	
	%\[\mathcal{C} = min \Bigg\{ \sum_{i=0}^{M} \mathcal{P}_{i}(n) \Bigg\} \]
	\begin{empheq}[box=\myBox]{equation*}
	\mathcal{C} = min \Bigg\{ \sum_{i=0}^{M} \mathcal{P}_{i}(n) \Bigg\}
	\end{empheq}
	
	\begin{itemize}
		\item
		$min$: is the arithmetical function that finds the minimum value given an expression; 
		
		\item
		$\mathcal{P}_{i}(n)$: it is the representation of the performance evaluation based on $n$-number of rules in the $i$ filtering point;		
		
		\item
		$\sum_{i=0}^{M}$: it sums all the performance values of all the filtering points available for the distribution;
		
		\item
		$n$: it is the number of rules which are enforced on the $i$ filtering point.
	\end{itemize}
\end{itemize}

