IAM Axiom Verifier
Un Motor de Inferencia Neuro-Simbólico para Seguridad AWS y FinOps — auditando matemáticamente políticas IAM con LLMs y solvers SMT.
🧪 Disclaimer - Prueba de Concepto (PoC): Prototipo en fase inicial. Es funcional, pero se encuentra en constante evolución. No se recomienda su uso en entornos de producción todavía.
Screenshots
Proceso de auditoría de políticas IAM mediante razonamiento simbólico
Generación de contra-ejemplos matemáticos para brechas de seguridad
Overview
IAM Axiom Verifier es una herramienta de auditoría matemática para entornos AWS. Combina la flexibilidad de los Modelos de Lenguaje Grande (LLMs) para el enrutamiento semántico con el rigor absoluto de los solvers SMT (Verificación Formal) para evaluar las políticas IAM. En lugar de basarse en expresiones regulares, heurísticas o alucinaciones de la IA, este motor traduce el estado de AWS a un sistema de desigualdades y lógica booleana, demostrando matemáticamente los vectores de riesgo. El motor funciona utilizando primero un LLM para analizar semánticamente y entender la intención de las políticas IAM; luego introduce estas intenciones interpretadas en un solver Z3 SMT que verifica formalmente las propiedades de seguridad. Este enfoque híbrido permite obtener tanto la comprensión del lenguaje de la IA como la certeza matemática de la verificación formal — eliminando los falsos positivos producidos por las alucinaciones sin perder la capacidad de razonar sobre relaciones complejas de permisos.
¿Por qué Verificación Formal?
CSPM Tradicional
Patrones con regex. Altas tasas de falsos positivos. No sabe razonar acerca de permisos transitivos.
Herramientas sólo IA
Pueden alucinar hallazgos. Ausencia de garantías matemáticas. Resultados variables.
IAM Axiom Verifier
Hallazgos probados matemáticamente. Cero falsos positivos por diseño. Reproducible cada vez.
Architecture
El motor está estructurado en dos fases: 1. Capa Semántica (LLM Router): Un LLM analiza el JSON en bruto de la política IAM, comprendiendo la intención semántica de cada declaración. Extrae principales, acciones, recursos y condiciones hacia una representación intermedia estructurada. 2. Capa de Verificación Formal (Z3 SMT Solver): La representación estructurada se traduce a restricciones Z3 — un conjunto de afirmaciones matemáticas sobre el sistema de permisos. El solver explora entonces el espacio de permisos completo para detectar violaciones de seguridad y vectores de riesgo demostrables. Esta separación asegura que la ambigüedad lingüística sea manejada por el LLM (el cual es experto en entendimiento de lenguaje natural), garantizando la corrección lógica mediante el solver SMT (quien provee las pruebas matemáticas).