I moderni cluster Kubernetes sono caratterizzati da un numero elevato di oggetti e da interazioni semantiche non immediatamente evidenti, in cui la combinazione di policy RBAC, namespace, binding, gerarchie strutturali e NetworkPolicy rende difficile determinare con precisione i permessi effettivamente concessi ai soggetti e le comunicazioni di rete realmente consentite tra i Pod. La verifica manuale di tali configurazioni risulta perciò complessa, soggetta a errori e poco scalabile in contesti reali. La presente tesi propone la progettazione e l'implementazione di un sistema per l'analisi e la verifica automatica delle configurazioni di sicurezza Kubernetes basato su tecniche SMT (Satisfiability Modulo Theories) e sul solver Z3.