# Secure Partitioning of Cloud Applications, with Cost Look-Ahead
## 5 Determining the Minimal Safe Partitioning
### Declarative Strategy for the Minimal Safe Partitioning  
We use the notation \(P\models\mathcal{L}\) to indicate that a partitioning \(P\) satisfies a labelling \(\mathcal{L}\) when the partitioning is safe with \(\mathcal{L}\). Safe partitionings split safely partitionable applications into a set of data-consistent and reliable domains. The software components of a safely partitionable application can be split and placed on SK domains. A domain is a triple (DTData, DTChar, HostedSw) where DTData is the secrecy label of the domain, DTChar is the trust label of the domain and HostSw is the list of the software components hosted by the domain. Inside a domain, the software components share the same environment. To avoid placing components in an environment containing data that they are not able to manage, a domain must be _data-consistent_, as defined in Equation (4)  
\[ \begin{split}\forall\texttt{software}(\texttt{Sw},\texttt{Data}, \texttt{Characteristics},\texttt{\_})\in\texttt{HostedSw}:\\ \texttt{labelC}(\texttt{Data},\texttt{Characteristics},(\texttt{ CTData},\texttt{\_}))\rightarrow\texttt{DTD}\texttt{data}=\texttt{CTData}\end{split}  \tag{4}\]  
meaning that in a domain there is no software component with a secrecy label different from the domain secrecy label, i.e., all the software components hosted by a domain have the same secrecy label of the domain. This property avoids placing a software component in a domain that contains data more sensitive than those the component is supposed to deal with. Another aspect to consider is that untrusted components bring out the risk of leaking sensitive data to other components of the domain or to linked components outside the domain. In order to isolate such components, the domains must be _reliable_, as defined in Equation (5)  
\[ \begin{split}\forall\texttt{software}(\texttt{Sw},\texttt{Data}, \texttt{Characteristics},\texttt{\_})\in\texttt{HostedSw}:\\ \texttt{labelC}(\texttt{Data},\texttt{Characteristics},(\texttt{ CTData},\texttt{CTChar}))\rightarrow\texttt{CTData}\geq\texttt{CTChar}\\ \lor\\ \forall\texttt{software}(\texttt{Sw},\texttt{Data},\texttt{Characteristics}, \texttt{\_})\in\texttt{HostedSw}:\\ \texttt{labelC}(\texttt{Data},\texttt{Characteristics},(\texttt{ CTData},\texttt{CTChar}))\rightarrow\texttt{CTChar}=\texttt{DTChar}\end{split}  \tag{5}\]  
meaning that all the software components of a domain are either trusted or have the same trust label as the domain. Domains hosting only trustable software components are considered secure from data leaks. Every component can manage its data and can exchange it outside the domain without the risk of leaks, according to the trust assigned by the developer. Untrusted components must be strongly isolated, and they can share a domain only with other untrusted components having the same trust label, in order to have a homogeneous level of trust inside the domain and mitigate the danger of a data leak. The top-level sKnife/3 predicate (Listing 4) finds the safe partitioning of a safely partitionable application. After retrieving the application information (line 17), it performs two main steps. First, it checks whether the application is safely partitionable (lines 18-20) and then, it creates the set of data-consistent and reliable domains, splitting the software component across them (line 21), starting from an empty partitioning (I of line 21). ```
16 sknife(AppId,Labelling,Partitioning):-
17 application(AppId,Hardware,Software),
18 hardwareOK(Labelling,Hardware),
19 software.label(Labelling,Software,LabelledSoftware),
20 softwareOK(Labelling,LabelledSoftware),
21 partitioning(LabelledSoftware,[],Partitioning). ```  
Listing 4: The sKnife/3 predicate. The partitioning/3 predicate is listed in Listing 5 and it has the task of splitting the labelled software components, placing them in data-consistent and reliable domains.