Leakage Models: A Leaky Abstraction in Cryptographic Software Verification

Explore a groundbreaking proposal to revolutionize the verification of timing properties in cryptographic software during this 12-minute conference talk from ACM SIGPLAN. Delve into the innovative approach presented by researchers from MIT and NYU, who suggest abandoning traditional leakage models in favor of direct verification against hardware implementations at the gate level. Discover the results of their early experiments, which successfully verified constant-time execution of Ed25519 signature computations on a 7-stage pipelined processor. Gain insights into the significant open challenges that lie ahead, including scaling up the tool for modern out-of-order speculative cores and extending the methodology to analyze library code beyond whole application contexts.