-
Notifications
You must be signed in to change notification settings - Fork 0
/
sknife.pl
83 lines (73 loc) · 3.57 KB
/
sknife.pl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
%Finds Partitioning for appliction AppId given the labelling Labelling
%Every query returns a new different partitioning (not only minimal)
sKnife(AppId,Labelling, Partitioning) :-
application(AppId, Hardware, Software),
hardwareOK(Labelling,Hardware),
softwareLabel(Labelling,Software, LabelledSoftware),
softwareOk(Labelling,LabelledSoftware),
partitioning(LabelledSoftware,0, inf,[], Partitioning).
%Finds Partitioning with at most PLimit partitions for appliction AppId given the labelling Labelling
%Every query returns a new different partitioning (not only minimal)
sKnife(AppId, Labelling,PLimit,Partitioning) :-
application(AppId, Hardware, Software),
hardwareOK(Labelling,Hardware),
softwareLabel(Labelling,Software, LabelledSoftware),
softwareOk(Labelling,LabelledSoftware),
partitioning(LabelledSoftware, 0,PLimit,[], Partitioning).
%check the labelling of hardware components
hardwareOK(Labelling,[H|Hs]) :-
hardware(H, Data, Characteristics,_),
labelC(Labelling,Data, Characteristics, (TData,TChar)),
gte(TChar,TData), %check if an hardware component is trusted for the level of its data
hardwareOK(Labelling,Hs).
hardwareOK(_,[]).
%labels software components with Type of Data and Type of Characteristics
softwareLabel(Labelling,[Sw|Sws],[(Sw,TData,TChar)|LabelledSws]):-
software(Sw, Data,Characteristics,_,_),
labelC(Labelling,Data, Characteristics,(TData,TChar)),
softwareLabel(Labelling,Sws,LabelledSws).
softwareLabel(_,[],[]).
softwareOk(Labelling,LabelledSoftware):-
\+ (
member((Sw,TData,TChar), LabelledSoftware),
lt(TChar,TData),
externalLeak(Labelling,[Sw], [] ,TData, LabelledSoftware)
).
externalLeak(Labelling,LinkedSW, Visited,TData, LabelledSoftware):-
member(Sw, LinkedSW), \+(member(Sw, Visited)), member((Sw,_,TChar), LabelledSoftware),
lt(TChar,TData),
software(Sw, _,_,_,(LinkedHW,_)),
\+ trustedHW(Labelling,LinkedHW, TData).
externalLeak(Labelling,LinkedSW, Visited,TData, LabelledSoftware):-
member(Sw, LinkedSW), \+(member(Sw, Visited)), member((Sw,_,TChar), LabelledSoftware),
lt(TChar,TData),
software(Sw, _,_,_,(LinkedHW,VisitLinkedSW)),
trustedHW(Labelling,LinkedHW, TData),
externalLeak(Labelling,VisitLinkedSW, [Sw|Visited], TData, LabelledSoftware).
%given the list of linked hardware, check if it is trustable with the data
trustedHW(Labelling,LinkedHW, TData):-
\+ (
member(HW,LinkedHW),hardware(HW,_,Characteristics,_),
characteristicsLabel(Labelling,Characteristics, CLabel), lowestType(CLabel, MinCType),
lt(MinCType, TData)
).
partitioning([(S,TData,TChar)|Ss], Npar,PLimit,Partitions, NewPartitions) :-
software(S,_,_,_,_),
partitionCharLabel(TChar,TData,TCP),
select( ((TData,TCP), P), Partitions, TmpPartitions),
PNew = ( (TData,TCP), [S|P]),
partitioning(Ss, Npar, PLimit,[PNew|TmpPartitions], NewPartitions).
partitioning([(S,TData,TChar)|Ss], Npar,PLimit,Partitions, NewPartitions) :-
software(S,_,_,_,_),
partitionCharLabel(TChar,TData,TCP),
%\+ member( ((TData,TCP), _), Partitions), % comment this to find all solutions combinatorially
P = ( (TData,TCP), [S]),
NewNpar is Npar + 1,
NewNpar =< PLimit,
partitioning(Ss, NewNpar,PLimit,[P|Partitions], NewPartitions).
partitioning([],_,_,P,P).
labelC(Labelling,Data, Characteristics, (MaxType,CharactSecType)):-
dataLabel(Labelling,Data,Labels),
highestType(Labels,MaxType),
characteristicsLabel(Labelling,Characteristics, ListOfCharactTypes),
lowestType(ListOfCharactTypes, CharactSecType).