diff --git a/.scratch/saas-production-readiness/issues/20-design-production-web-session-boundary.md b/.scratch/saas-production-readiness/issues/20-design-production-web-session-boundary.md index 76b1af3..10e4624 100644 --- a/.scratch/saas-production-readiness/issues/20-design-production-web-session-boundary.md +++ b/.scratch/saas-production-readiness/issues/20-design-production-web-session-boundary.md @@ -8,4 +8,7 @@ Status: open What same-origin/CSRF, proxy/TLS, security-header, session lifetime, revocation, secret rotation, and request-timeout contract should the initial org-admin web surface enforce, and which parts require server-side session state -rather than the current seven-day stateless cookie? +rather than the current seven-day stateless cookie? Apply the same browser +boundary to ADR-0023's separate server-side Platform Session while preserving +its distinct cookie/token namespace, immediate revocation, per-request grant +reload, and bounded recent-authentication requirement. diff --git a/.scratch/saas-production-readiness/issues/27-reconcile-audit-history-contract.md b/.scratch/saas-production-readiness/issues/27-reconcile-audit-history-contract.md index f0db122..4f26fcf 100644 --- a/.scratch/saas-production-readiness/issues/27-reconcile-audit-history-contract.md +++ b/.scratch/saas-production-readiness/issues/27-reconcile-audit-history-contract.md @@ -11,3 +11,6 @@ structured messages, and operational recovery events without weakening `Spec.System.Audit`'s pinned AuditEntry-to-run relation. Decide durability, failure, retention, and query semantics; then enforce referential integrity and observable/recoverable writes instead of silently swallowing lost evidence. +Do not merge these customer Project/Run records with ADR-0023's already-decided +separate, append-only, fail-closed Platform Audit; decide only any shared +retention/export infrastructure without weakening either semantic boundary. diff --git a/.scratch/saas-production-readiness/issues/31-write-and-drill-incident-runbooks.md b/.scratch/saas-production-readiness/issues/31-write-and-drill-incident-runbooks.md index 2a38c1d..fa77abe 100644 --- a/.scratch/saas-production-readiness/issues/31-write-and-drill-incident-runbooks.md +++ b/.scratch/saas-production-readiness/issues/31-write-and-drill-incident-runbooks.md @@ -16,3 +16,7 @@ production-shaped staging, and archive evidence that detection, mitigation, reconciliation, verification, escalation, and alert clearing all work. Include database/workspace backup failure, failed migration, full-host restore and cutover, duplicate/gap review, fallback, and achieved RPO/RTO evidence. +Also drill ADR-0023 platform-administrator lockout and Platform-owned Feishu +Application credential loss through the dual-factor offline recovery command, +expiring Emergency Platform Grant, session revocation, immutable Platform Audit, +and explicit recovery closeout; never introduce a standing break-glass account. diff --git a/.scratch/saas-production-readiness/issues/42-decide-platform-admin-identity-audit.md b/.scratch/saas-production-readiness/issues/42-decide-platform-admin-identity-audit.md index f6eb4f3..017c68f 100644 --- a/.scratch/saas-production-readiness/issues/42-decide-platform-admin-identity-audit.md +++ b/.scratch/saas-production-readiness/issues/42-decide-platform-admin-identity-audit.md @@ -1,7 +1,7 @@ # Decide the platform-administrator identity and audit boundary Type: grilling -Status: open +Status: resolved ## Question @@ -11,3 +11,44 @@ append-only audit contract will authenticate Platform Administrators for the initial service? The decision must keep `/admin/platform` private, make every Organization/connection/workload-control mutation attributable, and define a reviewable break-glass path without treating platform staff as customer members. + +## Answer + +Platform Administrators authenticate only through a dedicated Platform-owned +Feishu Application and a separate, server-side Platform Session. Platform +Identity, standing grant, invitation, session, audit and emergency grant are +independent of customer `User`, `OrganizationMembership`, Project permission +and Project/Run audit. The initial control plane has one peer role only. + +The first administrator is created by a versioned, idempotent, transactional +database bootstrap procedure that runs only when no standing administrator is +active and atomically records the Platform Audit Entry. Later administrators +receive short-lived, single-use invitations bound to a specific platform +Feishu account. The last active standing administrator cannot be revoked; +revocation immediately invalidates that identity's sessions and invitations. + +Every platform request reloads the revocable session and current standing or +unexpired emergency grant. Administrator, connection/credential, +Organization-lifecycle, workload-brake and emergency-grant actions require +recent Feishu OAuth step-up. + +Every successful platform mutation commits with a separate append-only +Platform Audit Entry or fails. Organization Administrators receive a redacted +projection of platform actions affecting their own Organization. No standing +break-glass account exists: offline recovery requires controlled host access, +an off-host recovery key, an incident and reason, and issues only an expiring +Emergency Platform Grant. + +The complete accepted decision and implementation divergences are in +[ADR-0023](../../../docs/adr/0023-platform-administrator-identity-and-audit.md). +The pinned semantic invariants are in +[`Spec.System.PlatformAdministration`](../../../spec/Spec/System/PlatformAdministration.lean), +and the canonical terms are in [`CONTEXT.md`](../../../CONTEXT.md). + +Exact numeric session/invitation/step-up limits and browser mechanics remain +with [Design the production browser and session boundary](20-design-production-web-session-boundary.md). +Customer Project/Run audit retention remains with +[Reconcile the audit and run-history contract](27-reconcile-audit-history-contract.md), +without reopening Platform Audit's separate fail-closed boundary. Implementation +is owned by [Build the private platform-administrator control plane](45-build-private-platform-admin-control-plane.md), +and recovery rehearsal by [Write and drill production incident recovery runbooks](31-write-and-drill-incident-runbooks.md). diff --git a/.scratch/saas-production-readiness/issues/45-build-private-platform-admin-control-plane.md b/.scratch/saas-production-readiness/issues/45-build-private-platform-admin-control-plane.md index a18a693..b8340f8 100644 --- a/.scratch/saas-production-readiness/issues/45-build-private-platform-admin-control-plane.md +++ b/.scratch/saas-production-readiness/issues/45-build-private-platform-admin-control-plane.md @@ -11,7 +11,15 @@ Implement authenticated `requirePlatformAdmin` APIs and a private Organizations, bootstrap their OWNER, view/change lifecycle state, configure and test each customer-owned Feishu Application, configure the Organization's distinct platform-managed Provider Connection, and manage platform-admin -allowlisting. Prove anonymous users, ordinary members, and Organization admins -cannot load either page data or mutations; every sensitive action is validated, -redacted, audited, observable, and covered by browser-level critical-journey -tests. Emergency workload controls remain integrated through ticket 37. +invitations and revocations. Implement ADR-0023's separate Platform Identity, +single standing role, guarded bootstrap procedure, identity-bound single-use +invitations, revocable server-side Platform Session, recent-authentication +step-up, last-administrator protection, fail-closed append-only Platform Audit, +Organization-safe audit projection, and dual-factor offline recovery with +expiring Emergency Platform Grants. Replace rather than reuse the legacy +customer-`User`-bound `PlatformRoleAssignment`/`TEACHER` model. Prove anonymous +users, ordinary members, and Organization admins cannot load either page data +or mutations; every sensitive action is validated, redacted, audited, +observable, and covered by browser-level critical-journey tests. Emergency +workload controls remain integrated through +[Add audited emergency workload brakes](37-emergency-workload-brakes.md). diff --git a/.scratch/saas-production-readiness/map.md b/.scratch/saas-production-readiness/map.md index ada7cf9..9cb8a65 100644 --- a/.scratch/saas-production-readiness/map.md +++ b/.scratch/saas-production-readiness/map.md @@ -42,6 +42,7 @@ rollback and recovery, and no known critical security or data-integrity gaps. - [Define initial abuse and capacity controls](issues/05-define-abuse-capacity-controls.md) — require layered fail-closed limits, durable Organization-fair admission, explicit backpressure, bounded files/storage/runs, soft usage alerts, and audited emergency workload brakes; calibrate numerical ceilings under production-like load. - [Audit backup, migration, and disaster recovery safety](issues/06-audit-backup-migration-recovery.md) — separate persistent state from releases, define a database/workspace checkpoint and recovery objectives, make migrations compatibility-gated, and prove complete off-host backup sets through isolated restore and cutover drills. - [Audit the accepted product surface for production completeness](issues/07-audit-product-surface-completeness.md) — retain the guarded Organization APIs and single-app Feishu vertical slice, but require explicit Organization-scoped Feishu/provider connections and external-identity namespaces, private platform and Organization admin control planes, and the full ADR-0022 capacity surface before release. +- [Decide the platform-administrator identity and audit boundary](issues/42-decide-platform-admin-identity-audit.md) — use a dedicated platform Feishu issuer, one peer administrator role, guarded bootstrap and identity-bound invitations, revocable server-side sessions, atomic append-only Platform Audit, and dual-factor offline recovery without a standing break-glass account. ## Fog diff --git a/AGENTS.md b/AGENTS.md index 6f1cd10..38ea31c 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -17,6 +17,9 @@ - 生产容量按不可突破的 platform ceiling 与 org 可下调 policy 分层;有效限制取两者较低值。 Agent admission 必须持久、有界、跨 org 公平且显式背压(见 ADR-0022 / `Spec.System.Capacity`)。 +- 平台管理员只通过独立的 platform-owned 飞书应用与可撤销 Platform Session 认证,不复用 + 客户 `User`/org membership;平台写操作与 append-only audit 同事务,break-glass 只走 + 双因子的离线恢复流程(见 ADR-0023 / `Spec.System.PlatformAdministration`)。 ## 纪律 diff --git a/CONTEXT.md b/CONTEXT.md index 1312ff7..0bac2d5 100644 --- a/CONTEXT.md +++ b/CONTEXT.md @@ -24,6 +24,30 @@ _Avoid_: Public management page, member portal The Organization-scoped Feishu application used for that Organization's login, bot messages, and directory integration; unrelated Organizations never share it. _Avoid_: Global Feishu app, platform bot +**Platform-owned Feishu Application**: +The dedicated Feishu application used only to authenticate Platform Administrators; it is separate from every Customer-owned Feishu Application and grants no Organization or Project authority. +_Avoid_: Customer-owned Feishu Application, Organization Feishu app + +**Platform Administrator Bootstrap**: +The one-time, guarded grant of Platform Administrator authority to a verified Platform Identity when no active Platform Administrator exists. +_Avoid_: Seed administrator, standing bootstrap account + +**Platform Administrator Invitation**: +A short-lived, single-use invitation issued by a Platform Administrator and bound to one expected identity from the Platform-owned Feishu Application. +_Avoid_: Open administrator enrollment, unbound administrator invitation + +**Platform Session**: +A revocable authentication session bound only to a Platform Identity and its active Platform Administrator authority; it carries no Organization membership or Project authority. +_Avoid_: Organization admin session, customer session + +**Platform Audit Entry**: +An immutable, durable record of a platform control-plane decision or action, separate from customer Project and Agent Run audit and mandatory for every platform mutation. Organization Administrators receive only a redacted projection of entries affecting their Organization. +_Avoid_: Best-effort log, Project audit entry + +**Emergency Platform Grant**: +Short-lived Platform Administrator authority issued only by the offline recovery procedure for a declared incident and automatically expired afterward. +_Avoid_: Standing break-glass account, permanent emergency administrator + **Provider Credential Mode**: The Organization's choice between a BYOK Provider Connection and a Platform-managed Provider Connection. _Avoid_: Global provider setting diff --git a/docs/adr/0021-org-admin-project-onboarding.md b/docs/adr/0021-org-admin-project-onboarding.md index 3752798..5e4b656 100644 --- a/docs/adr/0021-org-admin-project-onboarding.md +++ b/docs/adr/0021-org-admin-project-onboarding.md @@ -112,5 +112,6 @@ Organization for operational reporting; commercial billing remains deferred. and readiness checks. - Folder-level permissions are deferred until there is a concrete customer need. - Self-serve org signup and payment collection are deferred beyond pilot. -- The exact platform admin identity store and audit schema are separate from - this ADR and should be modeled before exposing the platform admin panel. +- The platform admin identity, session, bootstrap, invitation, audit, and + offline recovery boundary is decided by ADR-0023 and must be implemented + before exposing the platform admin panel. diff --git a/docs/adr/0023-platform-administrator-identity-and-audit.md b/docs/adr/0023-platform-administrator-identity-and-audit.md new file mode 100644 index 0000000..a96a98d --- /dev/null +++ b/docs/adr/0023-platform-administrator-identity-and-audit.md @@ -0,0 +1,136 @@ +# ADR 0023: Platform Administrator Identity And Audit Boundary + +## Status + +Accepted. + +## Context + +ADR-0021 separated `/admin/platform` from Organization administration but left +the exact platform identity store and audit schema open. That choice must be +settled before exposing the panel: customer Feishu identities are scoped by +their customer-owned applications, Organization membership must not confer +platform authority, and a platform operator can create tenants, change +connections, rotate credentials, or stop workloads across tenant boundaries. + +The current implementation is not the accepted platform model. +`PlatformRoleAssignment` points at the customer-side `User`, includes a legacy +`TEACHER` value, and has no platform login or guard. The current browser session +is a seven-day stateless customer cookie, while `AuditEntry` is Project/Run +oriented and deliberately best-effort. Reusing any of these would couple the +two control planes and make immediate revocation or fail-closed privileged +audit impossible. + +## Decision + +### Identity issuer and authority + +Platform Administrators authenticate only through one dedicated +**Platform-owned Feishu Application**. It is separate from every Organization's +Customer-owned Feishu Application and cannot grant Organization membership or +Project permission. + +A `PlatformIdentity` is scoped by that platform application and its verified +external Feishu user identity. It is not a customer `User`. The same person may +also have customer identities, but there is no implicit link, shared session, +or authority propagation between them. + +The initial platform control plane has exactly one standing role: +`Platform Administrator`. There is no Platform Owner, Super Admin, or Teacher +hierarchy. The first administrator has no permanent special authority after +another administrator is active. + +### Bootstrap, invitation, and revocation + +The first Platform Administrator is granted through a checked-in, versioned, +idempotent and transactional bootstrap database procedure. It accepts only a +verified Platform Identity, refuses to run while any standing Platform +Administrator is active, and atomically writes the grant plus its Platform +Audit Entry. Ad-hoc manual `INSERT` statements and permanent environment +allowlists are not supported bootstrap paths. + +Later administrators join through short-lived, single-use invitation links +created by an active Platform Administrator. An invitation is bound to one +specific Feishu account in the Platform-owned Feishu Application; possessing a +link without authenticating as that account is insufficient. The invitation +records its inviter and reason and becomes terminal after acceptance, expiry, +or revocation. One active Platform Administrator approval is sufficient for the +initial service. + +All standing Platform Administrators are peers. An administrator may invite or +revoke another administrator, but the last active standing administrator cannot +be revoked. Revocation immediately invalidates all Platform Sessions and all +unclaimed invitations belonging to the revoked identity. + +### Platform Session and step-up authentication + +`Platform Session` is a separate, server-side, revocable session with a distinct +cookie/token namespace. The browser receives an opaque random token; persistence +stores only its hash and binds the session to a Platform Identity. Every request +reloads the session and active grant. The session carries no Organization, +membership, Project, or customer Feishu authority. + +Administrator lifecycle changes, platform or customer Feishu connection +changes, platform-managed Provider credential changes, Organization lifecycle +changes, workload-brake changes, and Emergency Platform Grant changes require +recent Feishu OAuth reauthentication. Exact session/idle/step-up durations, +CSRF, cookie and proxy/TLS mechanics belong to the production browser/session +boundary decision; they must be configurable under checked maximums rather than +silently inheriting the current seven-day customer cookie. + +### Platform audit + +`Platform Audit Entry` is a separate append-only record from customer Project +and Agent Run audit. Every successful platform mutation and its audit entry +commit in the same database transaction. If the audit entry cannot be written, +the mutation fails. Platform audit is durable business evidence, not +best-effort telemetry. + +An entry identifies the Platform Identity and Platform Session, action, target +kind and identifier, affected Organization when applicable, mandatory reason +for security-sensitive actions, request/correlation identity, outcome, time, +and redacted before/after facts. It never stores credential, token, recovery-key +or other plaintext secret material. The normal service path can append and read +but cannot update or delete history. + +Platform Administrators can read the complete redacted platform audit. +Organization Administrators can read a customer-safe projection of entries +affecting their Organization, including Organization lifecycle, Feishu/provider +connection, and workload-brake changes; they cannot read other Organizations, +platform administrator lifecycle, recovery material, or internal security +events. + +### Offline recovery and break-glass + +There is no standing break-glass web account or shared emergency password. +Recovery uses a checked-in offline command from a controlled production-host +console. The supported procedure requires both privileged host access and a +recovery key held outside the host, environment file, and ordinary backup set. +It also requires an incident identifier, reason, and one explicit recovery +action. + +Recovery may revoke Platform Sessions, repair the Platform-owned Feishu +connection, or issue an `Emergency Platform Grant` to a verified Platform +Identity. An emergency grant is time-bounded, automatically expires, is not a +standing role, and must be explicitly closed when recovery finishes. Every +recovery action is represented in the append-only Platform Audit. Two factors +are mandatory for the initial service; two separate human approvers are not. + +## Consequences + +- Platform identity, invitation, standing grant, server-side session, platform + audit, and emergency-grant persistence must be distinct from customer + `User`, `OrganizationMembership`, Project permission, and Project/Run audit. +- `requirePlatformAdmin` must resolve the dedicated session and an active + standing or unexpired emergency grant on every request. It is never an + Organization-role override. +- The legacy `PlatformRoleAssignment`/`TEACHER` schema is not a compatible + shortcut and must be migrated or replaced before the platform panel ships. +- Bootstrap and recovery remain direct database/control-plane operations, but + only through versioned, asserted, auditable procedures rather than arbitrary + SQL. +- Exact numeric invitation/session/step-up/emergency durations, audit retention + and export policy, recovery-key custody rotation, and future multi-party + approval remain follow-on operational decisions. They may not weaken the + identity separation, last-administrator protection, fail-closed audit, or + two-factor recovery invariants fixed here. diff --git a/spec/Spec/Prelude.lean b/spec/Spec/Prelude.lean index a1d17fe..8f8c349 100644 --- a/spec/Spec/Prelude.lean +++ b/spec/Spec/Prelude.lean @@ -1,7 +1,7 @@ /-! # Prelude —— System 层共享标识符 -平台层反复引用一组标识符(项目、run、session、principal、chat)。其内部表示从未被决策 +平台层反复引用一组标识符(项目、run、session、principal、chat、platform identity/audit)。其内部表示从未被决策 (UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque 载体 `Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类 **关系**,却不对标识符表示作承诺。 @@ -33,5 +33,22 @@ structure Identifiers where ADR-0004 `feishu_chat` principal 三处共用同一实体。独立成载体而非 `Principal` 子 类型——principal 子类型学 OPEN 见上,本层不预设"chat 是 principal 的哪种子型")。 -/ ChatId : Type + /-- 平台管理员身份标识(`OPEN` 表示;ADR-0023,不复用客户 `User` 标识)。 -/ + PlatformIdentityId : Type + /-- 平台自有飞书应用标识(`OPEN` 表示;ADR-0023,与各 org 客户应用分离)。 -/ + PlatformFeishuApplicationId : Type + /-- 平台应用所验证的外部飞书用户标识(`OPEN` 表示;ADR-0023,其具体 open_id/user_id + 表示与迁移方式不在本层固定)。 -/ + PlatformExternalUserId : Type + /-- 可撤销 Platform Session 标识(`OPEN` 表示;ADR-0023)。 -/ + PlatformSessionId : Type + /-- Platform Administrator invitation 标识(`OPEN` 表示;ADR-0023)。 -/ + PlatformInvitationId : Type + /-- 一次平台控制面 mutation 标识(`OPEN` 表示;ADR-0023)。 -/ + PlatformMutationId : Type + /-- 独立 Platform Audit Entry 标识(`OPEN` 表示;ADR-0023)。 -/ + PlatformAuditEntryId : Type + /-- 平台离线恢复所声明的 incident 标识(`OPEN` 表示;ADR-0023)。 -/ + PlatformIncidentId : Type end Spec.System diff --git a/spec/Spec/System.lean b/spec/Spec/System.lean index ca55f45..b725b7a 100644 --- a/spec/Spec/System.lean +++ b/spec/Spec/System.lean @@ -2,6 +2,7 @@ import Spec.System.ProjectGroup import Spec.System.Organization import Spec.System.ProjectWorkspace import Spec.System.Capacity +import Spec.System.PlatformAdministration import Spec.System.Run import Spec.System.Lock import Spec.System.Memory @@ -22,6 +23,8 @@ import Spec.System.Audit (ADR-0021)。 - `Capacity` —— platform ceiling 与 org policy 的分层限制、持久 admission request 状态和 平台紧急工作负载制动(ADR-0022)。 +- `PlatformAdministration` —— 独立平台身份/会话、单一管理员角色、绑定邀请、最后管理员 + 保护、fail-closed 平台审计与离线 emergency grant(ADR-0023)。 - `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。 - `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。 - `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。 @@ -30,7 +33,8 @@ import Spec.System.Audit - `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。 - `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)结构 (ADR-0004);role-capability 与 settings-policy 的组合规则 OPEN。 -- `Audit` —— 有意从简(内容多为 plumbing,OPEN)。 +- `Audit` —— customer Project/Run 审计有意从简(内容多为 plumbing,OPEN);Platform + Audit 由 `PlatformAdministration` 独立钉死。 -标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020..0022。 +标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020..0023。 -/ diff --git a/spec/Spec/System/Audit.lean b/spec/Spec/System/Audit.lean index 114d4d1..7eee96e 100644 --- a/spec/Spec/System/Audit.lean +++ b/spec/Spec/System/Audit.lean @@ -1,7 +1,7 @@ import Spec.Prelude /-! -# Audit —— 审计日志(有意从简) +# Audit —— Project/Run 审计日志(有意从简) likec4 把 `AuditLog` 列为实体(`AgentRun -> AuditLog 'records lifecycle events'`), 但**审计记录里装什么**(事件 schema、保留策略、可查询维度)在任何 ADR / 散文里都 @@ -14,7 +14,8 @@ namespace Spec.System /-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录 关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`,待真实分歧点出现时由 -对应 ADR 落定。 -/ +对应 ADR 落定。ADR-0023 的 Platform Audit 是另一个 fail-closed 控制面,见 +`Spec.System.PlatformAdministration`,不复用本结构。 -/ structure AuditEntry (I : Identifiers) where /-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/ run : I.RunId diff --git a/spec/Spec/System/Organization.lean b/spec/Spec/System/Organization.lean index 499fd38..ba25c06 100644 --- a/spec/Spec/System/Organization.lean +++ b/spec/Spec/System/Organization.lean @@ -10,7 +10,8 @@ ADR-0020:Hub 长期按 SaaS 形态演进,`Organization` 是客户侧 tenant root 本模块只钉死会造成实现分歧的不变量:tenant root 存在、project/team 单归属、team grant 不得跨 org,以及 model provider connection 的凭据归属模式。用户身份、外部目录 -provider 细节、平台控制面角色集合仍为 `OPEN`。 +provider 细节仍为 `OPEN`;平台控制面身份/角色/审计已由 ADR-0023 与 +`Spec.System.PlatformAdministration` 独立决定。 -/ namespace Spec.System diff --git a/spec/Spec/System/Permission.lean b/spec/Spec/System/Permission.lean index daffb18..8fcc721 100644 --- a/spec/Spec/System/Permission.lean +++ b/spec/Spec/System/Permission.lean @@ -60,7 +60,8 @@ theorem Role.can_mono {r₁ r₂ : Role} {c : Capability} /-- **强制释放锁**要求 admin,**在 role 体系之外**(`PINNED`, ADR-0004 admin-only override)。即便 `manage` 也不经 `Role.can` 获得它,故它不是 `Capability` 而是独立 -谓词;`isAdmin` 由平台另行判定(本层不建 admin 模型)。 -/ +谓词;`isAdmin` 由 ADR-0023 的 `Spec.System.PlatformAdministration` 独立判定, +本层不把平台权力折进 project role。 -/ def RequiresAdmin (isAdmin : Prop) : Prop := isAdmin end Spec.System diff --git a/spec/Spec/System/PlatformAdministration.lean b/spec/Spec/System/PlatformAdministration.lean new file mode 100644 index 0000000..8396ca5 --- /dev/null +++ b/spec/Spec/System/PlatformAdministration.lean @@ -0,0 +1,221 @@ +import Spec.Prelude + +/-! +# PlatformAdministration —— 平台管理员身份、会话与审计边界(ADR-0023) + +平台控制面可以创建 org、写入连接凭据并制动全平台工作负载,因此不得借用客户 +`User`、`OrganizationMembership` 或 project role。ADR-0023 决定独立平台飞书 issuer、 +单一平级管理员角色、绑定身份的 invitation、可撤销服务端 session、mutation 与平台审计 +同成同败、最后管理员保护,以及无常驻账号的双因子离线恢复。 + +本模块只钉死这些会导致安全边界分歧的语义。cookie 属性、token hash、具体 TTL、审计 +字段表示/保留期、recovery key 介质和 CLI/SQL 机制仍为 `OPEN`,由对应实现决策承载。 +-/ + +namespace Spec.System + +variable (I : Identifiers) + +/-- 平台管理员的已验证外部身份(`PINNED`, ADR-0023):issuer 必须是专用 +Platform-owned Feishu Application;该身份与客户 `User`/org membership/project grant +是不同的授权根,即使现实中是同一个人也不自动传播权限。 -/ +structure PlatformIdentity where + /-- 平台身份自身标识(`OPEN` 表示,ADR-0023)。 -/ + id : I.PlatformIdentityId + /-- 验证该身份的平台自有飞书应用(`PINNED`, ADR-0023)。 -/ + application : I.PlatformFeishuApplicationId + /-- 在该平台应用作用域内验证的外部飞书用户(`PINNED` 作用域,表示 `OPEN`)。 -/ + externalUser : I.PlatformExternalUserId + +/-- 平台身份来自当前唯一受信 platform-owned app iff identity 的 issuer 与配置的 +平台应用相同(`PINNED`, ADR-0023);不能把客户 org app 的 identity 当平台身份。 -/ +def PlatformIdentity.FromPlatformApplication + (identity : PlatformIdentity I) + (platformApplication : I.PlatformFeishuApplicationId) : Prop := + identity.application = platformApplication + +/-- 初始平台控制面的 standing role(`PINNED` 封闭, ADR-0023):只有一个平级 +administrator;不存在 Platform Owner/Super Admin/Teacher 层级。 -/ +inductive PlatformRole where + | administrator + +/-- Standing Platform Administrator grant 的生命周期(`PINNED`, ADR-0023)。 -/ +inductive StandingPlatformAdminGrantState where + | active + | revoked + +/-- 一个普通、长期存在的 Platform Administrator grant(`PINNED`, ADR-0023)。 -/ +structure StandingPlatformAdminGrant where + /-- 被授予平台管理员权力的独立平台身份(`PINNED`, ADR-0023)。 -/ + identity : I.PlatformIdentityId + /-- standing role;当前封闭集合只有 administrator(`PINNED`, ADR-0023)。 -/ + role : PlatformRole + /-- grant 当前是否仍有效(`PINNED`, ADR-0023)。 -/ + state : StandingPlatformAdminGrantState + +/-- Standing grant 仅在 active 状态有效(`PINNED`, ADR-0023)。 -/ +def StandingPlatformAdminGrant.Active + (grant : StandingPlatformAdminGrant I) : Prop := + grant.state = .active + +/-- 首位平台管理员 bootstrap 的前置条件(`PINNED`, ADR-0023):只有 standing admin +集合为空时才允许;bootstrap 身份验证、审计与事务机制见 ADR,具体脚本表示 `OPEN`。 -/ +def CanBootstrapPlatformAdmin + (activeStandingAdmins : List I.PlatformIdentityId) : Prop := + activeStandingAdmins = [] + +/-- 撤销 standing Platform Administrator 的最后管理员保护(`PINNED`, ADR-0023): +target 必须当前有效,且列表中必须另有一个不同的有效管理员。Emergency grant 不计入 +standing admin 集合,不能用来绕过最后管理员保护。 -/ +def CanRevokePlatformAdmin + (activeStandingAdmins : List I.PlatformIdentityId) + (target : I.PlatformIdentityId) : Prop := + target ∈ activeStandingAdmins ∧ + ∃ other, other ∈ activeStandingAdmins ∧ other ≠ target + +/-- Platform Administrator invitation 的生命周期(`PINNED`, ADR-0023):accepted/ +expired/revoked 都是终态,所以邀请只能成功领取一次。 -/ +inductive PlatformAdminInvitationState where + | pending + | accepted + | expired + | revoked + +/-- 一个短期、单次且绑定具体平台飞书账号的管理员邀请(`PINNED`, ADR-0023)。 -/ +structure PlatformAdminInvitation where + /-- invitation 标识(`OPEN` 表示,ADR-0023)。 -/ + id : I.PlatformInvitationId + /-- 预期账号必须来自这个平台自有飞书应用(`PINNED`, ADR-0023)。 -/ + application : I.PlatformFeishuApplicationId + /-- 只有这个预期飞书账号可领取;链接本身不是 bearer admin 权力(`PINNED`)。 -/ + expectedExternalUser : I.PlatformExternalUserId + /-- 邀请过期的逻辑时刻(`PINNED` 有限寿命,数值单位/上限 `OPEN`)。 -/ + expiresAt : Nat + /-- 邀请当前状态(`PINNED`, ADR-0023)。 -/ + state : PlatformAdminInvitationState + +/-- 邀请可领取 iff 尚 pending、未过期且已验证 identity 与邀请绑定的 app+用户一致 +(`PINNED`, ADR-0023)。 -/ +def PlatformAdminInvitation.CanAccept + (invitation : PlatformAdminInvitation I) + (identity : PlatformIdentity I) + (now : Nat) : Prop := + invitation.state = .pending ∧ + now < invitation.expiresAt ∧ + identity.application = invitation.application ∧ + identity.externalUser = invitation.expectedExternalUser + +/-- 邀请状态转换(`PINNED`, ADR-0023):pending 只能结束为 accepted/expired/revoked; +任何终态都不能回到 pending 或再次 accepted。 -/ +def PlatformAdminInvitation.ValidTransition : + PlatformAdminInvitationState → PlatformAdminInvitationState → Prop + | .pending, .accepted | .pending, .expired | .pending, .revoked => True + | _, _ => False + +/-- 服务端 Platform Session 的生命周期(`PINNED`, ADR-0023)。 -/ +inductive PlatformSessionState where + | active + | revoked + | expired + +/-- 独立平台会话(`PINNED`, ADR-0023):只绑定 Platform Identity,不携带 org/project +权力;opaque cookie/token、hash 与 TTL 表示为 `OPEN`。 -/ +structure PlatformSession where + /-- 平台会话标识(`OPEN` 表示,ADR-0023)。 -/ + id : I.PlatformSessionId + /-- 会话认证的独立平台身份(`PINNED`, ADR-0023)。 -/ + identity : I.PlatformIdentityId + /-- 服务端可立即撤销/过期的状态(`PINNED`, ADR-0023)。 -/ + state : PlatformSessionState + +/-- 双因子离线恢复授权(`PINNED`, ADR-0023):受控主机权限、主机外 recovery key 与 +已声明 incident 三项都存在才是受支持的 recovery;具体因子实现与保管介质 `OPEN`。 -/ +structure PlatformRecoveryAuthorization where + /-- 已验证受控生产主机权限(`PINNED`, ADR-0023)。 -/ + hostControl : Bool + /-- 已验证独立的主机外 recovery key(`PINNED`, ADR-0023)。 -/ + offlineRecoveryKey : Bool + /-- 操作绑定了 incident id 与原因(`PINNED`, ADR-0023)。 -/ + incidentDeclared : Bool + +/-- Recovery authorization 只有三项因子均为真时有效(`PINNED`, ADR-0023)。 -/ +def PlatformRecoveryAuthorization.Valid + (authorization : PlatformRecoveryAuthorization) : Prop := + authorization.hostControl = true ∧ + authorization.offlineRecoveryKey = true ∧ + authorization.incidentDeclared = true + +/-- 只有有效双因子 recovery authorization 才能签发 Emergency Platform Grant +(`PINNED`, ADR-0023);不存在普通 web session 直接创建 break-glass 权力的路径。 -/ +def CanIssueEmergencyPlatformGrant + (authorization : PlatformRecoveryAuthorization) : Prop := + authorization.Valid + +/-- 无常驻 break-glass 账号的短期紧急授权(`PINNED`, ADR-0023)。它不属于 standing +role,必须绑定已声明 incident,自动过期且可在恢复完成时提前关闭。 -/ +structure EmergencyPlatformGrant where + /-- 获得临时平台权力的已验证 Platform Identity(`PINNED`, ADR-0023)。 -/ + identity : I.PlatformIdentityId + /-- 触发该授权的 incident(`PINNED`, ADR-0023)。 -/ + incident : I.PlatformIncidentId + /-- 自动过期的逻辑时刻(`PINNED` 有限寿命,数值单位/上限 `OPEN`)。 -/ + expiresAt : Nat + /-- 恢复完成后是否已显式关闭(`PINNED`, ADR-0023)。 -/ + closed : Bool + +/-- Emergency grant 仅在未关闭且未到期时有效(`PINNED`, ADR-0023)。 -/ +def EmergencyPlatformGrant.Active + (grant : EmergencyPlatformGrant I) (now : Nat) : Prop := + grant.closed = false ∧ now < grant.expiresAt + +/-- 每次平台请求的授权条件(`PINNED`, ADR-0023):session 必须仍为 active,且请求时 +重新解析到 active standing grant 或同 identity 的未关闭、未过期 emergency grant。 +cookie 内曾经出现过 role claim 不能代替这次解析。 -/ +def PlatformSession.Authorized + (session : PlatformSession I) + (standingGrants : List (StandingPlatformAdminGrant I)) + (emergencyGrants : List (EmergencyPlatformGrant I)) + (now : Nat) : Prop := + session.state = .active ∧ + ((∃ grant, grant ∈ standingGrants ∧ + grant.identity = session.identity ∧ + StandingPlatformAdminGrant.Active I grant) ∨ + ∃ grant, grant ∈ emergencyGrants ∧ + grant.identity = session.identity ∧ + EmergencyPlatformGrant.Active I grant now) + +/-- 必须做近期 OAuth step-up 的平台敏感操作集合(`PINNED`, ADR-0023;未来新增敏感 +操作时可扩):管理员生命周期、飞书连接、platform-managed provider 凭据、org 生命周期、 +workload brake 与 emergency grant 都不能只凭旧 session。 -/ +inductive PlatformSensitiveAction where + | administratorLifecycle + | feishuConnection + | platformManagedProviderCredential + | organizationLifecycle + | workloadBrake + | emergencyGrant + +/-- 敏感操作授权必须提供"近期重新认证"事实(`PINNED`, ADR-0023);具体时间窗 `OPEN`, +由 browser/session 决策给出受检上限。 -/ +def PlatformSensitiveAction.Authorized + (_action : PlatformSensitiveAction) + (recentAuthentication : Prop) : Prop := + recentAuthentication + +/-- 一个成功平台 mutation 与其独立 Platform Audit Entry 的原子提交事实(`PINNED`, +ADR-0023):没有 audit entry 就不存在合法成功 commit;具体数据库事务机制 `OPEN`。 -/ +structure PlatformMutationCommit where + /-- 成功的平台 mutation(`PINNED`, ADR-0023)。 -/ + mutation : I.PlatformMutationId + /-- 与 mutation 同成同败的 append-only 平台审计条目(`PINNED`, ADR-0023)。 -/ + auditEntry : I.PlatformAuditEntryId + +/-- Organization 管理员可读的平台审计脱敏投影(`PINNED`, ADR-0023):只关联影响该 +Organization 的 entry;完整平台审计和其他 org entry 不经此投影暴露。 -/ +structure OrganizationPlatformAuditProjection where + /-- 被投影的平台审计条目(`PINNED`, ADR-0023)。 -/ + auditEntry : I.PlatformAuditEntryId + /-- 唯一可见该投影的受影响 Organization(`PINNED`, ADR-0023)。 -/ + organization : I.OrganizationId + +end Spec.System