VeriSec: Automated Verification of Security-Critical Software

Im Rahmen dieser Industrial Fellowship wurde ein Ansatz entwickelt, Implementierungen von kryptographischen Protokollen gegenüber ihren Spezifikationen zu verifizieren, die wiederum gegenüber Sicherheitsanforderungen verifiziert werden, sodass die Verifikationskette eine Verifikation der Implementierung gegenüber den Sicherheitsanforderungen ergibt. Im Rahmen der Industrial Fellowship wurden in diesem Zusammenhang insbesondere kompositionale Techniken für Sicherheitsverifikation entwickelt. Der Ansatz wurde auf existierende Implementierungen von kryptographischen Protokollen angewendet.