Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Proposal: OIDC and OAuth2

Capability-native abstractions for OpenID Connect identity providers, OAuth 2.0 clients, issued tokens, workload identity federation, and the authentication/authorization flows that every modern cloud and enterprise deployment depends on.

Why a Separate Proposal

OIDC and OAuth2 are related but distinct from certificates and keys. Keys (cryptography-and-key-management-proposal.md) are secret material. Certificates (certificates-and-tls-proposal.md) are public assertions of identity binding validated against a PKI trust store. OIDC/OAuth2 is a delegated authority protocol family: tokens are short-lived bearer credentials or proof-of-possession handles issued by an identity provider after authenticating a subject, scoped by a set of permissions, and consumed by a relying party or resource server.

The failure modes barely overlap. Key compromise vs. IdP compromise vs. CA mis-issuance require different detection and recovery stories. Revoking a TLS certificate, revoking an access token, and revoking a KEK are three different operations with three different operational tempos (manifest update / IdP admin action / KMS grant edit).

Putting this in a separate proposal also matches the cross-cutting nature of the feature: OIDC/OAuth2 shows up in login (boot-to-shell-proposal.md), session state (user-identity-and-policy-proposal.md), key unlock (volume-encryption-proposal.md), cloud KMS access (cryptography-and-key-management-proposal.md CloudKmsKeySource), and service-to-service authentication (networking-proposal.md). Threading it through every touchpoint without a shared definition would be a silo-per-consumer repeat of the Linux ssh-agent/gpg-agent/keyctl story.

Problem

capOS needs to:

  • Accept federated authentication for console and web-terminal login (corporate IdP, Google, GitHub, Okta, Azure AD, Keycloak, Dex) so sessions do not depend on capOS storing or managing primary user credentials.
  • Run as a cloud workload without baked-in long-lived IAM credentials, using the modern workload identity federation pattern (RFC 8693 token exchange) to obtain short-lived cloud provider credentials from an attested instance identity or a local keypair.
  • Authenticate service-to-service calls using OAuth2 client credentials, private_key_jwt, DPoP, or mTLS, chosen by policy rather than hard-wired per consumer.
  • Consume OAuth2 access tokens from external clients (an HTTP API running under capOS verifies bearer tokens against an issuer’s JWKS) without every service writing its own JWT parser.
  • Expose scopes and OIDC claims as policy input to AuthorityBroker / PolicyEngine without letting them act as ambient authority.
  • Map external subjects to local principals, accounts, sessions, policy profiles, and resource profiles through explicit admission configuration rather than treating provider claims as local roles.

Without a shared abstraction each consumer would invent its own JWT parser, JWKS cache, issuer list, discovery-document fetcher, refresh scheduler, and token storage. That is roughly the OAuth/OIDC mess already visible in most operating systems and app stacks.

Scope

In scope:

  • Relying-party (RP) role for OIDC. capOS is the RP; the IdP is external.
  • Client role for OAuth2. capOS acts as confidential client, public client (PKCE), or federated workload client.
  • Resource-server role for OAuth2. A capOS service can validate inbound bearer tokens.
  • Token capability objects for ID tokens, access tokens, refresh tokens, DPoP proofs, and client assertions.
  • Integration with SessionManager, CredentialStore, AuthorityBroker, CloudKmsKeySource, EncryptedBlockDevice unlock flows.

Out of scope for v1:

  • OAuth2 authorization server / OIDC provider role. capOS does not issue tokens to third parties in the first iteration. A LocalIdentityProvider that issues tokens to other capOS services is possible later work; it sits on top of the same primitives.
  • SAML. The modern direction is OIDC; a deployment that needs SAML can add a second SessionManager.login adapter without reshaping the model.
  • OAuth 1.0a. Dead.
  • UMA 2.0. Out until a concrete consumer appears.
  • CIBA (Client-Initiated Backchannel Authentication). Useful for step-up on mobile devices; revisit once the web shell gateway ships.

Design Principle: Tokens Are Typed Capabilities

In the OAuth/JWT world a token is a byte string. Possession equals authority. Every library re-parses, re-validates, and re-caches the token; every log line risks leaking it; every service that needs to forward it must hand it over unattenuated. That is the same architectural failure mode as “a key is a byte string” — the protection mechanism (TLS in transit, DPoP, audience binding) is orthogonal to the system’s main abstraction.

In capOS, a token is a capability object. Holding an AccessToken cap means “you may present this token for one outbound request, read a bounded subset of its claims, or exchange it for a more specific token.” The raw token bytes live in the address space of the OAuth/OIDC service; callers reach them by invoking typed methods.

Consequences mirror the key-cap case:

  • Attenuation by scope. A caller that only needs to read sub receives a TokenClaims facet that does not expose the raw JWT. A caller that only needs to call one resource server receives a BoundToken that rejects use against other audiences.
  • Revocation is a cap drop plus server-side revocation. Dropping the cap prevents that holder from using the token; revoking the token at the IdP prevents any holder from using it. Both paths exist; neither requires a kernel mechanism.
  • Audit is intrinsic. Every token present, every refresh, every token exchange flows through the audit cap. Bearer-token leakage to logs becomes harder because the raw string is never returned.
  • Composition, not configuration. An OAuth client is a cap that encapsulates client_id, client authentication method, allowed grants, scopes, and target IdP. Building one means composing caps, not stringifying URLs into config files.
  • Per-consumer issuance by default. When a service needs a token for a downstream call, it asks its OAuthClient cap; the OAuth service issues a per-consumer down-scoped token. Transfer between processes is possible but explicit.

This also gives capOS a natural story for the agent shell’s “agent never sees secrets” rule: the agent holds an ApprovalGrant cap that internally holds the access token; the agent invokes the wrapped resource server cap; the token never appears as data in the model’s prompt window.

Schemas

Identity provider

interface OidcIdentityProvider {
    # The stable issuer URL (RFC 8414 / OIDC Discovery).
    issuer            @0 () -> (url :Text);

    # Discovery document (cached; refreshed on a schedule or on
    # signature-verification failure). Returning the parsed metadata,
    # not raw JSON, forces the implementation to validate it once.
    metadata          @1 () -> (meta :OidcProviderMetadata);

    # JWKS fetched from the provider's `jwks_uri`, exposed as a set of
    # PublicKey caps keyed by `kid`. Key rotation is invisible to
    # callers: they ask for a `kid`, they get a current PublicKey or
    # an error.
    jwks              @2 () -> (set :Jwks);

    # Verify an ID token fully — signature against jwks, issuer match,
    # audience match against the registered client, nonce, exp/nbf/iat
    # with clockSkewSeconds from policy, and required `acr`/`amr`
    # predicates if set by the OAuthClient.
    verifyIdToken     @3 (jwt :Data,
                          policy :IdTokenPolicy)
                      -> (claims :IdTokenClaims);
}

struct OidcProviderMetadata {
    issuer                           @0 :Text;
    authorizationEndpoint            @1 :Text;
    tokenEndpoint                    @2 :Text;
    userinfoEndpoint                 @3 :Text;
    jwksUri                          @4 :Text;
    endSessionEndpoint               @5 :Text;
    deviceAuthorizationEndpoint      @6 :Text;
    revocationEndpoint               @7 :Text;
    introspectionEndpoint            @8 :Text;

    responseTypesSupported           @9  :List(Text);
    grantTypesSupported              @10 :List(Text);
    tokenEndpointAuthMethodsSupported @11 :List(Text);
    scopesSupported                  @12 :List(Text);
    idTokenSigningAlgValuesSupported @13 :List(Text);
    codeChallengeMethodsSupported    @14 :List(Text);
    dpopSigningAlgValuesSupported    @15 :List(Text);
    requestObjectSigningAlgValuesSupported @16 :List(Text);
    # Present when the IdP advertises OAuth 2.0 Token Exchange (RFC 8693).
    tokenExchangeSupported           @17 :Bool;
}

struct IdTokenPolicy {
    expectedAudience     @0 :Text;           # registered client_id
    expectedAzp          @1 :Text;           # authorized party, if set
    requiredAcr          @2 :List(Text);     # any-of
    requiredAmr          @3 :List(Text);     # any-of
    maxAgeSeconds        @4 :UInt32;         # per OIDC core `max_age`
    clockSkewSeconds     @5 :UInt32;
    nonceMustMatch       @6 :Data;           # empty = no nonce check
    requireAtHashMatch   @7 :Bool;           # if accessToken present
    requireCHashMatch    @8 :Bool;           # if code present
}

