Am 27. und 28. März findet das EuroProofNet-Tutorial über ‚Usable Formal Methods for Security of Systems‘ (Anwendbare formale Methoden zur Sicherheit von Systemen) an der TU Dresden statt. Das BI nimmt mit folgenden zwei Beiträgen teil:

Unser Wissenschaftler Dr.-Ing. Carsten Weinhold wird über ein neuartiges Kommunikationsprotokoll sprechen, das eine sichere Verbindung zu einem entfernten Gerät herstellt und gleichzeitig überprüft, ob die erwartete Software auf diesem Gerät läuft. Zu diesem Zweck haben Carsten und sein Kollege Dr.-Ing. Michael Roitzsch die vorhandenen Techniken Transport Layer Security (TLS) und Remote Attestation so kombiniert, dass sich ihre Sicherheitseigenschaften ergänzen. Beide sind der Meinung, dass keine der in verwandten Arbeiten vorgeschlagenen Kombinationen dieser Protokolle dies erreicht, und möchten diese Idee mit den anderen Teilnehmern diskutieren. Der Vortrag geht auch darauf ein, wie sich diese Forschung in das umfassendere Konzept eines modularen Vertrauensankers einfügt, der die Anwendungen schützt, die dieses Protokoll verwenden.

BI-Wissenschaftler Jannik Mähn untersucht das gerade beschriebene Kommunikationsprotokoll aus formaler Perspektive. Das bedeutet, er und sein Kollege Sebastian Ertel haben das Protokoll und seine Eigenschaften in das SSProve-Tool übersetzt, das auf dem ‚Coq‘ Theorem-Prover basiert. Anschließend führte er die Beweise in SSProve durch, die zuvor manuell mit Papier und Bleistift durchgeführt worden waren. Auf diese Weise konnte er die Sicherheitseigenschaften dieses Protokolls mit computergestützter Unterstützung so nachweisen, dass Fehlerquellen und Fehler weitestgehend vermieden werden. Dadurch kann ein höheres Sicherheitsniveau für das Protokoll garantiert werden.

Weitere Informationen finden Sie unter: europroofnet.github.io/wg3-dresden24/