diff --git a/ProjectHome.md b/ProjectHome.md new file mode 100644 index 0000000..52177b6 --- /dev/null +++ b/ProjectHome.md @@ -0,0 +1,12 @@ +### Overview ### + +We implement a formal model of web security based on an abstraction of +the web platform and use this model to analyze the security of +several sample web mechanisms and applications. +The project is currently implemented in Alloy v4. + +### Coverage ### + +The current implementation defines web principals, and models browser behaviors including same origin policy, cookies, and redirects. + +The case studies we have undertaken include HTML5 forms, Referer validation, Cross-Origin Resource Sharing (CORS), and a single sign-on protocol. \ No newline at end of file diff --git a/authn.als b/authn.als deleted file mode 100644 index 9432616..0000000 --- a/authn.als +++ /dev/null @@ -1,22 +0,0 @@ - -open declarations - -// model user login - -pred hasLoggedIn [t0: HTTPTransaction ] { - some t: (t0.*cause) | t.req.path = LOGIN and some token : UserToken | token in t.req.body -} - -fact someUserCanLogin { - some t: HTTPTransaction | t.req.path = LOGIN and some token1 : UserToken | token1 in t.req.body -} - - -// model authentication token post user-login -/* -fun getAuthnId [t: HTTPTransaction]:Principal{ - {t1: (t.*cause) | isAuthenticated(t1) and none r2: (t.*cause).req| }.req.body. -} -*/ - -run show {} for 6 diff --git a/basicAuth.als b/basicAuth.als deleted file mode 100644 index e817fc1..0000000 --- a/basicAuth.als +++ /dev/null @@ -1,84 +0,0 @@ -open declarations - -// model basic auth login - -sig BAAuthHeader extends HTTPRequestHeader{ thebaToken : UserToken } - -sig BAAuthToken extends UserToken {} - -pred reqHasBAToken[ req:HTTPRequest, token: BAAuthToken]{ - token in (req.headers & BAAuthHeader).thebaToken -} - -// Add multi-realm support later. -pred isLoggedInViaBA [t: HTTPTransaction ] { - t.req.path = SENSITIVE and some token : BAAuthToken | reqHasBAToken[t.req, token] -} - - - -pred hasBAKnowledgeViaHTTP[token: BAAuthToken, usageEvent: Event]{ - some baReq : HTTPRequest | { - happensBeforeOrdering[baReq,usageEvent] - baReq.host.schema = HTTP - reqHasBAToken[baReq, token] - } -} - - -pred hasBAKnowledgeViaDirectHTTP[token: BAAuthToken, ne:NetworkEndpoint,usageEvent:Event]{ - some t: HTTPTransaction | { - happensBeforeOrdering[t.req,usageEvent] - reqHasBAToken[t.req, token] - (t.req.from = ne) or (t.req.to = ne) - } -} - -pred hasBAKnowledge[token: BAAuthToken, ne:NetworkEndpoint,usageEvent:Event]{ - hasBAKnowledgeViaHTTP[token,usageEvent] or hasBAKnowledgeViaDirectHTTP[token,ne,usageEvent] or - // We need at least one person who can login via Basic Auth. - (token.id = Alice and token.madeBy=Alice and isAuthorizedAccess[Alice,ne]) -} - -/* -fact someUserCanLoginViaBA { - some t: HTTPTransaction | t.req.path = PROTECTED and some token : BAAuthToken | { - reqHasBAToken[t.req, token] - token.id = Alice - t.req.from in Alice.browsers - } -} -*/ - -fact BeforeUsingBATokenYouNeedToKnowAboutIt{ - all req:HTTPRequest | all token: BAAuthToken |reqHasBAToken[req, token] => - hasBAKnowledge[token,req.from,req] -} - -// Alice's BA credential leaks to some principal beyond the endpoints of direct HTTP connection -pred baCredentialsLeakToAttackers{ - some req:HTTPRequest, token:BAAuthToken| { - reqHasBAToken[req, token] and - token.id = Alice and - not isAuthorizedAccess[Alice, req.from] and - req.from in (PASSIVEATTACKER+ACTIVEATTACKER+WEBATTACKER).servers - } -} - -fact BARemoveUnproductiveBranches { - no RequestAPI - no PassPetStore - all token:BAAuthToken| some req:HTTPRequest | reqHasBAToken[req, token] - no LOGOUT - no LOGIN -} - -// run show {} for 6 -run baCredentialsLeakToAttackers for 10 but 2 Origin, 1 BAAuthHeader, 2 Certificate//, 4 HTTPRequest, 4 HTTPResponse - -/* Result: -Executing "Run baCredentialsLeakToAttackers for 10 but 2 Origin" - Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 - 148678 vars. 4460 primary vars. 324813 clauses. 63353ms. - Instance found. Predicate is consistent. 5240ms. -*/ diff --git a/browserFacts.als b/browserFacts.als deleted file mode 100644 index 6c0f829..0000000 --- a/browserFacts.als +++ /dev/null @@ -1,96 +0,0 @@ -open declarations - -// This isn't quite right. We might need a concept of a "pure" client that isn't also a server. -fact ClientsOnlyRequest { - all ne:NetworkEvent | ne.from in HTTPClient implies ne in HTTPRequest -} - -fact BrowsersTrustGoodCAOnly{ - Browser.trustedCA = GOODCA -} - -fact OriginHeaders { - all t:ScriptContext.transactions | (transactions.t).location in OriginDraftConformingBrowsers implies { - let t'=t.cause | { - t' in RequestAPI implies (transactions.t).owner = (t.req.headers & OriginHeader).theorigin - t' in HTTPTransaction implies (t.req.headers & OriginHeader).theorigin = t'.resp.host + (t'.req.headers & OriginHeader).theorigin - } - } -} - -fact NoOriginByOthers { - all t:HTTPTransaction | not( (transactions.t).location in OriginDraftConformingBrowsers )implies no (t.req.headers & OriginHeader) -} - -fun OriginDraftConformingBrowsers[]:set Browser { - Firefox+Safari+ InternetExplorer8 -} - -pred correctHTTPSTransaction[t:HTTPTransaction] { - t.req.host.schema = HTTPS - t.cert.ca in (t.req.from).trustedCA - t.cert.cn = t.resp.host.dnslabel - t.cert.ne = t.resp.from -} -// smartClients don't click through errors, others do -fact browserDropsBadlyCertifiedPackets { - all t : ScriptContext.transactions | t.req.host.schema=HTTPS and t.req.from in smartClient implies correctHTTPSTransaction[t] -} - -run show{} for 6 but exactly 6 Time - -/************************* -* -* Redirection Behaviour of Browsers -* -**************************/ - -pred sameOrigin[o1:Origin , o2:Origin]{ - o1.schema=o2.schema and - o1.dnslabel = o2.dnslabel -} - - -fact BrowserRedirectionFact { -all first,second:HTTPTransaction | first=second.cause implies { -// you are either in the same scriptcontext or you are in no particular scriptcontext - some sc :ScriptContext | first+second in sc.transactions or no ((first+second) & ScriptContext.transactions) - //same from is implied by same ScriptContext - some first.resp - happensBeforeOrdering[first.resp,second.req] -// some (second & (transactions.first).transactions) //the second is in the same scriptContext - first.resp.statusCode in RedirectionStatus - second.req.host =(first.resp.headers & location).targetOrigin - second.req.path = (first.resp.headers & location).targetPath - let redirRelation = (transactions.first).location -> first.resp.statusCode -> first.req.method -> second.req.method | - sameOrigin[first.req.host,second.req.host ] implies redirRelation in BrowserRedirectionBehaviour else redirRelation in CrossOriginBrowserRedirectionBehaviour - } -} - -fun CrossOriginBrowserRedirectionBehaviour [] : Browser -> RedirectionStatus -> Method -> Method { - BrowserRedirectionBehaviour - ( InternetExplorer -> RedirectionStatus -> OPTIONS -> Method + - Firefox -> c307 -> OPTIONS -> Method + Safari -> RedirectionStatus -> OPTIONS -> Method ) -} - -fun BrowserRedirectionBehaviour [] : Browser -> RedirectionStatus -> Method -> Method { - Firefox->FirefoxRedirectionBehaviour - + Safari -> SafariRedirectionBehaviour - + InternetExplorer -> IERedirectionBehaviour - -} - -fun FirefoxRedirectionBehaviour [] : RedirectionStatus->Method->Method { - (c301 + c302 + c303) ->(GET+PUT+POST+DELETE + OPTIONS)->GET + - c304->GET->GET + - c307->( (GET+POST +PUT + DELETE + OPTIONS) <: iden ) -} - -fun SafariRedirectionBehaviour [] : RedirectionStatus->Method->Method { - (RedirectionStatus - c304) -> (GET+DELETE+PUT+POST+OPTIONS) -> GET -} - -fun IERedirectionBehaviour [] : RedirectionStatus -> Method -> Method { - c301-> GET -> GET + (c301+c302+c303)->POST -> GET + - (c301+c302+c303 + c307)->( (PUT+DELETE + OPTIONS) <: iden ) + - c307 -> POST -> POST -} diff --git a/cors.als b/cors.als deleted file mode 100644 index 1cb8672..0000000 --- a/cors.als +++ /dev/null @@ -1,37 +0,0 @@ -open declarations - - -/************************************ -* CORS -* -************************************/ -sig PreFlightRequest extends HTTPRequest {}{ - method = OPTIONS - some headers & AccessControlRequestMethod - some headers & OriginHeader - some headers & AccessControlRequestHeaders -} - -fact PreFlightIsAlwaysCrossOrigin{ - all pfr:PreFlightRequest | isCrossOriginRequest[pfr] -} - -abstract sig CORSResponseHeader extends HTTPResponseHeader{} -sig AccessControlAllowOrigin extends CORSResponseHeader {origin: Origin} -sig AccessControlAllowMethods extends CORSResponseHeader {allowedMethods : set Method} -sig AccessControlAllowHeaders extends CORSResponseHeader {allowedHeaders : set HTTPRequestHeader} -sig AccessControlMaxAge,AccessControlAllowCredentials extends CORSResponseHeader{} - - -abstract sig CORSRequestHeader extends HTTPRequestHeader{} -sig AccessControlRequestMethod extends CORSRequestHeader {requestedMethod : Method} -sig AccessControlRequestHeaders extends CORSRequestHeader {requestedHeaders : set HTTPRequestHeader} - -run show {} for 6 - -/* Execution result: -Executing "Run show for 6" - Solver=sat4j Bitwidth=4 MaxSeq=6 SkolemDepth=1 Symmetry=20 - 32458 vars. 1798 primary vars. 65424 clauses. 52047ms. - Instance found. Predicate is consistent. 201ms. -*/ diff --git a/declarations.als b/declarations.als deleted file mode 100644 index 5b759d9..0000000 --- a/declarations.als +++ /dev/null @@ -1,631 +0,0 @@ -open util/ordering[Time] - -sig DNS{ - parent : DNS + DNSRoot, - resolvesTo : set NetworkEndpoint -}{ -// A DNS Label resolvesTo something - some resolvesTo -} - -one sig DNSRoot {} - -fact dnsIsAcyclic { - all x: DNS | x !in x.^parent -// all x:dns-dnsRoot | some x.parent -} - -// s is a subdomain of d -pred isSubdomainOf[s: DNS, d: DNS]{ - // e.g. .stanford.edu is a subdomain of .edu - d in s.*parent -} - - -abstract sig Principal { -// without the -HTTPClient the HTTPS check fails - servers : set NetworkEndpoint, - dnslabels : set DNS, -} - -fun getPrincipalFromDNS[dns : DNS]:Principal{ - dnslabels.dns -} - -fun getPrincipalFromOrigin[o: Origin]:Principal{ - getPrincipalFromDNS[o.dnslabel] -} - -fact DNSIsDisjointAmongstPrincipals { - all disj p1,p2 : Principal | (no (p1.dnslabels & p2.dnslabels)) and ( no (p1.servers & p2.servers)) -//The servers disjointness is a problem for virtual hosts. We will replace it with disjoint amongst attackers and trusted people or something like that -} - -// turn this on for intermediate checks -// run show {} for 6 - -sig Time {} - -abstract sig Token {} - -abstract sig Secret extends Token { - madeBy : Principal, - expiration : lone Time, - -} - -// second.pre >= first.post -pred happensBeforeOrdering[first:Event,second:Event]{ - second.pre in first.post.*next -} - -// shorter name -pred happensBefore[first:Event,second:Event]{ - second.pre in first.post.*next -} - -fact Traces{ - all t:Time- last | one e:Event | e.pre=t and e.post=t.next - all e:Event | e.post=e.pre.next -} - - -sig NetworkEndpoint{} - -abstract sig Event {pre,post : Time} { } - -abstract sig NetworkEvent extends Event { - from: NetworkEndpoint, - to: NetworkEndpoint -} - -// we don't make HTTPServer abstract, it will be defined by the owner - -abstract sig HTTPConformist extends NetworkEndpoint{} -sig HTTPServer extends HTTPConformist{} -abstract sig HTTPClient extends HTTPConformist{ - owner:WebPrincipal // owner of the HTTPClient process -} -sig Browser extends HTTPClient { - trustedCA : set certificateAuthority -} -sig InternetExplorer extends Browser{} -sig InternetExplorer7 extends InternetExplorer{} -sig InternetExplorer8 extends InternetExplorer{} -sig Firefox extends Browser{} -sig Firefox3 extends Firefox {} -sig Safari extends Browser{} - -abstract sig Method {} -one sig GET extends Method {} -one sig PUT extends Method {} -one sig POST extends Method {} -one sig DELETE extends Method {} -one sig OPTIONS extends Method {} - -fun safeMethods[]:set Method { - GET+OPTIONS -} - -abstract sig HTTPHeader {} -abstract sig HTTPResponseHeader extends HTTPHeader{} -abstract sig HTTPRequestHeader extends HTTPHeader{} -abstract sig Status {} -abstract sig RedirectionStatus extends Status {} - -fact noOrphanedHeaders { - all h:HTTPRequestHeader|some req:HTTPRequest|h in req.headers - all h:HTTPResponseHeader|some resp:HTTPResponse|h in resp.headers -} - -////////////////// -////////////////// -////////////////// - -abstract sig HTTPEvent extends NetworkEvent { host : Origin } - -sig URL {path:Path, host:Origin} - -sig HTTPRequest extends HTTPEvent { - // host + path == url - method: Method, - path : Path, - queryString : set attributeNameValuePair, // URL query string parameters - headers : set HTTPRequestHeader, - body : set Token -} - -sig HTTPResponse extends HTTPEvent { - statusCode : Status , - headers : set HTTPResponseHeader -} - - -// Browsers run a scriptContext -sig ScriptContext { - owner : Origin, - location : Browser, - transactions: set HTTPTransaction -}{ -// Browsers are honest, they set the from correctly - transactions.req.from = location -} - - -lone sig c301,c302,c303,c304,c305,c306,c307 extends RedirectionStatus {} -lone sig c200,c401 extends Status{} -sig location extends HTTPResponseHeader {targetOrigin : Origin, targetPath : Path} -// The name location above easily conflicts with other attributes and variables with the same name. -// We should follow the convention of starting type names with a capital letter. -// Address this in later clean-up. - -sig attributeNameValuePair { name: Token, value: Token} - -sig LocationHeader extends HTTPResponseHeader { - targetOrigin : Origin, - targetPath : Path, - params : set attributeNameValuePair // URL request parameters -} - -abstract sig RequestAPI // extends Event -{} - -sig HTTPTransaction { - req : HTTPRequest, - resp : lone HTTPResponse, - cert : lone Certificate, - cause : lone HTTPTransaction + RequestAPI -}{ - some resp implies { - //response can come from anyone but HTTP needs to say it is from correct person and hosts are the same, so schema is same - resp.host = req.host - happensBeforeOrdering[req,resp] - } - - req.host.schema = HTTPS implies some cert and some resp - some cert implies req.host.schema = HTTPS - -} - -fact CauseHappensBeforeConsequence { - all t1: HTTPTransaction | some (t1.cause) implies { - (some t0:HTTPTransaction | (t0 in t1.cause and happensBeforeOrdering[t0.resp, t1.req])) - or (some r0:RequestAPI | (r0 in t1.cause )) - // or (some r0:RequestAPI | (r0 in t1.cause and happensBeforeOrdering[r0, t1.req])) - } -} - -fun getTrans[e:HTTPEvent]:HTTPTransaction{ - (req+resp).e -} - -fun getScriptContext[t:HTTPTransaction]:ScriptContext { - transactions.t -} - - - - -fun getContextOf[request:HTTPRequest]:Origin { - (transactions.(req.request)).owner -} - -pred isCrossOriginRequest[request:HTTPRequest]{ - getContextOf[request].schema != request.host.schema or - getContextOf[request].dnslabel != request.host.dnslabel -} - -// moved CORS to a separate file cors.alf for modularization - -/************************************ -* CSRF -* -************************************/ - - -// RFC talks about having Origin Chain and not a single Origin -// We handle Origin chain by having multiple Origin Headers -sig OriginHeader extends HTTPRequestHeader {theorigin: Origin} - - -fun getFinalResponse[request:HTTPRequest]:HTTPResponse{ - {response : HTTPResponse | not ( response.statusCode in RedirectionStatus) and response in ((req.request).*(~cause)).resp} -} - -pred isFinalResponseOf[request:HTTPRequest, response : HTTPResponse] { - not ( response.statusCode in RedirectionStatus) - response in ((req.request).*(~cause)).resp -} - - - - -//enum Port{P80,P8080} -enum Schema{HTTP,HTTPS} -sig Path{} -sig INDEX,HOME,SENSITIVE, PUBLIC, LOGIN,LOGOUT,REDIRECT extends Path{} -sig PATH_TO_COMPROMISE extends SENSITIVE {} - -// sig User extends WebPrincipal { } - -lone sig Alice extends WebPrincipal {} -lone sig Mallory extends WEBATTACKER {} - - -sig Origin { -// port: Port, - schema: Schema, - dnslabel : DNS, -} - - -abstract sig certificateAuthority{} -one sig BADCA,GOODCA extends certificateAuthority{} - -sig Certificate { - ca : certificateAuthority, - cn : DNS, - ne : NetworkEndpoint -}{ - - //GoodCAVerifiesNonTrivialDNSValues - ca in GOODCA and cn.parent != DNSRoot implies - some p:Principal | { - cn in p.dnslabels - ne in p.servers - ne in cn.resolvesTo - } -} - - -/**************************** -Cookie Stuff -****************************/ - - - - -// Currently the String type is taken but not yet implemented in Alloy -// We will replace String1 with String when the latter is fully available in Alloy -sig String1 {} - -sig UserToken extends Secret { - id : WebPrincipal -} - -sig Cookie extends Secret { - name : Token, - value : Token, - domain : DNS, - path : Path, -}{} - -sig SecureCookie extends Cookie {} - -sig CookieHeader extends HTTPRequestHeader{ thecookie : Cookie } -sig SetCookieHeader extends HTTPResponseHeader{ thecookie : Cookie } - -fact SecureCookiesOnlySentOverHTTPS{ - all e:HTTPEvent,c:SecureCookie | { - e.from in Browser + NormalPrincipal.servers - httpPacketHasCookie[c,e] - } implies e.host.schema=HTTPS - -} - - -fact CookiesAreSameOriginAndSomeOneToldThemToTheClient{ - all areq:HTTPRequest |{ - areq.from in Browser - some ( areq.headers & CookieHeader) - } implies all acookie :(areq.headers & CookieHeader).thecookie | some aresp: location.(areq.from).transactions.resp | { - //don't do same origin check as http cookies can go over https - aresp.host.dnslabel = areq.host.dnslabel - acookie in (aresp.headers & SetCookieHeader).thecookie - happensBeforeOrdering[aresp,areq] - } -} - -pred httpPacketHasCookie[c:Cookie,httpevent:HTTPRequest+HTTPResponse]{ - (httpevent in HTTPRequest and c in (httpevent.headers & CookieHeader).thecookie ) or - (httpevent in HTTPResponse and c in (httpevent.headers & SetCookieHeader).thecookie) -} - -pred hasKnowledgeViaUnencryptedHTTPEvent[c: Cookie, ne : NetworkEndpoint, usageEvent: Event]{ - ne !in WebPrincipal.servers + Browser - some httpevent : HTTPEvent | { - happensBeforeOrdering[httpevent,usageEvent] - httpevent.host.schema = HTTP - httpPacketHasCookie[c,httpevent] - } -} - -pred hasKnowledgeViaDirectHTTP[c:Cookie,ne:NetworkEndpoint,usageEvent:Event]{ - some t: HTTPTransaction | { - happensBeforeOrdering[t.req,usageEvent] - httpPacketHasCookie[c,t.req] - t.resp.from = ne - } or { - happensBeforeOrdering[t.resp,usageEvent] - httpPacketHasCookie[c,t.resp] - some ((transactions.t).location & ne) - } -} - -pred hasKnowledgeCookie[c:Cookie,ne:NetworkEndpoint,usageEvent:Event]{ - ne in c.madeBy.servers or hasKnowledgeViaUnencryptedHTTPEvent[c,ne,usageEvent] or hasKnowledgeViaDirectHTTP[c,ne,usageEvent] -} - -fact BeforeUsingCookieYouNeedToKnowAboutIt{ - all e:HTTPRequest + HTTPResponse | -// Use httpPacketHasCookie - all c:(e.(HTTPRequest <: headers) & CookieHeader).thecookie + (e.(HTTPResponse <: headers) & SetCookieHeader).thecookie | - hasKnowledgeCookie[c,e.from,e] -} - -fact NormalPrincipalsOnlyUseCookiesTheyMade{ - all e:HTTPResponse | - all c:(e.headers & SetCookieHeader).thecookie | { - e.from in NormalPrincipal.servers implies c.madeBy = e.from[servers] - } -} - -fact NormalPrincipalsDontReuseCookies{ - all p:NormalPrincipal | no disj e1,e2:HTTPResponse | { - (e1.from + e2.from) in p.servers - some ( (e1.headers & SetCookieHeader).thecookie & (e2.headers & SetCookieHeader).thecookie ) - } -} - -run show2 { - some (SetCookieHeader).thecookie -} for 6 -/*********************** - -HTTP Facts - -************************/ - - -fact scriptContextsAreSane { - all disj sc,sc':ScriptContext | no (sc.transactions & sc'.transactions) - all t:HTTPTransaction | t.req.from in Browser implies t in ScriptContext.transactions -} - - -fact HTTPTransactionsAreSane { - all disj t,t':HTTPTransaction | no (t.resp & t'.resp ) and no (t.req & t'.req) -} - - - - - -/**************************** - -HTTPServer Definitions - -****************************/ - -lone sig ACTIVEATTACKER extends Principal{} - -//Passive Principals match their http / network parts -abstract sig PassivePrincipal extends Principal{}{ - servers in HTTPConformist -} - -lone sig PASSIVEATTACKER extends PassivePrincipal{} -sig WebPrincipal extends PassivePrincipal { - httpClients : set HTTPClient -} { httpClients.owner = this } - -//HTTPAdherent so that it can make requests too -lone sig WEBATTACKER extends WebPrincipal{} - -abstract sig NormalPrincipal extends WebPrincipal{} { dnslabels.resolvesTo in servers} -lone sig GOOD extends NormalPrincipal{} -lone sig SECURE extends NormalPrincipal{} -lone sig ORIGINAWARE extends NormalPrincipal{} - -fact NonActiveFollowHTTPRules { -// Old rule was : -// all t:HTTPTransaction | t.resp.from in HTTPServer implies t.req.host.server = t.resp.from -// We rewrite to say HTTPAdherents cant spoof from part ... here we don't say anything about principal - all httpresponse:HTTPResponse | httpresponse.from in HTTPConformist implies httpresponse.from in httpresponse.host.dnslabel.resolvesTo -} - -fact SecureIsHTTPSOnly { -// Add to this the fact that transaction schema is consistent - all httpevent:HTTPEvent | httpevent.from in SECURE.servers implies httpevent.host.schema = HTTPS -// STS Requirement : all sc : ScriptContext | some (getPrincipalFromOrigin[sc.owner] & SECURE ) implies sc.transactions.req.host.schema=HTTPS -} - - -fact CSRFProtection { - all aResp:HTTPResponse | aResp.from in ORIGINAWARE.servers and aResp.statusCode=c200 implies { - (resp.aResp).req.method in safeMethods or ( - let theoriginchain = ((resp.aResp).req.headers & OriginHeader).theorigin | - some theoriginchain and theoriginchain.dnslabel in ORIGINAWARE.dnslabels - ) - } -} - -fact NormalPrincipalsHaveNonTrivialDNSValues { -// Normal Principals don't mess around with trivial DNS values - DNSRoot !in NormalPrincipal.dnslabels.parent -} - -fact WebPrincipalsObeyTheHostHeader { - all aResp:HTTPResponse | - let p = servers.(aResp.from) | - p in WebPrincipal implies { - //the host header a NormalPrincipal Sets is always with the DNSLabels it owns - aResp.host.dnslabel in p.dnslabels - // it also makes sure that the from server is the same one that the dnslabel resolvesTo - aResp.from in aResp.host.dnslabel.resolvesTo - - //additionally it responds to some request and keep semantics similar to the way Browsers keep them - some t:HTTPTransaction | t.resp = aResp and t.req.host.dnslabel = t.resp.host.dnslabel and t.req.host.schema = t.resp.host.schema - } -} - -fact NormalPrincipalsDontMakeRequests { - no aReq:HTTPRequest | aReq.from in NormalPrincipal.servers -} - -/*********************************** - -Client Definitions - -************************************/ - - - -// Each user is associated with a set of network locations -// from where they use their credentials -pred isAuthorizedAccess[user:WebPrincipal, loc:NetworkEndpoint]{ - loc in user.httpClients -} - -fun smartClient[]:set Browser { - Firefox3 + InternetExplorer8 -} - -// Ideally want tp use the old Principals thing - - -/* -one sig Accept extends HTTPRequestHeader{} -one sig AcceptCharset extends HTTPRequestHeader{} -one sig AcceptEncoding extends HTTPRequestHeader{} -one sig AcceptLanguage extends HTTPRequestHeader{} -one sig AcceptRanges extends HTTPRequestHeader{} -one sig Authorization extends HTTPRequestHeader{} -one sig CacheControl_Req extends HTTPRequestHeader{} -one sig Connection extends HTTPRequestHeader{} -one sig Cookie extends HTTPRequestHeader{} -one sig ContentLength_Req extends HTTPRequestHeader{} -one sig ContentType_Req extends HTTPRequestHeader{} -one sig Date_Req extends HTTPRequestHeader{} -one sig Expect extends HTTPRequestHeader{} -one sig From extends HTTPRequestHeader{} -one sig Host extends HTTPRequestHeader{} -one sig IfMatch extends HTTPRequestHeader{} -one sig IfModifiedSince extends HTTPRequestHeader{} -one sig IfNoneMatch extends HTTPRequestHeader{} -one sig IfRange extends HTTPRequestHeader{} -one sig IfUnmodifiedSince extends HTTPRequestHeader{} -one sig MaxForwards extends HTTPRequestHeader{} -one sig Pragma_Req extends HTTPRequestHeader{} -one sig ProxyAuthorization extends HTTPRequestHeader{} -one sig Range extends HTTPRequestHeader{} -one sig Referer extends HTTPRequestHeader{} -one sig TE extends HTTPRequestHeader{} -one sig Upgrade extends HTTPRequestHeader{} -one sig UserAgent extends HTTPRequestHeader{} -one sig Via_Req extends HTTPRequestHeader{} -one sig Warn extends HTTPRequestHeader{} - - -// one as right now we don't have any value in them -one sig Age extends HTTPResponseHeader{} -one sig Allow extends HTTPResponseHeader{} -one sig CacheControl_Resp extends HTTPResponseHeader{} -one sig ContentEncoding extends HTTPResponseHeader{} -one sig ContentLanguage extends HTTPResponseHeader{} -one sig ContentLength_Resp extends HTTPResponseHeader{} -one sig ContentLocation extends HTTPResponseHeader{} -one sig ContentDisposition extends HTTPResponseHeader{} -one sig ContentMD5 extends HTTPResponseHeader{} -one sig ContentRange extends HTTPResponseHeader{} -one sig ContentType_Resp extends HTTPResponseHeader{} -one sig Date_Resp extends HTTPResponseHeader{} -one sig ETag extends HTTPResponseHeader{} -one sig Expires extends HTTPResponseHeader{} -one sig LastModified extends HTTPResponseHeader{} -one sig Pragma_Resp extends HTTPResponseHeader{} -one sig ProxyAuthenticate extends HTTPResponseHeader{} -one sig RetryAfter extends HTTPResponseHeader{} -one sig Server extends HTTPResponseHeader{} - -one sig Trailer extends HTTPResponseHeader{} -one sig TransferEncoding extends HTTPResponseHeader{} -one sig Vary extends HTTPResponseHeader{} -one sig Via_Resp extends HTTPResponseHeader{} -one sig Warning extends HTTPResponseHeader{} - - -pred WWWAuthnHeaderExists { - some WWWAuthnHeader -} -run WWWAuthnHeaderExists for 6 - -fact allowedXMLHTTPRequestHeaders{ - all xhr:XMLHTTPRequest | - no xhr.headers & ( AcceptCharset + - AcceptEncoding + - Connection + - ContentLength_Req + - Cookie + -// ContentTransferEncoding + - Date_Req + - Expect + - Host + -// KeepAlive + - Referer + - TE + -// Trailer + -// TransferEncoding + - Upgrade + - UserAgent + - Via_Req - ) - -} - -*/ - -sig WWWAuthnHeader extends HTTPResponseHeader{}{ - all resp:HTTPResponse| (some (WWWAuthnHeader & resp.headers)) => resp.statusCode=c401 -} - - -// each user has at most one password -sig UserPassword extends UserToken { } - -// sig AliceUserPassword extends UserPassword {} {id = Alice and madeBy in Alice } - -pred somePasswordExists { - some UserPassword //|p.madeBy in Alice -} - -run somePasswordExists for 8 - - -pred basicModelIsConsistent { - some ScriptContext - some t1:HTTPTransaction |{ - some (t1.req.from & Browser ) and - some (t1.resp) - } -} -run basicModelIsConsistent for 8 but 3 HTTPResponse//, 3 HTTPRequest, - - -/* -run basicModelIsConsistent for 8 but 3 HTTPResponse//, 3 HTTPRequest, - Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 - Generating CNF... - Generating the solution... - Begin solveAll() - 81822 vars. 3817 primary vars. 162551 clauses. 125541ms. - Solving... - End solveAll() - . found. Predicate is consistent. 1009ms. -*/ - -// run findBasicModelInstance for 6 but 2 HTTPResponse, -//2 HTTPRequest, 2 RequestAPI, 0 GOOD, 0 SECURE ,2 Secret, 0 String1 -//1 ACTIVEATTACKER, 1 WEBATTACKER, 1 ORIGINAWARE, -//, 2 Origin, - diff --git a/digestAuth.als b/digestAuth.als deleted file mode 100644 index b2d8c15..0000000 --- a/digestAuth.als +++ /dev/null @@ -1,265 +0,0 @@ -open declarations - -// model digest auth -/*** -Possible attacks -1. MITM, once the user logs in, active attacker can intercept and modify the server response to 302 redirect to url of the attacker's choice. The browser will fill in digest auth token w/o input from the user. The server serves the protected doc of the attacker's choice. The attacker fakes another 302 to redirect the browser back to the original url, or alternatively caches the original content and sends it to the browser at the end. The user may not detect any abnormaly except possibly a slower response from the server. -2. Most of the req headers are not protected by digest, and can be modified at will by the attacker. -3. Request / response splitting. however, fixing this vulnerability is relatively easy at the implementation level. One needs to filter away CR/LF characters, whereas the attacks #1 and #2 reveal protocol weaknesses. -***/ - -// Message strctures as defined in RFC2617 - -// realm+user+pass+nonce are hashed in all modes of digest auth -// requested URI possibly combined with other info determines the realm of identities accepted for digest auth - -sig DigestRealm extends Token {} -sig DigestQOP extends Token {} -sig DigestNonce extends Token {} - -// Server's challenge to user agent -sig DigestAuthChallenge extends Token{ - realm:DigestRealm, - nonce:DigestNonce, - qop:DigestQOP - // The quality of protections accepted by the server - // Assume the higest quality of protection here, as trivial attacks exist at lower level. -}{} - -// Intermediate hash value computed by both server and user agent -sig DigestHashA1 extends Token{ - // technically the username:realm:password combo may be hashed twice in A1. - // This is irrelevant here if we assume the hashing algorithm is secure. - private username:WebPrincipal, - private realm:DigestRealm, - private password:UserPassword, - private nonce:DigestNonce, - private cnonce:DigestNonce -}{} - -sig DigestRequestEntityBodyHash extends Token { - private body:set Token // HTTP request body -}{} - -// Hash of A2 computed by user agent -sig DigestHashA2U extends Token{ - private method:Method, - private requestedURI:Path, - private requestBodyHash: DigestRequestEntityBodyHash -}{} - -// Hash of A2 computed by server. The Method field is skipped. -sig DigestHashA2S extends Token{ - private requestedURI:Path, - private requestBodyHash: DigestRequestEntityBodyHash -}{} - -// Hash of digest response computed by user agent -sig DigestHashResponseU extends Token{ - private hashA1:DigestHashA1, - private nonce:DigestNonce, - private nonceCount:Int, - private cnonce:DigestNonce, - private qop:DigestQOP, - private hashA2U:DigestHashA2U -}{} - -// Hash of digest response computed by server -sig DigestHashResponseS extends Token{ - private hashA1:DigestHashA1, - private nonce:DigestNonce, - private nonceCount:Int, - private cnonce:DigestNonce, - private qop:DigestQOP, - private hashA2S:DigestHashA2S -}{} - -sig DigestAuthResponseU extends Token{ - username:WebPrincipal, - realm:DigestRealm, - nonce:DigestNonce, - requestedURI:Path, - digestHashResponseU:DigestHashResponseU, - qop:DigestQOP, - // quality of protection chosen by the user agent - // Assume the higest quality of protection here, as trivial attacks exist at lower level. - cnonce:DigestNonce, - nonceCount:Int -}{} - -sig DigestAuthInfo{ - nextNonce:DigestNonce, - qop:DigestQOP, - // qop should be the same as in DigestAuthResponseU. - // Here we assume the highest level of protection is chosen. - digestHashResponseS:DigestHashResponseS, - cnonce:DigestNonce, - nonceCount:Int -}{} - -sig DigestWWWAuthnHeader extends WWWAuthnHeader -{ - digestChallenge:DigestAuthChallenge // challenge of digest auth -} - -sig DigestAuthzHeader extends HTTPRequestHeader { - digestResponseU:DigestAuthResponseU // User Agent's response to digest auth -}{} - -sig DigestAuthnInfoHeader extends HTTPResponseHeader { - digestAuthInfo:DigestAuthInfo -}{} - -// return the transaction that contains the previous Digest challenge -fun DigestPrevChallenge[t1:HTTPTransaction] : HTTPTransaction { - { t0:HTTPTransaction | // t0 contains a digest challenge for the given path - happensBeforeOrdering[t0.resp, t1.req] and - t1.req.path = t0.req.path and - ( some (t0.resp.headers & DigestWWWAuthnHeader).digestChallenge) and - no t2:HTTPTransaction |{ // the challenge(nonce) in t0 has not been responded to the server - happensBeforeOrdering[t2.req, t1.req] and - happensBeforeOrdering[t0.resp, t2.req] and - let t2DigestResponseU = (t2.req.headers & DigestAuthzHeader).digestResponseU | - let t1Header=(DigestAuthzHeader& t1.req.headers) | { - (t1Header.digestResponseU).requestedURI = t2DigestResponseU.requestedURI and - t2DigestResponseU.requestedURI = t2DigestResponseU.digestHashResponseU.hashA2U.requestedURI and - t2DigestResponseU.username = t2DigestResponseU.digestHashResponseU.hashA1.password.id and - t2DigestResponseU.nonce = ( t0.resp.headers & DigestWWWAuthnHeader).digestChallenge.nonce and - t2DigestResponseU.realm = ( t0.resp.headers & DigestWWWAuthnHeader).digestChallenge.realm and - t2.req.body = t2DigestResponseU.digestHashResponseU.hashA2U.requestBodyHash.body and - some t2.resp // i.e. t1.req has been received by the server - } - } - } -} - -pred containsValidDigestAuthResponseU [t1:HTTPTransaction] { - some (t1.req.headers & DigestAuthzHeader).digestResponseU and - let dRU1 = (t1.req.headers & DigestAuthzHeader).digestResponseU |{ - // chk uri, pwd, nonce, realm, body hash, etc - dRU1.requestedURI = dRU1.digestHashResponseU.hashA2U.requestedURI and - dRU1.username = dRU1.digestHashResponseU.hashA1.password.id and - dRU1.nonce = ( (DigestPrevChallenge[t1]).resp.headers & DigestWWWAuthnHeader).digestChallenge.nonce and - dRU1.realm = ( (DigestPrevChallenge[t1]).resp.headers & DigestWWWAuthnHeader).digestChallenge.realm and - t1.req.body = dRU1.digestHashResponseU.hashA2U.requestBodyHash.body - } -} - -pred hasDigestKnowledgeViaHTTP[token: DigestAuthResponseU, usageEvent: Event]{ - some t1 : HTTPTransaction | { - happensBeforeOrdering[t1.req,usageEvent] and - t1.req.host.schema = HTTP and - containsValidDigestAuthResponseU[t1] and - token = (t1.req.headers & DigestAuthzHeader).digestResponseU - } -} - -pred hasDigestKnowledgeViaDirectHTTP[token: DigestAuthResponseU, ne:NetworkEndpoint,usageEvent:Event]{ - some t1: HTTPTransaction | { - happensBeforeOrdering[t1.req, usageEvent] and - containsValidDigestAuthResponseU[t1] and - token = (t1.req.headers & DigestAuthzHeader).digestResponseU and - ((t1.req.from = ne) or (t1.req.to = ne) or ne in ACTIVEATTACKER.servers) - // fact: active attacker can read/write http traffic, but cannot recover the private fields in hash - } -} - - -fact BeforeUsingDigestTokenYouNeedToKnowAboutIt{ - /* - all t1:HTTPTransaction | - containsValidDigestAuthResponseU[t1] => - */ - all req:HTTPRequest | - all token:(req.headers & DigestAuthzHeader).digestResponseU | - hasDigestKnowledge[token , req.from, req] -} - - -pred hasDigestKnowledge[token: DigestAuthResponseU, ne:NetworkEndpoint,usageEvent:Event]{ - hasDigestKnowledgeViaHTTP[token,usageEvent] or hasDigestKnowledgeViaDirectHTTP[token,ne,usageEvent] or - ( - // We need at least one person who can login via Digest Auth. - token.digestHashResponseU.hashA1.password.id=Alice and - token.username = Alice and isAuthorizedAccess[Alice, ne] - ) -} - -pred isLoggedInViaDigest [t: HTTPTransaction ] { - t.req.path in SENSITIVE and containsValidDigestAuthResponseU [t] -} - -fact DigestSomeUserCanAccessProtectedPath { - some DigestAuthResponseU - some t1:HTTPTransaction| { - t1.req.path=SENSITIVE and - containsValidDigestAuthResponseU[t1] - and (t1.req.headers & DigestAuthzHeader).digestResponseU.username = Alice - and isAuthorizedAccess[Alice, t1.req.from] - } - // also remove irrelevant types - /* - no DELETE - no OPTIONS - */ - // no ScriptContext -} - -pred digestChosenURIAccessByAttackers [t1:HTTPTransaction]{ - (containsValidDigestAuthResponseU[t1]) and - all req1:(t1.req) | { - (req1.from in ((PASSIVEATTACKER+ACTIVEATTACKER+WEBATTACKER).servers)) and - (req1.path=PATH_TO_COMPROMISE) and - (not isAuthorizedAccess[Alice, req1.from]) and - ((req1.headers & DigestAuthzHeader).digestResponseU.username = Alice) - - } - -} - -// declare this as a fact and then try to construct a model consistent with all the facts -fact digestAttacks { - some t1:HTTPTransaction | - digestChosenURIAccessByAttackers[t1] -} - -fun findDigestAttacks: HTTPTransaction{ - { - t1:HTTPTransaction | - digestChosenURIAccessByAttackers[t1] - } -} - -// run digestAttacks {} for 10 -run findDigestAttacks for 10 but -2 Origin, 5 HTTPTransaction, 1 String1, -2 WebPrincipal, 1 OriginHeader, 1 Certificate, -3 UserToken, 3 DNS, -5 HTTPRequest, 5 HTTPResponse -, 1 Alice -, 0 PassPetPassword -, 0 RequestAPI -, 0 LOGIN -, 0 LOGOUT -, 1 UserPassword -, 1 PATH_TO_COMPROMISE - - -/* -Executing "Run findDigestAttacks for 10 but 2 Origin, 5 HTTPTransaction, 1 String1, 2 User, 1 OriginHeader, 1 Certificate, 3 UserToken, 3 DNS, 5 HTTPRequest, 5 HTTPResponse" - Solver=minisat(jni) Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 - 142038 vars. 7714 primary vars. 347555 clauses. 277158ms. - Instance found. Predicate is consistent. 3416ms. -*/ - -/* - run digestAttacks {} for 10 - Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 - Generating CNF... - Generating the solution... - Begin solveAll() - 236964 vars. 10601 primary vars. 589662 clauses. 1290894ms. - Solving... - End solveAll() - . found. Predicate is consistent. 44445ms. -*/ diff --git a/engine.als b/engine.als deleted file mode 100644 index 8e4edb8..0000000 --- a/engine.als +++ /dev/null @@ -1,267 +0,0 @@ -open declarations as d -open browserFacts -open requestAPIFacts - - -pred isNotCookieOwnerOrClient[c:madeBy.NormalPrincipal,ne : NetworkEndpoint]{ - ne !in c.madeBy.servers - no t:HTTPTransaction | t.resp.from in c.madeBy.servers and ne = t.req.from -} - -pred SecureUsesSecureCookies { - all e:HTTPResponse | - all c:(e.headers & SetCookieHeader).thecookie | - e.from in SECURE.servers implies c in SecureCookie -} - -pred CorrectSTSRequirement { - all t : ScriptContext.transactions | some (getPrincipalFromOrigin[t.req.host] &SECURE) implies correctHTTPSTransaction[t] //implies HTTPS -} - -pred noDNSRebinding { - all p:Principal | no d:DNS | d in p.dnslabels and d.resolvesTo !in p.servers -} - - -fact principalsOnlyTrustThemselves{ - all p:Principal, response:p.servers[from] | (response.headers & AccessControlAllowOrigin).origin.dnslabel in p.dnslabels -} - - -fact { - NetworkEndpoint = Principal.servers + HTTPClient -// all sc:ScriptContext | no disj t1,t2:sc.transactions | some ( t1.cause & t2.cause & HTTPTransaction) -// no client:HTTPClient | client in Principal.servers -// all t1,t2:HTTPTransaction | t1=t2.cause implies t1+t2 in ScriptContext.transactions - - // ScriptContext only connects to DNSLabels that it knows exists/owned by some Principal - DNS in Principal.dnslabels -} - -run WebAttackerCanBeClient { - some req:HTTPRequest | req.host.dnslabel in SECURE.dnslabels and req.from in WEBATTACKER.servers -} for 6 but exactly 2 Time - -run DNSRebindingIsPossible { - some p : Principal - SECURE | some (p.dnslabels.resolvesTo & SECURE.servers) -} for 5 - -run ActiveAttackerCanSpoof { - some resp:HTTPResponse | resp.from !in resp.host.dnslabel.resolvesTo -} for 8 - -check NonActiveAttackerCantSpoof { - no resp:HTTPResponse | resp.from !in resp.host.dnslabel.resolvesTo -} for 8 but exactly 0 ACTIVEATTACKER - - - -run GoodCanBeForged{ - some t:ScriptContext.transactions | let p = getPrincipalFromOrigin[t.resp.host] | { - some ( p & GOOD ) - t.resp.from !in p.servers - } - - -} for 6 but exactly 1 ACTIVEATTACKER,3 Time - - -run SecureCanBeForged{ - some t:ScriptContext.transactions | let p = getPrincipalFromOrigin[t.resp.host] | { - some ( p & SECURE) - t.resp.from !in p.servers - } - - -} for 6 but exactly 1 ACTIVEATTACKER,3 Time - -check SecureCantBeForgedbyNonActive{ - no t:ScriptContext.transactions | let p = getPrincipalFromOrigin[t.resp.host] | { - some ( p & SECURE) - t.resp.from !in p.servers - } -} for 8 but exactly 0 ACTIVEATTACKER//,3 Time//,0 HTTPHeader,0 RequestAPI - -check HTTPSProtectsNormalPrincipals{ - no t:ScriptContext.transactions | { - t.resp.from !in getPrincipalFromOrigin[t.resp.host].servers - t.resp.host.schema = HTTPS - some (getPrincipalFromOrigin[t.resp.host] & NormalPrincipal ) - (transactions.t).location in smartClient - } - -} for 8 - -run HTTPSDoesNotProtectOthers{ - no t:ScriptContext.transactions | t.resp.from !in getPrincipalFromOrigin[t.resp.host].servers and t.resp.host.schema = HTTPS and getPrincipalFromOrigin[t.resp.host] in NormalPrincipal and (transactions.t).location in smartClient -} for 4 but exactly 3 Time - - -check STSProtectsSecure{ - CorrectSTSRequirement implies { - no t:ScriptContext.transactions | let p = getPrincipalFromOrigin[t.resp.host] | { - some ( p & SECURE) - t.resp.from !in p.servers - (transactions.t).location in smartClient - } - } -} for 8// 5 but exactly 3 Time - - -run PrincipalsCanControlHTTPClient { - some (Principal.servers & HTTPClient) -} for 4 - - -check GOODCACERTS{ - no c:Certificate |{ - c.ca = GOODCA - c.ne !in (dnslabels.(c.cn).servers) - c.cn.parent != DNSRoot - } -} for 8 - - -check originHeaderProtectsFromCSRF{ - - no t:HTTPTransaction | { - // Transaction is in a OriginDraftConformingBrowser - some ( (transactions.t).location & (OriginDraftConformingBrowsers)) - //Intended for an OriginAware Principal - some getPrincipalFromOrigin[t.req.host] - getPrincipalFromOrigin[t.req.host] in ORIGINAWARE - // Its a non trivial request - t.req.method in Method - safeMethods - // The OriginAwareServer Responds - some t.resp - t.resp.from in ORIGINAWARE.servers -//CSRF Protection protects against only 200 responses - t.resp.statusCode = c200 - - //And the WebAttacker is involved in the causal chain - - some (WEBATTACKER.servers & involvedServers[t]) - } - -} for 10 but 0 ACTIVEATTACKER, 1 WEBATTACKER, 1 ORIGINAWARE, 0 GOOD, 0 SECURE ,0 Secret, 1 HTTPClient//, 2 Origin, 0 PreFlightRequest, 0 CORSRequestHeader, 0 CORSResponseHeader, 0 Secret//,8 Time//, 1 RequestAPI, 0 Secret - -fun involvedServers[t:HTTPTransaction]:set NetworkEndpoint{ -( (t.*cause & HTTPTransaction).resp.from + getPrincipalFromOrigin[(transactions.t).owner].servers ) -} - - -check noAttackerInvolvedDeleteToSecure{ - noDNSRebinding implies { - no t:ScriptContext.transactions | { - (transactions.t).location in OriginDraftConformingBrowsers - some (getPrincipalFromOrigin[t.req.host] & SECURE) - some ((Principal - NormalPrincipal).servers & involvedServers[t]) - t.req.method in DELETE + PUT - } -} -} for 6 but 0 ACTIVEATTACKER - - -run GoodCookiesCanLeak{ - some c:Cookie,ne:NetworkEndpoint,e:Event,sc:ScriptContext | some t:sc.transactions { - c.madeBy in GOOD - ne !in GOOD.servers - - httpPacketHasCookie[c,t.resp] - ne != sc.location - t.resp.from in GOOD.servers - hasKnowledgeCookie[c,ne,e] - } -} for 6 - -run SecureServerCookieCanLeak{ - some sc:ScriptContext, c:Cookie,ne:NetworkEndpoint,e:Event | some t:sc.transactions { - c.madeBy in SECURE - ne !in SECURE.servers - httpPacketHasCookie[c,t.resp] - ne != t.req.from - t.resp.from in SECURE.servers - // so there is ne which is not the client nor the SecureServer who has knowledge - hasKnowledgeCookie[c,ne,e] - } -} for 5 - -run SecureCookiesLeak_DumbClients{ - some sc:ScriptContext, c:SecureCookie,ne:NetworkEndpoint,e:Event | some t:sc.transactions { - c.madeBy in SECURE - ne !in SECURE.servers - httpPacketHasCookie[c,t.resp] - ne != t.req.from - t.resp.from in SECURE.servers - // so there is ne which is not the client nor the SecureServer who has knowledge - hasKnowledgeCookie[c,ne,e] - } -} for 6//but exactly 12 Time - - -check SecureCookiesDontLeak_SmartClient{ - no sc:ScriptContext, c:SecureCookie,ne:NetworkEndpoint,e:Event | some t:sc.transactions { - c.madeBy in SECURE - ne !in SECURE.servers - httpPacketHasCookie[c,t.resp] - ne != t.req.from - t.resp.from in SECURE.servers - // so there is ne which is not the client nor the SecureServer who has knowledge - hasKnowledgeCookie[c,ne,e] - sc.location in smartClient - } - -} for 6 - - -check STSMeansNoLeakageForAnyone{ - CorrectSTSRequirement implies { - no sc:ScriptContext, c:SecureCookie,ne:NetworkEndpoint,e:Event | some t:sc.transactions { - c.madeBy in SECURE - ne !in SECURE.servers - httpPacketHasCookie[c,t.resp] - ne != t.req.from - t.resp.from in SECURE.servers - // so there is ne which is not the client nor the SecureServer who has knowledge - hasKnowledgeCookie[c,ne,e] - // sc.location in smartClient - } - } -} for 6 - - - -fun trSchema[]:HTTPTransaction -> Schema { -(ScriptContext.transactions <: iden).req.host.schema -//~((~owner).transactions).schema -} - -fun requestTo_http[]:HTTPRequest->Principal { - d/HTTPRequest <: host.dnslabel.~dnslabels -} - - -fun responseFrom_http[]:HTTPResponse->Principal { - d/HTTPResponse <: host.dnslabel.~dnslabels -} - -fun scOwner[]: ScriptContext -> Principal { - owner.dnslabel.~dnslabels -} - -fun httpreqOrigin[]:HTTPRequest -> Principal { - (d/HTTPRequest <: headers).theorigin.dnslabel.~dnslabels -} - -fun responseFrom_actual[]:HTTPResponse -> Principal { - HTTPResponse <: from.~servers -} - -fun DNSOwnedBy[]:DNS->Principal { - ~dnslabels -} - -fun DNSownerServers[]:DNS->NetworkEndpoint { - ~dnslabels.servers -} - diff --git a/requestAPI.als b/requestAPI.als deleted file mode 100644 index a8c6306..0000000 --- a/requestAPI.als +++ /dev/null @@ -1,17 +0,0 @@ -open declarations - -/************************************ -* RequestAPI -* -************************************/ - - - -lone sig FormElement extends RequestAPI {} -sig XMLHTTPRequest extends RequestAPI { headers: set HTTPRequestHeader} - -sig XMLHTTPRequest2 extends RequestAPI { - headers: set HTTPRequestHeader -} - -sig XDomainRequest extends RequestAPI {} diff --git a/requestAPIFacts.als b/requestAPIFacts.als deleted file mode 100644 index 6b3e01a..0000000 --- a/requestAPIFacts.als +++ /dev/null @@ -1,93 +0,0 @@ -open requestAPI -open cors - -fact FormOnlyDoesPostOrGet { - all t:ScriptContext.transactions | t.cause in FormElement implies t.req.method in GET + POST + PUT+ DELETE -} - -fact { - all t:ScriptContext.transactions | t.cause in FormElement and t.req.method in PUT+DELETE implies { - not ( isCrossOriginRequest[t.req] ) - no t.(~cause) - } -} - - - -fact XHRNoCrossOriginRequestOrRedirect{ - all t:ScriptContext.transactions | - t.^cause in (XMLHTTPRequest+HTTPTransaction) implies not isCrossOriginRequest[t.req] -} - -fact XHR2_CrossOrigin { - all t:ScriptContext.transactions | - t.^cause in (XMLHTTPRequest2+HTTPTransaction) implies { - CORSPreFlightRequestTransaction[t] - or simpleCORSTransaction[t] - or complexCORSTransaction[t] - or (not isCrossOriginRequest[t.req]) - } -} - -pred simpleCORSTransaction[t:HTTPTransaction]{ - isCrossOriginRequest[t.req] - t.cause in XMLHTTPRequest2 //As simple CORS Transaction don't redirect - t.req.method in GET + POST -} - -pred CORSPreFlightRequestTransaction[t:HTTPTransaction]{ - t.req in PreFlightRequest - isCrossOriginRequest[t.req] - t.cause in XMLHTTPRequest2 - //no redirects for CORSPreflight - t.resp.statusCode in c301+c302+c303+c307 implies no t.(~cause) -} - - - -//Remove all preflight request requirement in this .. add that to servers, that they make such type response only for a preflightRequest -pred complexCORSTransaction[t:HTTPTransaction]{ - t.req !in PreFlightRequest - isCrossOriginRequest[t.req] - t.cause in XMLHTTPRequest2 // no redirect allowed - some t1:(transactions.t).transactions | { - CORSPreFlightRequestTransaction[t1] - t1.req.host = t.req.host - t1.req.path = t.req.path - some (t.req.method & (t1.resp.headers & AccessControlAllowMethods).allowedMethods) - some ((transactions.t).owner.dnslabel & (t1.resp.headers & AccessControlAllowOrigin).origin.dnslabel) - } - t.resp.statusCode in c301+c302+c303+c307 implies no t.(~cause) -} - -fact XDROnlyDoesPostOrGet { - all t:HTTPTransaction | t.cause in XDomainRequest implies { - t.req.method in GET + POST - t in (location.InternetExplorer).transactions - not (t.req.host.schema = (transactions.t).owner.schema and t.req.host.dnslabel = (transactions.t).owner.dnslabel ) - } -} - - -fact XDRRedirect { - all t:HTTPTransaction | t.cause in XDomainRequest implies { - (t.^(~cause)).req.method=GET //all transactions caused by this other than itself - some t.(~cause) implies { //if there is a transaction caused by this - (t.req.method=GET and t.resp.statusCode in c301+c302+c303+c307) or - (t.req.method=POST and t.resp.statusCode in c301+c302+c303) - } - } -} - -// What about how the server opts into letting XDR tell the script context about the value of the response? - -run show {} for 6 - -/* - -Executing "Run show for 6" - Solver=sat4j Bitwidth=4 MaxSeq=6 SkolemDepth=1 Symmetry=20 - 99857 vars. 2158 primary vars. 207102 clauses. 56137ms. - Instance found. Predicate is consistent. 1596ms. - -*/ diff --git a/serverFacts.als b/serverFacts.als deleted file mode 100644 index 04bf829..0000000 --- a/serverFacts.als +++ /dev/null @@ -1,10 +0,0 @@ -open declarations -open cors - -abstract sig CORSIgnorantServer extends HTTPServer {} -abstract sig MuteCORSIgnorantServer extends CORSIgnorantServer {} - -fact CORSIgnorantServerLacksCORSHeaders { -// we don't use resp.host , as attacker can edit that - all resp:HTTPResponse | resp.from=CORSIgnorantServer implies no (resp.headers & CORSResponseHeader) - } diff --git a/viewer.thm b/viewer.thm deleted file mode 100644 index 2f988ea..0000000 --- a/viewer.thm +++ /dev/null @@ -1,303 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/webAuth.als b/webAuth.als deleted file mode 100644 index cd70f75..0000000 --- a/webAuth.als +++ /dev/null @@ -1,232 +0,0 @@ -open declarations - -// Model the WebAuth Protocol - -sig WAToken extends Token {} - -// requester credentials -sig WAServiceToken extends WAToken { } -sig WAKrb5Token extends WAToken {} - -// subject credentials - -// The proxy token allow an application server to -// retrieve sensitive information (e.g. a user's -// mails or LDAP data) on behalf of the user. -sig WAProxyToken extends WAToken{} - -sig WALoginToken extends WAToken{} -sig WACredToken extends WAToken{} - -// request token -sig WARequestToken extends Token {} - -sig WARequest extends Token { - msgId: lone Int -} - -sig WAResponse extends Token { - causedByMsgId: lone Int -} - -sig WAGetTokenReq extends WARequest { - reqCred:WAToken, - subjCred:lone WAToken, - reqToken:lone WARequestToken, - tokens:set WAToken -} - -sig WASessionKey extends Secret {} - -sig WAGetTokenResp extends WAResponse { - respTokens:set WAToken, - sessionKey:WASessionKey -} - -sig WARequestTokenReq extends WARequest { - reqCred:WAServiceToken, - proxyTokens:set WAProxyToken, - loginTokens:WALoginToken, - reqToken:WARequestToken, - remoteUser:WebPrincipal - // optional IP addresses go here -} - -sig WAErrorToken extends WAToken {} -sig WAAppToken extends WAToken {} // opaque application token - -sig WARequestTokenResp extends WAResponse { - error:WAErrorToken, - proxyToken:lone WAProxyToken, // for login request - returnURL:URL, - requesterSubject:Principal, // identity of requester - subject:Principal, // identity in supplied credentials - requestedToken:lone WAIdToken+WAProxyToken, - loginCanceledToken:WAErrorToken, - appState:WAAppToken -} - -sig WAProxyData extends WAToken {} // may contain encrypted Krb data - -// This command converts an existing Kerberos token -// into a webkdc-proxy token, for improvied single sign-on. -sig WAProxyTokenReq extends WARequest { - subjCred:WAToken, - proxyData:WAProxyData -} - -sig WAProxyTokenResp extends WAResponse { - proxyToken:WAProxyToken, - subject:WebPrincipal // identity from subject credential in the request -} - -// This command extracts info from a proxy token -sig WAProxyTokenInfoReq extends WARequest { - proxyToken:WAProxyToken -} - -sig WAProxyTokenInfoResp extends WAResponse { - subject:WebPrincipal, // identity from proxy token - // proxy type - creation:Time, - expiration:Time -} - -sig WANonce extends Token {} - -// HMAC used in WebAuth. We may move them to a generic crypto file after we accumulate enough of them -sig WAHmac extends Token {} - -sig WAAttribute {name:Token, Value:Token} - -sig WAEncryptedToken extends WAToken { -// 4-byte UTC time to tell the server which key was used to encrypt this token - private keyHint:Token, - private nonce:WANonce, - private hmac:WAHmac, - // private attrs:set WAAttribute, - private padding:Token -} - -sig WAIdToken extends WAEncryptedToken{ - private username: WebPrincipal, - // we don't need Kerberos subject authn data for now - private creationTime: Time, - private expirationTime: Time -}{ - // Token should normally expire within 5 minutes based on WebAuth spec. - // Simulate using 5 ticks - expirationTime in creationTime.next.next.next.next.^next -} - -pred WAContainsIdToken [resp:HTTPResponse, token:WAIdToken] { - one (LocationHeader & resp.headers) and - some locHdr: LocationHeader | - locHdr in resp.headers and - locHdr.targetPath in WASAuthPath and - token in locHdr.params.value -} - -pred WAContainsIdToken [req:HTTPRequest, token:WAIdToken] { - token in req.queryString.value -} - -pred WARemoteScriptingIsPossible { - 1 = 1 // true unless user disables script support -} - -sig WASAuthPath extends Path {} -sig WAS extends HTTPServer {} -sig WAWebKDC extends HTTPServer {} - -pred WAPossessTokenViaLogin[httpClient:HTTPClient, token:WAIdToken, usageEvent:Event]{ - some t1:HTTPTransaction|{ - happensBeforeOrdering[t1.req, usageEvent] and - t1.req.path = LOGIN and - t1.req.to in WAWebKDC and - t1.req.from in httpClient and - t1.resp.statusCode in RedirectionStatus and - WAContainsIdToken[t1.resp, token] and - token.creationTime = t1.resp.post and - token.username in httpClient.owner - } -} - -pred WAPossessTokenViaRemoteScripting [httpClient1:HTTPClient, token:WAIdToken, usageEvent:Event]{ - // Through remote scripting, some user2(say, Mallory) can pass information to user1(say, Alice)'s browser - some t1:HTTPTransaction, httpClient2:HTTPClient|let user2=httpClient2.owner| - { - // Mallory possesses the token - WAPossessTokenViaLogin[httpClient2, token, usageEvent] and - // user1 (Alice) has a connection to user2(Mallory)'s web server - happensBefore[t1.req, usageEvent] and - t1.req.from in httpClient1 and - t1.req.to in (user2.servers & HTTPServer) - } and { - WARemoteScriptingIsPossible - } -} - -fact WABeforeUsingTokenYouNeedToPossessIt{ - all httpClient:HTTPClient, req:HTTPRequest, token:WAIdToken | - { - req.from in httpClient and - WAContainsIdToken [req, token] - } implies - WAPossessToken[httpClient, token, req] -} - -pred WAPossessToken[httpClient:HTTPClient, token:WAIdToken, usageEvent:Event]{ - WAPossessTokenViaLogin [httpClient, token, usageEvent] or - WAPossessTokenViaRemoteScripting [httpClient, token, usageEvent] -} - -// Constrain the web model in this module for better illustration. -// The general model does not enforce this. -fact WAHTTPFacts{ - all req:HTTPRequest | req.to in HTTPServer - all user:WebPrincipal | user.servers in HTTPServer - all t1:HTTPTransaction | some (t1.resp) implies (t1.req.from = t1.resp.to ) and (t1.req.to = t1.resp.from) - Mallory.servers in (HTTPServer - (WAS+WAWebKDC)) -} - -pred WALoginCSRF [t1:HTTPTransaction]{ - some token:WAIdToken|{ - t1.req.from in Alice.httpClients and - t1.req.path in WASAuthPath and - t1.req.to in WAS and - WAContainsIdToken [t1.req, token] and - token.username in Mallory - } -} - -fun WAFindAttacks: HTTPTransaction{ - { - t1:HTTPTransaction | - WALoginCSRF[t1] - } -} - -// run WAFindAttacks for 8 but exactly 0 ACTIVEATTACKER, exactly 0 PASSIVEATTACKER -check WANoLoginCSRF { - no WAFindAttacks -} -for 8 but exactly 0 ACTIVEATTACKER, exactly 0 PASSIVEATTACKER - -/* -Executing "Check WANoLoginCSRF for 8 but exactly 0 ACTIVEATTACKER, exactly 0 PASSIVEATTACKER" -Run 1: -==== - Solver=minisat(jni) Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 - Generating CNF... - Generating the solution... - Begin solveAll() - 194044 vars. 6761 primary vars. 386812 clauses. 601759ms. - Solving... - End solveAll() - Counterexample found. Assertion is invalid. 10889ms. - - -*/ - - diff --git a/webAuthWithFix.als b/webAuthWithFix.als deleted file mode 100644 index 7c5f39a..0000000 --- a/webAuthWithFix.als +++ /dev/null @@ -1,293 +0,0 @@ -open declarations - -/* Model the WebAuth Protocol and the interaction of the following: - WebKDC: the WebAuth Login Server - WAS : a WebAuth-enabled Web Server - UA : the user agent, i.e. browser -*/ - -sig WAToken extends Token {} - -// requester credentials -sig WAServiceToken extends WAToken { } -sig WAKrb5Token extends WAToken {} - -// subject credentials - -// The proxy token allow an application server to -// retrieve sensitive information (e.g. a user's -// mails or LDAP data) on behalf of the user. -sig WAProxyToken extends WAToken{} - -sig WALoginToken extends WAToken{} -sig WACredToken extends WAToken{} - -// request token -sig WARequestToken extends Token { - nonce:WANonce // add a WANonce to fix login CSRF in WebAuth -} - -sig WARequest extends Token { - msgId: lone Int -} - -sig WAResponse extends Token { - causedByMsgId: lone Int -} - -sig WAGetTokenReq extends WARequest { - reqCred:WAToken, - subjCred:lone WAToken, - reqToken:lone WARequestToken, - tokens:set WAToken -} - -sig WASessionKey extends Secret {} - -sig WAGetTokenResp extends WAResponse { - respTokens:set WAToken, - sessionKey:WASessionKey -} - -sig WARequestTokenReq extends WARequest { - reqCred:WAServiceToken, - proxyTokens:set WAProxyToken, - loginTokens:WALoginToken, - reqToken:WARequestToken, - remoteUser:WebPrincipal - // optional IP addresses go here -} - -sig WAErrorToken extends WAToken {} -sig WAAppToken extends WAToken {} // opaque application token - -sig WARequestTokenResp extends WAResponse { - error:WAErrorToken, - proxyToken:lone WAProxyToken, // for login request - returnURL:URL, - requesterSubject:Principal, // identity of requester - subject:Principal, // identity in supplied credentials - requestedToken:lone WAIdToken+WAProxyToken, - loginCanceledToken:WAErrorToken, - appState:WAAppToken -} - -sig WAProxyData extends WAToken {} // may contain encrypted Krb data - -// This command converts an existing Kerberos token -// into a webkdc-proxy token, for improvied single sign-on. -sig WAProxyTokenReq extends WARequest { - subjCred:WAToken, - proxyData:WAProxyData -} - -sig WAProxyTokenResp extends WAResponse { - proxyToken:WAProxyToken, - subject:WebPrincipal // identity from subject credential in the request -} - -// This command extracts info from a proxy token -sig WAProxyTokenInfoReq extends WARequest { - proxyToken:WAProxyToken -} - -sig WAProxyTokenInfoResp extends WAResponse { - subject:WebPrincipal, // identity from proxy token - // proxy type - creation:Time, - expiration:Time -} - -sig WANonce extends Token {} - -// HMAC used in WebAuth. We may move them to a generic crypto file after we accumulate enough of them -sig WAHmac extends Token {} - -sig WAAttribute {name:Token, Value:Token} - -sig WAEncryptedToken extends WAToken { -// 4-byte UTC time to tell the server which key was used to encrypt this token - private keyHint:Token, - private nonce:WANonce, - private hmac:WAHmac, - // private attrs:set WAAttribute, - private padding:Token -} - -sig WASCookie extends SecureCookie {}{ - value in WANonce -} - -fact WASCookieConstraints { - all disj c1, c2:WASCookie | c1.value != c2.value -} - -sig WAIdToken extends WAEncryptedToken{ - private username: WebPrincipal, - private wasNonce: WANonce, - // we don't need Kerberos subject authn data for now - private creationTime: Time, - private expirationTime: Time -}{ - // Token should normally expire within 5 minutes based on WebAuth spec. - // Simulate using 5 ticks - expirationTime in creationTime.next.next.next.next.^next -} - -// pred WAPossessWASCookie[httpClient:HTTPClient, token:WAIdToken, usageEvent:Event]{} - -pred WARemoteScriptingIsPossible { - 1 = 1 // true unless user disables script support -} - -sig WASAuthPath extends Path {} -sig WAS extends HTTPServer {} -sig WAWebKDC extends HTTPServer {} - -/* On initial access to WAS, WAS creates a host cookie containing a nonce, - and redirects the user's browser to the WebKDC with the nonce imbedded - in the query string -*/ -pred WARedirectedFromWAS[t2:HTTPTransaction] { - some t1:t2.^cause, c:WASCookie|{ - t1.req.to in WAS and - t1.resp.statusCode in RedirectionStatus and - WAWebKDC in (location & t1.resp.headers ).targetOrigin.dnslabel.resolvesTo and - c in (SetCookieHeader & t1.resp.headers).thecookie and - c.value in (t2.req.queryString.value & WARequestToken).nonce - } -} - -/* On successful user authentication, WebKDC sends the Id Token to WAS. - The ID token contains the nonce originally created by WAS. -*/ -pred WAPossessTokenViaLogin[httpClient:HTTPClient, token:WAIdToken, usageEvent:Event]{ - some t1:HTTPTransaction|{ - happensBeforeOrdering[t1.req, usageEvent] and - WARedirectedFromWAS[t1] and - t1.req.path = LOGIN and - t1.req.to in WAWebKDC and - t1.req.from in httpClient and - t1.resp.statusCode in RedirectionStatus and - WAContainsIdToken[t1.resp, token] and - token.creationTime = t1.resp.post and - token.username in httpClient.owner and - // IDToken includes the nonce created by WAS - token.wasNonce in (t1.req.queryString.value & WARequestToken).nonce - } -} - -pred WAContainsIdToken [resp:HTTPResponse, token:WAIdToken] { - one (LocationHeader & resp.headers) and - some locHdr: LocationHeader | - locHdr in resp.headers and - locHdr.targetPath in WASAuthPath and - token in locHdr.params.value -} - -/* The WAS accepts an ID Token in the query string only if - it is corroborated with a host cookie set by the WAS -*/ -pred WAContainsIdToken [req:HTTPRequest, token:WAIdToken] { - token in req.queryString.value - some c:WASCookie| { - c in (CookieHeader & req.headers).thecookie - c.value = token.wasNonce - } -} - -pred WAPossessTokenViaRemoteScripting [httpClient1:HTTPClient, token:WAIdToken, usageEvent:Event]{ - // Through remote scripting, some user2(say, Mallory) can pass information to user1(say, Alice)'s browser - some t1:HTTPTransaction, httpClient2:HTTPClient|let user2=httpClient2.owner| - { - // Mallory possesses the token - WAPossessTokenViaLogin[httpClient2, token, usageEvent] and - // user1 (Alice) has a connection to user2(Mallory)'s web server - happensBefore[t1.req, usageEvent] and - t1.req.from in httpClient1 and - t1.req.to in (user2.servers & HTTPServer) - } and { - WARemoteScriptingIsPossible - } -} - -fact WABeforeUsingTokenYouNeedToPossessIt{ - all httpClient:HTTPClient, req:HTTPRequest, token:WAIdToken | - { - req.from in httpClient and - WAContainsIdToken [req, token] - } implies - WAPossessToken[httpClient, token, req] -} - -pred WAPossessToken[httpClient:HTTPClient, token:WAIdToken, usageEvent:Event]{ - WAPossessTokenViaLogin [httpClient, token, usageEvent] or - WAPossessTokenViaRemoteScripting [httpClient, token, usageEvent] -} - -// Constrain the web model in this module for better illustration. -fact WAHTTPFacts{ - all req:HTTPRequest | {req.from in HTTPClient and req.to in HTTPServer} - all user:WebPrincipal | user.servers in HTTPServer - all t1:HTTPTransaction | some (t1.resp) implies (t1.req.from = t1.resp.to ) and (t1.req.to = t1.resp.from) - Mallory.servers in (HTTPServer - (WAS+WAWebKDC)) -} - -pred WALoginCSRF [t1:HTTPTransaction]{ - some token:WAIdToken|{ - t1.req.from in Alice.httpClients and - t1.req.path in WASAuthPath and - t1.req.to in WAS and - WAContainsIdToken [t1.req, token] and - token.username in Mallory - } -} - -fun WAFindAttacks: HTTPTransaction{ - { - t1:HTTPTransaction | - WALoginCSRF[t1] - } -} - -// run WAFindAttacks for 8 but exactly 0 ACTIVEATTACKER, exactly 0 PASSIVEATTACKER -check WANoLoginCSRF { - no WAFindAttacks -} -for 8 but exactly 0 ACTIVEATTACKER, exactly 0 PASSIVEATTACKER - -/* -Executing "Check WANoLoginCSRF for 8 but exactly 0 ACTIVEATTACKER, exactly 0 PASSIVEATTACKER" -Run 1: -====== -Generating facts... - Simplifying the bounds... - Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 - Generating CNF... - Generating the solution... - Begin solveAll() - 209396 vars. 6897 primary vars. 412890 clauses. 6058505ms. - Solving... - End solveAll() - No counterexample found. Assertion may be valid. 1612370ms. -Run 2: -====== - Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 - Generating CNF... - Generating the solution... - Begin solveAll() - 209396 vars. 6897 primary vars. 412890 clauses. 4285089ms. - Solving... - End solveAll() - No counterexample found. Assertion may be valid. 1981270ms. -Run 3: -==== - Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 - Generating CNF... - Generating the solution... - Begin solveAll() - 209396 vars. 6897 primary vars. 412890 clauses. 4412958ms. - Solving... - End solveAll() - No counterexample found. Assertion may be valid. 2087697ms. -*/