# Secure Partitioning of Cloud Applications, with Cost Look-Ahead
## 5 Determining the Minimal Safe Partitioning
### Declarative Strategy for the Minimal Safe Partitioning
The predicate recursively scans the list of labelled software components (LabelledSoftware) to place every component starting from a partitioning (Partitioning) that will be updated in the resulting partitioning (NewPartitioning). The domains of the resulting partitioning are data-consistent and reliable by construction. Every software component is placed in a domain with the same secrecy label to satisfy the data consistency of the domain. Trusted components are placed together in domains with the trust label named safe, indicating that all the hosted components are trusted. Untrusted components are placed in the domain with the same trust label, in order to create reliable domains. If the domain needed by a component is not in the starting partitioning, it is created with the correct labels and added to the partitioning. partitioning/3 has two main clauses (lines 22 and 27) and the empty software list case that leaves the partitioning unmodified (line 32). The first case describes the situation in which a software element can be placed on a domain already created. After determining the labelling of the hosting domain (line 23), the library predicate select/3 checks if such a domain is already created in the partitioning (line 24) and extracts it. Then, an updated domain is created by adding the current software component (line 25). Finally, partitioning/3 recurs on the rest of the software list, giving as the starting partitioning the old partitioning with the updated domain ([DNew|TmpPartitioning] of line 26). The second clause of the predicate (line 27) describes the situation in which the domain that has to host the software component is not already in the input partitioning. The initial step to determine the hosting-domain labelling is the same as the previous clause (line 28). Then, there is an explicit check that such a domain is not already in the partitioning (line 29). At this point, the new domain is created (line 30) and it is included in the partitioning during the recursive call ([DNew|Partitioning] of line 31). Figure 2 sketches the steps followed by our methodology to determine the minimal partitioning. As a safe partitioning example, the output of SKnife is represented by the four domains  
* ((top,safe),[AppManager,db,authenticator]),
* ((medium,safe),[UserConfig]),
* ((low,safe),[LapiGateway]),
* ((top,low),[aLearning]). where each domain is represented by their triple (DTDData, DTChar,HostedSw), where DTData and DTChar are a pair of labels (or safe) and HostedSw is a list of software components. In the following, we outline a proof to demonstrate that SKnife computes the minimal safe partitioning of the input application, if any. Proof. : **of Partitioning Minimality. ** As aforementioned, SKnife's main predicate fails if the application is non-safely partitionable. This is checked by hardware0k/2 of Listing 2 and software0k/2 of Listing 3. The minimum number of domains is not fixed for all possible applications, because it depends on the number of security types of the lattice and on the labelling of the application to be placed. To prove that the result of SKnife is the minimal partitioning, it is enough to prove that the predicate partitioning/3 of Listing 5 creates the minimal partitioning. We sketch the proof of minimality by defining the invariant of the partioning/3 predicate, which maintains the  
Figure 2: Overview of SKnife methodology. safety of the partitioning. Then, we show by induction that the invariant is preserved and that the resulting partitioning is minimal and unique. A partitioning is a set of domains. We denote a domain as a triple \((d,c,sw)\) where \(d\) is the secrecy label given by data, \(c\) is the trust label given by characteristics and \(sw\) is the list of software components hosted by the domain. The predicate partitioning/3 implements a function  
\[partitioning:S\times P\to P\]  
where \(S\) is the software components set and \(P\) is the partitioning set.