-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathproprov.vtt
353 lines (264 loc) · 11.5 KB
/
proprov.vtt
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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
WEBVTT
Kind: captions
Language: en
00:00:01.120 --> 00:00:03.440
This training session will cover ProProv.
00:00:05.920 --> 00:00:09.600
ProProv is a language and system
for specifying provenance policies
00:00:09.600 --> 00:00:12.720
over graphs representing the
provenance of secure computations.
00:00:13.360 --> 00:00:18.080
Policies in ProProv can be expressed as logical
statements or predicates over provenance graphs.
00:00:18.880 --> 00:00:23.280
ProProv also contains a graphical user
interface to specify and test policies.
00:00:25.680 --> 00:00:28.960
Now let's introduce the syntax
of the ProProv language.
00:00:28.960 --> 00:00:34.160
We use t as a generic variable to range over
the possible province node types which include:
00:00:34.160 --> 00:00:41.360
account agent, node agent, agent, data entity,
contract entity, key entity, entity, and activity.
00:00:41.360 --> 00:00:45.360
The agent type means that the node can be
either an account agent or a node agent.
00:00:45.360 --> 00:00:50.480
The entity type means that the node can be either
a data entity, a contract entity, or a key entity.
00:00:51.200 --> 00:00:55.360
Next, we use e as a generic variable
to range over possible edge labels
00:00:55.360 --> 00:01:00.880
which are the provenance relations between nodes.
The possible edge labels are: was derived from,
00:01:00.880 --> 00:01:06.800
was attributed to, was generated by, used,
acted on behalf of, and was associated with.
00:01:07.520 --> 00:01:12.240
Next, we use x as a generic variable to range
over variable names which can be any string.
00:01:12.960 --> 00:01:17.920
Next, we use n as a generic variable to arrange
over provenance node names which can also be any
00:01:17.920 --> 00:01:23.120
string, and we use p as a generic variable to
range over provenance policies, which can be:
00:01:23.120 --> 00:01:28.720
the negation of a policy p, the conjunction of
two policies, the disjunction of two policies,
00:01:28.720 --> 00:01:32.560
the for all keyword followed by
a variable, a colon, a type t,
00:01:32.560 --> 00:01:38.320
a dot, and a policy p and can be
pronounced "for all x of type t p holds".
00:01:38.320 --> 00:01:44.320
Next, a policy can consist of the exists keyword
followed by a variable, a colon, a type t, a dot,
00:01:44.320 --> 00:01:49.520
and a policy p and can be pronounced "there
exists an x of type t such that p holds".
00:01:50.080 --> 00:01:55.440
Next, the policy p1 can imply a policy p2,
and lastly, a policy can consist of an edge
00:01:55.440 --> 00:01:59.600
label followed by two nodes separated
by a comma and enclosed in parentheses.
00:02:02.160 --> 00:02:08.240
The negation policy asserts that policy p is not
true. We can specify a negation policy using the
00:02:08.240 --> 00:02:13.520
graphical user interface by clicking the drop-down
policy menu and selecting not. After making the
00:02:13.520 --> 00:02:18.080
selection, another drop-down menu will appear
for another policy selection. The pane at the
00:02:18.080 --> 00:02:22.800
bottom right of the screen will print the policy
in the ProProv language as it is constructed.
00:02:24.480 --> 00:02:31.120
The conjunction policy, also called "logical
and", asserts that both policy p1 and p2 are true.
00:02:31.120 --> 00:02:34.960
This policy can be specified using the
interface by clicking the policy drop-down
00:02:34.960 --> 00:02:41.040
menu and selecting and. After this selection,
two more policy menus will appear for p1 and p2.
00:02:42.720 --> 00:02:48.240
The disjunction policy, also called "logical
or", asserts that either policy p1 is true
00:02:48.240 --> 00:02:53.360
policy, p2 is true, or both p1 and p2
are true. This policy can be specified
00:02:53.360 --> 00:02:57.200
using the interface by clicking the
policy drop-down menu and selecting or.
00:02:57.200 --> 00:03:04.320
After this selection, two more policy
menus will appear for p1 and p2
00:03:04.320 --> 00:03:10.960
The universal policy asserts that policy p is true
for every provenance node of type t. Variable x
00:03:10.960 --> 00:03:16.720
can be used in p. This policy can be specified
using the interface by selecting for all.
00:03:16.720 --> 00:03:21.440
After this selection, three boxes will appear:
a typable box to enter a variable name,
00:03:21.440 --> 00:03:26.080
a drop-down menu to select a provenance node
type, and a drop-down menu to select a policy.
00:03:28.160 --> 00:03:33.200
The existential policy asserts that policy p
is true for some provenance node of type t.
00:03:33.760 --> 00:03:39.840
Variable x can be used in p. This policy can be
specified using the interface by selecting exists.
00:03:39.840 --> 00:03:44.400
After this selection, three boxes will appear:
a typable box to enter a variable name,
00:03:44.400 --> 00:03:48.880
a drop-down menu to select a provenance node
type, and a drop-down menu to select a policy.
00:03:50.800 --> 00:03:56.400
The implication policy asserts that if
policy p1 is true then policy p2 is true.
00:03:56.400 --> 00:04:00.400
This policy can be specified using
the interface by selecting implies.
00:04:00.400 --> 00:04:04.720
After the selection, two boxes will
appear for policy p1 and policy p2.
00:04:06.800 --> 00:04:12.960
The edge policy asserts that there is an edge with
label e between node n1 and node n2, where e can
00:04:12.960 --> 00:04:18.880
be any one of six provenance relations, which
includes was attributed to, was derived from,
00:04:18.880 --> 00:04:23.840
was generated by, used, acted on
behalf of, and was associated with.
00:04:23.840 --> 00:04:27.760
This policy can be specified by
selecting any one of the edge relations.
00:04:27.760 --> 00:04:32.000
After the selection is made, two boxes
will appear for node n1 and node n2.
00:04:34.480 --> 00:04:39.200
Now let's look at some examples of how we can
construct provenance policies using the ProProv
00:04:39.200 --> 00:04:43.680
interface. During this study, the panel on the
right will have five input provenance graphs
00:04:43.680 --> 00:04:47.760
to test your policy on. A graph that has a
green checkmark means that the graph should
00:04:47.760 --> 00:04:53.120
satisfy your policy. A graph that has a red
X means the graph should violate your policy.
00:04:53.120 --> 00:04:57.760
Lastly, ProProv is case insensitive; this
means that when typing provenance object names,
00:04:57.760 --> 00:05:00.960
it does not matter whether you
use upper or lower case letters.
00:05:00.960 --> 00:05:03.920
Now let's construct a policy
to ensure the activity average
00:05:03.920 --> 00:05:08.720
used data entity SalaryB. We can
construct this policy by selecting used,
00:05:08.720 --> 00:05:13.120
then typing average as the source node
and salary b as the destination node.
00:05:13.120 --> 00:05:17.360
We can then evaluate our policy on the input
graphs by clicking the evaluate button.
00:05:19.200 --> 00:05:24.160
Next, we want to write a policy to ensure that
data entity AverageSalary was not derived from
00:05:24.160 --> 00:05:30.800
SalaryC. We can construct this policy by first
selecting not, then selecting was derived from.
00:05:30.800 --> 00:05:37.840
Then we can type AverageSalary as the source node
and we can type SalaryC as the destination node.
00:05:47.040 --> 00:05:51.680
Next, we want to write a policy to ensure
the activity Average used key entity KeyB
00:05:51.680 --> 00:05:57.200
and KeyB was attributed to account agent Bob.
We can construct this policy by selecting and.
00:05:57.200 --> 00:06:01.680
Then for the first policy box, we can select
used and type Average for the source node,
00:06:03.360 --> 00:06:09.920
and KeyB for the destination node. For the
second policy, we can select was attributed to
00:06:09.920 --> 00:06:19.840
and type KeyB for the source node
and Bob for the destination node.
00:06:23.440 --> 00:06:27.040
Next, we want to write a policy to
ensure that there is some data entity
00:06:27.040 --> 00:06:33.040
that AverageSalary was derived from. We can
construct this policy by first selecting exists.
00:06:33.040 --> 00:06:37.680
We then enter a variable name, which we choose
to be d, we select the appropriate type,
00:06:37.680 --> 00:06:42.080
which is data entity, and for the
policy we select was derived from.
00:06:42.080 --> 00:06:47.840
For the source node, we type average salary,
and for the destination node, we select d.
00:06:54.880 --> 00:06:59.680
Next, we want to write a policy to ensure
for every data entity, if activity average
00:06:59.680 --> 00:07:05.280
used the data entity, then the data entity was
attributed to either Bob, Alice, or Mallory.
00:07:05.280 --> 00:07:11.040
To construct this policy, we first select for
all. We then enter a variable name d, select the
00:07:11.040 --> 00:07:17.200
appropriate type, which is data entity, and select
the implies policy. Then for the first policy,
00:07:17.200 --> 00:07:22.800
we select used and type average as the source
node, and select d as the destination node.
00:07:25.520 --> 00:07:30.080
For the second policy, we select
or, then select was attributed to
00:07:30.080 --> 00:07:35.680
for the first policy and select d as the source
node and type Bob for the destination node.
00:07:41.360 --> 00:07:46.240
For the second policy, we select or and for
the first policy we select was attributed to
00:07:46.240 --> 00:07:51.600
for the first policy and select d for the source
node and type Alice for the destination node,
00:07:56.080 --> 00:08:00.000
and for the second policy, we select
was attributed to and select d
00:08:00.000 --> 00:08:11.840
for the source node and type
Mallory for the destination node.
00:08:16.880 --> 00:08:19.520
If during this study you type an incorrect policy,
00:08:19.520 --> 00:08:24.320
ProProv will indicate on which graphs your
policy did not succeed. You can then click ok,
00:08:24.320 --> 00:08:28.400
after which you can try again or click save
and continue to proceed to the next question.
00:08:28.960 --> 00:08:31.440
This concludes the ProProv training.