C-Verifier: Understanding and Formally Verifying Cross-Service Flaws in AWS Cognito

Managed cloud-identity services issue short-lived credentials so that mobile and web clients can access storage, database, and serverless APIs without passing through application servers. These services are layered on top of a security-token engine and an account-wide policy system, yet prior work has examined each layer in isolation. We present the first end-to-end analysis of this multi-plane workflow, using Amazon Cognito as a representative case. Treating Cognito, the Security Token Service and IAM as a single security graph, we (i) provide the first in-depth security analysis of session-bypass risk and (ii) uncover two additional design flaws that allow users to exploit overly permissive or divergent trust policies and to assume “hanging” roles left behind after reconfiguration. A crawl of $\mathbf{8 4 4}$ Cognito-backed Android apps reveals these flaws in 179 deployments, affecting at least 1.7 million users. To detect such drift automatically, we build C-Verifier, a tool that converts an account snapshot into Satisfiability Modulo Theories formulas spanning all three control planes and checks five security properties. C-Verifier yields precise counter-examples, outperforms four state-of-the-art tools, and analyzes 400 identity pools with 1,400 roles in under 40 s. We release both the tool and a curated benchmark, Cognito Configuration Bench, to facilitate reproducible cross-service policy research.