struct IdTokenClaims {
    issuer     @0 :Text;
    subject    @1 :Text;
    audience   @2 :List(Text);
    issuedAt   @3 :Int64;
    expiresAt  @4 :Int64;
    notBefore  @5 :Int64;
    nonce      @6 :Data;

    acr        @7  :Text;
    amr        @8  :List(Text);
    azp        @9  :Text;
    authTime   @10 :Int64;

    email      @11 :Text;
    emailVerified @12 :Bool;
    preferredUsername @13 :Text;
    name       @14 :Text;
    groups     @15 :List(Text);

    # Opaque claim map for everything else (profile-specific fields,
    # custom claims). Values are JSON-encoded bytes.
    additional @16 :List(NamedBlob);
}

struct NamedBlob {
    name  @0 :Text;
    value @1 :Data;
}

IdTokenClaims is intentionally read-only metadata. Possessing a serialized copy must not grant authority. The durable external subject key is subjectHash = hash(providerKind, issuer, tenant, subject); admission policy maps it to a local principal, account, and profiles before a UserSession is minted.

External identity admission

OIDC authentication produces verified claims. It does not by itself create a local account, select local roles, or grant capabilities. After verifyIdToken succeeds, SessionManager resolves the external subject through one of the identity proposal’s admission sources:

  • a manifest-seeded external admission rule for bootstrap, recovery, or early console login before durable storage exists;
  • a local account-store ExternalIdentityBinding that maps hash(providerKind, issuer, tenant, subject) to an existing local principal; or
  • an explicit auto-creation rule that creates a pseudonymous or tenant-scoped account with named policy and resource profiles.

The binding shape belongs with the account model, but OIDC consumers depend on its semantics:

struct ExternalIdentityBinding {
    bindingId @0 :Data;
    provider @1 :Text;        # OIDC issuer or configured provider name
    subjectHash @2 :Data;     # hash(provider kind, issuer, tenant, subject)
    principalId @3 :Data;     # local or pseudonymous principal
    tenant @4 :Text;
    acceptedClaims @5 :List(Text);
    expiresAtMs @6 :UInt64;
    policyProfile @7 :ProfileRef;
    resourceProfile @8 :ProfileRef;
    schemaVersion @9 :UInt32;
    storeEpoch @10 :UInt64;
    recordVersion @11 :UInt64;
    policyEpoch @12 :UInt64;
    previousHash @13 :Data;
    contentHash @14 :Data;
}

OIDC groups, roles, acr, amr, tenant IDs, device posture, source network, and token age are normalized ABAC inputs. A binding rule may map a provider group to a local role only for a named provider/tenant, expiry, and policy version. Imported claims are discarded or refreshed when stale, and roles selected from them remain broker inputs rather than authority.

An external session receives durable storage only when a binding or auto-creation rule maps it to a local principal and a resource profile. Without that mapping, the session is guest, anonymous, or one-shot pseudonymous policy with narrow temporary resources.

OAuth client

interface OAuthClient {
    # Bound configuration.
    info              @0 () -> (meta :OAuthClientMetadata);

    # Authorization Code + PKCE (OAuth 2.1 default). The caller owns
    # the redirect side-channel; this cap drives the token exchange
    # after the code returns.
    startAuthCode     @1 (requested :TokenRequest)
                      -> (authUrl :Text, state :AuthCodeState);
    completeAuthCode  @2 (state :AuthCodeState,
                          code :Data)
                      -> (bundle :TokenBundle);

    # Device Authorization Grant (RFC 8628). Appropriate for serial
    # consoles, embedded displays, and TVs — anywhere the capOS
    # process has no browser.
    startDeviceCode   @3 (requested :TokenRequest)
                      -> (userCode :Text,
                          verificationUri :Text,
                          verificationUriComplete :Text,
                          expiresIn :UInt32,
                          interval :UInt32,
                          state :DeviceCodeState);
    pollDeviceCode    @4 (state :DeviceCodeState)
                      -> (outcome :DeviceCodePoll);

    # Client Credentials (RFC 6749 §4.4). Backend-to-backend; the
    # caller principal is the client itself.
    clientCredentials @5 (requested :TokenRequest)
                      -> (bundle :TokenBundle);

    # Refresh an existing bundle (RFC 6749 §6). Fails if the stored
    # refresh token is expired or revoked.
    refresh           @6 (token :RefreshToken,
                          requested :TokenRequest)
                      -> (bundle :TokenBundle);

    # JWT Bearer (RFC 7523). Caller presents a signed assertion about
    # a subject; issuer returns a token for that subject. Used for
    # service delegation and some IdP federation flows.
    jwtBearer         @7 (assertion :Data,
                          requested :TokenRequest)
                      -> (bundle :TokenBundle);

    # Token Exchange (RFC 8693). Foundation of modern workload
    # identity federation: exchange a subject token (e.g. a signed
    # instance-identity JWT or an attestation report envelope) for
    # an access token at the remote issuer.
    tokenExchange     @8 (subjectToken :Data,
                          subjectTokenType :Text,     # RFC 8693 §2.1
                          actorToken :Data,
                          actorTokenType :Text,
                          requested :TokenRequest)
                      -> (bundle :TokenBundle);

    # Revoke (RFC 7009). Best-effort; not all IdPs honor it.
    revoke            @9 (token :TokenRef, reason :Text) -> ();
}

struct OAuthClientMetadata {
    clientId          @0 :Text;
    issuer            @1 :Text;
    authMethod        @2 :ClientAuthMethod;
    defaultScopes     @3 :List(Text);
    defaultAudience   @4 :Text;
    redirectUris      @5 :List(Text);
    dpopRequired      @6 :Bool;
    pkceRequired      @7 :Bool;     # true for public clients
}

enum ClientAuthMethod {
    none              @0;   # public client with PKCE
    clientSecretBasic @1;   # HTTP Basic; confidential clients
    clientSecretPost  @2;   # form-encoded; legacy
    privateKeyJwt     @3;   # RFC 7523 §2.2 — signed JWT with client's PrivateKey
    tlsClientAuth     @4;   # RFC 8705 — mTLS using TlsClientConfig
    selfSignedTlsClientAuth @5;
}

struct TokenRequest {
    scopes            @0 :List(Text);
    audience          @1 :Text;
    resource          @2 :List(Text);   # RFC 8707
    acrValues         @3 :List(Text);
    maxAgeSeconds     @4 :UInt32;
    prompt            @5 :List(Text);   # "login", "consent", "select_account", "none"
    loginHint         @6 :Text;
    nonce             @7 :Data;         # empty = generate fresh
    requestedExpirySeconds @8 :UInt32;  # hint; IdP has final say
    dpopKey           @9 :PrivateKey;   # optional DPoP binding
    extraParams       @10 :List(NamedBlob);
}

struct AuthCodeState {
    opaque @0 :Data;    # server-held state; PKCE verifier, nonce, etc.
}
struct DeviceCodeState {
    opaque @0 :Data;
}

struct DeviceCodePoll {
    union {
        pending     @0 :Void;
        slowDown    @1 :Void;
        expired     @2 :Void;
        denied      @3 :Void;
        granted     @4 :TokenBundle;
    }
}

Tokens

interface AccessToken {
    # Claims view (parsed once; opaque tokens return empty claims and
    # let the IdP's introspection endpoint be the source of truth).
    claims            @0 () -> (claims :TokenClaims);

    # Present the token for a single outbound HTTP request. The token
    # service inserts the Authorization / DPoP headers into the
    # outbound request built by the caller. Raw bytes do not leave
    # the token service through this path.
    authorize         @1 (request :OutboundHttpRequest)
                      -> (prepared :OutboundHttpRequest);

    # Down-scope to a narrower scope set or audience. Fails if the
    # requested scopes are not a subset of the current token's scopes.
    # Implementation can either return a wrapper cap that performs
    # client-side attenuation (for simple bearer tokens) or call the
    # IdP's token-exchange endpoint (for cross-audience narrowing).
    attenuate         @2 (scopes :List(Text),
                          audience :Text)
                      -> (narrower :AccessToken);

