I am pursuing a PhD in Computer Science at Yale University under the guidance of Ruzica Piskac and Jakub Szefer. My current research focuses on the automated inference of program properties and invariants by integrating machine learning with formal methods.
Currently, I am an Applied Scientist Intern at the Automated Reasoning Group in AWS, working on neurosymbolic programming to capture symbolic knowledge and mitigate hallucinations of LLMs in logical reasoning. Previously, I developed tools for model-based conformance checking of distributed networked systems at AWS.
During my PhD, I focused on verifying the side-channel insecurity of low-level Post-Quantum Cryptographic code (EuroS&P 2023). My work included reverse engineering quantum circuits from power traces (CHES 2024, CCS 2023), exploring quantum fault injections (QCE 2024), and detecting quantum computer viruses (HOST 2023). Additionally, I developed a tool for analyzing the non-functional behaviors of intermittent programs (TECS 2023), developed a software countermeasure against physical attacks (ICCAD 2024), and surveyed security verification techniques (JETC 2023). Before my PhD, I worked as a research software engineer in industry, applying formal methods to engineering problems (COMPSAC 2019, FSE 2018, FSE 2017, ASE 2017, SAC 2017).
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
Research Asistant:
Teaching Asistant:
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.