Vivienne: Relational Verification of Cryptographic Implementations in WebAssembly
This provides a practical solution for verifying cryptographic implementations in WebAssembly against timing attacks, addressing a security-critical issue for developers and users of WebAssembly-based systems.
The paper tackled the problem of timing side channels in WebAssembly cryptographic programs by developing Vivienne, a tool using relational symbolic execution for automatic constant-time violation analysis, which successfully evaluated 57 real-world implementations including an unverified HACL* library.
This paper explores the use of relational symbolic execution to counter timing side channels in WebAssembly programs. We design and implement Vivienne, an open-source tool to automatically analyze WebAssembly cryptographic libraries for constant-time violations. Our approach features various optimizations that leverage the structure of WebAssembly and automated theorem provers, including support for loops via relational invariants. We evaluate Vivienne on 57 real-world cryptographic implementations, including a previously unverified implementation of the HACL* library in WebAssembly. The results indicate that Vivienne is a practical solution for constant-time analysis of cryptographic libraries in WebAssembly.