Alloy でユーザーの権限違反を検出する.md

GA みたいに、ブラウザに公開キーを埋め込んでイベントを送るサービスを考える。

公開キーは secret ではない。script tag や bundle に入るので、誰でも見える。ただしサーバー側では、その公開キーから token record を引いて、project と origin allowlist を見る。

このとき落とし穴になるのが domain verification。

「この origin はこの project のものだ」と確認できていることと、「この origin から telemetry を write してよい」ことは別の権限になる。

ここを混ぜると、こういうバグになる。

verified domain なら public key がなくても ingest を通す。

これは GA 風の公開キー ingest では危ない。通したいのは Origin + public key が揃った request だけ。

形

構成はだいたいこう。

flowchart LR
  Page[Customer website] -->|loads SDK with public key| Browser[Browser client]
  Browser -->|POST /ingest<br/>Origin + public key| IngestAPI[Ingest API]
  Server[Server client] -->|POST /ingest<br/>Bearer ingest secret| IngestAPI
  CI[CI/CD] -->|PUT /artifacts<br/>Bearer upload token| ArtifactAPI[Artifact API]
  Operator[Operator] -->|domain claim / verify| DomainAPI[Domain Verification API]

  IngestAPI --> Auth[Authorization]
  ArtifactAPI --> Auth
  DomainAPI --> SetupState[(Setup state)]

  Auth --> PublicKeyRecord[(Public key token record)]
  Auth --> PublicAllowlist[(Public key origin allowlist)]
  Auth --> IngestSecret[(Ingest secrets)]
  Auth --> UploadToken[(Upload tokens)]
  Auth --> VerificationClaim[(Verification claims)]

  PublicKeyRecord -->|belongs to project| PublicAllowlist
  VerificationClaim -. setup fact only .-> PublicAllowlist

  Auth --> Decision{Allowed?}
  Decision -->|yes| Queue[Telemetry queue / storage]
  Decision -->|no| Reject[403 / 401]

見るべきものは少ない。

public key は公開 identifier
public key record は project に属する
public key record は origin allowlist を持つ
verification claim は setup の事実であって runtime permission ではない
secret token は browser では使わない

VerificationClaim -. setup fact only .-> PublicAllowlist の点線が今回の肝。点線を実線にすると穴が開く。

RBAC として見る

CORS ではない。CORS は response を読めるかの制御で、write の認可ではない。 ingest は書き込みなので、サーバー側で見る。

subject: public key, ingest secret, upload token
resource: project ingest, artifact upload
action: browser ingest, trusted ingest, artifact upload
context: origin, revocation, project ownership

flowchart TD
  Project[Project]
  Request[Request]
  Credential[Credential]
  Origin[Origin]

  Project -->|owns token record| PublicKeyRecord[PublicKeyRecord]
  PublicKeyRecord -->|exposes| PublicKey[PublicKey]
  Project -->|owns| SecretKey[SecretKey]
  Project -->|owns| UploadToken[UploadToken]
  Project -->|has setup claim| VerificationClaim[VerificationClaim]

  Request -->|targets| Project
  Credential -->|has optional| Origin
  Credential -->|has optional| PublicKey
  Credential -->|has optional| SecretKey
  Credential -->|has optional| UploadToken

  PublicKeyRecord -->|allows| AllowedOrigin[Allowed Origin]
  AllowedOrigin --> Origin
  VerificationClaim -->|verified origin| Origin

  VerificationClaim -. must not imply .-> AllowedOrigin

VerificationClaim と AllowedOrigin を分けておく。

ここを分けないと、モデル上もバグを表現できない。

Alloy にする

HTTP も SQL も Queue も入れない。関係だけ書く。

module example/auth

sig Project {}
sig Origin {}

abstract sig Token {
  owner: one Project
}

sig PublicKey extends Token {
  allowedOrigins: set Origin
}

sig SecretKey extends Token {}
sig UploadToken extends Token {}

sig VerificationClaim {
  owner: one Project,
  verifiedOrigin: one Origin
}

sig Request {
  target: one Project
}

sig Credential {
  origin: lone Origin,
  publicKey: lone PublicKey,
  secretKey: lone SecretKey,
  uploadToken: lone UploadToken
}

この PublicKey は、ブラウザに出ている文字列というより、サーバー側の public key record。実装では公開文字列で DB row を引いて、owner と allowlist を見る。

browser ingest 。

pred noBearerCredential[c: Credential] {
  no c.secretKey
  no c.uploadToken
}

pred browserIngestAccepted[r: Request, c: Credential] {
  some c.origin
  some c.publicKey
  noBearerCredential[c]
  c.publicKey.owner = r.target
  c.origin in c.publicKey.allowedOrigins
}

