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/PolicyEnginewithout 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,EncryptedBlockDeviceunlock 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
LocalIdentityProviderthat 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.loginadapter 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
subreceives aTokenClaimsfacet that does not expose the raw JWT. A caller that only needs to call one resource server receives aBoundTokenthat 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
OAuthClientcap; 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
ExternalIdentityBindingthat mapshash(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;AssumeRoleWithWebIdentityreturns AWS-scoped credentials. - GCP Workload Identity Federation: subject token is an
InstanceIdentityJWT from the GCE metadata service or a Kubernetes projected token; IdP issts.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
TlsClientConfigandPinSetfrom the certificates proposal).
- Acceptable algorithms (
allowedAlgorithmsin 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,amrincludespwdonly,acrabsent or low.loa2— single-factor,amrincludespwd,pin, oremail-link style.loa3— multi-factor with a hardware-backed credential:amrcontainshwk,swkwith device attestation,face+pwd,fpt+pwd, or equivalent;acrtypically names a named MFA policy.loa4— high-assurance, typically requires identity proofing plus tamper-resistant hardware:amrcontainspopwith attested device,hwkplusface, in-person proofing claims, or vendor- specific high-assuranceacrvalues.
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
| Consumer | Uses |
|---|---|
| Console login (device code) | OAuthClient.startDeviceCode + verifyIdToken |
| Web text shell login | OAuthClient.startAuthCode + verifyIdToken; TLS from certs |
| Cloud KMS access (no baked creds) | WorkloadIdentityFederation.exchange → AccessToken.authorize |
CloudKmsKeySource unlock | Wraps AccessToken.authorize; no ambient cloud credentials |
| Service-to-service outbound HTTP | OAuthClient.clientCredentials + AccessToken.authorize |
| Inbound API token validation | TokenVerifier.verifyAccess |
Per-user EncryptedNamespace | OidcFederatedKeySource derives KEK from user’s AccessToken |
| Audit / telemetry export | Service identity via client credentials + DPoP |
| CI/CD runtime trust | WorkloadIdentityFederation from GitHub Actions OIDC |
Threat Model
Specific to this subsystem:
- Token leakage via logs. The classic OAuth failure mode. Raw
tokens never leave the OAuth service through claims, references,
or audit records.
exportRawis the only escape hatch and is audited with a mandatory reason string. - 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.
- 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. - Mixed-IdP confusion. A token issued by IdP A is presented to
a verifier expecting IdP B. Mitigations: strict
expectedIssuermatch; audience binding; IdP-specificOAuthClientcaps so services cannot confuse two OIDC providers; RFC 9207issparameter on authorization responses verified before the token exchange. - 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.
- PKCE downgrade. A public client accepts a token without
proving possession of the code verifier. Mitigations: PKCE is
mandatory (
pkceRequired = trueis not a bit the caller can clear from a derived cap);code_challenge_method = S256only. - 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.
- Open redirector via redirect URI. Mitigations:
exact-match redirect URIs per registration; no substring
matching; validated at both
startAuthCodeandcompleteAuthCode. - Cross-site request forgery on the authorization request.
Mitigations:
stateparameter generated fromEntropySource, stored inAuthCodeState.opaque, checked on completion; PKCE adds a second CSRF-resistant binding. - OIDC
nonceomission. Missingnonceon the ID token allows replay of an ID token from another session. Mitigations:IdTokenPolicy.nonceMustMatchis mandatory for interactive logins;verifyIdTokenrefuses an ID token whosenoncedoes not match the one baked intoAuthCodeState.opaque. - Mis-issued
subclaim. An IdP reuses asubacross tenants or rebinds it. Mitigations: the external subject key includes provider kind, issuer, normalized tenant, and subject; it is neversubalone. Tenant-scoped IdPs (Azure AD per-tenant, Google Workspace) still record the tenant explicitly before hashing. - JWKS flooding. An attacker forces repeated
unknownKeyIdfailures to trigger JWKS refreshes. Mitigations: refresh rate- limited perJwkscap; audit events recorded; repeated failures fail closed rather than refresh-in-loop. - 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.remoteIssuerand inspect returned scopes againstallowedScopes. - Clock skew attacks. Old tokens accepted, new tokens
rejected. Mitigations:
clockSkewSecondsis 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 dimension | Where it lives |
|---|---|
| Access control | AuthorityBroker + CapObject::call (ADF/AEF per X.812); scopes/claims as ABAC input |
| Authentication | OidcIdentityProvider.verifyIdToken; TokenVerifier.verifyAccess |
| Non-repudiation | Signed JWTs + audit records of verifyIdToken, issuance, exchange, revocation |
| Data confidentiality | TLS for every IdP call; encrypted audit payloads where applicable |
| Communication security | TlsClientConfig from the certificates proposal; issuer-pinned roots; HSTS-equivalent pins |
| Data integrity | JWT signature verification against Jwks; kid rotation handled without trust decay |
| Availability | Failure semantics defined for JWKS refresh, device-code expiry, introspection outage |
| Privacy | IdTokenClaims 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::calland 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,
AuthorityBrokerwhen returning scoped caps,TokenVerifierwhen 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/amr →
AuthStrength 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 term | capOS realization |
|---|---|
| Identity provider | OidcIdentityProvider |
| Relying party | Any service holding an OAuthClient cap |
| Credential | Bearer, DPoP-bound, or mTLS-bound AccessToken; IdToken; RefreshToken |
| Enrolment | CredentialStore bootstrap of IdP trust records + subject allow-list |
| Assurance level | AuthStrength (= X.1254 LoA) |
| Attribute authority | IdP via claims; optionally PolicyEngine for derived ABAC attributes |
| Identity binding | Canonical 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
issparameter”, “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.
OAuthClientMetadatais 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 anExternalIdentityBinding.confidentiality_labelandintegrity_labelresolved byLabelAuthorityfrom 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.authStrengthfromacr/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, andIdToken.rawareDeclassifytransitions. 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.tokenExchangeandAccessToken.attenuateareTransferLike; they cannot widen authority. The safety predicate is “issued-token scope ⊆ input-token scope ∩ policy permits” — exactly the wrapper-narrowing rule fromuser-identity-and-policy-proposal.md. The proof obligation is a scope-monotonicity lemma on the server side; capOS verifies the result by comparingTokenClaimsbefore accepting the returned cap.AccessToken.authorizeisWriteLikeagainst 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 — theintegrity(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:
OidcIdentityProviderendpoints declareObserveLikeon metadata calls andReadLikeon verification.OAuthClientendpoints declare the flow classes above and bind the output token’s label tomin(session.label, target_audience.label).TokenVerifierendpoints declareReadLikeand 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
minAuthStrengthon 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.
verify_id_tokentotality and policy soundness. Modeled as a trusted total function. Accepts only well-formed tokens under the configuredIdTokenPolicy(issuer, audience,acr/amr,exp/nbf/iatwith bounded skew,nonce,at_hash/c_hashwhen applicable). ReturnsIdTokenClaimsor a failure reason; never silently downgrades.- PKCE binding. No
completeAuthCode(state, code)succeeds unlessstatewas produced by a priorstartAuthCodeand the PKCE verifier stored inAuthCodeState.opaquehashes to thecode_challengethe IdP recorded forcode. - Nonce binding.
verifyIdTokenaccepts an ID token only ifclaims.nonceequals the nonce stored inAuthCodeState.opaquefor the matchingstate. Missing-nonce ID tokens on interactive logins are rejected. statebinding. The authorization response’sstatematches the one minted fromEntropySourceatstartAuthCode.- Scope monotonicity. Every
TransferLiketoken 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. - JWKS live-set invariant. A token signed under
kid = kis accepted iffkwas present inJwksat some timetwithiat - clockSkew ≤ t ≤ now. Rotation that removeskdoes not retroactively invalidate tokens already verified under it; rotation that addskdoes not accept tokens older than its introduction. - Device-code polling discipline.
pollDeviceCodehonors the IdP-issuedinterval;slow_downresponses monotonically increase the local backoff;expiredanddeniedare terminal. - Refresh rotation invariant. A successful
OAuthClient.refreshthat rotates the refresh token marks the priorRefreshTokencap broken; any subsequent use returnsrevoked(no parallel use of two generations of the same refresh-token family). - Session-creation MAC/MIC predicate.
create_sessionwith an OIDC proof establishesintegrity(session) ≤ integrity(admitting_IdP_trust_record)andconfidentiality(session) ⊑ confidentiality_ceiling(policy_profile, claims). - Broker-outbound MAC/MIC predicate. When the broker binds
an
AccessTokento an outbound request, the call site label satisfiesintegrity(src) ≥ integrity(dst)and the confidentiality flow is permitted.jwtBearerdelegations additionally satisfysupervise_allowed(invoker, delegated).
Additional implicit obligations:
Declassifytransitions (AccessToken.exportRaw,RefreshToken.exportRaw,IdToken.raw) are restricted to trusted subjects and produce audit records with the mandatoryreasonargument.- 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
| Obligation | Primary tool | Notes |
|---|---|---|
1. verify_id_token totality | TLA+ + Kani | TLA+ models the trusted function; Kani proves the Rust impl is total |
| 2. PKCE binding | TLA+ | 3-state machine (started/completed/failed); invariant on state |
| 3. Nonce binding | TLA+ | Joint state with PKCE, same module |
4. state binding | TLA+ | Joint with 2/3; plus Alloy for EntropySource uniqueness |
| 5. Scope monotonicity | Alloy + Prusti | Alloy for the attenuate/exchange graph; Prusti as post-condition |
| 6. JWKS live-set invariant | TLA+ | Temporal property; Apalache if TLC state-space explodes |
| 7. Device-code polling discipline | Z.100 SDL + TLA+ | SDL for state + timer structure; TLA+ for liveness |
| 8. Refresh rotation invariant | TLA+ | Safety + single-generation liveness |
| 9. Session-creation MAC/MIC predicate | Alloy | Extends the hold-edge graph model from formal-mac-mic |
| 10. Broker-outbound MAC/MIC predicate | Alloy | Same model; predicate over outbound endpoint declarations |
| Declassify auditing | Kani | Rust-level: every exportRaw path writes an audit record |
| Endpoint flow declarations | Review gate + Alloy | Enumerate 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/ccsproduces 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.mdtiered tooling plan. - Loom model for the concurrent
Jwksrefresh path: multiple verification requests racing with a refresh triggered byunknownKeyId. 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
minAuthStrengthon 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/Controlin 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:
- User authenticates to capOS via OIDC.
SessionManager.loginverifies the ID token and computessubjectHash = hash(providerKind, iss, tenant, sub). SessionManagerresolvessubjectHashthrough manifest seed admission, a local account-storeExternalIdentityBinding, or an explicit auto-creation rule. The result is a local or pseudonymous principal plus selected policy and resource profiles.SessionManagermints aUserSessionwhosePrincipalInfo.idis the resolved principal and whoseauthStrengthderives fromacr/amr.AuthorityBroker.requestreceives 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.- The broker returns a capability bundle (or denial). The access
token is delivered inside an
ApprovalGrantor a wrapper cap when the caller needs to invoke an external service; the raw bytes remain inside the OAuth service. - For outbound calls to an OAuth-protected resource, the capOS
service holds an
AccessTokencap; it does not see the token string. - For inbound calls, a capOS service configured as an OAuth2
resource server holds a
TokenVerifiercap plus itsAuthorityBrokercap; 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
JwtVerifieroverPublicKeyprimitives from the key proposal using a vetted Rust crate (jsonwebtoken,biscuit, or a purpose-built verifier on top ofrsa/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
OAuthClientwithclientCredentials,refresh, anddeviceCodegrants.- 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,pollDeviceCodereturns a bundle,verifyIdTokensucceeds, a manifest-seeded external admission rule selects policy/resource profiles, and aUserSessionis minted.
Phase 3 — Authorization code + PKCE
- Web text shell gateway redirects to the IdP and consumes the returned code.
startAuthCode/completeAuthCodeintegrated with the gateway’s HTTP listener.- Per-session
nonce,state, and PKCE verifier all live inAuthCodeState.opaque.
Phase 4 — Resource server verification
TokenVerifier.verifyAccesswith 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
WorkloadIdentityFederationwith subject sources for GCP and AWS.- Depends on
InstanceIdentityfrom cloud-metadata and a working outbound TLS client. CloudKmsKeySourcegains a no-baked-credentials unlock path.
Phase 6 — Private key client auth and DPoP
ClientAuthMethod.privateKeyJwtusingJwtSigner.DpopSigner+ConfirmationKind.dpopinTokenVerifier.- RFC 9449 nonces when the resource server supports them.
Phase 7 — mTLS-bound tokens and extended federation
ClientAuthMethod.tlsClientAuthper 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
AuthorityBrokeraccepts anAccessTokenorIdTokenplus scopes as policy input; decisions can return narrowed access tokens alongside narrower caps.- Account-store-backed
ExternalIdentityBindingrecords 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
EncryptedNamespaceunlock viaOidcFederatedKeySource(defined in the key-management proposal) using the user’s current access token as unlock context.
Phase 9 — Local IdP (optional, deferred)
- A
LocalIdentityProvidercap that issues tokens to other capOS services on the same host or fleet, signed by aJwtSignerbacked by aKeyVault-storedPrivateKey. 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. AddsKeySourceKind.oidcFederated,SealPolicy.tokenExchange,KeyPurpose.oauthClientAssertion, andKeyPurpose.oidcIdTokento 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 withPinSetfrom that proposal. mTLS client authentication for OAuth reusesTlsClientConfig. - boot-to-shell-proposal.md —
device code and authorization code grants are
SessionManager.loginmethods.CredentialStorestores 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
ApprovalGrantwrappers, not raw tokens. - user-identity-and-policy-proposal.md
— federated subjects resolve through manifest seed admission,
local account-store
ExternalIdentityBindingrecords, or explicit pseudonymous auto-creation rules; OAuth scopes and OIDC claims are ABAC attributes, not authority;AuthStrengthderives fromacr/amr. - volume-encryption-proposal.md
— OIDC-gated KMS unlock replaces baked IAM credentials; per-user
EncryptedNamespaceunlock usesOidcFederatedKeySource. - cloud-metadata-proposal.md —
InstanceIdentityis the primary subject token source for workload identity federation. The current proposal’s ownSubjectSource.instanceIdentityJwtis 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, andverifyAccessflows 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
- Do we ship our own OIDC RP implementation or wrap an existing
Rust crate?
openidconnect-rs,oauth2-rs, andbiscuitare candidates. The schema boundary is independent; the implementation choice affects TCB size and audit surface. - 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.
- 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.
- 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. - 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.
- How do tokens transfer across capability boundaries? Per-
consumer down-scoped issuance is the default. Should
AccessToken.attenuatebe a kernel-level badge, a userspace wrapper cap, or both depending on whether attenuation is server-side (token exchange) or client-side (scope subset)? - Logout semantics. OIDC end-session endpoints are
optional and frequently inconsistent across IdPs. When
UserSession.logoutfires, what is the best-effort expectation: local session drop + IdP revoke + RP-initiated logout redirect? Document a clear failure mode for each step. - Default audiences for
AuthorityBrokerdecisions. 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 perCapRequest, bundles emitted as multiple broker responses. - 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?
- 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.
- Clock source. OIDC verification depends on a reliable clock.
Before the Timer capability and a cloud attested-time source
exist,
verifyIdTokenmust either fail closed or consume a bootstrap clock from the manifest. Document the first-boot behavior. - Key binding for user sessions. Should a
UserSessionbe 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. - GOST / jurisdictional OIDC. Some deployments mandate
GOST-signed JWTs (GOST R 34.10-2012 on the JWT signature).
Adding the algorithms to
SignatureSchemeis schema-level; validating a GOST-signed discovery document requires matching trust-store support in the certificates proposal. Track, do not block.