# 🔐 `skyauth`
[](https://crates.io/crates/skyauth)
[](https://docs.rs/skyauth)
[](LICENSE-MIT)
[](src/lib.rs)
> **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`:
```toml
[dependencies]
skyauth = "0.3"
```
### 1. DPoP Proof Generation & Verification
```rust
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
```rust
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`](src/verification/verus_contracts.rs), 21 obligations) and the **kernel-bound layer** ([`src/verification/verus_kernels.rs`](src/verification/verus_kernels.rs), 48 obligations), whose contracts are proven over the *shipped* kernel source in [`src/kernels/`](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`](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`](src/verification/formal_models.rs) tested against property fuzzing and concurrent interleavings.
---
## 🧪 Running Tests, CI & Formal Proofs
```bash
# 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](LICENSE-MIT))
- **Apache License, Version 2.0** ([LICENSE-APACHE](LICENSE-APACHE))
---
## 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`.