Automated Side-Channel Analysis of Cryptographic Protocol Implementations
ACM CCS 2026
Zusammenfassung lesenZusammenfassung ausblenden
Die formale Verifikation kryptografischer Protokolle stützt sich üblicherweise auf symbolische Modelle, die kompilierten Code und mikroarchitekturelle Seitenkanäle wegabstrahieren. Zwischen verifizierten Spezifikationen und ausgelieferten Programmen bleibt so eine Lücke. Wir stellen eine Werkzeugkette vor, die protokollrelevante Modelle aus realen Binärdateien extrahiert und sie unter expliziten Leakage-Contracts für Constant-Time- und Spectre-PHT-artige spekulative Beobachtungen analysiert. Ausgehend von einem ausgewählten Bereich der Binärdatei heben wir Maschinencode in eine Zwischendarstellung, instrumentieren ihn mit Leakage-Contracts, führen ihn symbolisch aus, um Ereignis- und Beobachtungsspuren zu gewinnen, und übersetzen diese Spuren nach Sapic+ zur Analyse mit Tamarin, ProVerif und DeepSec. Als Fallstudien extrahieren wir Modelle der Sitzungsverwaltung und der Double-Ratchet-Komponenten von WhatsApp Desktop aus dessen Binärdatei und analysieren Forward Secrecy sowie Post-Compromise Security unter einem State-Cloning-Kompromiss. Für die Seitenkanalanalyse untersuchen wir das in elektronischen Reisepässen eingesetzte Protokoll Basic Access Control (BAC) sowie den Sitzungsaufbau von WhatsApp. Unter unseren Beobachtungsmodellen identifizieren wir einen Instruktions-Cache-Seitenkanal in WhatsApp Desktop, der Rückschlüsse auf den Sozialgraphen erlaubt, und reproduzieren bekannte Unverkettbarkeitsprobleme in BAC unter mikroarchitektureller Beobachtung.
@misc{nasrabadi2026sidechannel,
title = {Automated Side-Channel Analysis of Cryptographic
Protocol Implementations},
author = {Nasrabadi, Faezeh and K{\"u}nnemann, Robert and Nemati, Hamed},
year = {2026},
eprint = {2511.11385},
archivePrefix= {arXiv},
primaryClass = {cs.CR},
url = {https://arxiv.org/abs/2511.11385}
}