Research

We formally study the logical reasoning capabilities of decoder-only Transformers in the context of the boolean satisfiability (SAT) problem. First, we prove by construction that decoder-only Transformers can decide 3-SAT, in a non-uniform model of computation, using backtracking and deduction via Chain-of-Thought (CoT). Second, we implement our construction as a PyTorch model with a tool (PARAT) that we designed to empirically demonstrate its correctness and investigate its properties. Third, rather than programming a transformer to reason, we evaluate empirically whether it can be trained to do so by learning directly from algorithmic traces (‘reasoning paths’) from our theoretical construction. The trained models demonstrate strong out-of-distribution generalization on problem sizes seen during training but have limited length generalization, which is consistent with the implications of our theoretical result. This work was published at ICML 2025.

After a sophisticated attack or data breach occurs at an organization, a postmortem forensic analysis must be conducted to reconstruct and understand the root causes of the attack. Unfortunately, the majority of proposed forensic analysis systems rely on system-level auditing, making it difficult to reconstruct and investigate web-based attacks, due to the semantic-gap between system- and web-level semantics. This limited visibility into web-based attacks has recently become increasingly concerning because web-based attacks are commonly employed by nation-state adversaries to penetrate and achieve the initial compromise of an enterprise network. To enable forensic analysts to replay and investigate web-based attacks, we propose WebRR, a novel OS- and device- independent record and replay (RR) forensic auditing system for Chromium-based web browsers. While there exist prior works that focus on web-based auditing, current systems are either record-only or suffer from critical limitations that prevent them from deterministically replaying attacks. WebRR addresses these limitation by introducing a novel design that allows it to record and deterministically replay modern web applications by leveraging JavaScript Execution Unit Partitioning.

We have studied the problem of defending against sophisticated web-based social engineering techniques where attackers leverage low-tier ad networks to inject social engineering components onto web pages to lure users into websites that the attackers control for further exploitation. Most of these exploitations are Web-based Social Engineering Attacks (WSEAs), such as reward and lottery scams. We have developed TRIDENT, a novel defense system that aims to detect and block generic WSEAs in real-time. TRIDENT stops WSEAs by detecting Social Engineering Ads (SE-ads), the entry point of general web social engineering attacks distributed by low-tier ad networks at scale. Our extensive evaluation showed that TRIDENT can detect SE-ads with an accuracy of 92.63% and a false positive rate of 2.57% and is robust against evasion attempts. We also evaluated TRIDENT against the state-of-the-art ad-blocking tools. The results show that TRIDENT outperforms these tools with a 10% increase in accuracy. Additionally, TRIDENT only incurs 2.13% runtime overhead as a median rate, which is small enough to deploy in production. This work was published in the 2023 USENIX Security Symposium.

We have been developing machine learning techniques for program analysis. We have studied the problem of automating the identification of security bugs with the goal of classifying and identifying the line on which the vulnerability occurs in a program. We have developed VulChecker, a tool that can precisely locate vulnerabilities in source code (down to the exact instruction) as well as classify their type (CWE). To accomplish this, we developed a new program representation, program slicing strategy, and the use of a message-passing graph neural network to utilize all of code’s semantics and improve the reach between a vulnerability’s root cause and manifestation points. We also develop a novel data augmentation strategy for cheaply creating strong datasets for vulnerability detection in the wild, using free synthetic samples available online. With this training strategy, VulChecker was able to identify 24 CVEs (10 from 2019 & 2020) in 19 projects taken from the wild, with nearly zero false positives compared to a commercial tool that could only detect 4. VulChecker also discovered an exploitable zero-day vulnerability, which has been reported to developers for responsible disclosure. This work was published in the 2023 USENIX Security Symposium.