skyauth 0.3.4

High-assurance, formally verified OAuth 2.1 and RFC 9449 DPoP authentication engine for the AT Protocol (Bluesky)
Documentation

🔐 skyauth

crates.io docs.rs License Safety Guard

Pure Safe Rust (#![forbid(unsafe_code)]), Zero-Panic AT Protocol OAuth 2.1 Client with RFC 9449 DPoP, RFC 9126 PAR, RFC 7636 PKCE, & Formal Mathematical Verification

🌟 Highlights

  • 100% Pure Safe Rust: #![forbid(unsafe_code)] enforced crate-wide with 0 unsafe blocks and zero production panics.
  • RFC 9449 DPoP: Ephemeral ECDSA P-256 key generation, RFC 7517 JWK formatting, RFC 7638 JWK Thumbprints (jkt), signed dpop+jwt proof tokens, access token hash (ath), and transparent auto-nonce retry negotiation.
  • RFC 9126 PAR (Pushed Authorization Requests): Direct back-channel pushing of authorization parameters with signed DPoP headers.
  • RFC 7636 PKCE: High-entropy 43-character Base64URL verifier generation, SHA-256 S256 challenge derivation, and constant-time verification.
  • Decentralized Identity Discovery: Handle normalization, DNS TXT resolution (_atproto.<handle>), HTTPS fallback (/.well-known/atproto-did), DID resolution (did:plc, did:web), and bidirectional alsoKnownAs verification.
  • RFC 8414 & RFC 9728 Discovery: Protected Resource Metadata and Authorization Server Metadata discovery with automatic OIDC fallback.
  • Strict SSRF & DNS Rebinding Security: Full IP boundary filtering blocking RFC 1918 private IPs, loopback, link-local, cloud metadata (169.254.169.254), IPv6 ULA, and DNS socket pinning.
  • 64-Shard Partitioned State Store: Lock-free scaling state storage across 64 independent RwLock shards with atomic single-use state consumption ([OAuthStore::take_state]) and drift-free background TTL pruning.
  • Web Framework Integrations: Ready-to-use extractors, response generators, and middleware for Axum 0.7, Actix-Web 4, and Tower.
  • Formal Mathematical Verification: Verified using Verus deductive proofs (69 obligations across two layers, including kernel-bound contracts on the shipped IP-classification source), Kani bounded model checking with 57 machine-inventoried anti-vacuity reachability tags enforced across 8 symbolic proof harnesses (SSRF IPv4/IPv6 classifiers, constant-time equality, PKCE byte-level validator refinement, DPoP jti admission bound, DPoP htu normalization invariants, PKCE S256 verifier bounds, state consumption), and pure-Rust executable state transition models. Tag inventory and counts are machine-checked by tests/verification_tag_inventory_tests.rs; CI fails on any unsatisfied kani::cover! property.
  • Public-Client Profile (strict): skyauth implements only the public-client token_endpoint_auth_method: "none" path — the ATProto OAuth profile has no shared client_secret (confidential clients authenticate with private_key_jwt, planned for a future release). Static-secret support was removed as a credential-disclosure hazard (review H1).
  • Proxied-Deployment DPoP: with_htu_override on the Tower layer reconstructs absolute DPoP target URIs for servers behind reverse proxies receiving origin-form request targets.
  • Hardened SSRF Boundary: Deprecated 6to4 (2002::/16, with embedded-IPv4 re-evaluation) and Teredo (2001::/32) tunneling prefixes are blocked, mirrored in the formal verification models; test mode (allow_insecure_localhost) only exempts explicit loopback targets, never metadata/internal hosts.
  • Single-Use Server Nonces: Optional strict RFC 9449 § 8 nonce consumption (InMemoryServerNonceSource::with_single_use).
  • Resource-Server Token Validation: JwtAccessTokenValidator (RFC 9068 at+jwt verification with fail-closed issuer/audience matching and cnf.jkt DPoP binding) and an in-memory registry, with a Tower middleware layer enforcing DPoP proof verification, replay rejection, and server nonce challenges.
  • XRPC Client Hardening: Lexicon NSID grammar validation on send_xrpc_request, DPoP-signed requests with automatic nonce retry, and bounded response bodies.
  • Dynamic Schema Invariants: Bundled official ATProto Lexicons and RFC schemas with continuous automated upstream drift detection.

🚀 Quick Start

Add skyauth to your Cargo.toml:

[dependencies]
skyauth = "0.3"

1. DPoP Proof Generation & Verification

use skyauth::dpop::{compute_access_token_hash, DPoPKey, DPoPVerifier};
use skyauth::pkce::PkcePair;

fn main() -> Result<(), Box<dyn std::error::Error>> {
    // 1. Generate PKCE code challenge
    let pkce = PkcePair::generate();
    assert_eq!(pkce.verifier.len(), 43);

    // 2. Generate ephemeral DPoP keypair
    let dpop_key = DPoPKey::generate();
    let _jkt = dpop_key.jwk_thumbprint();

    // 3. Create a DPoP proof for an outgoing token request
    let proof = dpop_key.create_proof(
        "POST",
        "https://pds.example.com/oauth/token",
        None,
        None,
    )?;

    // 4. Verify inbound DPoP proof
    let verifier = DPoPVerifier::new();
    let (claims, _jwk) = verifier.verify_proof(
        &proof,
        "POST",
        "https://pds.example.com/oauth/token",
        None,
        None,
        None,
    )?;
    assert_eq!(claims.htm, "POST");

    Ok(())
}

2. Full OAuth Client Lifecycle

use skyauth::client::{AtprotoOAuthClient, CallbackParams, OAuthClientMetadata};
use skyauth::store::OAuthStateStore;
use std::sync::Arc;
use std::time::Duration;

#[tokio::main]
async fn main() -> Result<(), Box<dyn std::error::Error>> {
    // 1. Configure OAuth Client Metadata
    let metadata = OAuthClientMetadata::new(
        "https://my-app.example.com/client-metadata.json",
        "https://my-app.example.com/oauth/callback",
    )
    .with_client_name("My ATProto App")
    .with_scope("atproto transition:generic");

    // 2. Instantiate high-level client with 64-shard concurrent state store
    let state_store = Arc::new(OAuthStateStore::new(Duration::from_secs(300)));
    let client = AtprotoOAuthClient::builder()
        .metadata(metadata)
        .state_store(state_store)
        .state_ttl(Duration::from_secs(300))
        .build()?;

    // 3. Initiate login with handle or DID (pushes PAR, generates PKCE, registers state)
    let auth_req = client.authorize("alice.bsky.social").await?;
    println!("Redirect user to: {}", auth_req.authorization_url);

    // 4. Handle incoming callback after user authorization (single-use consumed)
    let callback_params = CallbackParams::new("auth_code_from_query", &auth_req.state)
        .with_iss("https://bsky.social");
    let session = client.handle_callback(&callback_params).await?;
    println!("Authenticated user DID: {}", session.sub);

    // 5. Execute authenticated XRPC request
    let response = client
        .send_xrpc_request(&session, "com.atproto.repo.describeRepo", &[])
        .await?;
    println!("XRPC response status: {}", response.status());

    Ok(())
}

🛡️ Formal Verification & Mathematical Invariants

skyauth incorporates a multi-layered formal verification hierarchy:

  1. Verus Deductive Contracts (verus!): Deductive mathematical proofs in two layers — the standalone specification layer (src/verification/verus_contracts.rs, 21 obligations) and the kernel-bound layer (src/verification/verus_kernels.rs, 48 obligations), whose contracts are proven over the shipped kernel source in src/kernels/ via #[path] inclusion: full IPv4/IPv6 restricted-range coverage theorems (RFC 1918, loopback, cloud metadata, CGNAT, Teredo, 6to4 embedded-IPv4 parity, mapped↔IPv4 reduction, ULA, link-local, multicast, documentation, plus public non-vacuity witnesses). SMT solving (Z3) verifies single-use state transition safety, terminality, SSRF IP range isolation, and PKCE bounds.
  2. Kani Bounded Model Checking (kani::proof): Exhaustive symbolic proof harnesses in src/verification/kani_harnesses.rs using symbolic kani::any() and kani::assume() inputs with 57 mandatory anti-vacuity reachability tags (kani::cover! / [AntiVacuityCoverage]) that the deterministic test suite must reach. The tag inventory is machine-checked against the proof source by tests/verification_tag_inventory_tests.rs (bidirectional exact match), and CI fails the build on any UNSATISFIABLE cover property.
  3. Executable Formal State Models: High-assurance transition models in src/verification/formal_models.rs tested against property fuzzing and concurrent interleavings.

🧪 Running Tests, CI & Formal Proofs

# Run unit, integration, and RFC vector test suites
cargo test --all-targets --all-features

# Verify strict clippy compliance (0 warnings)
cargo clippy --all-targets --all-features -- -D warnings

# Verify specification drift against upstream canonical Lexicons & RFC schemas
bash scripts/sync_specs.sh --verify

# Run Kani bounded model checking proof harnesses
cargo kani --harness proof_

# Run Verus deductive formal verification proofs
bash scripts/run_verus.sh

📄 License

Dual-licensed under either:

Packaging Note

skyauth ships with empty default features (default = []): the core client library compiles without any web-framework dependency. Framework integrations are opt-in (axum, actix, tower). The tokio dependency is minimal (runtime, net, time, sync, macros) rather than full.