Towards Automated Detection of Single-Trace Side-Channel Vulnerabilities in Constant-Time Cryptographic Code

TL;DR

This paper introduces Pascal, an automated tool that uses symbolic register analysis to detect potential power side-channel vulnerabilities in constant-time cryptographic code, aiding cryptographers in securing implementations.

Contribution

The work presents a novel symbolic register analysis technique for binary code, enabling high-precision detection of power side-channel vulnerabilities in constant-time cryptographic algorithms.

Findings

Pascal successfully identified dozens of known vulnerabilities.

The tool automates the detection process, reducing manual effort.

Evaluation on post-quantum algorithms demonstrates effectiveness.

Abstract

Although cryptographic algorithms may be mathematically secure, it is often possible to leak secret information from the implementation of the algorithms. Timing and power side-channel vulnerabilities are some of the most widely considered threats to cryptographic algorithm implementations. Timing vulnerabilities may be easier to detect and exploit, and all high-quality cryptographic code today should be written in constant-time style. However, this does not prevent power side-channels from existing. With constant time code, potential attackers can resort to power side-channel attacks to try leaking secrets. Detecting potential power side-channel vulnerabilities is a tedious task, as it requires analyzing code at the assembly level and needs reasoning about which instructions could be leaking information based on their operands and their values. To help make the process of detecting potential power side-channel vulnerabilities easier for cryptographers, this work presents Pascal: Power Analysis Side Channel Attack Locator, a tool that introduces novel symbolic register analysis techniques for binary analysis of constant-time cryptographic algorithms, and verifies locations of potential power side-channel vulnerabilities with high precision. Pascal is evaluated on a number of implementations of post-quantum cryptographic algorithms, and it is able to find dozens of previously reported single-trace power side-channel vulnerabilities in these algorithms, all in an automated manner.