🔐 skyauth

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, Kani bounded model checking with 25 mandatory anti-vacuity reachability tags enforced across 5 proof harnesses, and pure-Rust executable state transition models.
• Confidential Client Support: Automatic client_secret inclusion in PAR, code exchange, and refresh requests (RFC 6749 § 2.3.1 client_secret_post); extensible credential hook via execute_par_request_with_credentials.
• 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.2"

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 src/verification/verus_contracts.rs using SMT solving (Z3) to prove 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 25 mandatory anti-vacuity reachability tags (kani::cover! / [AntiVacuityCoverage]) that the deterministic test suite must reach.
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:

• MIT License (LICENSE-MIT)
• Apache License, Version 2.0 (LICENSE-APACHE)