Vivienne: Relational Verification of Cryptographic Implementations in WebAssembly

TL;DR

Vivienne is an automated tool that uses relational symbolic execution to verify constant-time properties in WebAssembly cryptographic libraries, effectively detecting timing side-channel vulnerabilities.

Contribution

This paper introduces Vivienne, a novel open-source tool that applies relational symbolic execution with optimizations for WebAssembly to verify cryptographic implementations.

Findings

Vivienne successfully analyzed 57 real-world cryptographic libraries.

It identified constant-time violations in some WebAssembly implementations.

Vivienne is practical for verifying cryptographic code in WebAssembly environments.

Abstract

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.