Confirming Safety of IAM Specifications and their OSS Implementations: Keycloak as a Case Study
Talkat Open Source Summit Europe 2025 · on Monday, 2025-08-25· at 15:35· Elicium 2B (Elicium Level 1)·
summary
Describes concrete steps and results for hardening IAM: formal analysis with model checkers and SMT solvers found and helped fix vulnerabilities in OAuth 2.0, OpenID Connect and FAPI specs; conformance suites from the OpenID Foundation and FAPI are run automatically via an in‑project test runner so every patch, minor and micro release is validated; vulnerability tooling stack includes CodeQL, Dependabot, Trivy and Snyk; project maintains an OpenSSF score ~9.23 and publishes security advisories and external audit reports.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:06IAM vulnerabilities types
- 4:49Formal security analysis
- 11:53Formal methods challenges
- 12:14Performance testing
- 19:12Vulnerability testing for IAM OSS
- 27:35Keycloak case study
- 28:41Formal analysis of specs
- 33:23Keycloak performance testing
- 38:10Keycloak vulnerability tools
- 38:31Keycloak security maintenance
- 41:09Summary
related talks
32mModern And Secure IAM For Modern Applications
31mHigh-level API Security
27mSecurity Issues In OAuth/OIDC Implementations
21mVetting Single Sign-On SDK Implementations via Symbolic Reasoning
30mInsecurity protocols: an overview of modern authentication
09mNavigating the Identity Abyss in the AI‑Native Era
17mAPI Security Simplified: Practical Tips & Tools
01h 02mOpenID Connect & OAuth 2.0 – Security Best Practices