When Obfuscations Preserve Constant-Time

This chapter delves into the world of obfuscating compilers and their role in enhancing the security of cryptographic software. The primary focus is on understanding whether obfuscation techniques preserve the constant-time property, a critical security feature that prevents timing attacks. The chapter introduces a sufficient condition for checking the preservation of this property and applies it to various obfuscation techniques, including control flow flattening, mixed boolean-arithmetic transformations, and opaque predicate transformations. Through detailed case studies, the chapter demonstrates how these techniques can be validated to ensure they do not introduce new vulnerabilities. The analysis is conducted within the Jasmin programming language framework, which is designed for high-assurance and high-speed cryptography. The chapter also explores the concept of translation validation, a method for assessing the preservation of constant-time properties on a case-by-case basis. By examining real-world obfuscating compilers and their components, the chapter provides insights into how these tools can be improved to better protect cryptographic software. The findings highlight the importance of careful consideration when applying obfuscation techniques to ensure they do not compromise the security of the software they are intended to protect.