    # Explicit export for rare cases where the caller truly needs the
    # raw token (e.g. a capOS HTTP client that has no token-aware
    # stack). Emits an audit event naming the reason. Excluded by
    # default from attenuated caps returned by `attenuate`.
    exportRaw         @3 (reason :Text) -> (bytes :Data);

    # Token reference for revocation, introspection, or logging. Always
    # a hash or opaque ID; never the raw token.
    reference         @4 () -> (ref :TokenRef);

    # Expiry information for client-side backoff and pre-refresh.
    expiry            @5 () -> (notBefore :Int64, notAfter :Int64);
}

interface RefreshToken {
    # Refresh tokens are always longer-lived secrets. They do not
    # expose an `authorize` path — their only use is through
    # OAuthClient.refresh. `reference` and `expiry` match AccessToken.
    reference         @0 () -> (ref :TokenRef);
    expiry            @1 () -> (notBefore :Int64, notAfter :Int64);
    # Export is available but guarded and audited; used for migration
    # between token stores, not for ordinary operation.
    exportRaw         @2 (reason :Text) -> (bytes :Data);
}

interface IdToken {
    claims            @0 () -> (claims :IdTokenClaims);
    raw               @1 (reason :Text) -> (bytes :Data);
}

struct TokenBundle {
    access    @0 :AccessToken;
    refresh   @1 :RefreshToken;   # may be null
    id        @2 :IdToken;        # may be null
    expiresIn @3 :UInt32;
    tokenType @4 :Text;           # "Bearer" or "DPoP"
    scopes    @5 :List(Text);
    resource  @6 :List(Text);
}

struct TokenClaims {
    issuer     @0 :Text;
    subject    @1 :Text;
    audience   @2 :List(Text);
    scope      @3 :List(Text);
    clientId   @4 :Text;
    issuedAt   @5 :Int64;
    expiresAt  @6 :Int64;
    notBefore  @7 :Int64;
    jwtId      @8 :Text;
    # Confirmation (cnf, RFC 7800) for proof-of-possession tokens.
    confirmation @9 :TokenConfirmation;
    additional @10 :List(NamedBlob);
}

struct TokenConfirmation {
    union {
        none     @0 :Void;
        jkt      @1 :Data;        # DPoP: thumbprint of holder public key
        x5tS256  @2 :Data;        # mTLS client cert thumbprint
    }
}

struct TokenRef {
    kind      @0 :TokenRefKind;
    value     @1 :Data;           # hash, jti, or opaque server ref
}

enum TokenRefKind {
    jti       @0;    # JWT `jti`
    sha256    @1;    # SHA-256 of the raw token
    serverId  @2;    # opaque IdP-side identifier
}

struct OutboundHttpRequest {
    method    @0 :Text;
    url       @1 :Text;
    headers   @2 :List(NamedBlob);
    body      @3 :Data;
}

Token verifier (resource-server side)

interface TokenVerifier {
    # Validate an inbound bearer token: signature against the
    # provider's JWKS (or introspection endpoint for opaque tokens),
    # issuer, audience, expiry, required scopes, confirmation claim
    # (DPoP proof or mTLS peer cert).
    verifyAccess      @0 (token :Data,
                          policy :TokenVerificationPolicy,
                          proof :VerificationProof)
                      -> (outcome :TokenVerificationOutcome);
}

struct TokenVerificationPolicy {
    expectedIssuer    @0 :Text;
    expectedAudience  @1 :Text;
    requiredScopes    @2 :List(Text);     # all-of
    anyRequiredScopes @3 :List(Text);     # any-of if non-empty
    clockSkewSeconds  @4 :UInt32;
    requireConfirmation @5 :ConfirmationKind;   # none / dpop / mtls
    allowedAlgorithms @6 :List(SignatureScheme);
    allowIntrospection @7 :Bool;          # opaque token support
}

enum ConfirmationKind {
    none @0;
    dpop @1;
    mtls @2;
}

struct VerificationProof {
    union {
        none      @0 :Void;
        dpopProof @1 :DpopProof;
        peerCert  @2 :Certificate;
    }
}

struct DpopProof {
    jwt       @0 :Data;                   # the DPoP header value
    httpMethod @1 :Text;
    httpUrl   @2 :Text;
    nonce     @3 :Data;                   # server-issued DPoP nonce (RFC 9449 §8)
}

struct TokenVerificationOutcome {
    union {
        valid   @0 :ValidToken;
        invalid @1 :TokenVerificationFailure;
    }
}

struct ValidToken {
    claims     @0 :TokenClaims;
    algorithm  @1 :SignatureScheme;
    keyId      @2 :Text;
}

struct TokenVerificationFailure {
    reason     @0 :TokenFailureReason;
    detail     @1 :Text;
}

enum TokenFailureReason {
    badSignature        @0;
    unknownKeyId        @1;
    unexpectedIssuer    @2;
    audienceMismatch    @3;
    expired             @4;
    notYetValid         @5;
    insufficientScopes  @6;
    missingConfirmation @7;
    dpopMismatch        @8;
    mtlsThumbprintMismatch @9;
    revoked             @10;
    malformed           @11;
    introspectionDenied @12;
    weakAlgorithm       @13;
}

JWKS

interface Jwks {
    # Public keys exposed as PublicKey caps keyed by `kid`. Key
    # rotation is invisible to callers: they ask for a `kid`, they
    # get a current PublicKey or `unknownKeyId`.
    keyById    @0 (kid :Text) -> (key :PublicKey);

    # Enumerate keys (for diagnostics and admin). Returns metadata
    # only; PublicKey caps come from keyById.
    listKeyMeta @1 () -> (keys :List(JwkMeta));

    # Monotonic version bumped on every refresh that changes the key
    # set; consumers cache validated signatures by (kid, version).
    version    @2 () -> (n :UInt64);

    # Force a refresh. Audited. Called automatically on
    # verification-time `unknownKeyId`; exposed for admin use.
    refresh    @3 () -> ();
}

struct JwkMeta {
    kid        @0 :Text;
    algorithm  @1 :AsymmetricAlgorithm;
    use        @2 :Text;        # "sig" or "enc"
    scheme     @3 :SignatureScheme;
    createdAt  @4 :Int64;
}

Workload identity federation

interface WorkloadIdentityFederation {
    # Produce a fresh remote access token by exchanging a local
    # subject token (instance-identity JWT, attestation report,
    # Kubernetes projected token, GitHub Actions OIDC token, ...)
    # at the remote issuer per RFC 8693.
    exchange   @0 (requested :TokenRequest)
               -> (bundle :TokenBundle);

    info       @1 () -> (meta :WorkloadFederationMeta);
}

struct WorkloadFederationMeta {
    remoteIssuer        @0 :Text;
    audience            @1 :Text;
    subjectSource       @2 :SubjectSource;
    allowedScopes       @3 :List(Text);
    minRefreshInterval  @4 :UInt32;
}

enum SubjectSource {
    instanceIdentityJwt    @0;   # from CloudMetadata.InstanceIdentity
    attestationReport      @1;   # SEV-SNP / TDX / Nitro
    projectedServiceAccount @2;  # e.g. Kubernetes projected token
    githubActionsOidc      @3;   # ci/cd trust anchor
    localPrivateKeyJwt     @4;   # private_key_jwt against remote STS
}

DPoP

DPoP (RFC 9449) binds a token to a client-held key. The binding is expressed as a TokenConfirmation.jkt on the access token plus a short-lived proof JWT per outbound request.

interface DpopSigner {
    # Returns a fresh DPoP proof JWT for an outbound request. The
    # signer holds the PrivateKey; the access token is `jkt`-bound to
    # that key's thumbprint.
    newProof   @0 (method :Text,
                   url :Text,
                   accessTokenHash :Data,
                   serverNonce :Data)
               -> (proofJwt :Data);

    publicKey  @1 () -> (pk :PublicKey);
}

A deployment requiring DPoP composes AccessToken + DpopSigner in a wrapper cap so ordinary callers just invoke authorize and receive a request with both Authorization: DPoP ... and DPoP: headers set.

JWT wrappers over key-management primitives

These live here rather than in the key-management proposal because JWT is a protocol frame, not a crypto primitive. They are thin adapters over PrivateKey / PublicKey.

interface JwtSigner {
    # Sign a compact-serialized JWT. The key lives in a KeyVault;
    # JwtSigner is the schema-aware wrapper.
    sign       @0 (header :JwtHeader, claims :Data) -> (jwt :Data);
    publicKey  @1 () -> (pk :PublicKey);
    keyId      @2 () -> (kid :Text);
}

