Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code
Die Studie „Broken by Default" widerlegt durch formale Verifikation mit dem Z3-Solver, dass alle getesteten KI-Code-Assistenten in sicherheitskritischen Anwendungen systematisch anfällig für Ausnutzungen sind, wobei 55,8 % der generierten Artefakte mathematisch beweisbare Schwachstellen aufweisen, die von herkömmlichen Sicherheitstools übersehen werden.