origin がある
public key がある
secret token はない
public key record の owner が target project
origin がその key の allowlist にある

通ってはいけないものを書く

Alloy は happy path より、通ってはいけない path を書くのがいい。

assert VerifiedDomainAloneIsInsufficient {
  all r: Request, c: Credential |
    (
      some c.origin and
      no c.publicKey and
      (some claim: VerificationClaim |
        claim.owner = r.target and claim.verifiedOrigin = c.origin)
    ) => not browserIngestAccepted[r, c]
}

origin はある
public key はない
その origin は verified domain
でも browser ingest は通らない

これを書いておくと、domain verification を runtime permission として使っていないかを見られる。

happy path も置く。全拒否モデルで安全っぽく見えるのを避けるため。

pred BrowserHappyPath {
  some r: Request, c: Credential | browserIngestAccepted[r, c]
}

run BrowserHappyPath for 4
check VerifiedDomainAloneIsInsufficient for 5

CLI

alloy6 exec -c '*' -t json -o /tmp/auth-model auth.als

Nix

nix shell nixpkgs#alloy6 -c alloy6 exec -c '*' -t json -o /tmp/auth-model auth.als

読み方はこれだけ覚える。

run ... SAT: 例がある
check ... UNSAT: 反例がない
check ... SAT: 反例がある

check SAT は即実装バグではない。モデルバグのこともある。

実装で再現する

Alloy は実装を読まない。なので assertion をそのまま API test にする。

バグのある実装はこうなりがち。

flowchart TD
  Start[Browser request with Origin] --> HasKey{Has public key?}
  HasKey -->|yes| KeyAllowed{Key allows origin?}
  KeyAllowed -->|yes| Accept[204 accepted]
  KeyAllowed -->|no| RejectKey[403 rejected]
  HasKey -->|no| Verified{Origin is verified domain?}
  Verified -->|yes| Bug[204 accepted<br/>BUG]
  Verified -->|no| RejectOrigin[403 rejected]

public key がないときに verified domain に fallback している。この fallback が穴。

POST /ingest?v=1
Origin: https://app.example.com
DB mock は verified domain があるように返す
key=<publicKey> も x-public-client-key も付けない
403 を期待する

これが 204 なら実バグ。

直し方

default では public key を必須にする。

flowchart TD
  Start[Browser request with Origin] --> HasKey{Has public key?}
  HasKey -->|no| RejectMissingKey[403 public key required]
  HasKey -->|yes| KeyAllowed{Key allows origin?}
  KeyAllowed -->|yes| Accept[204 accepted]
  KeyAllowed -->|no| RejectKey[403 rejected]

  Legacy[Legacy compatibility flag] -. explicit opt-in .-> LegacyVerified{Allow verified domain alone?}
  LegacyVerified -. only when enabled .-> AcceptLegacy[204 accepted]

互換用に verified domain 単体を残すなら、明示フラグに落とす。

const requirePublicClientKey = (env: Env): boolean =>
  env.REQUIRE_PUBLIC_CLIENT_KEY !== "0" &&
  env.REQUIRE_PUBLIC_CLIENT_KEY !== "false";

既存テストで verified domain 単体を通したいなら、REQUIRE_PUBLIC_CLIENT_KEY=0 を明示する。 default と legacy mode をテスト上でも分ける。

他にも見る

同じ要領で見るならこのへん。

verified claim 単体では write できない
browser action は secret token を使わない
public key / secret key / upload token は tenant 境界を越えない
upload token は ingest に使えない
ingest secret は artifact upload に使えない
revoked token は拒否される

手順は固定化できる。

credential と claim を分ける
setup state と runtime permission を分ける
action ごとに predicate を作る
confused permission の negative assertion を書く
happy path の run も書く
Alloy solver を実行する
assertion ごとに API test を 1 つ書く

Alloy の罠

空集合

c.publicKey in RevokedPublicKey

c.publicKey が空の場合、none in RevokedPublicKey は真になる。 public key を持っていない credential まで revoked 扱いになる。

こう書く。

some c.publicKey and c.publicKey in RevokedPublicKey

反例が出たら、まず counterexample を読む。実装が間違っているのか、モデルが雑すぎるのかを分ける。

まとめ

やったことは単純。

権限関係を整理する
-> 最小の Alloy model に落とす
-> solver を実行する
-> counterexample を読む
-> failing API test を 1 つ書く
-> 実装を直す
-> model と test を release gate に残す

効いたのは、domain を所有している証明 と runtime で telemetry を write できる権限 を別の関係としてモデル化したこと。

ここを分けると、実装の fallback がバグとして見える。

mizchi/Alloy でユーザーの権限違反を検出する.md

Select an option

No results found