I am pursuing my PhD in Computer Science at Yale University under the guidance of Ruzica Piskac and Jakub Szefer. My recent research focuses on the automated inference of nonlinear relational properties, equalities, inequalities, and random self-reducible properties from programs by integrating machine learning with formal methods.
I am an Applied Scientist Intern at the Automated Reasoning Group of Amazon Web Services (AWS) mentored by Rupak Majumdar. I am developing tools for model-based testing, conformance checking, and fuzzing of distributed networked systems.
I have worked on verifying the side-channel insecurity of low-level Post-Quantum Cryptographic (PQC) code (EuroS&P 2023). I explored reverse engineering quantum circuits from power side-channel traces (CHES 2024, CCS 2023), and contributed to a technique that detects quantum computer viruses (HOST 2023). Additionally, I explored automated analysis of non-functional behaviors of intermittent programs (TECS 2023), and surveyed security verification techniques (JETC 2023).
PhD in Computer Science, 2025
Yale University, CT, US
MSc, MPhil in Computer Science
Yale University, CT, US
MSc in Information Technologies
Ege University, Izmir, TR
BSc in Computer Science
Dokuz Eylul University, Izmir, TR
This work shows the first exploration and study of power-based side-channel attacks in quantum computers. The explored attacks could be used to recover information about the control pulses sent to these computers. By analyzing these control pulses, attackers can reverse-engineer the equivalent gate-level description of the circuits, and the algorithms being run, or data hard-coded into the circuits.
Pascal is a tool that introduces novel symbolic register analysis techniques for constant-time low-level cryptographic code, and verifies locations of potential single-trace 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.
Energy harvesting battery-free embedded devices rely only on ambient energy harvesting that enables stand-alone and sustainable IoT applications. These devices execute programs intermittently when the harvested ambient energy in their energy reservoir is sufficient to operate and stop execution abruptly (and start charging) otherwise. This work presents a probabilistic symbolic execution approach that analyzes the timing and energy behavior of intermittent programs at compile time.