28. November 2025. Die Forschung am Barkhausen Institut konzentriert sich darauf, digitale Systeme nachweislich sicherer und vertrauenswürdiger zu machen. Mit dem Paper „Formally-verified Security against Forgery of Remote Attestation using SSProve“ hat unsere Forschungsgruppe Verified System Design Automation einen wichtigen Beitrag zu diesem Ziel geleistet.
Kategorien
Schlagworte
Remote Attestation (RA) ist ein grundlegendes Protokoll, mit dem überprüft wird, ob ein Gerät – wie beispielsweise ein Laptop, ein Cloud-Server oder ein IoT-Sensor – manipuliert wurde. Es basiert auf digitalen Signaturen: Das Gerät generiert einen signierten Bericht über seinen internen Zustand, den ein Remote-Verifizierer überprüfen kann. Trotz seiner weit verbreiteten Nutzung fehlen RA strenge, maschinell überprüfte Nachweise für seine kryptografische Sicherheit.
In unserem Artikel haben wir die erste maschinell überprüfte kryptografische Verifizierung von digitalen Signaturen und Remote Attestation entwickelt. Wir zeigen, dass die Sicherheit von RA der Sicherheit der zugrunde liegenden digitalen Signaturen entspricht. Wir haben die Ergebnisse im SSProve-Framework mit Rocq Prover (ehemals Coq) formalisiert und bewiesen.
Flussdiagramm, das die modulare Spezifikation von RA unter Verwendung der SSProve-Paketzusammensetzung mit beschrifteten Kästchen und Pfeilen zeigt, die den Datenfluss und die Funktionen anzeigen.
Wir haben digitale Signaturen und RA innerhalb des SSProve-Frameworks definiert, wobei kryptografische Operationen und Zustandsübergänge durch mathematische Überlegungen spezifiziert wurden. Anschließend haben wir bewiesen, dass das RA-Protokoll ebenfalls sicher ist, wenn das zugrunde liegende digitale Signaturschema sicher ist (im starken, kryptografischen Sinne der Unfälschbarkeit). Unsere Entwicklung stellt den ersten Schritt für RA dar und kann dazu dienen, Anwendungsfälle für die reale Welt zu erstellen.
Die gesamte formale Entwicklung wurde mit SSProve durchgeführt, einem auf Rocq Prover basierenden Framework für zustandsbehaftete und modulare kryptografische Beweise. Unsere Beweisentwicklungen sind als Open-Source-Repository verfügbar.
Diese Arbeit stärkt die Mission des Barkhausen Instituts, durch formale Verifizierung vertrauenswürdige digitale Systeme aufzubauen. Durch die Bereitstellung eines maschinell überprüften Nachweises der RA-Sicherheit geben wir einem weit verbreiteten, aber bisher nicht verifizierten kryptografischen Mechanismus eine solide Grundlage. Dies bringt das Ziel der Verified System Design Automation-Gruppe, Vertrauenswürdigkeit durch Design, von der Theorie bis hin zu realen Systemen, voran.
Formal verifizierte Sicherheit gegen Fälschungen von Remote-Attestierungen mit SSProve
Sara Zain, Barkhausen Institut; Jannik Mähn, Stefan Köpsell, Barkhausen Institut; und Sebastian Ertel, Barkhausen Institut.
Link zum Paper: https://arxiv.org/pdf/2502.17653
– – – – –
Foto: Sara Zain
