🔐 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 contracts) and Kani (bounded model checking with 36 mandatory anti-vacuity reachability checks).
• Dynamic Schema Invariants: Bundled official ATProto Lexicons and RFC schemas with continuous automated upstream drift detection.

🚀 Quick Start

Add atproto-oauth to your Cargo.toml:

[dependencies]
atproto-oauth = "0.1"

1. DPoP Proof Generation & Verification

use skyauth::dpop::{DPoPKey, DPoPVerifier, compute_access_token_hash};
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 a 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, OAuthClientMetadata};
use skyauth::store::OAuthStateStore;
use std::sync::Arc;

#[tokio::main]
async fn main() -> Result<(), Box<dyn std::error::Error>> {
    let metadata = OAuthClientMetadata {
        client_id: "https://my-app.example.com/client-metadata.json".to_string(),
        client_name: Some("My ATProto App".to_string()),
        client_uri: Some("https://my-app.example.com".to_string()),
        redirect_uris: vec!["https://my-app.example.com/oauth/callback".to_string()],
        grant_types: vec!["authorization_code".to_string(), "refresh_token".to_string()],
        response_types: vec!["code".to_string()],
        scope: "atproto transition:generic".to_string(),
        token_endpoint_auth_method: "none".to_string(),
        dpop_bound_access_tokens: true,
        jwks_uri: None,
    };

    let state_store = Arc::new(OAuthStateStore::new());
    let client = AtprotoOAuthClient::builder()
        .metadata(metadata)
        .state_store(state_store)
        .build()?;

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

    Ok(())
}

🛡️ Formal Verification & Mathematical Invariants

skyauth incorporates a multi-layered formal verification hierarchy to eliminate security vulnerabilities:

1. Verus Deductive Contracts (verus!): Mathematical proofs for session state transitions, constant-time comparisons, and PKCE deterministic bounds.
2. Kani Bounded Model Checking (kani::proof): 5 exhaustive verification harnesses checking all symbolic byte inputs.
3. Anti-Vacuity Coverage (kani::cover!): 36 mandatory reachability checks ensuring harnesses actually exercise functional code paths.

🧪 Running Tests & Formal Proofs

# Run unit, integration, and RFC vector test suites (730+ tests)
cargo test --all-targets --all-features

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

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

📄 License

Dual-licensed under either:

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