Skip to content

Commit be120fd

Browse files
spderossospderosso
committed
setdomain changes
1 parent c292497 commit be120fd

6 files changed

Lines changed: 70 additions & 20 deletions

File tree

‎same-origin-policy/src/browser.als‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,7 @@ open http
99
sig Document {
1010
src: Url, -- URL from which this document was originated
1111
content: Resource -> Time, -- the content of the document (i.e., DOM)
12-
-- "document.domain" property, at any time it could match several hosts (if
13-
-- for example is set to something like *.foo.com)
14-
domain: Domain -> Time,
12+
domain: Domain -> Time, -- "document.domain" property
1513
}
1614

1715
sig Browser extends Client {

‎same-origin-policy/src/http.als‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,18 @@ open call[Endpoint]
99
abstract sig Resource {}
1010
abstract sig Endpoint {}
1111

12-
sig Protocol, Domain, Port, Path {}
12+
sig Protocol, Port, Path {}
13+
sig Domain { subsumes: set Domain }
14+
15+
fact subsumesRule {
16+
all disj d, d1, d2: Domain |
17+
-- reflexive
18+
d in d.subsumes and
19+
-- assymetric
20+
(d1 in d.subsumes => d not in d1.subsumes) and
21+
-- transitive
22+
(d1 in d.subsumes and d2 in d1.subsumes => d2 in d.subsumes)
23+
}
1324

1425
sig Url {
1526
protocol: Protocol,

‎same-origin-policy/src/origin.als‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,4 +19,8 @@ fun origin[u: Url] : Origin {
1919
{o: Origin | o.host = u.host and o.protocol = u.protocol and o.port = u.port }
2020
}
2121

22+
fun origin[u: Url, h: Domain] : Origin {
23+
{o: Origin | o.host = h and o.protocol = u.protocol and o.port = u.port }
24+
}
25+
2226
run {}

‎same-origin-policy/src/script.als‎

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -48,13 +48,6 @@ sig WriteDom extends BrowserOp { newDom: Resource }{
4848
domain.end = domain.start
4949
}
5050

51-
// Modify the document.domain property
52-
sig SetDomain extends BrowserOp { newDomain: set Domain }{
53-
doc = from.context
54-
domain.end = domain.start ++ doc -> newDomain
55-
-- no change to the content of the document
56-
content.end = content.start
57-
}
5851

5952
// Handlers for browser script events
6053
abstract sig EventHandler extends Call {
@@ -72,9 +65,3 @@ pred noBrowserChange[start, end: Time] {
7265
pred noDocumentChange[start, end: Time] {
7366
content.end = content.start and domain.end = domain.start
7467
}
75-
76-
/* Commands */
77-
78-
// Can a script set the "document.domain" property with a new_domain that doesn't
79-
// match the src?
80-
check { all sd: SetDomain | sd.doc.src.host in sd.newDomain }

‎same-origin-policy/src/setdomain.als‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
/**
2+
* setdomain.als
3+
* A model of the operations related to the document.domain
4+
* property
5+
*/
6+
module setDomain
7+
8+
open http
9+
open script
10+
11+
// Modify the document.domain property
12+
sig SetDomain extends BrowserOp { newDomain: Domain }{
13+
doc = from.context
14+
domain.end = domain.start ++ doc -> newDomain
15+
-- no change to the content of the document
16+
content.end = content.start
17+
}
18+
19+
// Scripts can only set the domain property to only one that is a right-hand,
20+
// fully-qualified fragment of its hostname
21+
fact setDomainRule {
22+
all d: Document | d.src.host in (d.domain.Time).subsumes
23+
}
24+
25+
/* Commands */
26+
27+
// Can a script set the "document.domain" property with a new_domain that
28+
// doesn't match the host of the src?
29+
check { all sd: SetDomain | sd.doc.src.host = sd.newDomain }
30+
31+
32+
// Can a script set the "document.domain" property with a new_domain that
33+
// doesn't match the host of the src even if there are no domains that subsume
34+
// others?
35+
run {
36+
some SetDomain
37+
all sd: SetDomain | sd.doc.src.host != sd.newDomain
38+
no d: Domain | some d.subsumes
39+
}

‎same-origin-policy/src/sop.als‎

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module sop
77
open http
88
open browser
99
open script
10+
open setDomain
1011
open cors
1112

1213
pred sameOriginPolicy {
@@ -19,9 +20,13 @@ pred domSop {
1920
all c: ReadDom + WriteDom |
2021
-- A script can only access the DOM of a document with the same origin or
2122
origin[c.doc.src] = origin[c.from.context.src] or
22-
-- (relaxation) script's context and the target document have the same
23-
-- domain property
24-
c.doc.domain = c.from.context.domain
23+
-- (relaxation) the domain property of both the script's context and the
24+
-- target document has either been set or unset in both and
25+
(#((c.prevs <: SetDomain).doc & (c.doc + c.from.context)) != 1 and
26+
-- they have the same origin (using the domain property as the host and not
27+
-- the src host)
28+
origin[c.doc.src, c.doc.domain.(c.start)] =
29+
origin[c.from.context.src, c.from.context.domain.(c.start)])
2530
}
2631

2732
pred xmlHttpReqSop {
@@ -31,3 +36,9 @@ pred xmlHttpReqSop {
3136
-- (relaxation) it's a CORS request
3237
x in CorsRequest
3338
}
39+
40+
41+
/* Commands */
42+
43+
// Can a script read or write the DOM of a document with another origin?
44+
check { no c: ReadDom + WriteDom | origin[c.doc.src] != origin[c.from.context.src] }

0 commit comments

Comments
 (0)