interface JwtVerifier {
    verify     @0 (jwt :Data, policy :JwtVerifyPolicy)
               -> (outcome :JwtVerifyOutcome);
}

struct JwtHeader {
    algorithm  @0 :SignatureScheme;
    keyId      @1 :Text;
    type       @2 :Text;            # "JWT", "at+jwt", "dpop+jwt"
    contentType @3 :Text;
}

struct JwtVerifyPolicy {
    expectedIssuer    @0 :Text;
    expectedAudience  @1 :Text;
    expectedType      @2 :Text;
    allowedAlgorithms @3 :List(SignatureScheme);
    clockSkewSeconds  @4 :UInt32;
    jwksSource        @5 :Jwks;     # preferred
    staticKey         @6 :PublicKey; # for single-signer cases
}

struct JwtVerifyOutcome {
    union {
        valid   @0 :JwtValid;
        invalid @1 :JwtInvalid;
    }
}

struct JwtValid {
    header     @0 :JwtHeader;
    claims     @1 :Data;
}

struct JwtInvalid {
    reason     @0 :TokenFailureReason;
    detail     @1 :Text;
}

SignatureScheme is reused from the key-management proposal. Adding ps256/ps384/ps512 and es256/es384/es512 aliases there covers the JWT algorithm registry without duplicating the enum.

Grant Types in Detail

Authorization Code + PKCE

Used by the web text shell gateway and any capOS native app with a browser. PKCE is mandatory (OAuth 2.1); code_challenge_method = S256. The AuthCodeState.opaque blob carries the PKCE verifier, nonce, and original TokenRequest; callers do not see or store these values. Redirect URIs are validated against OAuthClientMetadata exactly, no partial matching.

Device Authorization Grant (RFC 8628)

Used on serial consoles and other no-browser surfaces. The console prints verification_uri and user_code; the user completes the flow in a separate device’s browser; the console polls the token endpoint. pollDeviceCode honors the slow_down response and caps its polling rate at the IdP-advertised interval. Expiration is a hard fail; the console must restart the flow.

This is the primary OIDC path for boot-to-shell on headless hosts and for interactive cloud-VM serial consoles.

Client Credentials

Used for backend-to-backend service identity. The calling service holds an OAuthClient cap configured with privateKeyJwt or tlsClientAuth. No user is involved; the subject of the issued token is the client itself.

Refresh

Used to rotate a short-lived access token without re-authenticating the user. Refresh tokens are long-lived secrets and live in the RefreshToken cap; they never appear as bytes in session state. Rotated refresh tokens (IdPs that issue a new refresh token on every refresh) are installed into the same cap transparently.

JWT Bearer (RFC 7523)

Used for federation between systems that trust a common signing key. A capOS service holding a JwtSigner can mint an assertion identifying a subject and exchange it at the IdP for a token acting on behalf of that subject. Used sparingly; the delegation implication is strong.

Token Exchange (RFC 8693)

The foundation of modern workload identity federation. Described in its own subsystem (WorkloadIdentityFederation) because the subject-token source is platform-specific. Concrete mappings:

  • AWS IRSA / IAM OIDC provider: subject token is a Kubernetes projected service-account JWT; IdP is sts.amazonaws.com; AssumeRoleWithWebIdentity returns AWS-scoped credentials.
  • GCP Workload Identity Federation: subject token is an InstanceIdentity JWT from the GCE metadata service or a Kubernetes projected token; IdP is sts.googleapis.com; returned token is usable against GCP APIs including Cloud KMS.
  • Azure federated identity credentials: subject token is an OIDC token from a trusted IdP (GitHub, GitLab, Kubernetes, another capOS instance); IdP is Azure AD; returned token is a standard AAD access token.
  • SEV-SNP / TDX / Nitro attestation: subject token is the attestation report envelope; IdP is the cloud KMS or a standalone attestation verifier; returned token authorizes a KMS Decrypt against an attestation-policy-gated KEK.

In every case the capOS image contains no long-lived credentials. The boot path produces a local InstanceIdentity cap, passes it to a WorkloadIdentityFederation configured for the target cloud, and receives short-lived tokens that KMS and other services accept.

Trust Bootstrap

An OidcIdentityProvider cap is created by a trusted service (the OAuth service) from a provider configuration record. The record includes:

  • The canonical issuer URL.
  • One of:
    • a fixed JWKS snapshot baked into the manifest (for air-gapped or hermetic deployments), or
    • the discovery URL plus one or more pinned root certs / SPKI hashes for the TLS connection that fetches discovery and JWKS (via TlsClientConfig and PinSet from the certificates proposal).
  • Acceptable algorithms (allowedAlgorithms in policy).
  • Minimum token lifetime and maximum clock skew.
  • Whether the IdP advertises token exchange, DPoP, and PAR (pushed authorization requests).
  • Client registrations allowed to use this IdP.

The trust root for OIDC verification is ultimately the TLS trust chain back to a certificate authority plus the discovery document’s signing policy. OidcIdentityProvider therefore depends on a TlsClientConfig from the certificates proposal, not on raw sockets. Issuer URL mismatches and JWKS failures are hard errors; neither falls back to unauthenticated HTTP.

For enterprise IdPs that rotate signing keys frequently, Jwks caches keys with a short TTL and refreshes on verification-time unknownKeyId. A deployment that wants to forbid automatic refresh (to pin a specific key set) configures Jwks with refresh disabled; key rotation then requires a manifest update.

Authentication Strength Mapping

SessionInfo.authStrength from user-identity uses X.1254 LoA tiers. OIDC acr/amr claims map as follows (deployment-configurable):

  • loa1 — self-asserted, amr includes pwd only, acr absent or low.
  • loa2 — single-factor, amr includes pwd, pin, or email-link style.
  • loa3 — multi-factor with a hardware-backed credential: amr contains hwk, swk with device attestation, face+pwd, fpt+pwd, or equivalent; acr typically names a named MFA policy.
  • loa4 — high-assurance, typically requires identity proofing plus tamper-resistant hardware: amr contains pop with attested device, hwk plus face, in-person proofing claims, or vendor- specific high-assurance acr values.

The mapping table lives in OAuthClientMetadata policy, not hard- coded. loa0 (anonymous) is capOS-specific and has no matching OIDC claim; anonymous sessions do not use OIDC.

Consumers

ConsumerUses
Console login (device code)OAuthClient.startDeviceCode + verifyIdToken
Web text shell loginOAuthClient.startAuthCode + verifyIdToken; TLS from certs
Cloud KMS access (no baked creds)WorkloadIdentityFederation.exchangeAccessToken.authorize
CloudKmsKeySource unlockWraps AccessToken.authorize; no ambient cloud credentials
Service-to-service outbound HTTPOAuthClient.clientCredentials + AccessToken.authorize
Inbound API token validationTokenVerifier.verifyAccess
Per-user EncryptedNamespaceOidcFederatedKeySource derives KEK from user’s AccessToken
Audit / telemetry exportService identity via client credentials + DPoP
CI/CD runtime trustWorkloadIdentityFederation from GitHub Actions OIDC

Threat Model

