This website is meant to be used in conjunction with reading the paper Verification of IBOS Browser Security Properties in Reachability Logic. Typically, formal methods papers like ours have theoretical contributions as well as code contributions; this website exists to document our code contributions.
We present a rewriting logic specification of the Illinois Browser Operating System (IBOS) and define several security properties, including the same-origin policy in reachability logic. We then show how these properties can be deductively verified using our constructor-based reachability logic theorem prover. We also highlight the reasoning techniques used in our proof and three modularity principles that have been crucial to scale up and complete the verification effort.
We make the following code artifacts available (all code is written in Maude):
A recent Maude binary; binaries for Mac/Linux available at Maude website.
Complete source code for all code contributions: rtlool.zip.
Assuming:
PATHrltool.zip was extracted in your home directoryThen you can run the proof scripts as follows (terminal shown in Mac/Linux style; Windows CMD requires minor adjustments):
$ maude ~/rltool/tests/systems/ibos-sop.maude
$ maude ~/rltool/tests/systems/ibos-abc.maude
Our proof scripts exploit rule modularity as mentioned in our paper to simplify the proof process. In our current tool prototype, such rule modularity is not explicitly supported. Instead, we manually divide up our proof script into chunks for each proof rule and then:
(select-rls <rule-name> .) command to manually choose a rule to reason about;The list of rule names is repeated in each proof script to facilitate this process.
Currently, we just show our code listings with comments. In the future, we plan to add some Javascript to allow collapisibility of different sections.
Our same-origin policy invariant has a single predicate while address bar correctness has three predicates.
We define 41 kinds of auxiliary predicates to strengthen our invariants into inductive invariants.
fmod TRUTH-VALUE-COPY is
sort Bool? . --- used for partially defined Boolean functions
sort Bool .
subsort Bool < Bool? .
op true : -> Bool [ctor special (id-hook SystemTrue) metadata "10" ] .
op false : -> Bool [ctor special (id-hook SystemFalse) metadata "11" ] .
sort Pred .
op tt : -> Pred [ctor metadata "9"] .
endfm
fmod BOOL-NO-BUILTIN is
pr TRUTH-VALUE-COPY .
op _and_ : Bool Bool -> Bool [assoc comm prec 50 metadata "12"] .
op _or_ : Bool Bool -> Bool [assoc comm metadata "13"] .
op not_ : Bool -> Bool [metadata "14"].
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 metadata "0"] .
op 1 : -> NzNat [ctor metadata "15"] .
op _+_ : NzNat Nat -> NzNat [ctor assoc comm id: 0 metadata "16"] .
op _+_ : Nat Nat -> Nat [ctor ditto metadata "16"] .
endfm
fmod NAT-NO-BUILTIN is
pr NAT-CTOR-NO-BUILTIN .
op _<_ : Nat Nat -> Bool [metadata "18"] .
op _<=_ : Nat Nat -> Bool [metadata "19"] .
op _~n_ : Nat Nat -> Bool [comm metadata "22"] .
var N M : Nat . var P : NzNat .
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 N = true [variant] .
eq N ~n N + P = false [variant] .
endfm
fmod PROC-ID is
pr NAT-NO-BUILTIN .
sort MaybeProcessId .
sort MaybePipeId .
sort MaybeConcPipeId .
sort MaybeConcNetProcId .
sort MaybeConcWebProcId .
sort NullProcId .
sort ProcessId . **** Set of all process ids
sort AbsProcId .
sort ConcProcId .
sort PipeId . **** processes which can act like pipes
sort NonPipeId . **** Set of non-pipe processes
sort NetProcId . **** abstract/concrete network procs/webapps
sort WebProcId .
sort AbsPipeId .
sort AbsNetProcId .
sort AbsWebProcId .
sort ConcPipeId .
sort ConcNetProcId .
sort ConcWebProcId .
sort UIId .
sort NonNetPipeId . **** processes which are pipes and not networks
sort NonWebPipeId . **** processes which are pipes and not webapps
subsorts NullProcId < MaybeConcNetProcId MaybeConcWebProcId < MaybeConcPipeId < MaybePipeId < MaybeProcessId .
subsorts ProcessId < MaybeProcessId .
subsorts PipeId < MaybePipeId .
subsorts ConcPipeId < MaybeConcPipeId .
subsorts ConcNetProcId < MaybeConcNetProcId .
subsorts ConcWebProcId < MaybeConcWebProcId .
subsorts AbsProcId ConcProcId < ProcessId .
subsorts PipeId NonPipeId < ProcessId .
subsorts ConcPipeId NonPipeId < ConcProcId .
subsorts AbsPipeId < AbsProcId .
subsorts AbsPipeId ConcPipeId NetProcId WebProcId < PipeId .
subsorts UIId ConcNetProcId ConcWebProcId < ConcPipeId .
subsorts AbsNetProcId AbsWebProcId < AbsPipeId .
subsorts ConcNetProcId AbsNetProcId < NetProcId .
subsorts ConcWebProcId AbsWebProcId < WebProcId .
subsorts UIId AbsWebProcId WebProcId < NonNetPipeId < PipeId .
subsorts UIId AbsNetProcId NetProcId < NonWebPipeId < PipeId .
op none : -> NullProcId [ctor metadata "23"] .
op kernel : -> NonPipeId [ctor metadata "24"] .
op display : -> NonPipeId [ctor metadata "30"] .
op nic : -> NonPipeId [ctor metadata "31"] .
op webappmgr : -> NonPipeId [ctor metadata "32"] .
op webapp : -> AbsWebProcId [ctor metadata "25"] .
op webapp : Nat -> ConcWebProcId [ctor metadata "26"] .
op network : -> AbsNetProcId [ctor metadata "27"] .
op network : Nat -> ConcNetProcId [ctor metadata "28"] .
op ui : -> UIId [ctor metadata "29"] .
var MP : MaybeProcessId .
var !P : NullProcId .
var P : ProcessId .
var NPP : NonPipeId .
var PP : PipeId .
var APP : AbsPipeId .
var CPP : ConcPipeId .
var WP : WebProcId .
var NP : NetProcId .
var UI : UIId .
vars N M : Nat .
var Z : NzNat .
op _~p_ : MaybeProcessId MaybeProcessId -> Bool [comm metadata "33"] .
eq MP ~p MP = true [variant] .
eq !P ~p P = false [variant] .
eq NPP ~p PP = false [variant] .
--- NonPipeId Disequality
eq kernel ~p display = false [variant] .
eq kernel ~p nic = false [variant] .
eq kernel ~p webappmgr = false [variant] .
eq display ~p nic = false [variant] .
eq display ~p webappmgr = false [variant] .
eq nic ~p webappmgr = false [variant] .
--- PipeId Disequality
eq APP ~p CPP = false [variant] .
--- Net/WebProc Disequality
eq WP ~p NP = false [variant] .
eq NP ~p UI = false [variant] .
eq WP ~p UI = false [variant] .
eq network(N + Z) ~p network(N) = false [variant] .
eq webapp (N + Z) ~p webapp (N) = false [variant] .
endfm
fmod SYS is
pr PROC-ID .
sorts Object EmptyConfiguration NeConfiguration Configuration State .
sorts Attribute EmptyAttributeSet NeAttributeSet AttributeSet .
subsorts Object < NeConfiguration < Configuration .
subsort EmptyConfiguration < Configuration .
subsorts Attribute < NeAttributeSet < AttributeSet .
subsort EmptyAttributeSet < AttributeSet .
op <_|_> : ConcProcId AttributeSet -> Object [ctor metadata "34"] .
op _,_ : AttributeSet AttributeSet -> AttributeSet [ctor assoc comm id: none metadata "35"] .
op _,_ : AttributeSet NeAttributeSet -> NeAttributeSet [ctor ditto metadata "35"] .
op _,_ : EmptyAttributeSet EmptyAttributeSet -> EmptyAttributeSet [ctor ditto metadata "35"] .
op none : -> EmptyAttributeSet [ctor metadata "1"] .
op __ : Configuration Configuration -> Configuration [ctor assoc comm id: none metadata "36"] .
op __ : NeConfiguration Configuration -> NeConfiguration [ctor ditto metadata "36"] .
op __ : EmptyConfiguration EmptyConfiguration -> EmptyConfiguration [ctor ditto metadata "36"] .
op none : -> EmptyConfiguration [ctor metadata "2"] .
op {_} : Configuration -> State [ctor metadata "37"] .
endfm
fmod LABEL is pr NAT-NO-BUILTIN .
var ML : MaybeLabel .
var L : Label .
var N : Nat .
var P : NzNat .
sorts Label MaybeLabel .
subsorts Label < MaybeLabel .
op about-blank : -> Label [ctor metadata "38"] .
op url : Nat -> Label [ctor metadata "39"] .
op nolabel : -> MaybeLabel [ctor metadata "40"] .
**** Equality enrichment (added by Camilo)
op _~l_ : MaybeLabel MaybeLabel -> Bool [comm metadata "43"] .
eq ML ~l ML = true [variant] .
eq about-blank ~l url(N) = false [variant] .
eq nolabel ~l L = false [variant] .
eq url(N) ~l url(N + P) = false [variant] .
endfm
fmod LABEL-LIST is pr LABEL .
sort LabelList .
subsort Label < LabelList .
op mtLL : -> LabelList [ctor metadata "3"] .
op _;_ : LabelList LabelList -> LabelList [ctor assoc id: mtLL metadata "44"] .
endfm
fmod LABEL-SET is pr LABEL .
sort LabelSet .
subsorts Label < LabelSet .
op _&_ : LabelSet LabelSet -> LabelSet [ctor assoc comm id: mtLS metadata "45"] .
op mtLS : -> LabelSet [ctor metadata "4"] .
endfm
fmod MSG is pr PROC-ID . pr LABEL .
**** message type definition
sorts MsgType Message Message? .
subsort Message < Message? .
op MSG-NEW-URL : -> MsgType [ctor metadata "46"] . --- creates a new web app with given URL
op MSG-FETCH-URL : -> MsgType [ctor metadata "47"] . --- tells network to fetch data for given URL
op MSG-RETURN-URL : -> MsgType [ctor metadata "48"] . --- stores data that was fetched from internet by MSG-FETCH-URL
op MSG-SWITCH-TAB : -> MsgType [ctor metadata "49"] . --- causes displayed tab to be switched
op msg : PipeId PipeId MsgType Label -> Message [ctor metadata "50"] .
op none : -> Message? [ctor metadata "51"] .
--- equality predicate for message types
op _~m_ : MsgType MsgType -> Bool [comm metadata "52"] .
eq X:MsgType ~m X:MsgType = true .
eq MSG-NEW-URL ~m MSG-FETCH-URL = false .
eq MSG-NEW-URL ~m MSG-RETURN-URL = false .
eq MSG-NEW-URL ~m MSG-SWITCH-TAB = false .
eq MSG-FETCH-URL ~m MSG-RETURN-URL = false .
eq MSG-FETCH-URL ~m MSG-SWITCH-TAB = false .
eq MSG-RETURN-URL ~m MSG-SWITCH-TAB = false .
endfm
fmod MSG-LIST is pr MSG .
**** message list definition
sort MessageList .
subsort Message < MessageList .
op mt : -> MessageList [ctor metadata "5"] .
op _@_ : MessageList MessageList -> MessageList [ctor assoc id: mt metadata "53"] .
endfm
fmod PIPEPROC is inc MSG-LIST . inc SYS .
**** channels for messages to and from the kernel
op fromKernel : MessageList -> Attribute [ctor metadata "54"] .
op toKernel : MessageList -> Attribute [ctor metadata "55"] .
endfm
fmod WEBAPPMGR is inc SYS .
**** next web app number, i.e. unused process id number for a web app
op nextWPN : Nat -> Attribute [ctor metadata "56"] .
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 metadata "57"] .
**** This is where the webapp should load its data from!
op URL : Label -> Attribute [ctor metadata "58"] .
**** This notes whether it has already loaded, or has not yet started to do so.
op loading : Bool -> Attribute [ctor metadata "59"] .
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 : ConcPipeId -> Attribute [ctor metadata "60"] .
op in : LabelList -> Attribute [ctor metadata "61"] .
op out : LabelList -> Attribute [ctor metadata "62"] .
endfm
fmod MEMORY is inc SYS . inc LABEL .
op mem-in : MaybeLabel -> Attribute [ctor metadata "64"] .
op mem-out : MaybeLabel -> Attribute [ctor metadata "63"] .
endfm
fmod NIC is inc SYS . inc LABEL-SET . inc LABEL-LIST .
--- NOTE: this isn't used
op nic-in : LabelList -> Attribute [ctor metadata "66"] .
op nic-out : LabelSet -> Attribute [ctor metadata "65"] .
endfm
fmod KERNEL-POLICIES-FVP 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 metadata "6"] .
op _,ps_ : PolicySet PolicySet -> PolicySet [ctor assoc comm id: mtPS metadata "67"] .
op msgPolicy : PolicySet -> Attribute [ctor metadata "68"] . **** make the policylist an attribute with this wrapper
op policy : PipeId PipeId MsgType -> Policy [ctor metadata "69"] . **** a policy is a sender Id, receiver Id and MsgType (only PipeProcs can communicate with kernel)
op nextNPN : Nat -> Attribute [ctor metadata "70"] . **** the next available proc id for a network proc
op handledCurrently : Message? -> Attribute [ctor metadata "71"] . **** 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 WebProcInfo WebProcInfoSet .
subsorts WebProcInfo < WebProcInfoSet .
op pi : ConcWebProcId Label -> WebProcInfo [ctor metadata "72"] .
op mtWPIS : -> WebProcInfoSet [ctor metadata "7"] .
op _,wp_ : WebProcInfoSet WebProcInfoSet -> WebProcInfoSet [ctor assoc comm id: mtWPIS metadata "73"] .
op weblabels : WebProcInfoSet -> Attribute [ctor metadata "74"] .
****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 NetProcInfo NetProcInfoSet .
subsorts NetProcInfo < NetProcInfoSet .
op pi : ConcNetProcId Label Label -> NetProcInfo [ctor metadata "75"] .
op mtNPIS : -> NetProcInfoSet [ctor metadata "8"] .
op _,np_ : NetProcInfoSet NetProcInfoSet -> NetProcInfoSet [ctor assoc comm id: mtNPIS metadata "76"] .
op netlabels : NetProcInfoSet -> Attribute [ctor metadata "77"] .
**** 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 metadata "78"] . **** kernel-owned address bar - part of the 'secure' UI
op activeWebapp : MaybeConcWebProcId -> Attribute [ctor metadata "79"] . **** display memory modeled as an object.
op displayedContent : Label -> Attribute [ctor metadata "80"] . **** label of the things being displayed as an attribute of that object
****
**** 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
****
endfm
fmod KERNEL-POLICIES-NONFVP is
pr KERNEL-POLICIES-FVP .
var L L' L'' : Label . var N N' : Nat .
var NI NI' : ConcNetProcId . var WI WI' : ConcWebProcId .
var NPIS : NetProcInfoSet . var WPIS : WebProcInfoSet .
var PI PI' : ConcProcId .
var NPI NPI' : NonPipeId .
var UI : UIId .
**** auxiliary function for checking that a network process links to a given label
op np-by-lbl? : Label NetProcInfoSet -> Bool [metadata "82"] .
eq np-by-lbl?(L',(pi(network(N),L,L') ,np NPIS)) = true [variant] .
ceq np-by-lbl?(L',(pi(network(N),L,L'') ,np NPIS)) = np-by-lbl?(L',NPIS) if L' ~l L'' = false .
eq np-by-lbl?(L',mtNPIS) = false .
endfm
mod KERNEL is
**** A lot of the 'kernel' things are found above in 'KERNEL-POLICIES' instead
inc KERNEL-POLICIES-NONFVP .
var Att Att2 : AttributeSet .
var Att3 : AttributeSet .
var Cnf : Configuration .
var L L' L'' : Label .
var L1 L2 L3 : Label .
var LL : LabelList .
var LS : LabelSet .
var ML ML' : MessageList .
var NPIS : NetProcInfoSet .
var MP : PolicySet .
var WPIS : WebProcInfoSet .
var MT : MsgType .
var N : Nat .
var URL : Label .
var ORG : ConcPipeId .
var PPI1 PPI2 : ConcPipeId .
var GPPI : PipeId .
var WI WI' : ConcWebProcId .
var NI NI' : ConcNetProcId .
var WI? : WebProcId .
var NI? : NetProcId .
var NNPI1 NNPI2 : NonNetPipeId .
var NWPI1 NWPI2 : NonWebPipeId .
var MWI : MaybeConcWebProcId .
**** 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(PPI1, 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(PPI1), out(LL), fromKernel(msg(PPI2, NI, MSG-FETCH-URL, L) @ ML'), Att > Cnf }
=> { < NI | returnTo(PPI2), 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(PPI1) , in(L ; LL), toKernel(ML) , Att > Cnf }
=> { < NI | returnTo(PPI1) , in(LL) , toKernel(ML @ msg(NI, PPI1, 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 | netlabels(pi(NI, L, L'),np NPIS) , Att2 >
< nic | nic-out(LS) , Att3 > Cnf }
=> { < NI | mem-out(nolabel) , Att >
< kernel | netlabels(pi(NI, L, L'),np 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 | netlabels(pi(NI, L, L'),np NPIS) , Att2 >
< nic | in(L' ; LL) , Att3 > Cnf }
=> { < NI | mem-in(L') , Att >
< kernel | netlabels(pi(NI, L, L'),np 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),ps MP), Att >
< PPI1 | toKernel(msg(ORG,PPI2,MT,L) @ ML), Att2 > Cnf }
=>
{ < kernel | handledCurrently(msg(PPI1, PPI2, MT, L)), msgPolicy(policy(PPI1,PPI2,MT),ps 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),ps MP), Att >
< WI | toKernel(msg(ORG, NNPI2, MT, L) @ ML), Att2 > Cnf }
=>
{ < kernel | handledCurrently(msg(WI, NNPI2, MT, L)), msgPolicy(policy(webapp,NNPI2,MT),ps 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),ps MP), Att >
< NNPI1 | toKernel(msg(ORG, WI, MT, L) @ ML), Att2 > Cnf }
=>
{ < kernel | handledCurrently(msg(NNPI1, WI, MT, L)), msgPolicy(policy(NNPI1,webapp,MT),ps 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),ps MP), Att >
< NI | toKernel(msg(ORG, NWPI2, MT, L) @ ML), Att2 > Cnf }
=>
{ < kernel | handledCurrently(msg(NI, NWPI2, MT, L)), msgPolicy(policy(network,NWPI2,MT),ps 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),ps MP), Att >
< NWPI1 | toKernel(msg(ORG, NI, MT, L) @ ML), Att2 > Cnf }
=>
{ < kernel | handledCurrently(msg(NWPI1, NI, MT, L)), msgPolicy(policy(NWPI1,network,MT),ps 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-a] :
{ < kernel |
handledCurrently(none),
msgPolicy(policy(webapp,network,MT),ps MP),
weblabels(pi(WI,L),wp WPIS),
netlabels(pi(NI',L,L'),np NPIS),
Att >
< WI |
toKernel(msg(ORG, NI?, MT, L') @ ML),
Att2 >
Cnf }
=>
{ < kernel |
handledCurrently(msg(WI, NI', MT, L')),
msgPolicy(policy(webapp,network,MT),ps MP),
weblabels(pi(WI,L),wp WPIS),
netlabels(pi(NI',L,L'),np 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-b] :
{ < kernel |
handledCurrently(none),
msgPolicy(policy(webapp,network,MT),ps MP),
weblabels(pi(WI, L),wp WPIS),
netlabels(NPIS),
nextNPN(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),ps MP),
weblabels(pi(WI, L),wp WPIS),
netlabels(pi(network(N),L,L'),np NPIS),
nextNPN(N + 1),
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 np-by-lbl?(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:
**** if there is no connection, we drop by pa10
rl [kernelReceivesOPMessage-pa7] :
{ < kernel |
handledCurrently(none),
msgPolicy(policy(network,webapp,MT),ps MP),
weblabels(pi(WI,L),wp WPIS),
netlabels(pi(NI,L,L'),np NPIS),
Att >
< NI |
toKernel(msg(ORG, WI, MT, L'') @ ML),
Att2 >
Cnf }
=>
{ < kernel |
handledCurrently(msg(NI, WI, MT, L'')),
msgPolicy(policy(network,webapp,MT),ps MP),
weblabels(pi(WI,L),wp WPIS),
netlabels(pi(NI,L,L'),np NPIS),
Att >
< NI |
toKernel(ML) ,
Att2 >
Cnf } .
**** 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),ps MP),
Att >
< ui |
toKernel(msg(ORG, WI, MSG-SWITCH-TAB, L) @ ML),
Att2 >
Cnf }
=>
{ < kernel |
handledCurrently(msg(ui,WI,MSG-SWITCH-TAB,L)),
msgPolicy(policy(ui,webapp,MSG-SWITCH-TAB),ps 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),ps MP), Att >
< ui | toKernel(msg(ORG,webapp, MSG-NEW-URL, L) @ ML), Att2 >
Cnf }
=>
{ < kernel |
handledCurrently(msg(ui, webapp, MSG-NEW-URL, L)),
msgPolicy(policy(ui,webapp,MSG-NEW-URL),ps 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 >
< PPI1 | toKernel(msg(ORG, GPPI, MT, L) @ ML), Att2 > Cnf }
=>
{ < kernel | handledCurrently(none), msgPolicy(MP), Att >
< PPI1 | toKernel(ML), Att2 > Cnf } .
**** Made into a topmost rule from module KERNEL-POLICIES
rl [kernelForwardsOPMessage] :
{ < kernel | handledCurrently(msg(PPI1, PPI2, MT, L)) , Att >
< PPI2 | fromKernel(ML) , Att2 > Cnf }
=>
{ < kernel | handledCurrently(none), Att >
< PPI2 | fromKernel(ML @ msg(PPI1, PPI2, MT, L)) , Att2 > Cnf } .
**** Made into a topmost rule from module KERNEL-POLICIES
rl [tab-change] :
{ < kernel |
handledCurrently(msg(ui, WI', MSG-SWITCH-TAB, L1)),
displayedTopBar(L2),
weblabels(pi(WI', L'),wp WPIS),
Att >
< display |
activeWebapp(MWI),
displayedContent(L3),
Att2 >
Cnf }
=>
{ < kernel |
handledCurrently(none),
displayedTopBar(L'),
weblabels(pi(WI', L'),wp 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 L' = false .
**** Made into a topmost rule from module KERNEL-POLICIES
rl [new-url] :
{ < kernel |
handledCurrently(msg(ui, webapp, MSG-NEW-URL, URL)),
displayedTopBar(L),
weblabels(WPIS),
Att >
< display |
activeWebapp(MWI),
displayedContent(L'),
Att2 >
< webappmgr | nextWPN(N), Att3 > Cnf }
=>
{ < kernel |
handledCurrently(none),
displayedTopBar(URL),
weblabels(pi(webapp(N), URL),wp WPIS),
Att >
< display |
activeWebapp(webapp(N)),
displayedContent(about-blank),
Att2 >
< webappmgr | nextWPN(N + 1), Att3 >
< webapp(N) |
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 metadata "87"] .
rl [stop] : { C } => [ C ] .
endm---
--- [PARTIALLY] FVP
---
---
--- 1. Separate ProcessIds into Net/WebProcs and everything else
---
fmod PROC-ID-FVP-EXT is
pr PROC-ID .
--- 1. Separate ProcessIds into Net/WebProcs and everything else
sort ConcNetWebProcId .
subsort ConcNetProcId ConcWebProcId < ConcNetWebProcId < ConcPipeId .
sort NonConcNetWebProcId .
subsort UIId NonPipeId < NonConcNetWebProcId .
endfm
---
--- 2. Separate Configurations into those made up of Net/WebProcs and everything else
--- 3. Add partially FVP predicate for checking if an object with the named ID is in the configuration
--- 4. Add partially FVP predicate for checking for duplicate object IDs in the configuration
---
fmod CONFIGURATION-FVP-EXT is
pr PROC-ID-FVP-EXT .
pr KERNEL-POLICIES-FVP .
var P P' : ConcProcId . var A A' : AttributeSet . var C : Configuration .
var P? : ProcessId .
--- 2. Separate Configurations into those made up of Net/WebProcs and everything else
sorts NetWebProcObject NetWebProcConfig NetWebProcNeConfig .
subsort NetWebProcObject < Object .
subsort NetWebProcObject < NetWebProcNeConfig < NeConfiguration NetWebProcConfig < Configuration .
subsort EmptyConfiguration < NetWebProcConfig .
op <_|_> : ConcNetWebProcId AttributeSet -> NetWebProcObject [ctor ditto metadata "34"] .
op __ : NetWebProcConfig NetWebProcConfig -> NetWebProcConfig [ctor ditto metadata "36"] .
op __ : NetWebProcNeConfig NetWebProcConfig -> NetWebProcNeConfig [ctor ditto metadata "36"] .
sorts SpecialObject SpecialConfig SpecialNeConfig .
subsort SpecialObject < Object .
subsort SpecialObject < SpecialNeConfig < NeConfiguration SpecialConfig < Configuration .
subsort EmptyConfiguration < SpecialConfig .
op <_|_> : NonConcNetWebProcId AttributeSet -> SpecialObject [ctor ditto metadata "34"] .
op __ : SpecialConfig SpecialConfig -> SpecialConfig [ctor ditto metadata "36"] .
op __ : SpecialNeConfig SpecialConfig -> SpecialNeConfig [ctor ditto metadata "36"] .
--- 3. Add partially FVP predicate for checking if an object with the named ID is in the configuration
op in-conf? : ProcessId Configuration -> Bool [metadata "108 true"] .
eq in-conf?(P, < P | A' > C) = true [variant] .
ceq in-conf?(P?,< P' | A' > C) = in-conf?(P?,C) if P? ~p P' = false .
eq in-conf?(P?,none) = false .
--- 4. Add partially FVP predicate for checking for duplicate object IDs in the configuration
op conf-dupl? : Configuration -> Bool [metadata "109 true"] .
eq conf-dupl?(< P | A > < P | A' > C) = true .
eq conf-dupl?(none) = false .
ceq conf-dupl?(< P | none > C) = conf-dupl?(C) if in-conf?(P,C) = false .
endfm
---
--- 5. Add LabelPair and MaybeLabelPair datatypes
--- 6. Add MaybeLabelPair equality predicate _~lp_
--- 7. Add LabelPair projection functions
--- 8. Add _blank-or-equal_ function
---
fmod LABEL-FVP-EXT is
pr LABEL .
var L L' : Label .
var N : Nat .
var P : NzNat .
var L1 L2 L1' L2' : MaybeLabel .
var MMLP : MaybeMaybeLabel+Pair .
var MLP : MaybeLabelPair .
--- 5. Add LabelPair and MaybeLabelPair datatypes
sort LabelPair MaybeLabelPair MaybeLabel+Pair MaybeMaybeLabel+Pair .
subsort LabelPair < MaybeLabelPair < MaybeMaybeLabel+Pair .
subsort LabelPair < MaybeLabel+Pair < MaybeMaybeLabel+Pair .
op ((_,_)) : Label Label -> LabelPair [ctor metadata "88"] .
op ((_,_)) : MaybeLabel MaybeLabel -> MaybeMaybeLabel+Pair [ctor metadata "88"] .
op nopair : -> MaybeLabelPair [ctor metadata "89"] .
--- 6. Add MaybeLabelPair equality predicate _~lp_
op _~lp_ : MaybeMaybeLabel+Pair MaybeMaybeLabel+Pair -> Bool [comm metadata "90"] .
eq MMLP ~lp MMLP = true [variant] .
eq (L1,L2) ~lp (L1',L2') = L1 ~l L1' and L2 ~l L2' [variant] .
eq nopair ~lp (L1, L2 ) = false [variant] .
eq (nolabel,L2) ~lp MLP = false [variant] .
eq (L1,nolabel) ~lp MLP = false [variant] .
--- 7. Add LabelPair projection functions
op inlbl : MaybeLabelPair -> MaybeLabel [metadata "91"] .
eq inlbl((L1,L2)) = L1 [variant] .
eq inlbl(nopair) = nolabel [variant] .
op outlbl : MaybeLabelPair -> MaybeLabel [metadata "92"] .
eq outlbl((L1,L2)) = L2 [variant] .
eq outlbl(nopair) = nolabel [variant] .
--- 8. Add _blank-or-equal_ function
op _blank-or-equal_ : Label Label -> Bool [metadata "94"] .
eq about-blank blank-or-equal L = true [variant] .
eq L blank-or-equal L = true [variant] .
eq url(N) blank-or-equal about-blank = false [variant] .
eq url(N) blank-or-equal url(N + P) = false [variant] .
eq url(N + P) blank-or-equal url(N) = false [variant] .
endfm
---
--- 9. Refine MsgType/Msg into subsorts for each kind of message
--- 10. Refine MessageList into empty and non-empty variants
--- 11. Refine MessageList into those with a FETCH message and those without
--- 12. Add MaybeMessageList type
--- 13. Add predicate that returns false iff a MessageList contains a NEW-URL message with a given label
---
fmod MSG-FVP-EXT is
pr MSG-LIST .
var PI PI' : PipeId .
var L OUT : Label .
var ML ML2 : MessageList .
var RetMT : RetMsgType .
var FetchMT : FetchMsgType .
--- 9. Refine MsgType/Msg into subsorts for each kind of message
sort FetchMsgType RetMsgType NonRetFetchMsgType NonRetMsgType NonFetchMsgType .
subsort NonRetFetchMsgType < NonRetMsgType NonFetchMsgType < MsgType .
subsort FetchMsgType < NonRetMsgType .
subsort RetMsgType < NonFetchMsgType .
op MSG-NEW-URL : -> NonRetFetchMsgType [ctor metadata "46"] .
op MSG-FETCH-URL : -> FetchMsgType [ctor metadata "47"] .
op MSG-RETURN-URL : -> RetMsgType [ctor metadata "48"] .
op MSG-SWITCH-TAB : -> NonRetFetchMsgType [ctor metadata "49"] .
----------------------------------------------------
eq MSG-RETURN-URL ~m M:NonRetMsgType = false .
eq MSG-FETCH-URL ~m M:NonFetchMsgType = false .
sort NonRetFetchMsg FetchMsg RetMsg NonRetMsg NonFetchMsg .
subsort NonRetFetchMsg < NonRetMsg NonFetchMsg < Message .
subsort FetchMsg < NonRetMsg .
subsort RetMsg < NonFetchMsg .
op msg : PipeId PipeId FetchMsgType Label -> FetchMsg [ctor ditto metadata "50"] .
op msg : PipeId PipeId RetMsgType Label -> RetMsg [ctor ditto metadata "50"] .
op msg : PipeId PipeId NonFetchMsgType Label -> NonFetchMsg [ctor ditto metadata "50"] .
op msg : PipeId PipeId NonRetMsgType Label -> NonRetMsg [ctor ditto metadata "50"] .
op msg : PipeId PipeId NonRetFetchMsgType Label -> NonRetFetchMsg [ctor ditto metadata "50"] .
--- 10. Refine MessageList into empty and non-empty variants
sort EmptyMessageList .
subsort EmptyMessageList < MessageList .
op mt : -> EmptyMessageList [ctor ditto metadata "5"] .
op _@_ : EmptyMessageList EmptyMessageList -> EmptyMessageList [ctor ditto metadata "53"] .
sort NeMessageList .
subsort Message < NeMessageList < MessageList .
op _@_ : NeMessageList MessageList -> NeMessageList [ctor ditto metadata "53"] .
op _@_ : MessageList NeMessageList -> NeMessageList [ctor ditto metadata "53"] .
--- 11. Refine MessageList into those with a FETCH message and those without
sort NonFetchMsgList NeNonFetchMsgList HasFetchMsgList .
subsort EmptyMessageList < NonFetchMsgList < MessageList .
subsort NonFetchMsg < NeNonFetchMsgList < NonFetchMsgList NeMessageList .
subsort FetchMsg < HasFetchMsgList < NeMessageList .
op _@_ : NonFetchMsgList NeNonFetchMsgList -> NeNonFetchMsgList [ctor ditto metadata "53"] .
op _@_ : NeNonFetchMsgList NonFetchMsgList -> NeNonFetchMsgList [ctor ditto metadata "53"] .
op _@_ : NonFetchMsgList NonFetchMsgList -> NonFetchMsgList [ctor ditto metadata "53"] .
op _@_ : NonFetchMsgList HasFetchMsgList -> HasFetchMsgList [ctor ditto metadata "53"] .
op _@_ : HasFetchMsgList NonFetchMsgList -> HasFetchMsgList [ctor ditto metadata "53"] .
op _@_ : HasFetchMsgList HasFetchMsgList -> HasFetchMsgList [ctor ditto metadata "53"] .
op _@_ : MessageList HasFetchMsgList -> HasFetchMsgList [ctor ditto metadata "53"] .
op _@_ : HasFetchMsgList MessageList -> HasFetchMsgList [ctor ditto metadata "53"] .
--- 12. Add MaybeMessageList type
sort MaybeMessageList .
subsort MessageList < MaybeMessageList .
op nolist : -> MaybeMessageList [ctor metadata "93"] .
--- 13. Add predicate that returns false iff a MessageList contains a NEW-URL message with a given label
--- NB: this is an auxiliary predicate for ui-consistent
op newurl-nodupl? : Label MessageList -> Bool [metadata "198 false"] .
eq newurl-nodupl?(L,ML @ msg(PI,PI',MSG-NEW-URL, L) @ ML2) = false [variant] .
ceq newurl-nodupl?(L,ML @ msg(PI,PI',MSG-NEW-URL, OUT) @ ML2) = true if L ~l OUT = false /\ newurl-nodupl?(L,ML @ ML2) = true .
ceq newurl-nodupl?(L,ML @ msg(PI,PI',RetMT, OUT) @ ML2) = true if newurl-nodupl?(L,ML @ ML2) = true .
ceq newurl-nodupl?(L,ML @ msg(PI,PI',FetchMT, OUT) @ ML2) = true if newurl-nodupl?(L,ML @ ML2) = true .
ceq newurl-nodupl?(L,ML @ msg(PI,PI',MSG-SWITCH-TAB,OUT) @ ML2) = true if newurl-nodupl?(L,ML @ ML2) = true .
eq newurl-nodupl?(L,mt) = true .
endfm
---
--- 14. Refine Net/WebProcInfoSet into empty and non-empty variants
--- 15. Add Net/WebProcInfo equality predicates
--- 16. Add partially FVP predicates for checking if a ProcessId is mapped in a Net/WebProcInfoSet
---
fmod KERNEL-METADATA-FVP-EXT is
pr KERNEL-POLICIES-FVP .
pr LABEL-FVP-EXT .
var WI WI' : WebProcInfo . var WIS : WebProcInfoSet .
var NI NI' : NetProcInfo . var NIS : NetProcInfoSet .
var WP WP' : ConcWebProcId .
var NP NP' : ConcNetProcId .
var L1 L2 L3 L4 : Label .
--- 14. Refine Net/WebProcInfoSet into empty and non-empty variants
sort NeWebProcInfoSet .
subsort WebProcInfo < NeWebProcInfoSet < WebProcInfoSet .
sort NeNetProcInfoSet .
subsort NetProcInfo < NeNetProcInfoSet < NetProcInfoSet .
op _,wp_ : NeWebProcInfoSet WebProcInfoSet -> NeWebProcInfoSet [ctor ditto metadata "73"] .
op _,np_ : NeNetProcInfoSet NetProcInfoSet -> NeNetProcInfoSet [ctor ditto metadata "76"] .
--- 15. Add Net/WebProcInfo equality predicates
op _~wpi_ : WebProcInfo WebProcInfo -> Bool [metadata "129"] .
eq pi(WP,L1) ~wpi pi(WP',L2) = WP ~p WP' and L1 ~l L2 .
op _~npi_ : NetProcInfo NetProcInfo -> Bool [metadata "130"] .
eq pi(NP,L1,L2) ~npi pi(NP',L3,L4) = NP ~p NP' and L1 ~l L3 and L2 ~l L4 .
--- 16. Add partially FVP predicates for checking if a ProcessId is mapped in a Net/WebProcInfoSet
op weblabel-and-pid? : WebProcInfo WebProcInfoSet -> Bool [ctor metadata "131 true"] .
eq weblabel-and-pid?(WI,(WI ,wp WIS)) = true [variant] .
ceq weblabel-and-pid?(WI,(WI' ,wp WIS)) = false if WI ~wpi WI' = false /\ weblabel-and-pid?(WI,WIS) = false .
eq weblabel-and-pid?(WI,mtWPIS) = false .
op netlabelpair-and-pid? : NetProcInfo NetProcInfoSet -> Bool [ctor metadata "132 true"] .
eq netlabelpair-and-pid?(NI,(NI ,np NIS)) = true [variant] .
ceq netlabelpair-and-pid?(NI,(NI',np NIS)) = false if NI ~npi NI' = false /\ netlabelpair-and-pid?(NI,NIS) = false .
eq netlabelpair-and-pid?(NI,mtNPIS) = false .
endfm
---
--- 17. Generalize typing of returnTo(), rendered(), fromKernel(), and toKernel() attributes (used for attribute canonicalization)
--- 18. Add attribute type equality predicate _~a_
--- 19. Add partially FVP in-attrset?(_|_) predicate for checking if an attribute of a given type exists in an attribute set
--- 20. Add partially FVP attr-dupl?() predicate for checking if an attribute type occurs twice in a given attribute set
---
fmod ATTRIBUTE-FVP-EXT is
pr PROC-ID-FVP-EXT .
pr KERNEL-POLICIES-FVP .
pr MSG-FVP-EXT .
var A A' : Attribute . var AS AS' : AttributeSet .
--- 17. Generalize typing of returnTo(), rendered(), fromKernel(), and toKernel() attributes (used for attribute canonicalization)
op returnTo : MaybeConcPipeId -> Attribute [ctor metadata "60"] .
op rendered : MaybeLabel -> Attribute [ctor metadata "57"] .
op fromKernel : MaybeMessageList -> Attribute [ctor metadata "54"] .
op toKernel : MaybeMessageList -> Attribute [ctor metadata "55"] .
--- 18. Add attribute type equality predicate _~a_
op _~a_ : Attribute Attribute -> Bool [comm metadata "100"] .
eq fromKernel (X:MaybeMessageList) ~a fromKernel (Y:MaybeMessageList) = true [variant] .
eq toKernel (X:MaybeMessageList) ~a toKernel (Y:MaybeMessageList) = true [variant] .
eq nextWPN (X:Nat) ~a nextWPN (Y:Nat) = true [variant] .
eq rendered (X:MaybeLabel) ~a rendered (Y:MaybeLabel) = true [variant] .
eq URL (X:Label) ~a URL (Y:Label) = true [variant] .
eq loading (X:Bool) ~a loading (Y:Bool) = true [variant] .
eq returnTo (X:MaybeConcPipeId) ~a returnTo (Y:MaybeConcPipeId) = true [variant] .
eq in (X:LabelList) ~a in (Y:LabelList) = true [variant] .
eq out (X:LabelList) ~a out (Y:LabelList) = true [variant] .
eq mem-in (X:MaybeLabel) ~a mem-in (Y:MaybeLabel) = true [variant] .
eq mem-out (X:MaybeLabel) ~a mem-out (Y:MaybeLabel) = true [variant] .
eq nic-in (X:LabelList) ~a nic-in (Y:LabelList) = true [variant] .
eq nic-out (X:LabelSet) ~a nic-out (Y:LabelSet) = true [variant] .
eq msgPolicy (X:PolicySet) ~a msgPolicy (Y:PolicySet) = true [variant] .
eq nextNPN (X:Nat) ~a nextNPN (Y:Nat) = true [variant] .
eq handledCurrently(X:Message?) ~a handledCurrently(Y:Message?) = true [variant] .
eq weblabels (X:WebProcInfoSet) ~a weblabels (Y:WebProcInfoSet) = true [variant] .
eq netlabels (X:NetProcInfoSet) ~a netlabels (Y:NetProcInfoSet) = true [variant] .
eq displayedTopBar (X:Label) ~a displayedTopBar (Y:Label) = true [variant] .
eq displayedContent(X:Label) ~a displayedContent(Y:Label) = true [variant] .
eq activeWebapp (X:WebProcId) ~a activeWebapp (Y:WebProcId) = true [variant] .
eq fromKernel (X:MaybeMessageList) ~a toKernel (Y:MaybeMessageList) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a nextWPN (Y:Nat) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a rendered (Y:MaybeLabel) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a URL (Y:Label) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a loading (Y:Bool) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a returnTo (Y:MaybeConcPipeId) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a in (Y:LabelList) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a out (Y:LabelList) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a mem-in (Y:MaybeLabel) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a mem-out (Y:MaybeLabel) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a nic-in (Y:LabelList) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a nic-out (Y:LabelSet) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a nextNPN (Y:Nat) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a handledCurrently(Y:Message?) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a displayedTopBar (Y:Label) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a displayedContent(Y:Label) = false [variant] .
eq fromKernel (X:MaybeMessageList) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a nextWPN (Y:Nat) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a rendered (Y:MaybeLabel) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a URL (Y:Label) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a loading (Y:Bool) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a returnTo (Y:MaybeConcPipeId) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a in (Y:LabelList) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a out (Y:LabelList) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a mem-in (Y:MaybeLabel) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a mem-out (Y:MaybeLabel) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a nic-in (Y:LabelList) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a nic-out (Y:LabelSet) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a nextNPN (Y:Nat) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a handledCurrently(Y:Message?) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a displayedTopBar (Y:Label) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a displayedContent(Y:Label) = false [variant] .
eq toKernel (X:MaybeMessageList) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq nextWPN (X:Nat) ~a rendered (Y:MaybeLabel) = false [variant] .
eq nextWPN (X:Nat) ~a URL (Y:Label) = false [variant] .
eq nextWPN (X:Nat) ~a loading (Y:Bool) = false [variant] .
eq nextWPN (X:Nat) ~a returnTo (Y:MaybeConcPipeId) = false [variant] .
eq nextWPN (X:Nat) ~a in (Y:LabelList) = false [variant] .
eq nextWPN (X:Nat) ~a out (Y:LabelList) = false [variant] .
eq nextWPN (X:Nat) ~a mem-in (Y:MaybeLabel) = false [variant] .
eq nextWPN (X:Nat) ~a mem-out (Y:MaybeLabel) = false [variant] .
eq nextWPN (X:Nat) ~a nic-in (Y:LabelList) = false [variant] .
eq nextWPN (X:Nat) ~a nic-out (Y:LabelSet) = false [variant] .
eq nextWPN (X:Nat) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq nextWPN (X:Nat) ~a nextNPN (Y:Nat) = false [variant] .
eq nextWPN (X:Nat) ~a handledCurrently(Y:Message?) = false [variant] .
eq nextWPN (X:Nat) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq nextWPN (X:Nat) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq nextWPN (X:Nat) ~a displayedTopBar (Y:Label) = false [variant] .
eq nextWPN (X:Nat) ~a displayedContent(Y:Label) = false [variant] .
eq nextWPN (X:Nat) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq rendered (X:MaybeLabel) ~a URL (Y:Label) = false [variant] .
eq rendered (X:MaybeLabel) ~a loading (Y:Bool) = false [variant] .
eq rendered (X:MaybeLabel) ~a returnTo (Y:MaybeConcPipeId) = false [variant] .
eq rendered (X:MaybeLabel) ~a in (Y:LabelList) = false [variant] .
eq rendered (X:MaybeLabel) ~a out (Y:LabelList) = false [variant] .
eq rendered (X:MaybeLabel) ~a mem-in (Y:MaybeLabel) = false [variant] .
eq rendered (X:MaybeLabel) ~a mem-out (Y:MaybeLabel) = false [variant] .
eq rendered (X:MaybeLabel) ~a nic-in (Y:LabelList) = false [variant] .
eq rendered (X:MaybeLabel) ~a nic-out (Y:LabelSet) = false [variant] .
eq rendered (X:MaybeLabel) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq rendered (X:MaybeLabel) ~a nextNPN (Y:Nat) = false [variant] .
eq rendered (X:MaybeLabel) ~a handledCurrently(Y:Message?) = false [variant] .
eq rendered (X:MaybeLabel) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq rendered (X:MaybeLabel) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq rendered (X:MaybeLabel) ~a displayedTopBar (Y:Label) = false [variant] .
eq rendered (X:MaybeLabel) ~a displayedContent(Y:Label) = false [variant] .
eq rendered (X:MaybeLabel) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq URL (X:Label) ~a loading (Y:Bool) = false [variant] .
eq URL (X:Label) ~a returnTo (Y:MaybeConcPipeId) = false [variant] .
eq URL (X:Label) ~a in (Y:LabelList) = false [variant] .
eq URL (X:Label) ~a out (Y:LabelList) = false [variant] .
eq URL (X:Label) ~a mem-in (Y:MaybeLabel) = false [variant] .
eq URL (X:Label) ~a mem-out (Y:MaybeLabel) = false [variant] .
eq URL (X:Label) ~a nic-in (Y:LabelList) = false [variant] .
eq URL (X:Label) ~a nic-out (Y:LabelSet) = false [variant] .
eq URL (X:Label) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq URL (X:Label) ~a nextNPN (Y:Nat) = false [variant] .
eq URL (X:Label) ~a handledCurrently(Y:Message?) = false [variant] .
eq URL (X:Label) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq URL (X:Label) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq URL (X:Label) ~a displayedTopBar (Y:Label) = false [variant] .
eq URL (X:Label) ~a displayedContent(Y:Label) = false [variant] .
eq URL (X:Label) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq loading (X:Bool) ~a returnTo (Y:MaybeConcPipeId) = false [variant] .
eq loading (X:Bool) ~a in (Y:LabelList) = false [variant] .
eq loading (X:Bool) ~a out (Y:LabelList) = false [variant] .
eq loading (X:Bool) ~a mem-in (Y:MaybeLabel) = false [variant] .
eq loading (X:Bool) ~a mem-out (Y:MaybeLabel) = false [variant] .
eq loading (X:Bool) ~a nic-in (Y:LabelList) = false [variant] .
eq loading (X:Bool) ~a nic-out (Y:LabelSet) = false [variant] .
eq loading (X:Bool) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq loading (X:Bool) ~a nextNPN (Y:Nat) = false [variant] .
eq loading (X:Bool) ~a handledCurrently(Y:Message?) = false [variant] .
eq loading (X:Bool) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq loading (X:Bool) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq loading (X:Bool) ~a displayedTopBar (Y:Label) = false [variant] .
eq loading (X:Bool) ~a displayedContent(Y:Label) = false [variant] .
eq loading (X:Bool) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a in (Y:LabelList) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a out (Y:LabelList) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a mem-in (Y:MaybeLabel) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a mem-out (Y:MaybeLabel) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a nic-in (Y:LabelList) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a nic-out (Y:LabelSet) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a nextNPN (Y:Nat) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a handledCurrently(Y:Message?) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a displayedTopBar (Y:Label) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a displayedContent(Y:Label) = false [variant] .
eq returnTo (X:MaybeConcPipeId) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq in (X:LabelList) ~a out (Y:LabelList) = false [variant] .
eq in (X:LabelList) ~a mem-in (Y:MaybeLabel) = false [variant] .
eq in (X:LabelList) ~a mem-out (Y:MaybeLabel) = false [variant] .
eq in (X:LabelList) ~a nic-in (Y:LabelList) = false [variant] .
eq in (X:LabelList) ~a nic-out (Y:LabelSet) = false [variant] .
eq in (X:LabelList) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq in (X:LabelList) ~a nextNPN (Y:Nat) = false [variant] .
eq in (X:LabelList) ~a handledCurrently(Y:Message?) = false [variant] .
eq in (X:LabelList) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq in (X:LabelList) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq in (X:LabelList) ~a displayedTopBar (Y:Label) = false [variant] .
eq in (X:LabelList) ~a displayedContent(Y:Label) = false [variant] .
eq in (X:LabelList) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq out (X:LabelList) ~a mem-in (Y:MaybeLabel) = false [variant] .
eq out (X:LabelList) ~a mem-out (Y:MaybeLabel) = false [variant] .
eq out (X:LabelList) ~a nic-in (Y:LabelList) = false [variant] .
eq out (X:LabelList) ~a nic-out (Y:LabelSet) = false [variant] .
eq out (X:LabelList) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq out (X:LabelList) ~a nextNPN (Y:Nat) = false [variant] .
eq out (X:LabelList) ~a handledCurrently(Y:Message?) = false [variant] .
eq out (X:LabelList) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq out (X:LabelList) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq out (X:LabelList) ~a displayedTopBar (Y:Label) = false [variant] .
eq out (X:LabelList) ~a displayedContent(Y:Label) = false [variant] .
eq out (X:LabelList) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq mem-in (X:MaybeLabel) ~a mem-out (Y:MaybeLabel) = false [variant] .
eq mem-in (X:MaybeLabel) ~a nic-in (Y:LabelList) = false [variant] .
eq mem-in (X:MaybeLabel) ~a nic-out (Y:LabelSet) = false [variant] .
eq mem-in (X:MaybeLabel) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq mem-in (X:MaybeLabel) ~a nextNPN (Y:Nat) = false [variant] .
eq mem-in (X:MaybeLabel) ~a handledCurrently(Y:Message?) = false [variant] .
eq mem-in (X:MaybeLabel) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq mem-in (X:MaybeLabel) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq mem-in (X:MaybeLabel) ~a displayedTopBar (Y:Label) = false [variant] .
eq mem-in (X:MaybeLabel) ~a displayedContent(Y:Label) = false [variant] .
eq mem-in (X:MaybeLabel) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq mem-out (X:MaybeLabel) ~a nic-in (Y:LabelList) = false [variant] .
eq mem-out (X:MaybeLabel) ~a nic-out (Y:LabelSet) = false [variant] .
eq mem-out (X:MaybeLabel) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq mem-out (X:MaybeLabel) ~a nextNPN (Y:Nat) = false [variant] .
eq mem-out (X:MaybeLabel) ~a handledCurrently(Y:Message?) = false [variant] .
eq mem-out (X:MaybeLabel) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq mem-out (X:MaybeLabel) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq mem-out (X:MaybeLabel) ~a displayedTopBar (Y:Label) = false [variant] .
eq mem-out (X:MaybeLabel) ~a displayedContent(Y:Label) = false [variant] .
eq mem-out (X:MaybeLabel) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq nic-in (X:LabelList) ~a nic-out (Y:LabelSet) = false [variant] .
eq nic-in (X:LabelList) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq nic-in (X:LabelList) ~a nextNPN (Y:Nat) = false [variant] .
eq nic-in (X:LabelList) ~a handledCurrently(Y:Message?) = false [variant] .
eq nic-in (X:LabelList) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq nic-in (X:LabelList) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq nic-in (X:LabelList) ~a displayedTopBar (Y:Label) = false [variant] .
eq nic-in (X:LabelList) ~a displayedContent(Y:Label) = false [variant] .
eq nic-in (X:LabelList) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq nic-out (X:LabelSet) ~a msgPolicy (Y:PolicySet) = false [variant] .
eq nic-out (X:LabelSet) ~a nextNPN (Y:Nat) = false [variant] .
eq nic-out (X:LabelSet) ~a handledCurrently(Y:Message?) = false [variant] .
eq nic-out (X:LabelSet) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq nic-out (X:LabelSet) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq nic-out (X:LabelSet) ~a displayedTopBar (Y:Label) = false [variant] .
eq nic-out (X:LabelSet) ~a displayedContent(Y:Label) = false [variant] .
eq nic-out (X:LabelSet) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq msgPolicy (X:PolicySet) ~a nextNPN (Y:Nat) = false [variant] .
eq msgPolicy (X:PolicySet) ~a handledCurrently(Y:Message?) = false [variant] .
eq msgPolicy (X:PolicySet) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq msgPolicy (X:PolicySet) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq msgPolicy (X:PolicySet) ~a displayedTopBar (Y:Label) = false [variant] .
eq msgPolicy (X:PolicySet) ~a displayedContent(Y:Label) = false [variant] .
eq msgPolicy (X:PolicySet) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq nextNPN (X:Nat) ~a handledCurrently(Y:Message?) = false [variant] .
eq nextNPN (X:Nat) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq nextNPN (X:Nat) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq nextNPN (X:Nat) ~a displayedTopBar (Y:Label) = false [variant] .
eq nextNPN (X:Nat) ~a displayedContent(Y:Label) = false [variant] .
eq nextNPN (X:Nat) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq handledCurrently(X:Message?) ~a weblabels (Y:WebProcInfoSet) = false [variant] .
eq handledCurrently(X:Message?) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq handledCurrently(X:Message?) ~a displayedTopBar (Y:Label) = false [variant] .
eq handledCurrently(X:Message?) ~a displayedContent(Y:Label) = false [variant] .
eq handledCurrently(X:Message?) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq weblabels (X:WebProcInfoSet) ~a netlabels (Y:NetProcInfoSet) = false [variant] .
eq weblabels (X:WebProcInfoSet) ~a displayedTopBar (Y:Label) = false [variant] .
eq weblabels (X:WebProcInfoSet) ~a displayedContent(Y:Label) = false [variant] .
eq weblabels (X:WebProcInfoSet) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq netlabels (X:NetProcInfoSet) ~a displayedTopBar (Y:Label) = false [variant] .
eq netlabels (X:NetProcInfoSet) ~a displayedContent(Y:Label) = false [variant] .
eq netlabels (X:NetProcInfoSet) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq displayedTopBar (X:Label) ~a displayedContent(Y:Label) = false [variant] .
eq displayedTopBar (X:Label) ~a activeWebapp (Y:WebProcId) = false [variant] .
eq displayedContent(X:Label) ~a activeWebapp (Y:WebProcId) = false [variant] .
--- 19. Add partially FVP in-attrset?(_|_) predicate for checking if an attribute of a given type exists in an attribute set
op in-attrset?(_|_) : Attribute AttributeSet -> Bool [metadata "104 true"] .
eq in-attrset?(fromKernel (X:MaybeMessageList) | (fromKernel (Y:MaybeMessageList), AS)) = true [variant] .
eq in-attrset?(toKernel (X:MaybeMessageList) | (toKernel (Y:MaybeMessageList), AS)) = true [variant] .
eq in-attrset?(nextWPN (X:Nat) | (nextWPN (Y:Nat), AS)) = true [variant] .
eq in-attrset?(rendered (X:MaybeLabel) | (rendered (Y:MaybeLabel), AS)) = true [variant] .
eq in-attrset?(URL (X:Label) | (URL (Y:Label), AS)) = true [variant] .
eq in-attrset?(loading (X:Bool) | (loading (Y:Bool), AS)) = true [variant] .
eq in-attrset?(returnTo (X:MaybeConcPipeId) | (returnTo (Y:MaybeConcPipeId), AS)) = true [variant] .
eq in-attrset?(in (X:LabelList) | (in (Y:LabelList), AS)) = true [variant] .
eq in-attrset?(out (X:LabelList) | (out (Y:LabelList), AS)) = true [variant] .
eq in-attrset?(mem-in (X:MaybeLabel) | (mem-in (Y:MaybeLabel), AS)) = true [variant] .
eq in-attrset?(mem-out (X:MaybeLabel) | (mem-out (Y:MaybeLabel), AS)) = true [variant] .
eq in-attrset?(nic-in (X:LabelList) | (nic-in (Y:LabelList), AS)) = true [variant] .
eq in-attrset?(nic-out (X:LabelSet) | (nic-out (Y:LabelSet), AS)) = true [variant] .
eq in-attrset?(msgPolicy (X:PolicySet) | (msgPolicy (Y:PolicySet), AS)) = true [variant] .
eq in-attrset?(nextNPN (X:Nat) | (nextNPN (Y:Nat), AS)) = true [variant] .
eq in-attrset?(handledCurrently(X:Message?) | (handledCurrently(Y:Message?), AS)) = true [variant] .
eq in-attrset?(weblabels (X:WebProcInfoSet) | (weblabels (Y:WebProcInfoSet), AS)) = true [variant] .
eq in-attrset?(netlabels (X:NetProcInfoSet) | (netlabels (Y:NetProcInfoSet), AS)) = true [variant] .
eq in-attrset?(displayedTopBar (X:Label) | (displayedTopBar (Y:Label), AS)) = true [variant] .
eq in-attrset?(displayedContent(X:Label) | (displayedContent(Y:Label), AS)) = true [variant] .
eq in-attrset?(activeWebapp (X:WebProcId) | (activeWebapp (Y:WebProcId), AS)) = true [variant] .
ceq in-attrset?(A | A', AS) = in-attrset?(A | AS) if A ~a A' = false .
eq in-attrset?(A | none) = false .
--- 20. Add partially FVP attr-dupl?() predicate for checking if an attribute type occurs twice in a given attribute set
op attr-dupl? : AttributeSet -> Bool [metadata "105 true"] .
eq attr-dupl?(fromKernel (X:MaybeMessageList), fromKernel (Y:MaybeMessageList), AS) = true [variant] .
eq attr-dupl?(toKernel (X:MaybeMessageList), toKernel (Y:MaybeMessageList), AS) = true [variant] .
eq attr-dupl?(nextWPN (X:Nat), nextWPN (Y:Nat), AS) = true [variant] .
eq attr-dupl?(rendered (X:MaybeLabel), rendered (Y:MaybeLabel), AS) = true [variant] .
eq attr-dupl?(URL (X:Label), URL (Y:Label), AS) = true [variant] .
eq attr-dupl?(loading (X:Bool), loading (Y:Bool), AS) = true [variant] .
eq attr-dupl?(returnTo (X:MaybeConcPipeId), returnTo (Y:MaybeConcPipeId), AS) = true [variant] .
eq attr-dupl?(in (X:LabelList), in (Y:LabelList), AS) = true [variant] .
eq attr-dupl?(out (X:LabelList), out (Y:LabelList), AS) = true [variant] .
eq attr-dupl?(mem-in (X:MaybeLabel), mem-in (Y:MaybeLabel), AS) = true [variant] .
eq attr-dupl?(mem-out (X:MaybeLabel), mem-out (Y:MaybeLabel), AS) = true [variant] .
eq attr-dupl?(nic-in (X:LabelList), nic-in (Y:LabelList), AS) = true [variant] .
eq attr-dupl?(nic-out (X:LabelSet), nic-out (Y:LabelSet), AS) = true [variant] .
eq attr-dupl?(msgPolicy (X:PolicySet), msgPolicy (Y:PolicySet), AS) = true [variant] .
eq attr-dupl?(nextNPN (X:Nat), nextNPN (Y:Nat), AS) = true [variant] .
eq attr-dupl?(handledCurrently(X:Message?), handledCurrently(Y:Message?), AS) = true [variant] .
eq attr-dupl?(weblabels (X:WebProcInfoSet), weblabels (Y:WebProcInfoSet), AS) = true [variant] .
eq attr-dupl?(netlabels (X:NetProcInfoSet), netlabels (Y:NetProcInfoSet), AS) = true [variant] .
eq attr-dupl?(displayedTopBar (X:Label), displayedTopBar (Y:Label), AS) = true [variant] .
eq attr-dupl?(displayedContent(X:Label), displayedContent(Y:Label), AS) = true [variant] .
eq attr-dupl?(activeWebapp (X:WebProcId), activeWebapp (Y:WebProcId), AS) = true [variant] .
ceq attr-dupl?(A,AS) = false if in-attrset?(A | AS) = false /\ attr-dupl?(AS) = false .
eq attr-dupl?(none) = false .
endfm
---
--- 21. Extract a Label/Pair from a Web/NetProcInfoSet by ProcessId
--- 22. Find a WebProcId in a WebProcInfoSet via NetProcId and NetProcInfoSet
--- 23. Check if a label appears in a WebProcInfo in a WebProcInfoSet
--- 24. Check if a label appears in the first component of a NetProcInfo in a NetProcInfoSet
--- 25. Check if a WebProc (specified by name or indirectly by NetProcId, NetProcInfoSet, and WebProcInfoSet)
--- has a loading?() attribute that is set to true
---
fmod IBOS-AUX-FVP is
pr CONFIGURATION-FVP-EXT .
pr LABEL-FVP-EXT .
pr MSG-FVP-EXT .
pr KERNEL-METADATA-FVP-EXT .
pr ATTRIBUTE-FVP-EXT .
var P? : ProcessId .
var P : ConcProcId .
var PP PP' : ConcPipeId .
var MP MP' : MaybePipeId .
var AP : AbsPipeId .
var WP : ConcWebProcId .
var NP NP' : ConcNetProcId .
var NN : NullProcId .
var SP : NonPipeId .
var C : Configuration .
var At : Attribute .
var A : AttributeSet .
var WIS : WebProcInfoSet .
var NIS : NetProcInfoSet .
var IN IN' OUT U R : Label .
--- 21. Extract a Label/Pair from a Web/NetProcInfoSet by ProcessId
op weblabel-by-pid : MaybeProcessId WebProcInfoSet -> MaybeLabel [metadata "121 L:Label"] .
eq weblabel-by-pid(WP, (pi(WP,IN),wp WIS)) = IN [variant] .
ceq weblabel-by-pid(P?, (pi(WP,IN),wp WIS)) = weblabel-by-pid(P?,WIS) if P? ~p WP = false . --- FIXME: this rule needed to solve problem in ABC proof
eq weblabel-by-pid(P?, mtWPIS) = nolabel .
eq weblabel-by-pid(NP, WIS) = nolabel .
eq weblabel-by-pid(ui, WIS) = nolabel .
eq weblabel-by-pid(AP, WIS) = nolabel .
eq weblabel-by-pid(SP, WIS) = nolabel .
eq weblabel-by-pid(NN, WIS) = nolabel .
op netlabelpair-by-pid : MaybeProcessId NetProcInfoSet -> MaybeLabelPair [metadata "122 L:LabelPair"] .
eq netlabelpair-by-pid(NP, (pi(NP,IN,OUT),np NIS)) = (IN,OUT) [variant] .
ceq netlabelpair-by-pid(P?, (pi(NP,IN,OUT),np NIS)) = netlabelpair-by-pid(P?,NIS) if P? ~p NP = false .
eq netlabelpair-by-pid(P?, mtNPIS) = nopair .
eq netlabelpair-by-pid(WP, NIS) = nopair .
eq netlabelpair-by-pid(ui, NIS) = nopair .
eq netlabelpair-by-pid(AP, NIS) = nopair .
eq netlabelpair-by-pid(SP, NIS) = nopair .
eq netlabelpair-by-pid(NN, NIS) = nopair .
--- 22. Find a WebProcId in a WebProcInfoSet via NetProcId and NetProcInfoSet
op webprocid-by-np : ConcNetProcId NetProcInfoSet WebProcInfoSet -> MaybeConcWebProcId [metadata "128 W:WebProcId"] .
eq webprocid-by-np(NP,pi(NP ,IN,OUT),np NIS,pi(WP,IN),wp WIS) = WP [variant] .
ceq webprocid-by-np(NP,pi(NP',IN,OUT),np NIS, WIS) = none if NP ~p NP' = false /\ webprocid-by-np(NP,NIS,WIS) = none .
ceq webprocid-by-np(NP,pi(NP ,IN,OUT),np NIS, WIS) = none if lbl-in-weblabels?(IN,WIS) = false /\ webprocid-by-np(NP,NIS,WIS) = none .
ceq webprocid-by-np(NP, NIS, WIS) = none if netlabelpair-by-pid(NP,NIS) = nopair .
eq webprocid-by-np(NP, mtNPIS, WIS) = none .
eq webprocid-by-np(NP, NIS, mtWPIS) = none .
--- 23. Check if a label appears in a WebProcInfo in a WebProcInfoSet
op lbl-in-weblabels? : Label WebProcInfoSet -> Bool [metadata "119 true"] .
eq lbl-in-weblabels?(IN,(pi(WP,IN ),wp WIS)) = true [variant] .
ceq lbl-in-weblabels?(IN,(pi(WP,IN'),wp WIS)) = lbl-in-weblabels?(IN,WIS) if IN ~l IN' = false .
eq lbl-in-weblabels?(IN,mtWPIS) = false .
--- 24. Check if a label appears in the first component of a NetProcInfo in a NetProcInfoSet
op np-by-inlbl? : Label NetProcInfoSet -> Bool [metadata "134 true"] .
eq np-by-inlbl?(IN,pi(NP,IN, OUT),np NIS) = true [variant] .
ceq np-by-inlbl?(IN,pi(NP,IN',OUT),np NIS) = np-by-inlbl?(IN,NIS) if IN ~l IN' = false .
eq np-by-inlbl?(IN, mtNPIS) = false .
--- 25. Check if a WebProc (specified by name or indirectly by NetProcId, NetProcInfoSet, and WebProcInfoSet)
--- has a loading?() attribute that is set to true
op proc-loaded? : MaybePipeId MaybePipeId NetProcInfoSet WebProcInfoSet Configuration -> Bool [metadata "133 true"] .
--- true if loaded proc exists and is matched by netproc
eq proc-loaded?(NN,WP, NIS, WIS,< WP | loading(true), A > C) = true [variant] .
eq proc-loaded?(NP,NN, pi(NP,IN,OUT),np NIS,pi(WP,IN),wp WIS,< WP | loading(true), A > C) = true [variant] .
eq proc-loaded?(NP,WP, pi(NP,IN,OUT),np NIS,pi(WP,IN),wp WIS,< WP | loading(true), A > C) = true [variant] .
--- discard attributes
ceq proc-loaded?(MP,MP', NIS, WIS,< WP | At, A > C) = proc-loaded?(MP,MP',NIS,WIS,< WP | A > C) if loading(true) ~a At = false .
--- discard processes
ceq proc-loaded?(MP,MP', NIS, WIS,< WP | A > C) = proc-loaded?(MP,MP',NIS,WIS,C) if in-attrset?(loading(true) | A) = false .
ceq proc-loaded?(MP,MP', NIS, WIS,< WP | A > C) = proc-loaded?(MP,MP',NIS,WIS,C) if weblabel-by-pid(WP,WIS) = nolabel .
eq proc-loaded?(MP,MP', NIS, WIS,< NP | A > C) = proc-loaded?(MP,MP',NIS,WIS,C) .
eq proc-loaded?(MP,MP', NIS, WIS,< ui | A > C) = proc-loaded?(MP,MP',NIS,WIS,C) .
eq proc-loaded?(MP,MP', NIS, WIS,< SP | A > C) = proc-loaded?(MP,MP',NIS,WIS,C) .
--- discard WebProcInfo
ceq proc-loaded?(MP,MP', NIS,pi(WP,IN),wp WIS, C) = proc-loaded?(MP,MP',NIS,WIS,C) if np-by-inlbl?(IN,NIS) = false .
ceq proc-loaded?(MP,MP', NIS,pi(WP,IN),wp WIS, C) = proc-loaded?(MP,MP',NIS,WIS,C) if in-conf?(WP,C) = false .
--- discard NetProcInfo
ceq proc-loaded?(MP,MP',pi(NP,IN,OUT),np NIS, WIS, C) = proc-loaded?(MP,MP',NIS,WIS,C) if MP ~p NP = false .
ceq proc-loaded?(MP,MP',pi(NP,IN,OUT),np NIS, WIS, C) = proc-loaded?(MP,MP',NIS,WIS,C) if lbl-in-weblabels?(IN,WIS) = false .
--- false if we cannot find our webproc in the configuration
ceq proc-loaded?(MP,WP, NIS, WIS, C) = false if in-conf?(WP,C) = false .
--- false if we cannot find our netproc in metadata
ceq proc-loaded?(NP,MP', NIS, WIS, C) = false if netlabelpair-by-pid(NP,NIS) = nopair .
--- false if our webproc cannot possibly match up with our netproc
ceq proc-loaded?(NP,WP, NIS, WIS, C) = false if weblabel-by-pid(WP,WIS) = nolabel .
--- false if our netproc id is wrong
eq proc-loaded?(WP,MP', NIS, WIS, C) = false .
eq proc-loaded?(ui,MP', NIS, WIS, C) = false .
eq proc-loaded?(AP,MP', NIS, WIS, C) = false .
--- false if our webproc id is wrong
eq proc-loaded?(MP,NP, NIS, WIS, C) = false .
eq proc-loaded?(MP,ui, NIS, WIS, C) = false .
eq proc-loaded?(MP,AP, NIS, WIS, C) = false .
--- false if both ids are none
eq proc-loaded?(NN,NN, NIS, WIS, C) = false .
endfm
---
--- This module defines neeeded FVP predicates for specifying the same-origin policy (SOP) invariant
---
fmod IBOS-SOP-PRED-FVP is
pr IBOS-AUX-FVP .
endfm
---
--- This module defines neeeded FVP predicates for specifying the address bar correctness (ABC) invariant
--- ABC-1. check that the rendered() and URL() attributes of each WebProc agree --- called R() in the paper
--- ABC-2. check that the display and address bar are consistent with the rendered() and URL() attributes of the active WebProc
--- [this is the intersection of properties 9 and 10 in the IBOS paper]
---
fmod IBOS-ABC-PRED-FVP is
pr IBOS-AUX-FVP .
var WP : ConcWebProcId .
var P : ConcProcId .
var U R : Label .
var A : AttributeSet .
var C : Configuration .
--- ABC-1. check that the rendered() and URL() attributes of each WebProc agree --- called R() in the paper
op webapp-url-render : ConcWebProcId Configuration -> MaybeLabelPair [metadata "136 L:LabelPair"] .
eq webapp-url-render(WP,< WP | URL(U), rendered(R), A > C) = (U,R) [variant] .
ceq webapp-url-render(WP,< P | A > C) = webapp-url-render(WP,C) if WP ~p P = false .
eq webapp-url-render(WP, none) = nopair .
ceq webapp-url-render(WP,< WP | A > C) = nopair if in-attrset?(URL(about-blank) | A) and in-attrset?(rendered(about-blank) | A) = false /\ webapp-url-render(WP,C) = nopair .
--- ABC-2. check that the display and address bar are consistent with the rendered() and URL() attributes of the active WebProc
--- [this is the intersection of properties P_9 and P_10 in the IBOS paper]
op display-topbar-consistent? : ConcWebProcId Label Label Configuration -> Bool [metadata "137 true"] .
eq display-topbar-consistent?(WP,about-blank,U,< WP | URL(U), A > C) = true [variant] .
eq display-topbar-consistent?(WP,R,U, < WP | rendered(R), URL(U), A > C) = true [variant] .
ceq display-topbar-consistent?(WP,R,U, < P | A > C) = display-topbar-consistent?(WP,R,U,C) if WP ~p P = false .
ceq display-topbar-consistent?(WP,R,U, < WP | A > C) = display-topbar-consistent?(WP,R,U,C) if in-attrset?(URL(about-blank) | A) = false .
ceq display-topbar-consistent?(WP,R,U, < WP | A > C) = display-topbar-consistent?(WP,R,U,C) if R ~l about-blank = false /\ in-attrset?(rendered(about-blank) | A) = false .
eq display-topbar-consistent?(WP,R,U, none) = false .
endfm
fmod IBOS-PREDS-FVP is
pr IBOS-SOP-PRED-FVP .
pr IBOS-ABC-PRED-FVP .
endfm
---
--- NON-FVP
---
---
--- 26. Canonicalizes attribute values so attribute types can be compared by standard equality
--- 27. Checks that each kind of attribute in an attribute set appears in a different set
---
fmod ATTRIBUTE-NONFVP-EXT is
pr ATTRIBUTE-FVP-EXT .
var A A' : Attribute . var AS AS' : AttributeSet .
--- 26. Canonicalizes attribute values so attribute types can be compared by standard equality
op _!a : AttributeSet -> AttributeSet [metadata "103"] .
eq (fromKernel (X:MaybeMessageList), AS) !a = fromKernel(mt), (AS !a) .
eq (toKernel (X:MaybeMessageList), AS) !a = toKernel(mt), (AS !a) .
eq (nextWPN (X:Nat), AS) !a = nextWPN(0), (AS !a) .
eq (rendered (X:MaybeLabel), AS) !a = rendered(about-blank), (AS !a) .
eq (URL (X:Label), AS) !a = URL(about-blank), (AS !a) .
eq (loading (X:Bool), AS) !a = loading(true), (AS !a) .
eq (returnTo (X:MaybeConcPipeId), AS) !a = returnTo(ui), (AS !a) .
eq (in (X:LabelList), AS) !a = in(mtLL), (AS !a) .
eq (out (X:LabelList), AS) !a = out(mtLL), (AS !a) .
eq (mem-in (X:MaybeLabel), AS) !a = mem-in(nolabel), (AS !a) .
eq (mem-out (X:MaybeLabel), AS) !a = mem-out(nolabel), (AS !a) .
eq (nic-in (X:LabelList), AS) !a = nic-in(mtLL), (AS !a) .
eq (nic-out (X:LabelSet), AS) !a = nic-out(mtLS), (AS !a) .
eq (msgPolicy (X:PolicySet), AS) !a = msgPolicy(mtPS), (AS !a) .
eq (nextNPN (X:Nat), AS) !a = nextNPN(0), (AS !a) .
eq (handledCurrently(X:Message?), AS) !a = handledCurrently(none), (AS !a) .
eq (weblabels (X:WebProcInfoSet), AS) !a = weblabels(mtWPIS), (AS !a) .
eq (netlabels (X:NetProcInfoSet), AS) !a = netlabels(mtNPIS), (AS !a) .
eq (displayedTopBar (X:Label), AS) !a = displayedTopBar(about-blank), (AS !a) .
eq (displayedContent(X:Label), AS) !a = displayedContent(about-blank), (AS !a) .
eq (activeWebapp (X:WebProcId), AS) !a = activeWebapp(webapp(0)), (AS !a) .
eq none !a = none .
eq (AS !a) !a = AS !a .
--- 27. Checks that each kind of attribute in an attribute set appears in a different set
op attr-subset?(_|_) : AttributeSet AttributeSet -> Bool [metadata "106"] .
ceq attr-subset?(A, AS | AS') = attr-subset?(AS | AS') if in-attrset?(A | AS') .
ceq attr-subset?(A, AS | AS') = false if in-attrset?(A | AS') = false .
eq attr-subset?(none | AS') = true .
endfm
---
--- 28. Lemmas for some FVP symbols
--- 29. Canonicalize all attribute values in all objects in Configuration
--- 30. Check that given Net/WebProcId is greater than all those in the Configuration
--- 31. Return true iff an attribute type is duplicated in some object in the Configuration
--- 32. Return true iff all Net/WebProcs in a Configuration have their required attributes (part of WF() predicate in paper)
--- 33. Check that there are no duplicate ProcessIds in a Web/NetProcInfoSet
--- 34. Check that given Net/WebProcId is greater than all those in the Net/WebProcInfoSet
--- 35. Check if a given Label occurs as first component in some NetProcInfo in a NetProcInfoSet
--- 36. Given a Net/WebProcId, extract the first/second component of a Net/WebProcInfo in a Net/WebProcInfoSet
--- 37. Check if a given ProcessId appears in a Net/WebProcInfo in a Net/WebProcInfoSet
--- 38. Check that all of the Net/WebProcs in a Configuration map bijectively to each Net/WebProcInfos in the given Net/WebProcInfoSets
--- 39. Check that each WebProc and URL() attribute map bijectively to each WebProcInfo in the given WebProcInfoSet
--- 40. For each NetProcInfo in the NetProcInfoSet, we require that IN and OUT labels match
--- 41. Check that all Fetch messages in a given message list have unique labels
---
fmod IBOS-AUX-NONFVP is
pr IBOS-PREDS-FVP .
pr KERNEL-POLICIES-NONFVP .
pr ATTRIBUTE-NONFVP-EXT .
var W N M : Nat .
var Z : NzNat .
var C C' : Configuration .
var NC : NeConfiguration .
var At At' : Attribute .
var A A' : AttributeSet .
var NA : NeAttributeSet .
var P? : ProcessId .
var P P' : ConcProcId .
var PP PP' : PipeId .
var NPP : NonPipeId .
var NP NP' : ConcNetProcId .
var NNP : NonNetPipeId .
var WP WP' : ConcWebProcId .
var NWP : NonWebPipeId .
var NNWP : NonConcNetWebProcId .
var NIS : NetProcInfoSet .
var WIS : WebProcInfoSet .
var NWIS : NeWebProcInfoSet .
var NNIS : NeNetProcInfoSet .
var B : Bool .
var RetMT : RetMsgType .
var FetchMT : FetchMsgType .
var MSGL MSGL2 : MessageList .
var L L' L1 L2 IN OUT : Label .
--- 28. Lemmas for some FVP symbols
eq attr-dupl?((A !a), A') = attr-dupl?(A, A') .
eq in-attrset?(At | (A !a), A') = in-attrset?(At | A, A') .
ceq in-conf?(NP,C) = false if fresh-np-id?(NP,C) = true .
ceq in-conf?(WP,C) = false if fresh-wp-id?(WP,C) = true .
ceq in-conf?(WP,C) = false if webapp-url-render(WP,C) = nopair .
eq conf-dupl?(< P | NA > C) = conf-dupl?(< P | none > C) .
ceq weblabel-by-pid(WP,WIS) = nolabel if fresh-weblabel?(WP,WIS) .
ceq netlabelpair-by-pid(NP,NIS) = nopair if fresh-netlabel?(NP,NIS) .
--- 29. Canonicalize all attribute values in all objects in Configuration
op _!c : Configuration -> Configuration [metadata "107"] .
op _!c : NetWebProcConfig -> NetWebProcConfig [metadata "107"] .
eq (< P | A > C) !c = < P | A !a > (C !c) .
eq none !c = none .
--- 30. Check that given Net/WebProcId is greater than all those in the Configuration
op fresh-np-id? : ConcNetProcId Configuration -> Bool [metadata "110"] .
eq fresh-np-id?(network(N ), < network(N + M) | A > C) = false .
eq fresh-np-id?(network(N + Z), < network(N) | A > C) = fresh-np-id?(network(N + Z),C) .
eq fresh-np-id?(NP, none ) = true .
eq fresh-np-id?(NP, < N:NonNetPipeId | A > C) = fresh-np-id?(NP,C) .
eq fresh-np-id?(NP, < NPP | A > C) = fresh-np-id?(NP,C) .
eq fresh-np-id?(NP, < P | NA > C) = fresh-np-id?(NP, < P | none > C) .
ceq fresh-np-id?(network(N + 1), C) = true if fresh-np-id?(network(N),C) .
op fresh-wp-id? : ConcWebProcId Configuration -> Bool [metadata "111"] .
eq fresh-wp-id?(webapp(N ), < webapp(N + M) | A > C) = false .
eq fresh-wp-id?(webapp(N + Z), < webapp(N) | A > C) = fresh-wp-id?(webapp(N + Z),C) .
eq fresh-wp-id?(WP, none ) = true .
eq fresh-wp-id?(WP, < N:NonWebPipeId | A > C) = fresh-wp-id?(WP,C) .
eq fresh-wp-id?(WP, < NPP | A > C) = fresh-wp-id?(WP,C) .
eq fresh-wp-id?(WP, < P | NA > C) = fresh-wp-id?(WP, < P | none > C) .
ceq fresh-wp-id?(webapp(N + 1), C) = true if fresh-wp-id?(webapp(N),C) .
--- 31. Return true iff an attribute type is duplicated in some object in the Configuration
op conf-attr-dupl? : Configuration -> Bool [metadata "112"] .
ceq conf-attr-dupl?(< P | At, At', A > C) = conf-attr-dupl?(< P | A > C) if At ~a At' = false /\ attr-dupl?(At, A) = false /\ attr-dupl?(At', A) = false .
eq conf-attr-dupl?(< P | At > C) = conf-attr-dupl?( C) .
eq conf-attr-dupl?(< P | none > C) = conf-attr-dupl?( C) .
ceq conf-attr-dupl?(< P | A > C) = true if attr-dupl?(A) .
eq conf-attr-dupl?(none) = false .
--- 32. Return true iff all Net/WebProcs in a Configuration have their required attributes (part of WF() predicate in paper)
op nwp-reqattrs? : NetWebProcConfig -> Bool [metadata "114"] .
eq nwp-reqattrs?(< NP | toKernel(TK:MessageList), fromKernel(FK:MessageList), returnTo(P:MaybeConcPipeId), mem-in(M1:MaybeLabel), mem-out(M2:MaybeLabel), A > C)
= nwp-reqattrs?(C) .
eq nwp-reqattrs?(< WP | toKernel(TK:MessageList), fromKernel(FK:MessageList), URL(L1:Label), rendered(L2:MaybeLabel), loading(B:Bool), A > C)
= nwp-reqattrs?(C) .
ceq nwp-reqattrs?(< NP | A > C) = false if attr-subset?(toKernel(mt),fromKernel(mt),returnTo(ui),mem-in(nolabel),mem-out(nolabel) | A) = false .
ceq nwp-reqattrs?(< WP | A > C) = false if attr-subset?(toKernel(mt),fromKernel(mt),URL(about-blank),rendered(about-blank),loading(true) | A) = false .
eq nwp-reqattrs?(none) = true .
--- 33. Check that there are no duplicate ProcessIds in a Web/NetProcInfoSet
op weblabels-dupl? : WebProcInfoSet -> Bool [metadata "115"] .
eq weblabels-dupl?(pi(WP,L) ,wp pi(WP,L') ,wp WIS) = true .
ceq weblabels-dupl?(pi(WP,L) ,wp WIS) = weblabels-dupl?(WIS) if pid-in-weblabels?(WP,WIS) = false .
eq weblabels-dupl?(pi(WP,L)) = false .
eq weblabels-dupl?(mtWPIS) = false .
op netlabels-dupl? : NetProcInfoSet -> Bool [metadata "116"] .
eq netlabels-dupl?(pi(NP,L,L') ,np pi(NP,L1,L2) ,np NIS) = true .
ceq netlabels-dupl?(pi(NP,L,L') ,np NIS) = netlabels-dupl?(NIS) if pid-in-netlabels?(NP,NIS) = false .
eq netlabels-dupl?(pi(NP,L,L')) = false .
eq netlabels-dupl?(mtNPIS) = false .
--- 34. Check that given Net/WebProcId is greater than all those in the Net/WebProcInfoSet
op fresh-weblabel? : ConcWebProcId WebProcInfoSet -> Bool [metadata "117"] .
eq fresh-weblabel?(webapp(N + Z),(pi(webapp(N ),L),wp WIS)) = fresh-weblabel?(webapp(N + Z),WIS) .
eq fresh-weblabel?(webapp(N), (pi(webapp(N + M),L),wp WIS)) = false .
eq fresh-weblabel?(webapp(N),mtWPIS) = true .
ceq fresh-weblabel?(webapp(N + Z),WIS) = true if fresh-weblabel?(webapp(N),WIS) .
op fresh-netlabel? : ConcNetProcId NetProcInfoSet -> Bool [metadata "118"] .
eq fresh-netlabel?(network(N + Z),(pi(network(N ),L,L'),np NIS)) = fresh-netlabel?(network(N + Z),NIS) .
eq fresh-netlabel?(network(N), (pi(network(N + M),L,L'),np NIS)) = false .
eq fresh-netlabel?(network(N),mtNPIS) = true .
ceq fresh-netlabel?(network(N + Z),NIS) = true if fresh-netlabel?(network(N),NIS) .
--- 35. Check if a given Label occurs as first component in some NetProcInfo in a NetProcInfoSet
op inlbl-in-netlabels? : Label NetProcInfoSet -> Bool [metadata "120"] .
eq inlbl-in-netlabels?(IN,(pi(NP,IN,OUT),np NIS)) = true .
ceq inlbl-in-netlabels?(L, (pi(NP,IN,OUT),np NIS)) = inlbl-in-netlabels?(L,NIS) if L ~l IN = false .
eq inlbl-in-netlabels?(L,mtNPIS) = false .
--- 36. Given a Net/WebProcId, extract the first/second component of a Net/WebProcInfo in a Net/WebProcInfoSet
op in-netlabel-by-pid : ProcessId NetProcInfoSet -> MaybeLabel [metadata "123"] .
eq in-netlabel-by-pid(P?,NIS) = inlbl(netlabelpair-by-pid(P?,NIS)) .
op out-netlabel-by-pid : ProcessId NetProcInfoSet -> MaybeLabel [metadata "124"] .
eq out-netlabel-by-pid(P?,NIS) = outlbl(netlabelpair-by-pid(P?,NIS)) .
--- 37. Check if a given ProcessId appears in a Net/WebProcInfo in a Net/WebProcInfoSet
op pid-in-netlabels? : ProcessId NetProcInfoSet -> Bool [metadata "125"] .
ceq pid-in-netlabels?(P?,NIS) = true if (netlabelpair-by-pid(P?,NIS) ~lp nopair) = false .
ceq pid-in-netlabels?(P?,NIS) = false if (netlabelpair-by-pid(P?,NIS) ~lp nopair) = true .
op pid-in-weblabels? : ProcessId WebProcInfoSet -> Bool [metadata "126"] .
ceq pid-in-weblabels?(P?,WIS) = true if (weblabel-by-pid(P?,WIS) ~l nolabel) = false .
ceq pid-in-weblabels?(P?,WIS) = false if (weblabel-by-pid(P?,WIS) ~l nolabel) = true .
--- 38. Check that all of the Net/WebProcs in a Configuration map bijectively to each Net/WebProcInfos in the given Net/WebProcInfoSets
op conf-labels-eqset? : Configuration WebProcInfoSet NetProcInfoSet -> Bool [metadata "127"] .
--- throw away useless processes
eq conf-labels-eqset?(< ui | A > C,WIS,NIS) = conf-labels-eqset?(C,WIS,NIS) .
eq conf-labels-eqset?(< NPP | A > C,WIS,NIS) = conf-labels-eqset?(C,WIS,NIS) .
--- check web/netprocs are compatible
eq conf-labels-eqset?(< WP | A > C,(pi(WP,L),wp WIS), NIS ) = conf-labels-eqset?(C,WIS,NIS) .
eq conf-labels-eqset?(< NP | A > C, WIS, (pi(NP,L,L'),np NIS)) = conf-labels-eqset?(C,WIS,NIS) .
--- true termination
eq conf-labels-eqset?(none,mtWPIS, mtNPIS) = true .
--- non-recursive failure modes
eq conf-labels-eqset?(none,NWIS, NIS ) = false .
eq conf-labels-eqset?(none,WIS, NNIS ) = false .
--- recursive failure modes
ceq conf-labels-eqset?(< WP | A > C, WIS, NIS ) = false if pid-in-weblabels?(WP,WIS) = false .
ceq conf-labels-eqset?(< NP | A > C, WIS, NIS ) = false if pid-in-netlabels?(NP,NIS) = false .
ceq conf-labels-eqset?(C,(pi(WP,L),wp WIS), NIS ) = false if in-conf?(WP,C) = false .
ceq conf-labels-eqset?(C, WIS,(pi(NP,L,L'),np NIS)) = false if in-conf?(NP,C) = false .
--- simplification
eq conf-labels-eqset?(< P | NA > C,WIS,NIS) = conf-labels-eqset?(< P | none > C,WIS,NIS) .
--- 39. Check that each WebProc and URL() attribute map bijectively to each WebProcInfo in the given WebProcInfoSet
op webapp-url-eqset? : Configuration WebProcInfoSet -> Bool [metadata "138"] .
---
eq webapp-url-eqset?(< ui | A > C,WIS) = webapp-url-eqset?(C,WIS) .
eq webapp-url-eqset?(< NPP | A > C,WIS) = webapp-url-eqset?(C,WIS) .
eq webapp-url-eqset?(< NP | A > C,WIS) = webapp-url-eqset?(C,WIS) .
---
eq webapp-url-eqset?(< WP | URL(L), A > C,(pi(WP,L ),wp WIS)) = webapp-url-eqset?(C,WIS) .
eq webapp-url-eqset?(none, mtWPIS ) = true .
eq webapp-url-eqset?(NC, mtWPIS ) = false .
eq webapp-url-eqset?(none, NWIS ) = false .
ceq webapp-url-eqset?(< WP | URL(L), A > C,(pi(WP,L'),wp WIS)) = false if L ~l L' = false .
ceq webapp-url-eqset?(< WP | A > C, WIS ) = false if pid-in-weblabels?(WP,WIS) = false .
ceq webapp-url-eqset?( C,(pi(WP,L ),wp WIS)) = false if in-conf?(WP,C) = false .
---
eq webapp-url-eqset?(< WP | toKernel(MSGL), A > C,WIS) = webapp-url-eqset?(< WP | A > C,WIS) .
eq webapp-url-eqset?(< WP | fromKernel(MSGL), A > C,WIS) = webapp-url-eqset?(< WP | A > C,WIS) .
eq webapp-url-eqset?(< WP | rendered(L), A > C,WIS) = webapp-url-eqset?(< WP | A > C,WIS) .
eq webapp-url-eqset?(< WP | loading(B), A > C,WIS) = webapp-url-eqset?(< WP | A > C,WIS) .
--- 40. For each NetProcInfo in the NetProcInfoSet, we require that IN and OUT labels match
op netlabels-match? : NetProcInfoSet -> Bool [metadata "197"] .
ceq netlabels-match?(pi(NP,IN,OUT),np NIS) = netlabels-match?(NIS) if IN ~l OUT .
ceq netlabels-match?(pi(NP,IN,OUT),np NIS) = false if IN ~l OUT = false .
eq netlabels-match?( mtNPIS) = true .
--- 41. Check that all Fetch messages in a given message list have unique labels
op ui-consistent? : MessageList WebProcInfoSet -> Bool [metadata "199"] .
--- SWITCH-TAB
ceq ui-consistent?(MSGL @ msg(PP,PP',MSG-SWITCH-TAB,OUT) @ MSGL2,WIS) = ui-consistent?(MSGL @ MSGL2,WIS)
if pid-in-weblabels?(PP',WIS) .
ceq ui-consistent?(MSGL @ msg(PP,PP',MSG-SWITCH-TAB,OUT) @ MSGL2,WIS) = false
if pid-in-weblabels?(PP',WIS) = false .
--- NEW-URL
ceq ui-consistent?(MSGL @ msg(PP,webapp,MSG-NEW-URL,OUT) @ MSGL2,WIS) = ui-consistent?(MSGL @ MSGL2,WIS)
if newurl-nodupl?(OUT,MSGL @ MSGL2) .
ceq ui-consistent?(MSGL @ msg(PP,PP',MSG-NEW-URL,OUT) @ MSGL2,WIS) = false
if PP' ~p webapp and newurl-nodupl?(OUT,MSGL @ MSGL2) = false .
--- OTHER MESSAGES
eq ui-consistent?(MSGL @ msg(PP,PP',RetMT, OUT) @ MSGL2,WIS) = false .
eq ui-consistent?(MSGL @ msg(PP,PP',FetchMT,OUT) @ MSGL2,WIS) = false .
eq ui-consistent?(mt,WIS) = true .
--- Simplification of WIS
ceq ui-consistent?(MSGL,pi(WP,IN),wp WIS) = true if fresh-weblabel?(WP,WIS) /\ ui-consistent?(MSGL,WIS) .
endfm
---
--- This module defines needed Non-FVP predicates for specifying the same-origin (SOP) invariant
--- SOP-1. Check the same-origin policy (SOP), written `p` for brevity
---
fmod IBOS-SOP-PRED is
pr IBOS-AUX-NONFVP .
var B : Bool .
var NWC : NetWebProcConfig .
var W N NNP NWA : Nat .
var A A' : AttributeSet .
var WIS : WebProcInfoSet .
var NIS : NetProcInfoSet .
var ML ML2 : MessageList .
var UI : UIId .
var NI NI1 NI2 : ConcNetProcId .
var WI : ConcWebProcId .
var PI PI' : PipeId .
var CPI CPI' : ConcPipeId .
var L IN OUT OUT1 OUT2 : Label .
var LL LL' : LabelList .
var MT : MsgType .
var RetMT : RetMsgType .
var FetchMT : FetchMsgType .
var NonFetchMT : NonFetchMsgType .
var NonRetMT : NonRetMsgType .
var NonRFMT : NonRetFetchMsgType .
var AMsg : Message .
var NFL NFL2 : NonFetchMsgList .
var HFL HFL2 : HasFetchMsgList .
var FM : FetchMsg .
var M? : Message? .
var NRM : NonRetMsg .
var NFM : NonFetchMsg .
--- SOP-1. Check the same-origin policy (SOP), written `p` for brevity
op p : NetWebProcConfig WebProcInfoSet NetProcInfoSet Message? -> Bool? [metadata "200"] .
--- Prop 1 ---
--- any FETCH message in fromKernel queue of NetProc, agrees with kernel metadata
ceq p(< NI | fromKernel(ML @ msg(PI,PI',MSG-FETCH-URL,OUT) @ ML2), A > NWC,WIS,NIS,M?) =
p(< NI | fromKernel(ML @ ML2), A > NWC,WIS,NIS,M?)
if PI' ~p NI
/\ (weblabel-by-pid(PI,WIS),OUT) ~lp netlabelpair-by-pid(NI,NIS)
/\ proc-loaded?(NI,PI,NIS,WIS,NWC) .
ceq p(< NI | fromKernel(ML @ NFM @ ML2), A > NWC, WIS, NIS,M?) =
p(< NI | fromKernel(ML @ ML2), A > NWC, WIS, NIS,M?)
if pid-in-netlabels?(NI,NIS) .
ceq p(< NI | fromKernel(mt), A > NWC, WIS, NIS, M?) =
p(< NI | fromKernel(nolist), A > NWC, WIS, NIS, M?)
if pid-in-netlabels?(NI,NIS) .
--- Prop 1 Negation ---
ceq p(< NI | fromKernel(ML @ msg(PI,PI',MSG-FETCH-URL,OUT) @ ML2), A > NWC,WIS,NIS,M?) = false
if PI' ~p NI and (weblabel-by-pid(PI,WIS),OUT) ~lp netlabelpair-by-pid(NI,NIS) and proc-loaded?(NI,PI,NIS,WIS,NWC) = false .
--- Prop 2 ---
--- mem-in() attr correlates with kernel metadata
ceq p(< NI | mem-in(OUT), A > NWC,WIS,NIS,M?) =
p(< NI | mem-in(nolabel), A > NWC,WIS,NIS,M?)
if out-netlabel-by-pid(NI,NIS) ~l OUT
/\ proc-loaded?(NI,none,NIS,WIS,NWC) .
--- Prop 2 Negation ---
ceq p(< NI | mem-in(OUT), A > NWC,WIS,NIS,M?) = false
if out-netlabel-by-pid(NI,NIS) ~l OUT = false .
--- Prop 3 ---
--- mem-out() attr correlates with kernel metadata
ceq p(< NI | mem-out(OUT), A > NWC,WIS,NIS,M?) =
p(< NI | mem-out(nolabel), A > NWC,WIS,NIS,M?)
if out-netlabel-by-pid(NI,NIS) ~l OUT
/\ proc-loaded?(NI,none,NIS,WIS,NWC) .
--- Prop 3 Negation ---
ceq p(< NI | mem-out(OUT), A > NWC,WIS,NIS,M?) = false
if out-netlabel-by-pid(NI,NIS) ~l OUT = false .
--- Prop 4 ---
--- NOTE: should false case be relaxed to don't care instead of NonRetMsgList
ceq p(< WI | loading(true), fromKernel(ML @ msg(PI,PI',MSG-RETURN-URL,OUT) @ ML2), A > NWC,WIS,NIS,M?) =
p(< WI | loading(true), fromKernel(ML @ ML2), A > NWC,WIS,NIS,M?)
if WI ~p PI'
/\ (weblabel-by-pid(WI,WIS),OUT) ~lp netlabelpair-by-pid(PI,NIS) .
ceq p(< WI | fromKernel(ML @ NRM @ ML2), A > NWC,WIS,NIS,M?) =
p(< WI | fromKernel(ML @ ML2), A > NWC,WIS,NIS,M?)
if pid-in-weblabels?(WI,WIS) .
ceq p(< WI | fromKernel(mt), A > NWC,WIS,NIS,M?) =
p(< WI | fromKernel(nolist), A > NWC,WIS,NIS,M?)
if pid-in-weblabels?(WI,WIS) .
ceq p(< WI | loading(false), fromKernel(ML ), A > NWC,WIS,NIS,M?) =
p(< WI | loading(false), fromKernel(nolist), A > NWC,WIS,NIS,M?)
if pid-in-weblabels?(WI,WIS) .
--- Prop 4 -- Negation
ceq p(< WI | loading(true), fromKernel(ML @ msg(PI,PI',MSG-RETURN-URL,OUT) @ ML2), A > NWC,WIS,NIS,M?) = false
if WI ~p PI' and (weblabel-by-pid(WI,WIS),OUT) ~lp netlabelpair-by-pid(PI,NIS) = false .
--- Other needed pieces:
---
--- 1. WebProc toKernel queue invariant
--- 2. NetProc toKernel queue invariant
--- 3. NetProc in/out attribute invariants
--- 4. currentlyHandled attribute invariant
--- 5. NetProcInfoSet/WebProcInfoSet invariants
--- 6. Miscellaneous
---
--- 1. WebProc toKernel queue invariant
--- a. A fetch msg should be in the queue only if the loading attribute is true
--- b. The fetch msg src/target should be consistent with our policy
ceq p(< WI | toKernel(ML @ NFM @ ML2), A > NWC,WIS,NIS,M?) =
p(< WI | toKernel(ML @ ML2), A > NWC,WIS,NIS,M?)
if pid-in-weblabels?(WI,WIS) .
ceq p(< WI | loading(true), URL(OUT1), toKernel(ML @ msg(PI,PI',MSG-FETCH-URL,OUT2) @ ML2), A > NWC,WIS,NIS,M?) =
p(< WI | loading(true), URL(OUT1), toKernel(ML @ ML2), A > NWC,WIS,NIS,M?)
if pid-in-weblabels?(WI,WIS)
/\ PI ~p WI
/\ PI' ~p network
/\ OUT1 ~l OUT2 .
ceq p(< WI | toKernel(mt), A > NWC,WIS,NIS,M?) =
p(< WI | toKernel(nolist), A > NWC,WIS,NIS,M?)
if pid-in-weblabels?(WI,WIS) .
ceq p(< WI | URL(OUT1), toKernel(ML @ msg(PI,PI',MSG-FETCH-URL,OUT2) @ ML2), A > NWC,WIS,NIS,M?) = false
if OUT1 ~l OUT2 = false .
ceq p(< WI | toKernel(ML @ msg(PI,PI',MSG-FETCH-URL,OUT2) @ ML2), A > NWC,WIS,NIS,M?) = false
if PI ~p WI and PI' ~p network = false .
eq p(< WI | loading(false), toKernel(HFL), A > NWC,WIS,NIS,M?) = false .
--- 2. NetProc toKernel queue invariant
--- a. if the message type is MSG-RETURN-URL, then:
--- i. message target is from returnTo - which comes from a webapp that matches this one on the IN
--- ii. message label is from the in() attribute --- which means it comes from the Webapp URL, encoded in the OUT
ceq p(< NI | toKernel(ML @ msg(PI,PI',MSG-RETURN-URL,OUT) @ ML2), A > NWC,WIS,NIS,M?) =
p(< NI | toKernel(ML @ ML2), A > NWC,WIS,NIS,M?)
if PI ~p NI
/\ (weblabel-by-pid(PI',WIS),OUT) ~lp netlabelpair-by-pid(NI,NIS)
/\ proc-loaded?(NI,PI',NIS,WIS,NWC) .
ceq p(< NI | toKernel(ML @ NRM @ ML2), A > NWC,WIS,NIS,M?) =
p(< NI | toKernel(ML @ ML2), A > NWC,WIS,NIS,M?)
if pid-in-netlabels?(NI,NIS) .
ceq p(< NI | toKernel(mt), A > NWC,WIS,NIS,M?) =
p(< NI | toKernel(nolist), A > NWC,WIS,NIS,M?)
if pid-in-netlabels?(NI,NIS) .
--- negation
ceq p(< NI | toKernel(ML @ msg(PI,PI',MSG-RETURN-URL,OUT) @ ML2), A > NWC,WIS,NIS,M?) = false
if PI ~p NI and (weblabel-by-pid(PI',WIS),OUT) ~lp netlabelpair-by-pid(PI,NIS) and proc-loaded?(NI,PI',NIS,WIS,NWC) = false .
--- 3. in()/out() attribute invariants
ceq p(< NI | out(LL ; OUT ; LL'), A > NWC,WIS,NIS,M?) =
p(< NI | out(LL ; LL'), A > NWC,WIS,NIS,M?)
if out-netlabel-by-pid(NI,NIS) ~l OUT
/\ proc-loaded?(NI,none,NIS,WIS,NWC) .
ceq p(< NI | in(LL ; OUT ; LL'), A > NWC,WIS,NIS,M?) =
p(< NI | in(LL ; LL'), A > NWC,WIS,NIS,M?)
if out-netlabel-by-pid(NI,NIS) ~l OUT
/\ proc-loaded?(NI,none,NIS,WIS,NWC) .
--- in/out invariant negation
ceq p(< NI | in (LL ; OUT ; LL'), A > NWC,WIS,NIS,M?) = false
if out-netlabel-by-pid(NI,NIS) ~l OUT = false .
ceq p(< NI | out(LL ; OUT ; LL'), A > NWC,WIS,NIS,M?) = false
if out-netlabel-by-pid(NI,NIS) ~l OUT = false .
--- 4. currentlyHandled() attribute invariant
--- NB: FetchMT cases needed for 6-a or 6-b
--- NB: NEW-URL case needed for new-url
--- a. handle messages to NetProcs
eq p(NWC, WIS,NIS,msg(ui, webapp,MSG-NEW-URL, OUT)) = p(NWC,WIS,NIS,none) .
ceq p(NWC, WIS,NIS,msg(ui, CPI, MSG-SWITCH-TAB,OUT)) = p(NWC,WIS,NIS,none) if pid-in-weblabels?(CPI,WIS) .
ceq p(NWC, WIS,NIS,msg(ui, CPI, MSG-SWITCH-TAB,OUT)) = false if pid-in-weblabels?(CPI,WIS) = false .
---
ceq p(NWC,WIS,NIS,msg(CPI, NI, FetchMT, OUT)) = p(NWC,WIS,NIS,none) if proc-loaded?(NI,CPI,NIS,WIS,NWC) /\ (weblabel-by-pid(CPI, WIS),OUT) ~lp netlabelpair-by-pid(NI,NIS) .
ceq p(NWC,WIS,NIS,msg(CPI, NI, NonFetchMT, OUT)) = p(NWC,WIS,NIS,none) if pid-in-netlabels?(NI,NIS) .
ceq p(NWC,WIS,NIS,msg(CPI, NI, FetchMT, OUT)) = false if proc-loaded?(NI,CPI,NIS,WIS,NWC) and (weblabel-by-pid(CPI, WIS),OUT) ~lp netlabelpair-by-pid(NI,NIS) = false .
ceq p(NWC,WIS,NIS,msg(CPI, NI, NonFetchMT, OUT)) = false if pid-in-netlabels?(NI,NIS) = false .
--- b. handle messages to WebProcs
ceq p(NWC,WIS,NIS,msg(CPI, WI, RetMT, OUT)) = p(NWC,WIS,NIS,none) if proc-loaded?(CPI,WI,NIS,WIS,NWC) /\ (weblabel-by-pid(WI,WIS),OUT) ~lp netlabelpair-by-pid(CPI,NIS) .
ceq p(NWC,WIS,NIS,msg(CPI, WI, NonRetMT, OUT)) = p(NWC,WIS,NIS,none) if pid-in-weblabels?(WI,WIS) .
ceq p(NWC,WIS,NIS,msg(CPI, WI, RetMT, OUT)) = false if proc-loaded?(CPI,WI,NIS,WIS,NWC) and (weblabel-by-pid(WI,WIS),OUT) ~lp netlabelpair-by-pid(CPI, NIS) = false .
ceq p(NWC,WIS,NIS,msg(CPI, WI, NonRetMT, OUT)) = false if pid-in-weblabels?(WI,WIS) = false .
--- 5. NetProcInfoSet/WebProcInfoSet invariants
ceq p(NWC,(pi(WI,IN),wp WIS), NIS, M?) = p(NWC,WIS,NIS,M?) if in-conf?(WI,NWC) = false /\ inlbl-in-netlabels?(IN,NIS) = false .
ceq p(NWC,(pi(WI,IN),wp WIS),(pi(NI,IN,OUT),np NIS),M?) = p(NWC,WIS,NIS,M?) if in-conf?(WI,NWC) = false /\ in-conf?(NI,NWC) = false .
--- Needed for 6-a/6-b and new-url
ceq p(NWC, WIS ,(pi(NI,IN,OUT),np NIS),M?) = true if p(NWC,WIS,NIS,M?) = true .
ceq p(NWC,(pi(WI,IN),wp WIS), NIS, M?) = true if p(NWC,WIS,NIS,M?) = true .
--- 6. Miscellaneous invariants
--- a. process consumption invariants
eq p(< WI | toKernel(nolist), fromKernel(nolist), A > NWC,WIS,NIS,M?) = p(NWC,WIS,NIS,M?) .
eq p(< NI | toKernel(nolist), fromKernel(nolist), mem-in(nolabel), mem-out(nolabel), in(mtLL), out(mtLL), A > NWC,WIS,NIS,M?) = p(NWC,WIS,NIS,M?) .
--- b. attribute canonization
ceq p(< WI | loading(true), A > NWC,WIS,NIS,M?) = true if p(< WI | loading(false), A > NWC,WIS,NIS,M?) .
eq p(< WI | rendered(L), A > NWC,WIS,NIS,M?) = p(< WI | rendered(nolabel), A > NWC,WIS,NIS,M?) .
ceq p(< NI | returnTo(CPI), A > NWC,WIS,NIS,M?) = p(< NI | returnTo(none), A > NWC,WIS,NIS,M?)
if proc-loaded?(NI,CPI,NIS,WIS,NWC) .
--- c.i. any WebProc corresponding to a NetProc must be loaded
ceq p(< NI | A > NWC,WIS,NIS,M?) = false
if proc-loaded?(NI,none,NIS,WIS,NWC) = false .
--- c.ii. any WebProc referenced by a returnTo() attribute must be loaded
ceq p(< NI | returnTo(CPI), A > NWC,WIS,NIS,M?) = false
if proc-loaded?(NI,CPI,NIS,WIS,NWC) = false .
--- e. every NetProc must have a metadata label
ceq p(< NI | A > NWC,WIS,NIS,M?) = false
if pid-in-netlabels?(NI,NIS) = false .
--- f. every WebProc must have a metadata label
ceq p(< WI | A > NWC,WIS,NIS,M?) = false
if pid-in-weblabels?(WI,WIS) = false .
--- g. the true case, i.e. everything is consumed
eq p(none,mtWPIS,mtNPIS,none) = true .
endfm
---
--- This module defines neeeded Non-FVP predicates for specifying the address bar correctness (ABC) invariant
--- ABC-3. For each WebProc, the rendered() attribute should be blank or equal to the URL() attribute
---
fmod IBOS-ABC-PRED is
pr IBOS-AUX-NONFVP .
var NIS : NetProcInfoSet .
var NWC : NetWebProcConfig .
var WI : ConcWebProcId .
var NI : ConcNetProcId .
var A : AttributeSet .
var ML : MessageList .
var IN OUT L : Label .
var B : Bool .
--- ABC-3. For each WebProc, the rendered() attribute should be blank or equal to the URL() attribute
op render-consistent? : NetWebProcConfig -> Bool [metadata "196"] .
eq render-consistent?(< NI | A > NWC) = render-consistent?(NWC) .
ceq render-consistent?(< WI | URL(OUT), rendered(L), A > NWC) = render-consistent?(NWC) if L blank-or-equal OUT .
ceq render-consistent?(< WI | URL(OUT), rendered(L), A > NWC) = false if L blank-or-equal OUT = false .
eq render-consistent?(none) = true .
---
eq render-consistent?(< WI | loading(B), A > NWC) = render-consistent?(< WI | A > NWC) .
eq render-consistent?(< WI | toKernel(ML), A > NWC) = render-consistent?(< WI | A > NWC) .
eq render-consistent?(< WI | fromKernel(ML), A > NWC) = render-consistent?(< WI | A > NWC) .
endfm
--- This module gathers all additional predicates together
fmod IBOS-PREDS is
pr IBOS-SOP-PRED .
pr IBOS-ABC-PRED .
endfm
--- This module enriches the IBOS system extended with the `stop` rule with all additional predicates
mod IBOS-STOP-WITH-PREDS is
pr IBOS-PREDS .
pr IBOS-STOP .
endm