# Secure Partitioning of Cloud Applications, with Cost Look-Ahead
## 4 A Declarative Solution: SKnife
### Declarative Modelling Applications and Labelling  
Application developers model their applications through suitable Prolog facts and clauses, as  
```
application(AppId,Hardware,Software).
```  
where AppId is the application identifier, Hardware is the list of hardware components interacting with the application and Software is the list of software components to place on the SK.  
**Example.** The iotApp1 application of our example is declared by the fact  
```
application(iotApp1,[network,disk],[userConfig,appManager,authenticator,ailearning,apiGateway,db]).
```  
Software and hardware components are declared as in  
```
software(SwId,Data,Characters,Cost,[LinkedW,LinkedSW]). hardware(HwId,Data,Characters,[LinkedW,LinkedSM]).
```  
where SwId and HwId are the unique identifiers of each component, Data is the list of names of the data managed by the component, Characts is the list of names of the component characteristics, LinkedW is the list of linked hardware components and LinkedSW is the list of linked software components. The only difference is the components definition Cost, which is the integer value representing the migration cost of the software.  
**Example.** The db and disk components are declared as  
```
software(db,[iotMeasurements,userPreferences,cryptedData],[dbms],50,([disk],[userConfig,appManager])). hardware(disk,[cryptedData],[fromProvider],([1,[db])).
```  
Application developers must also declare a security lattice formed by ordered labels and they have to label the relevant data of the application and the relevant characteristics of the components. The higher the label of the data, the higher the secrecy of the data. Similarly, the higher the label of a characteristic, the higher the trust in the characteristic. We call the labels assigned to the data _secrecy labels_ and the labels assigned to the characteristics _trust labels_.  
Every data type and characteristic can be labelled using  
```
tag(Name,Label).
```  
where Name is the name of the data or characteristic to be labelled and Label is the assigned label. Obviously, the labels must be part of the lattice. We call _labelling_ the set of all pairs \(\langle\texttt{Name},\texttt{Label}\rangle\) where all data and characteristics have been assigned a security label.  
**Example.** The label of the data and the characteristics of the Disk are declared as  
```
tag(cryptedData,low). tag(fromProvider,low).
```  
which represents the cryptedData data with a low secrecy label and the fromProvider characteristic with a low trust label.  
The probability of changing the label for a data type or characteristic is declared as  
```
tagChange(DC,label,P).
```  
representing how the data or characteristic DC changes to label with probability P. To have the full distribution for DC we need facts for every label of the security lattice and the sum of the probabilities of those facts must be 1.  
**Example.** The probabilities of changing the label of the data and the characteristics of the Disk are declared aswhich represents the cryptedData data with a probability of 100% to have a low secrecy label and the fromProvider characteristic with a probability of 60% to remain low, 30% to change to medium and 30% to change to top.