CSRF Forge

#lang forge

-- Inspiration: https://cacm.acm.org/research/alloy/

abstract sig EndPoint {}

sig Server extends EndPoint {
  causes: set HTTPEvent
}

sig Client extends EndPoint {}

abstract sig HTTPEvent {
  from : one EndPoint,
  to : one EndPoint,
  origin : one EndPoint
}

sig Request extends HTTPEvent {
  response: lone Response
}

sig Response extends HTTPEvent {
  embeds: set Request
}

sig Redirect extends Response {}

// run {} for exactly 2 Server, exactly 1 Client

---

pred Directions {
  Request.from + Response.to in Client
  Request.to + Response.from in Server
}

pred RequestResponse {
  -- every Response is paired with a unique request
  all r: Response | one response.r
  -- every pair (Response,Request) has matching to/from fields
  all r: Response | r.to = response.r.from and r.from = response.r.to
  -- no Request embedded in a Response to itself (transitively)
  all r: Request | r not in r.^(response.embeds)
}

pred Causality {
  all e: HTTPEvent, s: Server | e in s.causes iff {
    e.from = s or (some r: Response | e in r.embeds and r in s.causes)
  }
}

pred Origin {
  all r: Response | all e: r.embeds | e.origin = r.origin
  all r: Response | r.origin = (r in Redirect => response.r.origin else r.from)
  all r: Request | no embeds.r => r.origin in r.from
}

pred EnforceOrigins [s: Server] {
  all r:Request | r.to = s => r.origin = r.to or r.origin = r.from
}

---

run {
  -- facts
  Directions
  RequestResponse
  Causality
  Origin
  -- and yet, it's possible to find...
  some good, bad: Server | {
    EnforceOrigins[good]
    no r: Request | r.to = bad and r.origin in Client
    some r: Request | r.to = good and r in bad.causes
  }
} for exactly 2 Server, exactly 1 Client, 5 HTTPEvent