# Secure Partitioning of Cloud Applications, with Cost Look-Ahead
## 5 Determining the Minimal Safe Partitioning
### Labels Suggestions  
Not all existing applications are safely partitionable, precluding the possibility of finding a safe partitioning. To assist application developers in these situations we show how SKnife can suggest _relaxed labellings_ of application data or characteristics that make the application safely partitionable. These suggestions reduce the secrecy or increase the trustability of components, relaxing the labelling of an application in order to find a safe partitioning. This feature is intended to help the review of an application, preventing the risk of leaking the confidentiality of data.  
The basic version of SKnife either finds the minimal partitioning or fails if there is a risk of a data leak given by untrusted components. To support the suggestions feature, we suitably modified SKnife to individuate the source of a failure and to retry the partitioning after relaxing the labelling of such a source.  
Listing 6 lists the main code of the labelling-suggestion feature. The main predicate of the refinement prototype is sknife/3 (line 33). It has as the first variable the application identifier Appld, as in the base version. The second variable is the list of relaxed labelling NewTags, pairs of data/characteristic names with new labels. The third variable Partitioning is the safe partitioning found with the relaxed labelling. Note that this predicate does not compute a unique solution. Indeed, for every query, a different relaxed labelling with the associated safe partitioning is computed. This allows SKnife to give the developer different suggestions.  
```
3 sknife(Appld,NewTags,Partitioning):-
4 application(Appld,Hardware,Software),
5 eligiblePartitioning(Hardware,Software,NewTags,Partitioning).
6 eligiblePartitioning(H,S,T,P):-eligiblePartitioning([],H,S,T,P).
7 eligiblePartitioning(Tags,Hardware,Software,Tags,Partitioning):-
8 partitioningResult(Tags,Hardware,Software,Partitioning,ok).
9 eligiblePartitioning(Tags,Hardware,Software,NewTags,Partitioning):-
10 partitioningResult(Tags,Hardware,Software,...,Ko(E,DT,CT)),
11 tagsOK(Tags,Ko(C,DT,CT),TmpTags),
12 eligiblePartitioning(TmpTags,Hardware,Software,NewTags,Partitioning).
```  
Listing 6: The sknife and eligiblePartitioning predicates.  
The eligiblePartioning/4 predicate (line 36) initialises the relaxed labelling as an empty list []. The eligiblePartioning/5 predicate (lines 37-42) has two clauses. The first one determines an eligible partitioning, indicated by the ok fact (line 38). The second one acknowledges that the application is non-safely partitionable with the current labelling, indicated by the ko(C, DT, CT) fact (line 40). The information given by this fact is about the untrusted component C involved in the data leak and its pair of labels DT and CT. That information is used to relax the labelling, by the tagsOK/3, which generates alternative new labels (TmpTags) to be added to the previous one (Tags) predicate (line 41). These labels are generated by increasing the characteristic labels of the component C and decreasing its data labels. Then, the new labels are used to determine an eligible placement, querying recursively eligiblePartioning/5 (line 42). Note that an eligible partitioning is eventually determined. In the worst-case scenario, the data labels are relaxed to the lowest security label (i.e., low) and the characteristic labels are relaxed to the highest security label (i.e., top). For the sake of presentation, the full code is omitted.  
The predicates that check if an application is safely partitionable are hardwareOk/2 and softwareOk/2. These predicates are modified in order to return the fact ko(C, DT, CT) for every component responsible for a failure when the application is non-safely partitionable.