-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathibos.maude
814 lines (745 loc) · 34 KB
/
ibos.maude
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
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
set include BOOL off .
fmod BOOL-NO-BUILTIN is
pr TRUTH-VALUE .
op _and_ : Bool Bool -> Bool [assoc comm prec 50] .
op _or_ : Bool Bool -> Bool [assoc comm] .
op not_ : Bool -> Bool .
op _==_ : Bool Bool -> Bool . **** stub for real equality/disequality
op _=/=_ : Bool Bool -> Bool .
vars B : Bool .
eq B and true = B [variant] .
eq B and false = false [variant] .
eq B or false = B [variant] .
eq B or true = true [variant] .
eq not true = false [variant] .
eq not false = true [variant] .
endfm
fmod NAT-CTOR-NO-BUILTIN is
pr BOOL-NO-BUILTIN .
sorts Nat NzNat .
subsorts NzNat < Nat .
op 0 : -> Nat [ctor] .
op 1 : -> NzNat [ctor] .
op _+_ : NzNat Nat -> NzNat [ctor assoc comm id: 0] .
op _+_ : Nat Nat -> Nat [ctor assoc comm id: 0] .
endfm
fmod NAT-NO-BUILTIN is
pr NAT-CTOR-NO-BUILTIN .
op s : Nat -> Nat .
op _<_ : Nat Nat -> Bool .
op _<=_ : Nat Nat -> Bool .
op _==_ : Nat Nat -> Bool .
op _=/=_ : Nat Nat -> Bool .
op _~_ : Nat Nat -> Bool [comm] .
var N M : Nat . var P : NzNat .
eq s(N) = N + 1 [variant] .
eq N < P + N = true [variant] .
eq N + M < N = false [variant] .
eq P + N <= N = false [variant] .
eq N <= N + M = true [variant] .
eq N ~ N = true [variant] .
eq N ~ N + P = false [variant] .
endfm
fmod PROC-ID is
pr NAT-NO-BUILTIN .
sort ProcessId . **** general sort of process identifiers
sort NonNetProcId . **** processes which cannot act like a network
sort NonWebAppId . **** processes which are not webapps
sort NonPipeId . **** processes that cannot act like pipes
sort PipeId . **** processes which can act like pipes
sort NonNetPipeId . **** processes which are pipes and not networks
sort NonWebPipeId . **** processes which are pipes and not webapps
sort KernelId . **** the kernel process's id
sort WebAppMgrId . **** the web app manager's id
sort UIId . **** the UI process's id
sort DisplayId . **** the display process's id
sort NICId . **** the NIC process's id
sort NetProcId . **** processes which can act like a network
sort WebAppId . **** processes which can act like a webapp
subsorts UIId NetProcId WebAppId < PipeId < ProcessId .
subsorts KernelId DisplayId NICId WebAppMgrId < NonPipeId < ProcessId .
subsorts UIId WebAppId < NonNetPipeId < PipeId .
subsorts UIId NetProcId < NonWebPipeId < PipeId .
subsorts NonPipeId NonNetPipeId < NonNetProcId < ProcessId .
subsorts NonPipeId NonWebPipeId < NonWebAppId < ProcessId .
op kernel : -> KernelId .
op webapp : -> WebAppId .
op webapp : Nat -> WebAppId .
op network : -> NetProcId .
op network : Nat -> NetProcId .
op ui : -> UIId .
op display : -> DisplayId .
op nic : -> NICId .
op webappmgr : -> WebAppMgrId .
vars PId : ProcessId .
vars KeId : KernelId .
vars WAId : WebAppId .
vars NPId : NetProcId .
vars DiId : DisplayId .
vars UiId : UIId .
var WAMId : WebAppMgrId .
vars N N' : Nat .
op _~_ : ProcessId ProcessId -> Bool [comm] .
eq PId ~ PId = true [variant] .
eq KeId ~ WAId = false [variant] .
eq KeId ~ NPId = false [variant] .
eq KeId ~ UiId = false [variant] .
eq KeId ~ DiId = false [variant] .
eq webapp ~ webapp(N) = false [variant] .
eq webapp(N) ~ webapp(N') = N ~ N' [variant] .
eq WAId ~ NPId = false [variant] .
eq WAId ~ UiId = false [variant] .
eq WAId ~ DiId = false [variant] .
eq network ~ network(N) = false [variant] .
eq network(N) ~ network(N') = N ~ N' [variant] .
eq NPId ~ UiId = false [variant] .
eq NPId ~ DiId = false [variant] .
eq UiId ~ DiId = false [variant] .
eq WAMId ~ KeId = false [variant] .
eq WAMId ~ WAId = false [variant] .
eq WAMId ~ NPId = false [variant] .
eq WAMId ~ DiId = false [variant] .
eq WAMId ~ UiId = false [variant] .
eq WAMId ~ NPId = false [variant] .
endfm
fmod SYS is
pr PROC-ID .
sorts Object EmptyConfiguration Configuration State .
sorts Attribute EmptyAttributeSet NeAttributeSet AttributeSet .
subsorts Object EmptyConfiguration < Configuration .
subsorts Attribute < NeAttributeSet < AttributeSet .
subsorts EmptyAttributeSet < AttributeSet .
op <_|_> : ProcessId AttributeSet -> Object [ctor] .
op _,_ : AttributeSet AttributeSet -> AttributeSet [ctor assoc comm id: none] .
op _,_ : AttributeSet NeAttributeSet -> NeAttributeSet [ctor ditto] .
op _,_ : EmptyAttributeSet EmptyAttributeSet -> EmptyAttributeSet [ctor ditto] .
op none : -> EmptyAttributeSet [ctor] .
op __ : Configuration Configuration -> Configuration [ctor assoc comm id: none] .
op __ : EmptyConfiguration EmptyConfiguration -> EmptyConfiguration [ctor ditto] .
op none : -> EmptyConfiguration [ctor] .
op {_} : Configuration -> State [ctor] .
endfm
fmod LABEL is pr NAT-NO-BUILTIN .
sorts Label MaybeLabel .
subsorts Label < MaybeLabel .
op about-blank : -> Label [ctor] .
op url : Nat -> Label [ctor] .
op nolabel : -> MaybeLabel [ctor] .
**** use var-sat built-in equality/diseqaulity
op _==_ : Label Label -> Bool .
op _=/=_ : Label Label -> Bool .
**** Equality enrichment (added by Camilo)
op _~_ : Label Label -> Bool [comm] .
eq L:Label ~ L:Label = true [variant] .
eq about-blank ~ url(N:Nat) = false [variant] .
eq url(N:Nat) ~ url(N':Nat) = N:Nat ~ N':Nat [variant] .
endfm
fmod LABEL-LIST is pr LABEL .
sort LabelList .
subsort Label < LabelList .
op mtLL : -> LabelList [ctor] .
op _;_ : LabelList LabelList -> LabelList [ctor assoc id: mtLL] .
endfm
fmod LABEL-SET is pr LABEL .
sort LabelSet .
subsorts Label < LabelSet .
op _&_ : LabelSet LabelSet -> LabelSet [ctor assoc comm id: mtLS] .
op mtLS : -> LabelSet [ctor] .
endfm
fmod MSG is pr PROC-ID . pr LABEL .
**** message type definition
sorts MsgType Message .
op MSG-NEW-URL : -> MsgType [ctor] . --- creates a new web app with given URL
op MSG-FETCH-URL : -> MsgType [ctor] . --- tells network to fetch data for given URL
op MSG-RETURN-URL : -> MsgType [ctor] . --- stores data that was fetched from internet by MSG-FETCH-URL
op MSG-SWITCH-TAB : -> MsgType [ctor] . --- causes displayed tab to be switched
op msg : ProcessId ProcessId MsgType Label -> Message [ctor] .
endfm
fmod MSG-LIST is pr MSG .
**** message list definition
sort MessageList .
subsort Message < MessageList .
op none : -> Message [ctor] .
op mt : -> MessageList [ctor] .
op _;_ : MessageList MessageList -> MessageList [ctor assoc id: mt] .
endfm
fmod PIPEPROC is inc MSG-LIST . inc SYS .
**** channels for messages to and from the kernel
op fromKernel : MessageList -> Attribute [ctor] .
op toKernel : MessageList -> Attribute [ctor] .
endfm
fmod WEBAPPMGR is inc SYS .
**** next web app number, i.e. unused process id number for a web app
op nextWAN : Nat -> Attribute [ctor] .
endfm
**** Note that the webapp does not check whether what it gets back
**** from the network is actually the website it asked for in the
**** first place. We represent the data it gets by only giving its
**** URL, that is, only giving its label. This changes the rendered
**** URL to the URL the data is received from.
**** The 'missing' check above is essentially happening in
**** checkConnection(), in that only appropriately connected network
**** processes and web apps can communicate, based on the policies,
**** and only the right data can be transmitted.
****
**** need the capability to check whether a process id is for a webapp
**** this is now handled by subsorting
fmod WEBAPP is
inc WEBAPPMGR .
inc LABEL .
inc SYS .
**** Webapps have data to be put on screen - we only refer to it by
**** the label of the page where it is from.
op rendered : Label -> Attribute [ctor] .
**** This is where the webapp should load its data from!
op URL : Label -> Attribute [ctor] .
**** This notes whether it has already loaded, or has not yet started to do so.
op loading : Bool -> Attribute [ctor] .
endfm
**** network process gets a request from a webapp; network process
**** forms an ethernet frame; the kernel check that frame and give to
**** NIC; NIC generate instant answer in form of EF; that ethernet
**** frame then gets returned to the (correct! check origin, hopefully
**** this one) network process which returns data to the web page that
**** requested it originally
****
**** network proc forms packet for transmission - kernel has physical
**** address, kernel gives physical address to driver (but NO access
**** to that location's content), driver can program NIC to send the
**** packet at given address [kernel double checks that this address
**** is the given one request from a webapp:
**** Made into the topmost labeled rule [request-from-webapp]
**** in module KERNEL
****
**** The network process writes a request into the memory for pickup
**** by NIC - needing to go through kernel in next step
**** Made into the labeled topmost conditional rule [proc-out]
**** in module KERNEL
****
**** Kernel now gives this to NIC - checking that target is what is
**** allowed for this network process .
**** That DMA rule is in the kernel
**** The NIC can create a response for any message -
**** order of returns is NOT guaranteed
**** Extended to two rewrite rules to simulate the associativity
**** axiom removed from the lists; the first rule rotates the labels
**** in attribute out, while the second one moves the top label in
**** out to the end of the list in attribute in
**** Made into topmost rules [nic0] and [nic1]
**** in module KERNEL
****
**** Incoming ethernet frame in the NIC gets assigned to the
**** appropriate network process by the kernel
**** That DMA rule is in the kernel
**** The network process reads a return by NIC from memory - did go
**** through kernel in prior step
**** Made into labeled topmost rule [proc-in]
**** in module KERNEL
****
**** Sending a message from the network process to the webapp - this
**** will be subject to kernel checking according to regular policies
**** Made into labeled topmost conditional rule [msg-to-kernel]
**** in module KERNEL
**** need the capability to check whether a process id is for a netproc
**** this is now handled by subsorting
fmod NETPROC is inc LABEL-LIST . inc SYS .
op returnTo : ProcessId -> Attribute [ctor] .
op in : LabelList -> Attribute [ctor] .
op out : LabelList -> Attribute [ctor] .
endfm
fmod MEMORY is inc SYS . inc LABEL .
ops mem-out mem-in : MaybeLabel -> Attribute [ctor] .
endfm
fmod NIC is inc SYS . inc LABEL-SET . inc LABEL-LIST .
op nic-out : LabelSet -> Attribute [ctor] .
op nic-in : LabelList -> Attribute [ctor] .
endfm
fmod KERNEL-POLICIES is
inc SYS .
inc BOOL-NO-BUILTIN .
inc MSG .
inc LABEL .
inc MSG-LIST .
inc LABEL-LIST .
inc WEBAPP .
inc PIPEPROC .
inc NETPROC .
inc MEMORY .
inc NIC .
**** define how to build a single policy! then add them into the initial configuration
**** Q: where to find the policies? A: ibos_source/dKernel/access.h
**** ibos_source/dKernel/access.cc (line 195 and down; shows who can
**** communicate to whom)
****
**** Q: for those things allowed to communicate with each other, can
**** ANYTHING be sent or is there further control? A: Only the
**** MsgType given in that assignment can be sent! These are all
**** OP(browser)-related messages!
****
**** Policies are mostly browser-related, but can be on a lower level
**** [i.e., syscall level], e.g., for networkProc -> hardware
**** communication
sort Policy .
sort PolicySet .
subsort Policy < PolicySet .
op mtPS : -> PolicySet [ctor] .
op _,_ : PolicySet PolicySet -> PolicySet [ctor assoc comm id: mtPS] .
op msgPolicy : PolicySet -> Attribute [ctor] . **** make the policylist an attribute with this wrapper
op policy : PipeId PipeId MsgType -> Policy [ctor] . **** a policy is a sender Id, receiver Id and MsgType (only PipeProcs can communicate with kernel)
op nextNetworkProc : Nat -> Attribute [ctor] . **** the next available proc id for a network proc
op handledCurrently : Message -> Attribute [ctor] . **** the message currently handled by the kernel
**** webapp info stored by kernel
**** label identifies the website this webapp is showing - this needs to match the
**** first label of a network proc to allow communication
sorts WebappProcInfo WebappProcInfoSet .
subsorts WebappProcInfo < WebappProcInfoSet .
op pi : WebAppId Label -> WebappProcInfo [ctor] .
op mtWPIS : -> WebappProcInfoSet [ctor] .
op _,_ : WebappProcInfoSet WebappProcInfoSet -> WebappProcInfoSet [ctor assoc comm id: mtWPIS] .
op weblabels : WebappProcInfoSet -> Attribute [ctor] .
****network proc info stored by kernel
**** first label to identify related webapps, second label for whom
**** this network proc can communicate with (via actual ethernet; to outside world)
sorts NetworkProcInfo NetworkProcInfoSet .
subsorts NetworkProcInfo < NetworkProcInfoSet .
op pi : NetProcId Label Label -> NetworkProcInfo [ctor] .
op mtNPIS : -> NetworkProcInfoSet [ctor] .
op _,_ : NetworkProcInfoSet NetworkProcInfoSet -> NetworkProcInfoSet [ctor assoc comm id: mtNPIS] .
op networklabels : NetworkProcInfoSet -> Attribute [ctor] .
**** These next two rules are what was promised above in the network
**** process module above when referring to DMA rules.
**** Kernel gives network process DMA to NIC - checking that target is
**** what is allowed for this network process .
**** Made into a labeled topmost conditional rule [mem-out]
**** in module KERNEL
****
**** Incoming ethernet frame in the NIC gets assigned to the
**** appropriate network process DMA by the kernel
**** Made into a labeled topmost conditional rule [mem-in]
**** in module KERNEL
****
**** Receiving an OP message sets the sender ProcessId correctly. This
**** also subjects the message to policy checking.
****
**** Made into a topmost rule in module KERNEL
****
**** Once the policy has been checked and any further processing has
**** been dealt with, OP messages are forwarded.
****
**** Made into a topmost rule in module KERNEL
****
op displayedTopBar : Label -> Attribute [ctor] . **** kernel-owned address bar - part of the 'secure' UI
op activeWebapp : WebAppId -> Attribute [ctor] . **** display memory modeled as an object.
op displayedContent : Label -> Attribute [ctor] . **** label of the things being displayed as an attribute of that object
****
op kernelDo : Message -> Message [ctor] . **** Kernel needs to do something
**** Once the policy has been checked, further processing is taken care of;
**** switching the active tab in the UI is done here.
**** The kernel will change topbar, change memory access
**** for display - zero display memory first - let new owner refresh
**** display
****
**** Made into a topmost rule in module KERNEL
****
**** Allow the active webapp to change the display whenever it wants to do so.
**** ONLY the active webapp can make changes to the display!
**** Note that this is the more abstract version, for the concrete and buggy one, see the memory.maude file.
**** Made into a tomost rule that uses equality enrichment in the condition
**** in module KERNEL
****
**** Creating a NEW webapp:
**** Once the policy has been checked, further processing is taken care of;
**** this switches the active webapp to the newly created webapp for this URL
**** The kernel will change topbar, change memory access
**** for display - zero display memory first - let new owner refresh
**** display later
**** Q: How does the UI signal if the user types a new URL into the
**** address bar for a fresh webapp; and what about an existing
**** webapp [say that webapp is at URL A and the user types a URL B]
**** A: new webapp! label NEVER changes - so new webapp is needed!
****
**** check whether there is a policy in the policyset that allows the
**** message to be sent - initial policy set defined in RUN
**** Transformed into labeled conditional rules in module KERNEL
****
var L L' L'' : Label . var N N' : Nat .
var NI NI' : NetProcId . var WI WI' : WebAppId .
var NPIS : NetworkProcInfoSet . var WPIS : WebappProcInfoSet .
**** auxiliary function for checking that a network process links to a given label
op networkproc-for-label : Label NetworkProcInfoSet -> Bool .
eq [nnpl] : networkproc-for-label(L',(pi(network(N),L,L'),NPIS)) = true [variant] .
ceq [nnpl2] : networkproc-for-label(L',(pi(network(N),L,L''),NPIS)) = networkproc-for-label(L',NPIS) if L' ~ L'' = false .
eq [nnplf] : networkproc-for-label(L',mtNPIS) = false .
**** auxiliary functions for checking connections for network procs and
**** webapps in the information sets that are defined in the kernel
**** checks if a particular network process exists in a kernel-maintained set of network information
op networkproc : Nat NetworkProcInfoSet -> Bool .
eq [nnp] : networkproc(N,(pi(network(N),L,L'),NPIS)) = true [variant] .
ceq [nnp2] : networkproc(N,(pi(network(N'),L,L'),NPIS)) = networkproc(N,NPIS) if N ~ N' = false .
eq [nnpf] : networkproc(N,mtNPIS) = false .
**** checks if a particular web application exists in a kernel-maintained set of webapp information
op webapp : Nat WebappProcInfoSet -> Bool .
eq [nwa] : webapp(N,(pi(webapp(N),L),WPIS)) = true [variant] .
ceq [nwa2] : webapp(N,(pi(webapp(N'),L),WPIS)) = webapp(N,WPIS) if N ~ N' = false .
eq [nwaf] : webapp(N,mtWPIS) = false .
op matching-procs : NetProcId WebAppId WebappProcInfoSet NetworkProcInfoSet -> Bool .
eq matching-procs(NI,WI,(pi(WI,L),WPIS),NPIS) = matching-procs1(NI,L,NPIS) or matching-procs(NI,WI,WPIS,NPIS) .
ceq matching-procs(NI,WI,(pi(WI',L),WPIS),NPIS) = matching-procs(NI,WI,WPIS,NPIS) if WI ~ WI' = false .
eq matching-procs(NI,WI,mtWPIS,NPIS) = false .
op matching-procs1 : NetProcId Label NetworkProcInfoSet -> Bool .
eq matching-procs1(NI,L,(pi(NI,L,L''),NPIS)) = true .
ceq matching-procs1(NI,L,(pi(NI',L',L''),NPIS)) = matching-procs1(NI,L,NPIS) if NI ~ NI' and L ~ L' = false .
eq matching-procs1(NI,L,mtNPIS) = false .
endfm
mod KERNEL is
**** A lot of the 'kernel' things are found above in 'KERNEL-POLICIES' instead
inc KERNEL-POLICIES .
var Att Att2 : AttributeSet .
var Att3 : AttributeSet .
var Cnf : Configuration .
var L L' L'' : Label .
var L1 L2 L3 : Label .
var LL LL' LL2 : LabelList .
var LS : LabelSet .
var ML ML' : MessageList .
var NPIS : NetworkProcInfoSet .
var MP : PolicySet .
var WPIS : WebappProcInfoSet .
var MT : MsgType .
var N N' NewWA : Nat .
var URL : Label .
var PI PI' : ProcessId .
var ORG : PipeId .
var WI WI' : WebAppId .
var NI NI' : NetProcId .
var PPI PPI' : PipeId .
var PPI1 PPI2 : PipeId .
var NNPI : NonNetPipeId .
var NNPI1 NNPI2 : NonNetPipeId .
var NWPI1 NWPI2 : NonWebPipeId .
**** Page Fault and other invalid messages need not be modeled, as
**** they are simply dropped in the actual source code, and in the
**** model they will never be generated.
**** Made into a topmost labeled conditional rule from module WEBAPP
rl [fetch] :
{ < WI | rendered(L) , URL(L') , loading(false) , toKernel(ML) , Att > Cnf }
=> { < WI | rendered(L) , URL(L') , loading(true) , toKernel(ML ; msg(WI,network,MSG-FETCH-URL,L')) , Att > Cnf } .
**** Made into a labeled topmost conditional rule from module WEBAPP
rl [render] :
{ < WI | rendered(L) , URL(L') , loading(true) , fromKernel(msg(PI, WI, MSG-RETURN-URL,L2) ; ML) , Att > Cnf }
=> { < WI | rendered(L2) , URL(L') , loading(true) , fromKernel(ML) , Att > Cnf } .
**** Made into a topmost rule from module NETWORK
**** kernel tells network process to fetch data for a webapp
**** TODO: check that returnTo does the right thing (it seems like returnTo should be stored per URL to fetch)
rl [request-from-webapp] :
{ < NI | returnTo(PI), out(LL), fromKernel(msg(PI', NI, MSG-FETCH-URL, L) ; ML'), Att > Cnf }
=> { < NI | returnTo(PI'), out(LL ; L), fromKernel(ML') , Att > Cnf } .
**** Made into a labeled topmost rule from module NETWORK
**** network process moves data from its DMA response buffer into its input buffer
rl [proc-in] :
{ < NI | in(LL), mem-in(L) , Att > Cnf }
=> { < NI | in(LL ; L) , mem-in(nolabel) , Att > Cnf } .
**** Made into a topmost rule from module NETWORK
**** network process moves data from its output buffer into its DMA request buffer
rl [proc-out] :
{ < NI | out(L ; LL), mem-out(nolabel) , Att > Cnf }
=> { < NI | out(LL) , mem-out(L) , Att > Cnf } .
rl [nic1] :
{ < nic | nic-out(L & LS) , in(LL') , Att > Cnf }
=> { < nic | nic-out(LS) , in(LL' ; L) , Att > Cnf } .
**** Made into a topmost rule from module NETWORK
**** network process hands data back to other process (in this case: webapp)
rl [msg-to-kernel] :
{ < NI | returnTo(PI) , in(L ; LL), toKernel(ML) , Att > Cnf }
=> { < NI | returnTo(PI) , in(LL) , toKernel(ML ; msg(NI, PI, MSG-RETURN-URL, L)) , Att > Cnf } .
**** Made into a topmost rule from module KERNEL-POLICIES
**** kernel moves dma request from dma request buffer to NIC
rl [mem-out] :
{ < NI | mem-out(L') , Att >
< kernel | networklabels(pi(NI, L, L'), NPIS) , Att2 >
< nic | nic-out(LS) , Att3 > Cnf }
=> { < NI | mem-out(nolabel) , Att >
< kernel | networklabels(pi(NI, L, L'), NPIS) , Att2 >
< nic | nic-out(L' & LS) , Att3 > Cnf } .
**** Made into a topmost rule from module KERNEL-POLICIES
**** kernel moves dma response from NIC to dma response buffer
rl [mem-in] :
{ < NI | mem-in(nolabel) , Att >
< kernel | networklabels(pi(NI, L, L'), NPIS) , Att2 >
< nic | in(L' ; LL) , Att3 > Cnf }
=> { < NI | mem-in(L') , Att >
< kernel | networklabels(pi(NI, L, L'), NPIS) , Att2 >
< nic | in(LL) , Att3 > Cnf } .
**** the following [kernelReceviesOPMessage] rules all have a kernel object and a pipe
**** policy allows message from PPI1 to PPI2 with MsgType
rl [kernelReceivesOPMessage-pa1] :
{ < kernel | handledCurrently(none), msgPolicy(policy(PPI1,PPI2,MT),MP), Att >
< PPI1 | toKernel(msg(ORG,PPI2,MT,L) ; ML), Att2 > Cnf }
=>
{ < kernel | handledCurrently(msg(PPI1, PPI2, MT, L)), msgPolicy(policy(PPI1,PPI2,MT),MP), Att >
< PPI1 | toKernel(ML) , Att2 > Cnf } .
**** policy allows message from webapp to NNPI2 (not network proc) with MT
rl [kernelReceivesOPMessage-pa2] :
{ < kernel | handledCurrently(none), msgPolicy(policy(webapp,NNPI2,MT),MP), Att >
< WI | toKernel(msg(ORG, NNPI2, MT, L) ; ML), Att2 > Cnf }
=>
{ < kernel | handledCurrently(msg(WI, NNPI2, MT, L)), msgPolicy(policy(webapp,NNPI2,MT),MP), Att >
< WI | toKernel(ML) , Att2 > Cnf } .
**** policy allows message from NNPI1 (not network proc) to webapp with MT
rl [kernelReceivesOPMessage-pa3] :
{ < kernel | handledCurrently(none), msgPolicy(policy(NNPI1,webapp,MT),MP), Att >
< NNPI1 | toKernel(msg(ORG, WI, MT, L) ; ML), Att2 > Cnf }
=>
{ < kernel | handledCurrently(msg(NNPI1, WI, MT, L)), msgPolicy(policy(NNPI1,webapp,MT),MP), Att >
< NNPI1 | toKernel(ML) , Att2 > Cnf } .
**** policy allows message from network proc to NWPI2 (not webapp) with MT
rl [kernelReceivesOPMessage-pa4] :
{ < kernel | handledCurrently(none), msgPolicy(policy(network,NWPI2,MT),MP), Att >
< NI | toKernel(msg(ORG, NWPI2, MT, L) ; ML), Att2 > Cnf }
=>
{ < kernel | handledCurrently(msg(NI, NWPI2, MT, L)), msgPolicy(policy(network,NWPI2,MT),MP), Att >
< NI | toKernel(ML), Att2 > Cnf } .
**** policy allows message from NWPI1 (not webapp) to network proc with MT
rl [kernelReceivesOPMessage-pa5] :
{ < kernel | handledCurrently(none), msgPolicy(policy(NWPI1,network,MT),MP), Att >
< NWPI1 | toKernel(msg(ORG, NI, MT, L) ; ML), Att2 > Cnf }
=>
{ < kernel | handledCurrently(msg(NWPI1, NI, MT, L)), msgPolicy(policy(NWPI1,network,MT),MP), Att >
< NWPI1 | toKernel(ML) , Att2 > Cnf } .
**** policy allows message from webapp to network proc, but requires
**** further checking of them being connected based on the label -
**** that further check will deduce the actual target process and may
**** start a new one if necessary
**** a webapp sends a message to a network process
**** webapp WI is labelled with L, sending message ORG -> NI with label L'
**** netproc NI source is labelled with L, target is labelled with L'
**** resulting message is WI -> NI with label L'
rl [kernelReceivesOPMessage-pa6-cc2a] :
{ < kernel |
handledCurrently(none),
msgPolicy(policy(webapp,network,MT),MP),
weblabels(pi(WI,L),WPIS),
networklabels(pi(NI',L,L'),NPIS),
Att >
< WI |
toKernel(msg(ORG, NI, MT, L') ; ML),
Att2 >
Cnf }
=>
{ < kernel |
handledCurrently(msg(WI, NI', MT, L')),
msgPolicy(policy(webapp,network,MT),MP),
weblabels(pi(WI,L),WPIS),
networklabels(pi(NI',L,L'),NPIS),
Att >
< WI |
toKernel(ML) ,
Att2 >
Cnf } .
**** If no appropriate network process can be found in the above
**** rule, start a new network proc - this assumes that there will
**** be no more than 772 network procs started, to prevent that, we
**** would need to check "Num'' < 1024" :
crl [kernelReceivesOPMessage-pa6-cc2b] :
{ < kernel |
handledCurrently(none),
msgPolicy(policy(webapp,network,MT),MP),
weblabels(pi(WI, L), WPIS),
networklabels(NPIS),
nextNetworkProc(N),
Att >
< WI |
toKernel(msg(ORG, NI, MT, L') ; ML),
Att2 >
Cnf }
=>
{ < kernel |
handledCurrently(msg(WI, network(N), MT, L')),
msgPolicy(policy(webapp,network,MT),MP),
weblabels(pi(WI, L), WPIS),
networklabels(NPIS),
nextNetworkProc(s(N)),
Att >
< WI |
toKernel(ML),
Att2 >
< network(N) |
returnTo(WI),
in(mtLL) , out(mtLL) ,
mem-in(nolabel) , mem-out(nolabel) ,
toKernel(mt) , fromKernel(mt) >
Cnf }
if networkproc-for-label(L,NPIS) = false .
**** mirrored, for the reverse direction from network process to webapp:
**** there is a connection, just forward the message
**** network proc answering to webapp, thus having the correct recipient:
rl [kernelReceivesOPMessage-pa7-cc1a] :
{ < kernel |
handledCurrently(none),
msgPolicy(policy(network,webapp,MT),MP),
weblabels(pi(WI,L),WPIS),
networklabels(pi(NI,L,L'),NPIS),
Att >
< NI |
toKernel(msg(ORG, WI, MT, L'') ; ML),
Att2 >
Cnf }
=>
{ < kernel |
handledCurrently(msg(NI, WI, MT, L'')),
msgPolicy(policy(network,webapp,MT),MP),
weblabels(pi(WI,L),WPIS),
networklabels(pi(NI,L,L'),NPIS),
Att >
< NI |
toKernel(ML) ,
Att2 >
Cnf } .
**** there is no connection, then drop the message
crl [kernelReceivesOPMessage-pa7-cc1b] :
{ < kernel |
handledCurrently(none),
msgPolicy(policy(network,webapp,MT),MP),
weblabels(WPIS),
networklabels(NPIS),
Att >
< network(N) |
toKernel(msg(ORG, webapp(N'), MT, L'') ; ML),
Att2 > Cnf }
=>
{ < kernel |
--- handledCurrently(msg(network(N), webapp(N'), MT, L'')),
handledCurrently(none),
msgPolicy(policy(network,webapp,MT),MP),
weblabels(WPIS),
networklabels(NPIS),
Att >
< network(N) |
toKernel(ML) ,
Att2 >
Cnf }
if networkproc(N,NPIS) and webapp(N',WPIS) = false .
**** policy allows message from UI to change current webapp to webapp WI with MSG-SWITCH-TAB
rl [kernelReceivesOPMessage-pa8] :
{ < kernel |
handledCurrently(none),
msgPolicy(policy(ui,webapp,MSG-SWITCH-TAB),MP),
Att >
< ui |
toKernel(msg(ORG, WI, MSG-SWITCH-TAB, L) ; ML),
Att2 >
Cnf }
=>
{ < kernel |
handledCurrently(kernelDo(msg(ui,WI,MSG-SWITCH-TAB,L))),
msgPolicy(policy(ui,webapp,MSG-SWITCH-TAB),MP),
Att >
< ui |
toKernel(ML),
Att2 >
Cnf } .
**** policy allows message from UI to change current webapp to a new webapp loading URL with MSG-NEW-URL
rl [kernelReceivesOPMessage-pa9] :
{ < kernel | handledCurrently(none), msgPolicy(policy(ui,webapp,MSG-NEW-URL),MP), Att >
< ui | toKernel(msg(ORG,webapp, MSG-NEW-URL, L) ; ML), Att2 >
Cnf }
=>
{ < kernel |
handledCurrently(kernelDo(msg(ui, webapp, MSG-NEW-URL, L))),
msgPolicy(policy(ui,webapp,MSG-NEW-URL),MP),
Att >
< ui |
toKernel(ML) ,
Att2 >
Cnf } .
**** no policy allowed this, therefore implicitly disallowed and dropped
rl [kernelReceivesOPMessage-pa10] :
{ < kernel | handledCurrently(none), msgPolicy(MP), Att >
< PPI | toKernel(msg(ORG, PPI', MT, L) ; ML), Att2 > Cnf }
=>
{ < kernel | handledCurrently(none), msgPolicy(MP), Att >
< PPI | toKernel(ML), Att2 > Cnf } .
**** Made into a topmost rule from module KERNEL-POLICIES
rl [kernelForwardsOPMessage] :
{ < kernel | handledCurrently(msg(ORG, PPI', MT, L)) , Att >
< PPI' | fromKernel(ML) , Att2 > Cnf }
=>
{ < kernel | handledCurrently(none), Att >
< PPI' | fromKernel(ML ; msg(ORG, PPI', MT, L)) , Att2 > Cnf } .
**** Made into a topmost rule from module KERNEL-POLICIES
rl [tab-change] :
{ < kernel |
handledCurrently(kernelDo(msg(ui, WI', MSG-SWITCH-TAB, L1))) ,
displayedTopBar(L2),
weblabels(pi(WI', L'), WPIS) ,
Att >
< display |
activeWebapp(WI),
displayedContent(L3),
Att2 >
Cnf }
=>
{ < kernel |
handledCurrently(none) ,
displayedTopBar(L'),
weblabels(pi(WI', L'), WPIS) ,
Att >
< display |
activeWebapp(WI'),
displayedContent(about-blank),
Att2 >
Cnf } .
**** Made into a tomost rule that uses equality enrichment in the condition
**** from module KERNEL-POLICIES
**** Q. what could be wrong with this since the number of solutions
**** in one of the experiments change (Camilo) See equational enrichment
**** for labels.
**** A. there was another constructor for label in the specification;
**** such a definition was moved to module LABEL and the equality
**** enrichment defined accordingly
crl [change-display] :
{ < display | activeWebapp(WI), displayedContent(L), Att2 >
< WI | rendered(L'), Att3 > Cnf }
=> { < display | activeWebapp(WI), displayedContent(L'), Att2 >
< WI | rendered(L'), Att3 > Cnf }
if L =/= L' .
**** Made into a topmost rule from module KERNEL-POLICIES
rl [new-url] :
{ < kernel |
handledCurrently(kernelDo(msg(ui, webapp, MSG-NEW-URL, URL))) ,
displayedTopBar(L),
weblabels(WPIS) ,
Att >
< display |
activeWebapp(WI),
displayedContent(L'),
Att2 >
< webappmgr | nextWAN(NewWA) , Att3 > Cnf }
=>
{ < kernel |
handledCurrently(none) ,
displayedTopBar(URL),
weblabels(pi(webapp(NewWA), URL), WPIS) ,
Att >
< display |
activeWebapp(webapp(NewWA)),
displayedContent(about-blank),
Att2 >
< webappmgr | nextWAN(s(NewWA)) , Att3 >
< webapp(NewWA) |
rendered(about-blank) ,
URL(URL) ,
loading(false) ,
fromKernel(mt) ,
toKernel(mt) > Cnf } .
endm
mod IBOS is
pr KERNEL .
endm
mod IBOS-STOP is
pr IBOS .
var C : Configuration .
op [_] : Configuration -> State [ctor] .
rl [stop] : { C } => [ C ] .
endm
eof