The authors built an automated toolchain that extracts symbolic models from real binaries of cryptographic protocols and analyzes them for constant-time and speculative side-channel leaks, demonstrated on WhatsApp and e-passport implementations.
Proving noninterference and functional correctness using traces
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
years
2025 2verdicts
UNVERDICTED 2representative citing papers
TREBL is a sound and relatively complete temporal logic fragment for expressing and proving liveness conditions in Event-B machines under sufficient refinement.
citing papers explorer
-
Automated Side-Channel Analysis of Cryptographic Protocol Implementations
The authors built an automated toolchain that extracts symbolic models from real binaries of cryptographic protocols and analyzes them for constant-time and speculative side-channel leaks, demonstrated on WhatsApp and e-passport implementations.
-
TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory
TREBL is a sound and relatively complete temporal logic fragment for expressing and proving liveness conditions in Event-B machines under sufficient refinement.