Maschinell geprüfte Sicherheit digitaler Systeme am Barkhausen Institut
Die Forschung am Barkhausen Institut zielt darauf ab, digitale Systeme nachweislich sicherer und vertrauenswürdiger zu gestaltet. Mit dem Paper „Formally-verified Security against Forgery of Remote Attestation using SSProve“ hat die Forschungsgruppe Verified System Design Automation einen großen Beitrag dazu geleistet.
Worum geht es in dem Paper?
Remote Attestation (RA) ist ein grundlegendes Protokoll, das überprüft, ob ein Gerät – wie ein Laptop, Cloud-Server oder IoT-Sensor – manipuliert wurde. Es basiert auf digitalen Signaturen: Das Gerät erstellt einen signierten Bericht über seinen internen Zustand, den eine entfernte Instanz (remote verifier) geprüft werden kann. Trotz seiner weiten Verbreitung fehlen RA bisher strenge, maschinell geprüfte Nachweise für die kryptografische Sicherheit.
In unserem Paper haben wir die erste maschinell geprüfte kryptografische Verifikation von digitalen Signaturen und Remote Attestation entwickelt. Wir zeigen, dass die Sicherheit von RA der Sicherheit der zugrunde liegenden digitalen Signaturen entspricht. Die Ergebnisse wurden im SSProve-Framework unter Verwendung des Rocq Prover (ehemals Coq) formalisiert und bewiesen.
Was genau wurde entwickelt?
Wir haben digitale Signaturen und RA im SSProve-Framework definiert, indem kryptografische Operationen und Zustandsübergänge mathematisch beschrieben wurden. Anschließend haben wir bewiesen, dass das RA-Protokoll sicher ist, wenn das zugrunde liegende digitale Signaturschema sicher ist (im starken kryptografischen Sinne der Unfälschbarkeit). Unsere Entwicklung ist ein erster grundlegender Schritt für die formale Verifikation von RA und dient als Grundlage für reale Anwendungsfälle.
Die gesamte Formalisierung wurde mit SSProve, einem auf Rocq Prover basierenden Framework für zustandsbehaftete und modulare kryptografische Beweise, durchgeführt. Unsere Beweise stehen in einem Open-Source-Repository zur Verfügung.
Was bedeutet das für uns?
Diese Arbeit stärkt die Mission des Barkhausen Instituts, vertrauenswürdige digitale Systeme durch formale Verifikation zu entwickeln. Durch den Nachweis der RA-Sicherheit mittels maschinell geprüfter Beweise geben wir einem weit verbreiteten, bislang jedoch nicht verifizierten kryptographischen Mechanismus eine solide Grundlage. Dies fördert das Ziel der Gruppe Verified System Design Automation, Vertrauenswürdigkeit durch Design zu erreichen – von der Theorie bis hin zu realen Systemen.
Wo können wir mehr erfahren?
Formally-verified Security against Forgery of Remote Attestation using SSProve
Sara Zain, Barkhausen Institut; Jannik Mähn, Stefan Köpsell, Barkhausen Institut; and Sebastian Ertel, Barkhausen Institut.
Link zum Paper: arxiv.org/pdf/2502.17653