Specific to this subsystem:

  1. Token leakage via logs. The classic OAuth failure mode. Raw tokens never leave the OAuth service through claims, references, or audit records. exportRaw is the only escape hatch and is audited with a mandatory reason string.
  2. Refresh token theft. Refresh tokens are long-lived secrets. Mitigations: storage in the same service that holds the cap (not in session state, not in cookies readable by shells), optional rotation on refresh, revocation on logout.
  3. Replay of bearer tokens. A stolen bearer token is usable until expiry. Mitigations: short TTLs; require DPoP (ConfirmationKind.dpop) for sensitive resources; mTLS for service-to-service. Nonce-bound DPoP proofs (RFC 9449 §8) with server-issued nonces where the resource server supports them.
  4. Mixed-IdP confusion. A token issued by IdP A is presented to a verifier expecting IdP B. Mitigations: strict expectedIssuer match; audience binding; IdP-specific OAuthClient caps so services cannot confuse two OIDC providers; RFC 9207 iss parameter on authorization responses verified before the token exchange.
  5. Discovery-document tampering. An attacker on the TLS path returns a forged discovery document or JWKS. Mitigations: pinned TLS roots or SPKI hashes per IdP; JWKS fetched over the same pinned TLS client; signature algorithm allow-list rejects downgrades; manifest-defined acceptable discovery URL prevents runtime redirect to attacker IdP.
  6. PKCE downgrade. A public client accepts a token without proving possession of the code verifier. Mitigations: PKCE is mandatory (pkceRequired = true is not a bit the caller can clear from a derived cap); code_challenge_method = S256 only.
  7. Authorization code replay. A leaked code is redeemed by an attacker. Mitigations: PKCE binds the code to the verifier the browser holds; codes are single-use; redirect URI exact match.
  8. Open redirector via redirect URI. Mitigations: exact-match redirect URIs per registration; no substring matching; validated at both startAuthCode and completeAuthCode.
  9. Cross-site request forgery on the authorization request. Mitigations: state parameter generated from EntropySource, stored in AuthCodeState.opaque, checked on completion; PKCE adds a second CSRF-resistant binding.
  10. OIDC nonce omission. Missing nonce on the ID token allows replay of an ID token from another session. Mitigations: IdTokenPolicy.nonceMustMatch is mandatory for interactive logins; verifyIdToken refuses an ID token whose nonce does not match the one baked into AuthCodeState.opaque.
  11. Mis-issued sub claim. An IdP reuses a sub across tenants or rebinds it. Mitigations: the external subject key includes provider kind, issuer, normalized tenant, and subject; it is never sub alone. Tenant-scoped IdPs (Azure AD per-tenant, Google Workspace) still record the tenant explicitly before hashing.
  12. JWKS flooding. An attacker forces repeated unknownKeyId failures to trigger JWKS refreshes. Mitigations: refresh rate- limited per Jwks cap; audit events recorded; repeated failures fail closed rather than refresh-in-loop.
  13. Token exchange policy evasion. An attacker with a narrow subject token exchanges it for a broader one. Mitigations: the remote issuer enforces its own policy on token exchange; capOS cannot prevent a misconfigured STS. Defense is to pin WorkloadFederationMeta.remoteIssuer and inspect returned scopes against allowedScopes.
  14. Clock skew attacks. Old tokens accepted, new tokens rejected. Mitigations: clockSkewSeconds is small by default; consumers that require hard bounds use an attested time source.

Security Verification in ITU-T and GOST Terms

OIDC and OAuth2 are IETF/OpenID protocols, but capOS’s broader security vocabulary is ITU-T/ISO-IEC plus, where a deployment requires it, GOST. The same verification surface this proposal defines (signature checks on JWTs, discovery and JWKS integrity, token binding, claim validation, scope enforcement, auth strength, logout semantics) maps onto those frameworks cleanly; it does not require a parallel vocabulary.

ITU-T X.805 security dimensions

X.805 (“Security architecture for systems providing end-to-end communications”) decomposes security into eight dimensions. The relevant mapping for the OIDC subsystem:

X.805 dimensionWhere it lives
Access controlAuthorityBroker + CapObject::call (ADF/AEF per X.812); scopes/claims as ABAC input
AuthenticationOidcIdentityProvider.verifyIdToken; TokenVerifier.verifyAccess
Non-repudiationSigned JWTs + audit records of verifyIdToken, issuance, exchange, revocation
Data confidentialityTLS for every IdP call; encrypted audit payloads where applicable
Communication securityTlsClientConfig from the certificates proposal; issuer-pinned roots; HSTS-equivalent pins
Data integrityJWT signature verification against Jwks; kid rotation handled without trust decay
AvailabilityFailure semantics defined for JWKS refresh, device-code expiry, introspection outage
PrivacyIdTokenClaims exposes only claims the client actually requires; scope minimization

Each cell is a discrete thing to verify, test, and review. Keeping the dimensions explicit makes gaps visible: for example, “what is our availability story if the IdP’s JWKS endpoint is down for 2 hours” is a concrete X.805 question; the answer is Jwks cache TTL + refresh audit + fail-closed behavior on unknown kid.

ITU-T X.812 ADF/AEF

Already inherited from user-identity-and-policy-proposal.md. The OIDC-specific instances:

  • AEF (enforcement point): CapObject::call and wrapper caps (AccessToken.authorize, TokenVerifier.verifyAccess). Bypass requires subverting the cap graph, not forging a claim.
  • ADF (decision point): the OAuth service when issuing a token, AuthorityBroker when returning scoped caps, TokenVerifier when accepting a bearer. A decision returns a capability (or denial); it does not return a boolean that downstream code might ignore.

ITU-T X.1254 / ISO/IEC 29115 LoA

Already built into the mapping: IdTokenClaims.acr/amrAuthStrength enum (loa1..loa4). The mapping table lives in OAuthClientMetadata so each deployment can specify which IdP acr/amr values count as each tier. SealPolicy.tokenExchange carries minAuthStrength so unlock policy can say “require LoA 3+” without knowing any specific IdP’s acr taxonomy.

ITU-T X.1252 identity management terms

X.1252 defines identity, credential, entity, enrolment, identity provider, relying party, and identity assurance. The proposal’s entities map directly:

X.1252 termcapOS realization
Identity providerOidcIdentityProvider
Relying partyAny service holding an OAuthClient cap
CredentialBearer, DPoP-bound, or mTLS-bound AccessToken; IdToken; RefreshToken
EnrolmentCredentialStore bootstrap of IdP trust records + subject allow-list
Assurance levelAuthStrength (= X.1254 LoA)
Attribute authorityIdP via claims; optionally PolicyEngine for derived ABAC attributes
Identity bindingCanonical subjectHash mapped to a local PrincipalInfo.id; never sub alone

ITU-T X.1255 and federated-identity discovery

X.1255 is the discovery framework for federated identity. The closest IETF analog is OIDC Discovery (RFC 8414 + OpenID Discovery 1.0). OidcIdentityProvider.metadata is the capOS surface for both. The manifest-declared discovery URL + pinned TLS root closes the “federated discovery must be trustworthy” requirement that X.1255 leaves to deployment.

ITU-T X.813 / ISO/IEC 10181-4 non-repudiation

Non-repudiation of authentication comes from the IdP’s signed ID token. Non-repudiation of authorization decisions comes from AuditLog records that include the decision inputs (claim summaries, policy IDs, outcome). The framework deliberately does not promise non-repudiation of shell commands — the agent shell is a planner, not a signer of operator intent.

IETF OAuth security BCPs

For completeness, the proposal tracks:

  • RFC 6819 — OAuth 2.0 Threat Model and Security Considerations. Covered by the threat-model section above.
  • RFC 9700 — OAuth 2.0 Security Best Current Practice. The “PKCE mandatory”, “exact redirect URI match”, “mix-up defense via iss parameter”, “no implicit grant”, and “rotate refresh tokens” items are all baked in rather than opt-in.
  • FAPI 2.0 (OpenID Foundation) — financial-grade API profile. Useful as a pre-packaged high-assurance profile: DPoP or mTLS sender-constrained tokens, PAR, signed authorization requests, strict algorithms. OAuthClientMetadata is deliberately shaped so a “FAPI profile” is a set of required fields, not a separate interface.

GOST MAC/MIC (ГОСТ Р 59383-2021, ГОСТ Р 59453.1-2021)

capOS’s mandatory-access-control and mandatory-integrity-control story is described at two levels in user-identity-and-policy-proposal.md and formal-mac-mic-proposal.md:

  • a pragmatic level where userspace brokers and wrapper caps enforce labels at grant paths, and
  • a formal level where an abstract automaton (subjects, objects, containers, hold edges, rights, accesses, information flows) carries explicit safety predicates and proof obligations in the shape ГОСТ Р 59453.1-2021 requires.

OIDC integration must fit both levels without introducing a second authority channel. Concretely:

Federated principals and subjects

An OIDC-authenticated UserSession creates a subject in the formal automaton with:

  • subjectHash = hash(providerKind, iss, tenant, sub) — the durable external subject key, not reusable across IdPs or tenants. The local session principal may be a pseudonymous principal created for this external key or the local principal named by an ExternalIdentityBinding.
  • confidentiality_label and integrity_label resolved by LabelAuthority from the policy profile plus optional claim-derived refinement (e.g. groups = ["ops"] narrows to a specific compartment). Claims influence labels at mint time; they are not authority downstream.
  • authStrength from acr/amr, already folded into LoA tiers.

