该论文针对 AWS Cognito 服务中跨服务缺陷的识别与形式化验证问题展开研究。AWS Cognito 作为一项用户身份与访问管理服务，常与 API Gateway、Lambda 等其他 AWS 服务集成，这种跨服务组合可能引入安全漏洞。作者提出了一种名为 C-Verifier 的形式化验证框架，能够自动建模 AWS Cognito 的配置及其与其他服务的交互行为，通过符号模型检测技术发现潜在的跨服务逻辑缺陷，例如权限提升、未授权访问等。该方法首先将 AWS 资源配置抽象为形式化模型，然后利用 SMT 求解器对安全属性进行验证。实验结果表明，C-Verifier 在多个真实世界的 AWS 架构中成功识别出未知的跨服务漏洞，并提供了形式化证明。该工作的主要贡献在于：首次将形式化验证系统性地应用于 AWS Cognito 的跨服务场景，提出了可扩展的建模方法，并实际发现了若干高危缺陷。适合云安全研究人员、AWS 服务开发者以及安全工程师阅读。