-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathSTATUS.txt
94 lines (77 loc) · 3.65 KB
/
STATUS.txt
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
84
85
86
87
88
89
90
91
92
93
TECHNICAL COMPONENTS
Language models:
- "simple": Subroutines without sharing.
- "sharing" Subroutines with sharing of arguments and/or address-taken locals
- "coroutine" Adds coroutines to a subroutine model.
Trace properties for confidentiality, integrity.
- Hyper-eager
- Eager
- Generic notions of trace confidentiality/integrity
- Hyper-eager as instance of generic notion.
- Eager as instance of generic notion.
- Lazy as instance of generic notion.
Properties for control correctness.
- Subroutines (WBCF)
= Control separation
+ Entry integrity
+ Return integrity
- Coroutines (Well Structured Control Flow(?))
as above + Yield integrity.
Program Logic Perspective (PLP) -- Motivation?
(Combines trace properties + control correctness.)
- Call rule
- Yield rule
- Insensitivity rules (for subroutine, coroutine cases).
Micro-policies enforcing properties.
Options for subroutines:
- Eager with depth tags.
- Lazy tagging/clearing with depth tags.
- Lazy tagging/clearing with per-activation tags.
Coroutines use per-coroutine tags.
- Eager.
- Maybe lazy? (would need a motivation)
Testing.
- Eager micro-policy supporting simple subroutines + WBCF.
- What else do we need? How much is code generation already done?
---------
Technical open questions:
*TODO*: Decide what to do when confidentiality variants failstop. (Current Coq: ignore such runs, in spirit of termination insensitivity).
*TODO*: Decide whether to have a separate policy state. (Current Coq: there is one.)
(Note: whether or not this is in the Coq, could elide in the paper.)
*TODO*: Decide which of the two versions of lazy integrity to present/favor.
*TODO*: Readily testable lazy integrity.
--------
Coq files:
Machine.v : abstract characterization of machines
MachineImpl.v : concretization of machine as a RISC-V machine
Trace.v : characterization of traces
ObsTrace.v : similarity of observation traces
TraceProperties.v : generic notions of (hyper)eager trace conf/integ
SubroutineSimple.v : "simple" model, hyper-eager and eager (w/ and w/o use of generic notions), WBCF, PLP Call and Insensitivity rules.
SubroutineShared.v : "shared" model, hyper-eager and eager (using generic notions), WBCF, PLP Call and Insensitivity rules.
Coroutine.v : "coroutine" model on top of shared model, hyper-eager and eager (using generic notions), WSCF, PLP yield and insensitivity rules.
Lazy.v : generic notion of lazy trace integrity, "coroutine" model, lazy integrity (using generic notion), eager confidentiality (unchanged), WSCF (unchanged).
*TODO*: Probably needs more comments to be intelligible within the group.
*TODO*: Rename everything as needed to match latex names, once those are settled.
*TODO*: Separate file for PLP.
Logic.v : Will include PLP rules.
*TODO*: PIPE model and implemented properties
Policy.v : abstract characterization of PIPE policy
TagMachine.v : characterization of PIPE parameterized by policy
[policy].v: various implementations of policies
---------
Paper Status:
1 Intro: ready to be reviewed, except that contributions need to be updated.
2 Threat model: need to explain annotation philosophy/scheme
3 Examples: existing stuff needs review: is example format good? Does it need more than two examples?
4 Traces: needs review (there have been some changes)
5 LSE. Needs rework to reflect focus on stepwise properties.
Coroutines are TBD.
6 WBCF/WSCF. Lots to TBD.
7 Enforcement. Needs review. Extension to coroutines TBD.
8 Testing. TBD.
9 Lazy properties and Enforcement. Lots TBD.
10 CHERI? TBD
11 Software enforcement? TBD
12 Related Work. Needs rewriting to please the Danes and Belgians (and to take account of most recent pubs)
13 Future Work. Needs review.