The create_session transition in the formal automaton therefore has one additional precondition when the login method is OIDC:

create_session(principal, policy_profile, resource_profile, oidc_proof):
  pre:
    verify_id_token(oidc_proof) succeeds with IdTokenPolicy
    IdP trust record in CredentialStore permits (subjectHash, policy_profile)
    manifest seed or AccountStore admission permits the binding
    acr/amr satisfy policy_profile's minimum AuthStrength
    subject allow-list or ExternalIdentityBinding admits subjectHash
  effect:
    new subject s with labels derived from policy_profile + claims
    Hold(s, session_bundle) per AuthorityBroker(
        session,
        policy_profile,
        resource_profile,
    )

This is the same precondition shape as password and passkey login — the safety proof does not branch on authentication method. It only requires that verify_id_token is modeled as a trusted verifier that rejects inputs failing the IdP’s published policy.

Integrity labels on IdP trust

IdP trust records carry an integrity level. An IdP configured as the corporate operator IdP can mint sessions with higher integrity than an IdP configured for guest/partner access. LabelAuthority encodes this in the trust-record metadata; SessionManager refuses to mint a session whose policy profile claims higher integrity than the admitting IdP’s integrity level.

The formal invariant:

integrity(session) <= integrity(admitting_IdP_trust_record)

This closes the federated analog of “any trusted login path can mint a maximally trusted session” — a gap that is easy to introduce by accident when enterprises add a second, looser IdP.

Flow classes for token capabilities

Each method on the typed token interfaces needs a flow class per the formal-mac-mic-proposal.md table. Proposed classifications:

OidcIdentityProvider.verifyIdToken    ReadLike + NoFlow   (pure verification)
OidcIdentityProvider.metadata         ObserveLike
Jwks.keyById                          ObserveLike
Jwks.refresh                          ControlLike         (on the Jwks object)

OAuthClient.startAuthCode             ObserveLike         (emits a URL; no subject-bearing data crosses)
OAuthClient.completeAuthCode          TransferLike        (materializes new authority as a token cap)
OAuthClient.startDeviceCode           ObserveLike
OAuthClient.pollDeviceCode            TransferLike        (on "granted")
OAuthClient.clientCredentials         TransferLike
OAuthClient.refresh                   TransferLike
OAuthClient.jwtBearer                 TransferLike + ControlLike  (delegation)
OAuthClient.tokenExchange             TransferLike        (see narrowing below)
OAuthClient.revoke                    ControlLike

