# Secure Partitioning of Cloud Applications, with Cost Look-Ahead
## 4 A Declarative Solution: SKnife
### Safe Partitioning  
Our methodology assigns to every component a pair of labels, one indicating its secrecy level and one indicating its trust level. A component is _trusted_ if its trust label is greater than or equal to its secrecy label; otherwise, it is considered _untrusted_. All the comparisons between labels are based on the ordering of the security lattice. A trusted component is able to manage its data without the risk of leaking them.  
The label assignment to a component is performed by the predicate labelC/4 of Listing 1, using the lists of data and characteristics of the component and the labelling of the application.  
```
1 labelC(Labelling,Ds,Cs,OType,CType)):-
2 dataLabel(Labelling,Ds,DLabels),
3 highestType(DL_abels,OType),
4 characteristicsLabel(Labelling,Cs,CLabels),
5 lowestType(CLabels,CType).
```  
The secrecy label is determined by the highest label of its data in order to consider the most critical data managed by the component. The trust label is determined by the lowest label of its characteristics because the worst characteristic could compromise the trust of the component, e.g., a component using a simple logging library and a certified encryption software could be endangered by a bug in the former.  
A component without relevant characteristics is considered reliable and its trust label is the highest of the security lattice. We choose this level of granularity (i.e., the developer labels the data and characteristics instead of directly labelling the components) to have a better insight into the application and to have a more accurate understanding of the situations in which the application is non-safely partitionable.  
Untrusted components can leak their data to directly linked components. If such components have a trust label lower than the leaked data they can propagate the leakage through their links. If such data reach a hardware component, then an _external leak_ occurs. An external leak is a path from an untrusted software component to a hardware component where all the components of the path have a trust label lower than the secrecy label of the first software component of the path. The presence of such paths indicates the potential for data leakage from an untrusted component toward the outside of the SK that is not avoidable by the partitioning.  
Recall that an application is called _safely partitionable_ when there is no leakage outside the SK, i.e., all its hardware components are trusted and all its untrusted software components do not incur any external leaks.  
The predicate hardware0K/2 of Listing 2 checks that all the hardware components of the application are trusted, which avoids hardware attacks that cannot be contrasted by the SK partitioning.  
```
6[]hardwareOK(Labelling,[M|Hs]):-
7 hardware(H,Ds,Cs,_),
8 label(Labelling,Ds,Cs,(TData,TChar)),
9 get(TChar,TData),
10 hardwareOK(Labelling,Hs).
11 hardwareOK(_,[]).
```  
The predicate recursively scans the list of hardware components to check their labelling. Initially, information about a single component is retrieved (line 7), and then the labelling of the hardware component is determined (line 8). The predicate checks for the component trustability (line 9), where gte/2 checks if the trust is greater than or equal to the secrecy. Finally, hardwareOK/2 recurs on the rest of the list (line 10) until it is empty (line 11).  
Similarly, the predicate softwareOK/2 of Listing 3 checks that no software component (line 13) that is untrusted (line 14) has an external leak toward an untrusted hardware component (line 15).  
```
12 softwareOK(Labelling,LabelledSoftware):-
13\+(member((Sw,TData,TChar),LabelledSw),
14 lt(TChar,TData),
15 externalLeak(Labelling,[Sw,],TData,LabelledSw)).
```  
Listing 3: The softwareOK/2 predicate.