Hamed Nemati, a WASP assistant professor at KTH in the Division of Network and Systems Engineering, was awarded a $60,000 USD Amazon Research Award within the category of Automated Reasoning.
“I am excited about pushing the boundaries of automated verification to ensure cryptographic software is secure against side-channel attacks, even at the binary level,” says Hamed.
Verifying compiled binary code for safety
Hamed’s project aims to make cryptographic software more secure by protecting it from hardware-related leaks, like those that use timing or speculative execution tricks. The goal is to create an automated tool that can check if the compiled code is safe from these vulnerabilities. Using the HolBA framework, the goal is to accurately verify that cryptographic software, like OpenSSL, is protected against these types of hardware attacks.
“With our work on the HolBA and Scam-V frameworks, we aim to provide formally verified guarantees that these defenses hold up in real-world conditions,” says Nameti. “It is a step toward making trustworthy software verification both rigorous and practical.”
Published: April 25th, 2025