AccessToken.claims                    ReadLike            (claims are metadata of the token object)
AccessToken.authorize                 WriteLike           (outbound side-effect under the token's authority)
AccessToken.attenuate                 TransferLike        (narrower cap minted)
AccessToken.exportRaw                 Declassify          (trusted, audited, restricted)
AccessToken.reference/expiry          ObserveLike

RefreshToken.*                        as above; exportRaw is Declassify
IdToken.raw                           Declassify
IdToken.claims                        ReadLike

TokenVerifier.verifyAccess            ReadLike + NoFlow
DpopSigner.newProof                   WriteLike           (produces a short-lived authenticator bound to a request)
WorkloadIdentityFederation.exchange   TransferLike

The key formal-level consequences:

  • AccessToken.exportRaw, RefreshToken.exportRaw, and IdToken.raw are Declassify transitions. They must be modeled as trusted transitions with explicit audit. Excluding them by default from attenuated caps is consistent with the formal model’s requirement that declassification go through explicit trusted subjects.
  • OAuthClient.tokenExchange and AccessToken.attenuate are TransferLike; they cannot widen authority. The safety predicate is “issued-token scope ⊆ input-token scope ∩ policy permits” — exactly the wrapper-narrowing rule from user-identity-and-policy-proposal.md. The proof obligation is a scope-monotonicity lemma on the server side; capOS verifies the result by comparing TokenClaims before accepting the returned cap.
  • AccessToken.authorize is WriteLike against the external resource. In the formal model this is an outbound information flow from the subject to an object whose label is the label of the downstream service the broker wired into the request. Deployments needing a MIC proof must ensure the broker refuses to bind a low-integrity session’s token into a request against a high-integrity service — the integrity(src) >= integrity(dst) rule applied through the broker.

Token attenuation as the wrapper-cap discipline

ГОСТ Р 59453.1 requires that every transfer either preserves or narrows rights; capability attenuation is the capOS mechanism for that. OIDC’s scope is a list of strings; treating scope narrowing as cap attenuation means the verifier at issuance time must reject any attenuate / tokenExchange result whose claimed scope is not a subset of the source token’s scope. This is already the spec’s behavior — the point is that the capOS implementation must enforce it locally as well, because a misbehaving STS would otherwise be a covert widening channel.

Subject-controls-subject and delegation

OAuthClient.jwtBearer (RFC 7523) lets a client speak on behalf of another principal. That is a ControlLike transition in the formal model: the invoking subject is exercising control over the minted subject. The safety predicate is:

supervise_allowed(invoker, delegated):
  integrity(invoker) >= integrity(delegated)
  and invoker holds a delegation capability for the target IdP
  and confidentiality/compartment labels are compatible

This is the formal reason a jwtBearer cap is not a default session authority — it must come from a broker that checks the control relation.

Endpoint declarations

formal-mac-mic-proposal.md requires every endpoint to declare its flow policy. For OIDC-facing services that is:

  • OidcIdentityProvider endpoints declare ObserveLike on metadata calls and ReadLike on verification.
  • OAuthClient endpoints declare the flow classes above and bind the output token’s label to min(session.label, target_audience.label).
  • TokenVerifier endpoints declare ReadLike and bind the verified claims to the caller’s object label (the claims flow into an object owned by the calling service).

Declaring these up-front lets the formal-mac-mic-proposal.md review gate apply without a separate OIDC-specific checker.

ГОСТ Р 58833-2020 — identification and authentication

Beyond MAC/MIC, ГОСТ Р 58833-2020 defines organizational and technical requirements for identification and authentication. OIDC integration satisfies its technical baseline:

  • Identifiers use subjectHash = hash(providerKind, issuer, tenant, subject); subject reuse across IdPs or tenants is disallowed by construction.
  • Credentials (tokens, refresh tokens, DPoP keys) are held inside the OAuth service; raw material does not reach the model, the shell, or audit.
  • Issuance and revocation (OAuthClient.startAuthCode/ startDeviceCode/clientCredentials/..., revoke, SessionManager.logout) are audited.
  • Credential-strength policy is selectable per resource via minAuthStrength on seal policies and broker decisions, aligned to X.1254 / ISO/IEC 29115 LoA.

Organizational measures (credential lifecycle, incident response, operator training) remain a deployment responsibility the OS cannot enforce alone.

Proof-obligation checklist

A deployment aiming for a GOST-style MAC/MIC claim with OIDC federation must add these obligations to the formal-mac-mic-proposal.md proof. The checklist is explicit so reviewers can point at individual items, and so each obligation maps to one of the tools listed in the next subsection.

  1. verify_id_token totality and policy soundness. Modeled as a trusted total function. Accepts only well-formed tokens under the configured IdTokenPolicy (issuer, audience, acr/amr, exp/nbf/iat with bounded skew, nonce, at_hash / c_hash when applicable). Returns IdTokenClaims or a failure reason; never silently downgrades.
  2. PKCE binding. No completeAuthCode(state, code) succeeds unless state was produced by a prior startAuthCode and the PKCE verifier stored in AuthCodeState.opaque hashes to the code_challenge the IdP recorded for code.
  3. Nonce binding. verifyIdToken accepts an ID token only if claims.nonce equals the nonce stored in AuthCodeState.opaque for the matching state. Missing-nonce ID tokens on interactive logins are rejected.
  4. state binding. The authorization response’s state matches the one minted from EntropySource at startAuthCode.
  5. Scope monotonicity. Every TransferLike token transition (AccessToken.attenuate, OAuthClient.tokenExchange, OAuthClient.refresh, OAuthClient.jwtBearer) produces a result whose scope is a subset of the input scope intersected with the broker/IdP-permitted set. No transition widens scope.
  6. JWKS live-set invariant. A token signed under kid = k is accepted iff k was present in Jwks at some time t with iat - clockSkew ≤ t ≤ now. Rotation that removes k does not retroactively invalidate tokens already verified under it; rotation that adds k does not accept tokens older than its introduction.
  7. Device-code polling discipline. pollDeviceCode honors the IdP-issued interval; slow_down responses monotonically increase the local backoff; expired and denied are terminal.
  8. Refresh rotation invariant. A successful OAuthClient.refresh that rotates the refresh token marks the prior RefreshToken cap broken; any subsequent use returns revoked (no parallel use of two generations of the same refresh-token family).
  9. Session-creation MAC/MIC predicate. create_session with an OIDC proof establishes integrity(session) ≤ integrity(admitting_IdP_trust_record) and confidentiality(session) ⊑ confidentiality_ceiling(policy_profile, claims).
  10. Broker-outbound MAC/MIC predicate. When the broker binds an AccessToken to an outbound request, the call site label satisfies integrity(src) ≥ integrity(dst) and the confidentiality flow is permitted. jwtBearer delegations additionally satisfy supervise_allowed(invoker, delegated).

Additional implicit obligations:

  • Declassify transitions (AccessToken.exportRaw, RefreshToken.exportRaw, IdToken.raw) are restricted to trusted subjects and produce audit records with the mandatory reason argument.
  • Endpoint flow declarations for OIDC services cover every method in the schemas above; adding a new method without a declaration is a review failure.

These are additive to the obligations in formal-mac-mic-proposal.md. None require a new kernel mechanism; they extend the same wrapper-cap / endpoint-flow-declaration discipline to OIDC-backed subjects and token-typed capabilities.

Tool assignment

ObligationPrimary toolNotes
1. verify_id_token totalityTLA+ + KaniTLA+ models the trusted function; Kani proves the Rust impl is total
2. PKCE bindingTLA+3-state machine (started/completed/failed); invariant on state
3. Nonce bindingTLA+Joint state with PKCE, same module
4. state bindingTLA+Joint with 2/3; plus Alloy for EntropySource uniqueness
5. Scope monotonicityAlloy + PrustiAlloy for the attenuate/exchange graph; Prusti as post-condition
6. JWKS live-set invariantTLA+Temporal property; Apalache if TLC state-space explodes
7. Device-code polling disciplineZ.100 SDL + TLA+SDL for state + timer structure; TLA+ for liveness
8. Refresh rotation invariantTLA+Safety + single-generation liveness
9. Session-creation MAC/MIC predicateAlloyExtends the hold-edge graph model from formal-mac-mic
10. Broker-outbound MAC/MIC predicateAlloySame model; predicate over outbound endpoint declarations
Declassify auditingKaniRust-level: every exportRaw path writes an audit record
Endpoint flow declarationsReview gate + AlloyEnumerate methods, check coverage relationally

Supporting artifacts (useful even before the full proof lands):

  • Z.120 MSC sequence charts for the three primary flows (authorization code + PKCE, device code, token exchange). MSC traces from a running capOS are already shaped like the sequence dumps tools/ccs produces for capability rings, which makes property-checking “no RETURN without a matching CALL” a straightforward analog to “no token issuance without a matching authorization event.”
  • Proptest/fuzz harnesses for the JWT parser, claim validator, PKCE verifier hash, DPoP proof parser, and discovery-document parser. These are not formal proofs but are the first line of defense for obligations 1 and 2. Tracked under the existing security-and-verification-proposal.md tiered tooling plan.
  • Loom model for the concurrent Jwks refresh path: multiple verification requests racing with a refresh triggered by unknownKeyId. Obligation 6’s live-set invariant is the correctness condition.

Out of scope for the formal track

  • The external IdP’s own correctness. The model treats the IdP as a trusted oracle that emits signed tokens matching its published policy; bugs in the IdP itself are not capOS-provable.
  • Network-layer adversaries. TLS authentication of the IdP and the token endpoint is assumed; that proof lives in the certificates proposal’s track.
  • Timing and microarchitectural side channels on signature verification and DPoP checks. Treated as deployment-level mitigations (constant-time libraries, cache partitioning) rather than modeled flows.
  • User behavior. Phishing, social engineering, and operator credential sharing are outside the model.
  • IdP key compromise. Modeled as an assumption violation; the formal proof cannot recover from a signing-key compromise at the IdP.

Note on GOST cryptographic primitives

Separately from MAC/MIC, a deployment may also require GOST cryptographic algorithms (GOST R 34.10-2012 signatures, GOST R 34.11-2012 Streebog hashes, GOST R 34.12-2015 symmetric ciphers) throughout the JWT/JWS and TLS stack. Those are additive enum extensions in SignatureScheme, HashAlgorithm, AsymmetricAlgorithm, and SymmetricAlgorithm across the key, certificates, and OIDC proposals plus a certified cryptographic library. The interface shape does not change; the MAC/MIC analysis above is independent of the algorithm choice.

ФСТЭК threat modeling

The threat-model section above enumerates OAuth/OIDC-specific attacks (leakage, replay, mixed-IdP confusion, discovery tampering, PKCE downgrade, code replay, redirect hijack, CSRF, nonce omission, sub confusion, JWKS flooding, token-exchange evasion, clock skew). Mapping that enumeration to ФСТЭК’s “Методика оценки угроз” taxonomy is a deployment-specific documentation exercise; the raw facts are already here.

How this combines

A capOS deployment choosing a high-assurance profile selects:

  • X.805 dimensions to audit explicitly (all eight for a regulated service).
  • X.1254 LoA floor per resource (via minAuthStrength on seal policies and broker bundles).
  • A label lattice (confidentiality + integrity) and which IdP trust records can mint sessions at which labels.
  • Which token transitions are modeled as Declassify / Transfer / Control in the MAC/MIC automaton.
  • A concrete IdP trust bootstrap (manifest-pinned JWKS snapshot vs. discovery with pinned TLS root).
  • A concrete audit redaction and retention policy consistent with applicable regulation (ITU-T X.816, ФСТЭК guidance, GDPR, or sector-specific rules).

No kernel change is required to land any of these. Each choice narrows the behavior of userspace services — OAuthClient, OidcIdentityProvider, TokenVerifier, CredentialStore, SessionManager, AuthorityBroker, LabelAuthority, AuditLog — inside the same capability model.

Interaction with capOS Authority Model

OIDC and OAuth2 decide which external subject was authenticated and which scopes apply to this call. Admission policy decides which local principal, account, policy profile, and resource profile that external subject maps to. They do not decide which caps exist in the process. That remains the job of AuthorityBroker.

Practical flow:

  1. User authenticates to capOS via OIDC. SessionManager.login verifies the ID token and computes subjectHash = hash(providerKind, iss, tenant, sub).
  2. SessionManager resolves subjectHash through manifest seed admission, a local account-store ExternalIdentityBinding, or an explicit auto-creation rule. The result is a local or pseudonymous principal plus selected policy and resource profiles.
  3. SessionManager mints a UserSession whose PrincipalInfo.id is the resolved principal and whose authStrength derives from acr/amr.
  4. AuthorityBroker.request receives the session and any relevant access token. Scopes and OIDC claims are inputs to the RBAC/ABAC/MAC decision. They are never sufficient authority on their own.
  5. The broker returns a capability bundle (or denial). The access token is delivered inside an ApprovalGrant or a wrapper cap when the caller needs to invoke an external service; the raw bytes remain inside the OAuth service.
  6. For outbound calls to an OAuth-protected resource, the capOS service holds an AccessToken cap; it does not see the token string.
  7. For inbound calls, a capOS service configured as an OAuth2 resource server holds a TokenVerifier cap plus its AuthorityBroker cap; verification yields claims, and the broker converts claims into narrower caps for the call.

This is the same “decision returns a capability” pattern the user-identity proposal already uses for Cedar/OPA. OIDC just provides one more input shape.

Phases

Phases follow the consumers.

Phase 1 — IdP and client schemas, JWT verification

  • Add the schemas above to schema/capos.capnp.
  • Implement a RAM-only IdP cache that can load a discovery document and JWKS from a static test fixture and verify a sample ID token.
  • Implement JwtVerifier over PublicKey primitives from the key proposal using a vetted Rust crate (jsonwebtoken, biscuit, or a purpose-built verifier on top of rsa / ed25519-dalek / p256).
  • Host tests: signature verification across RS256/ES256/EdDSA, issuer/audience/exp checks, clock skew, algorithm allow-list.

Phase 2 — OAuth client and device code

  • OAuthClient with clientCredentials, refresh, and deviceCode grants.
  • Outbound HTTPS via the networking and certificate stacks (requires those to be real).
  • Console OIDC login proof: QEMU serial starts startDeviceCode, an operator completes the flow out-of-band, pollDeviceCode returns a bundle, verifyIdToken succeeds, a manifest-seeded external admission rule selects policy/resource profiles, and a UserSession is minted.

Phase 3 — Authorization code + PKCE

  • Web text shell gateway redirects to the IdP and consumes the returned code.
  • startAuthCode / completeAuthCode integrated with the gateway’s HTTP listener.
  • Per-session nonce, state, and PKCE verifier all live in AuthCodeState.opaque.

Phase 4 — Resource server verification

  • TokenVerifier.verifyAccess with JWKS refresh and introspection-endpoint fallback for opaque tokens.
  • Policy enforcement: required scopes, audience binding, cnf confirmation (DPoP or mTLS).

Phase 5 — Workload identity federation

  • WorkloadIdentityFederation with subject sources for GCP and AWS.
  • Depends on InstanceIdentity from cloud-metadata and a working outbound TLS client.
  • CloudKmsKeySource gains a no-baked-credentials unlock path.

Phase 6 — Private key client auth and DPoP

  • ClientAuthMethod.privateKeyJwt using JwtSigner.
  • DpopSigner + ConfirmationKind.dpop in TokenVerifier.
  • RFC 9449 nonces when the resource server supports them.

Phase 7 — mTLS-bound tokens and extended federation

  • ClientAuthMethod.tlsClientAuth per RFC 8705.
  • Attestation-report-backed federation (SubjectSource.attestationReport) for confidential computing.
  • CIBA grant (RFC 9126 + OpenID CIBA) if a deployment needs it for step-up on mobile devices.

Phase 8 — Token exchange as a first-class broker input

  • AuthorityBroker accepts an AccessToken or IdToken plus scopes as policy input; decisions can return narrowed access tokens alongside narrower caps.
  • Account-store-backed ExternalIdentityBinding records replace manifest-only external admission for ordinary federated logins. Unknown external subjects are denied unless an explicit auto-creation rule names policy and resource profiles.
  • Per-user EncryptedNamespace unlock via OidcFederatedKeySource (defined in the key-management proposal) using the user’s current access token as unlock context.

Phase 9 — Local IdP (optional, deferred)

  • A LocalIdentityProvider cap that issues tokens to other capOS services on the same host or fleet, signed by a JwtSigner backed by a KeyVault-stored PrivateKey. Useful for air-gapped deployments and for bootstrapping workload federation between two capOS instances. Not in v1.

Relationship to Other Proposals

  • cryptography-and-key-management-proposal.md — supplies PrivateKey / PublicKey / SignatureScheme / AsymmetricAlgorithm. Adds KeySourceKind.oidcFederated, SealPolicy.tokenExchange, KeyPurpose.oauthClientAssertion, and KeyPurpose.oidcIdToken to support this proposal’s consumer shapes.
  • certificates-and-tls-proposal.md — OIDC discovery, JWKS, token endpoint, and IdP admin endpoints are all reached over TLS clients built from TlsClientConfig. IdP pinning composes with PinSet from that proposal. mTLS client authentication for OAuth reuses TlsClientConfig.
  • boot-to-shell-proposal.md — device code and authorization code grants are SessionManager.login methods. CredentialStore stores IdP trust records (issuer URL, JWKS, allowed audiences) alongside password verifiers and passkey public credentials.
  • shell-proposal.md — the authority broker consumes access tokens as ABAC input; the agent shell holds ApprovalGrant wrappers, not raw tokens.
  • user-identity-and-policy-proposal.md — federated subjects resolve through manifest seed admission, local account-store ExternalIdentityBinding records, or explicit pseudonymous auto-creation rules; OAuth scopes and OIDC claims are ABAC attributes, not authority; AuthStrength derives from acr/amr.
  • volume-encryption-proposal.md — OIDC-gated KMS unlock replaces baked IAM credentials; per-user EncryptedNamespace unlock uses OidcFederatedKeySource.
  • cloud-metadata-proposal.mdInstanceIdentity is the primary subject token source for workload identity federation. The current proposal’s own SubjectSource.instanceIdentityJwt is implemented by that cap.
  • networking-proposal.md — outbound OAuth calls use a userspace HTTP/TLS client built over the networking stack. Service-to-service OAuth coexists with mTLS as two delegation patterns rather than competing ones.
  • system-monitoring-proposal.md — every verifyIdToken, token issuance, refresh, exchange, and verifyAccess flows through the audit cap. Redaction rules from the boot-to-shell proposal apply: claim summaries and token references, never raw tokens.
  • security-and-verification-proposal.md — JWT/JWS/JWE parsers are classic fuzz targets; PKCE and device-code state machines are Loom candidates; token-exchange policy evaluation is a Kani candidate.
  • live-upgrade-proposal.md — the OAuth service holds sensitive live state (refresh tokens, DPoP private keys, PKCE verifiers). Live upgrade needs a state-transfer path that does not leak tokens through shared memory.

Open Questions

  1. Do we ship our own OIDC RP implementation or wrap an existing Rust crate? openidconnect-rs, oauth2-rs, and biscuit are candidates. The schema boundary is independent; the implementation choice affects TCB size and audit surface.
  2. Opaque access token handling. Some IdPs issue opaque tokens validated only by introspection (RFC 7662). Latency and load on the introspection endpoint are operational concerns; caching introspection responses is fiddly (when is the cache allowed to serve stale “active”?). Probably: support introspection with short cache TTL and per-policy opt-in.
  3. PKCE-less legacy clients. A deployment against an old IdP that cannot do PKCE. Do we allow a config escape hatch, or do we refuse to boot? Leaning “refuse” given OAuth 2.1 guidance.
  4. DPoP nonce plumbing. Server-issued nonces (RFC 9449 §8) require the caller to retry after the first 401 with the returned nonce. Fits naturally in a wrapper cap around AccessToken, but the retry policy on non-idempotent methods needs a clear rule.
  5. Device code on air-gapped consoles. Device code presumes the user has another device with a browser. Pure-air-gapped hosts must fall back to password + passkey; what about console-only OIDC without internet? Probably: no-op; offline OIDC is an oxymoron, use local auth.
  6. How do tokens transfer across capability boundaries? Per- consumer down-scoped issuance is the default. Should AccessToken.attenuate be a kernel-level badge, a userspace wrapper cap, or both depending on whether attenuation is server-side (token exchange) or client-side (scope subset)?
  7. Logout semantics. OIDC end-session endpoints are optional and frequently inconsistent across IdPs. When UserSession.logout fires, what is the best-effort expectation: local session drop + IdP revoke + RP-initiated logout redirect? Document a clear failure mode for each step.
  8. Default audiences for AuthorityBroker decisions. When the broker down-scopes an access token, what audience does the narrower token target — always the resource server the broker just returned a cap for? Or a list, for broker decisions that return a compound bundle? Probably: one audience per CapRequest, bundles emitted as multiple broker responses.
  9. External auto-creation policy. Which OIDC providers may create pseudonymous local accounts, which policy/resource profiles may they name, and what rollback/recovery record proves the mapping was not replayed from stale account-store state?
  10. Support for JAR / PAR / JARM. Pushed Authorization Requests and JWT-Secured Authorization Response Mode are increasingly expected by enterprise IdPs. Phase 3 should support PAR; JAR and JARM can follow.
  11. Clock source. OIDC verification depends on a reliable clock. Before the Timer capability and a cloud attested-time source exist, verifyIdToken must either fail closed or consume a bootstrap clock from the manifest. Document the first-boot behavior.
  12. Key binding for user sessions. Should a UserSession be bound to a DPoP key by default (so a leaked session ID is useless without the key), or is that overkill for console sessions? Probably: yes for web gateway sessions; no for direct local console sessions where session state never leaves the host.
  13. GOST / jurisdictional OIDC. Some deployments mandate GOST-signed JWTs (GOST R 34.10-2012 on the JWT signature). Adding the algorithms to SignatureScheme is schema-level; validating a GOST-signed discovery document requires matching trust-store support in the certificates proposal. Track, do not block.