forked from aosabook/500lines
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathanalysis.als
More file actions
38 lines (33 loc) · 1.08 KB
/
Copy pathanalysis.als
File metadata and controls
38 lines (33 loc) · 1.08 KB
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
/**
* analysis.als
* End-to-end analysis of security properties
*/
module analysis
open flow
// General security properties
sig TrustedModule, MaliciousModule in DataflowModule {}
sig CriticalData, MaliciousData in Data {}
// No malicious module should be able to access private data
assert Confidentiality {
no m: DataflowModule - TrustedModule, t: Time |
some CriticalData & m.accesses.t
}
// No malicious data should ever flow into a trusted module
assert Integrity {
no u: TrustedModule, t: Time |
some MaliciousData & u.accesses.t
}
fact {
-- no malicious module begins with critical data
no m: MaliciousModule | some CriticalData & m.accesses.init
-- no trusted module begins with malicious data
no m: TrustedModule | some MaliciousData & m.accesses.init
-- no module is both trusted and malicious
no TrustedModule & MaliciousModule
-- every module is either trusted or malicious
DataflowModule = TrustedModule + MaliciousModule
-- no data is both critical and malicious
no CriticalData & MaliciousData
}
check Confidentiality for 3
check Integrity for 3