CyberSec Research

EFI pairs (Brakerski, Canetti, and Qian, ITCS 2023) and one-way puzzles (Khurana and Tomer, STOC 2024) are the leading candidates for the minimal assumption of quantum cryptography. The first are efficiently preparable quantum states, statistically far yet computationally indistinguishable; the second are classical puzzles, easy to sample and hard to solve. One-way puzzles imply EFI pairs, and whether the converse holds is open. We construct a single classical oracle relative to which one-way puzzles do not exist, even with an unbounded verifier, while an EFI pair survives every distinguisher that queries the oracle classically throughout and holds advice about it, making its one superposition query at the end. The oracle answers every question about the output probabilities of quantum samplers, which removes the puzzles, and hides a Haar-random half-dimensional subspace. To prove security we reduce it to communication complexity. An adversary whose knowledge of the subspace arrives as classical query answers can be simulated inside a two-party protocol against the party holding it, so it does no better than the best classical protocol for Vector-in-Subspace (Klartag and Regev, STOC 2011), whatever the oracle computes. That argument does not cover the superposition query, which we bound instead using tools from random matrix theory. The same attack gives a classical simulation of any quantum party in a classical-message protocol with no entanglement shared in advance, so relative to the oracle there is no proof of quantumness either. Quantum polynomial time therefore offers no advantage on any task with classical inputs and outputs, while the two quantum states stay indistinguishable. We state conjectures on removing the restriction on superposition queries.

The Signal protocol is a prominent messaging protocol that secures communication for billions of users. It powers WhatsApp, the most widely used messaging application worldwide, and the Signal app, popular among privacy-conscious users. Extensive research in the computational and Dolev-Yao settings provides strong formal security guarantees for the protocol itself. However, a gap remains between the guarantees of the protocol specification and the implementation's actual behavior at runtime. In this work, we bridge this gap by applying SpecMon, a recently proposed runtime monitor, to check whether observed executions conform to formal protocol models. To this end, we instrument two applications (WhatsApp Web and Signal Desktop) to capture their interactions with the network and the cryptographic components. Using this instrumentation, we develop two multiset-rewrite models that are compatible with Tamarin, thus enabling verification. We derive the first model of WhatsApp Web's implementation of the Signal protocol and the most detailed model to date of Signal's original protocol. Monitoring establishes that observed executions conform to these models, relative to the trusted event extraction and the symbolic abstraction. For the core components of the Signal protocol, we verify authentication and secrecy properties. Finally, monitoring reveals previously undocumented differences between the original libsignal library and WhatsApp's fork. We evaluate our methodology and demonstrate its reproducibility. Developing the WhatsApp Web model, instrumenting the app, adding fuzzing, and running the experiments took three person-weeks. We also demonstrate efficient monitoring of real-world applications and detection of deliberately injected security faults, with low overhead in our measured setting.

Cyber attacks are increasingly automated, narrowing the time available for human analysts to detect, reason about, and respond to intrusions. Large language models (LLMs) offer a promising foundation for autonomous cyber defense because they can correlate heterogeneous evidence and reason about previously unseen threats. However, directly applying LLMs to operational security telemetry is impractical: raw logs arrive faster than current models can process them, individual events are often ambiguous, and unconstrained LLM actions can introduce significant operational risk. We present BlueSTAR, a tiered agentic architecture for autonomous cyber defense in enterprise IT/OT networks. BlueSTAR first transforms high-volume security telemetry into compact indicators of compromise. We further introduce a resilience metric that jointly captures attacker reach, impact on mission-critical assets, and disruption caused by defensive actions. We evaluate BlueSTAR on two live enterprise IT/OT cyber ranges using seven attack chains based on real-world intrusion techniques. Across attack chains, BlueSTAR retains the fast containment of deterministic response for known threats while successfully defending against attacks requiring contextual and cross-cycle reasoning, including credential theft, repeated compromise, concurrent attackers, and attacks against physical processes.

Semantic search is a core primitive of modern applications, powering recommender systems, web search, and retrieval-augmented generation for language models. The provider controls the index and query execution, leaving clients to trust that results come from the right algorithm over the intended index. A provider may truncate search to cut cost, bias results, or otherwise deviate from the specified execution undetected. Verifiability can remove this trust assumption by proving that results follow the agreed algorithm over a committed index. Realizing this efficiently is hard, as retrieval at scale relies on HNSW, a graph-based algorithm whose data-dependent traversal maps poorly onto the fixed constraint systems of zero-knowledge proofs. Prior verifiable systems therefore target regular, cluster-based indices that are easier to encode, sacrificing the recall of graph-based search. We present Atlas, a system that lets a provider prove a query was answered correctly against its committed index without revealing the index. At its core is a new zero-knowledge proof for HNSW search, built on three techniques: preprocessing that shifts all database-dependent cost offline, so per-query proving scales with the traversal rather than the database; a restructuring of HNSW into a fixed-size-state procedure that we prove returns the same result; and a timestep-tagged batching that merges the per-step arguments of the entire traversal into one. Atlas is the first to demonstrate verifiable graph-based search at scale, proving a query in under a second on the SIFT1M benchmark and in 2.0 seconds at 100 million vectors, while maintaining the recall of plaintext HNSW and revealing nothing about the index beyond the result. In a complete RAG pipeline, Atlas' proven retrieval preserves end-to-end answer quality, and reaches higher quality at lower proving cost than all prior verifiable retrieval systems.

Super-apps, an emerging mobile architecture, host third-party mini-apps inside a single app, allowing users to access diverse services. A decade of security research on the super-app ecosystem has all assumed super-apps to be a trusted intermediary. We argue this implicit trust is difficult to justify: China's WeChat is already shown to passively track its user's activity across mini-apps at extraordinary scale; Russia's MAX's parent company is reported to be deeply entangled with the state prosecution of online speech; and Iran's Bale was reported to be functioning in the world's longest internet shutdown due to its state-backed support. In this paper, we show how malicious super-apps have undeniable capabilities to silently undermine the security and privacy of mini-apps and users without leaving any trace. Using MAX as an example, we show how it can capture mini-app UI, read and write mini-app local storage, inject arbitrary JavaScript into a mini-app's runtime, mediate mini-app network traffic, and control authentication context in ways that can enable silent user impersonation. Sadly, these capabilities manifest themselves in any super-app because of the architectural privileges granted to them by design. We argue that mobile OS and app store interventions are urgently needed to close this architectural blind spot before it is further exploited.

Large language models are often fine-tuned, shared, or downloaded from third parties, so a deployed model may carry a hidden backdoor that behaves normally on benign inputs but switches to attacker-controlled behavior when a secret trigger appears. While backdoors can be audited before deployment, runtime monitoring remains important for models that are frequently updated. The challenge is that LLM serving is latency-sensitive: existing inference-time detectors either rely on assumptions about the trigger form, which can fail on stealthy attacks, or require extra model computation, such as input perturbations or an additional generation pass. We introduce SpecGuard, an inference-time backdoor detector that repurposes speculative decoding at zero added model-computation cost. Speculative decoding speeds up inference by using a small draft model to propose tokens and a target model to verify them. We observe that this verification process already exposes a useful signal: when a backdoor is triggered, the target model shifts toward the attacker's behavior, while a clean draft model does not predict this shift, causing the draft-token acceptance rate to change. We formalize when this signal appears and show that an attacker who suppresses it must also weaken the backdoor. Across diverse backdoor types and model families, SpecGuard reliably detects triggered behavior, including stealthy cases where input-level filters are blind, while avoiding the extra generation cost of existing runtime detectors. Speculative decoding therefore doubles as a free, always-on signal for detecting backdoored LLM behavior.

Membership inference attacks (MIAs) are widely used to audit the privacy disclosure risk of machine learning models, however current state-of-the-art attacks require training computationally expensive shadow models, making large-scale privacy evaluation impractical. In this work, we investigate whether inexpensive spectral metrics derived from the heavy-tailed self-regularisation framework can serve as proxies for MIA vulnerability. We evaluate several WeightWatcher spectral metrics on image and tabular classification tasks and compare their relationship with MIA privacy leakage against conventional measures of generalisation. Across datasets, stable rank exhibits a strong positive correlation with overall MIA success, while Log alpha-Norm shows a consistent negative correlation with MIA vulnerability at the low false-positive regime. These associations are observed to be stronger than those obtained using the generalisation gap. The results indicate that neural network spectra may contain information about privacy leakage that is not fully captured by conventional measures of overfitting, motivating spectral analysis as a promising direction for scalable privacy auditing.

Clinical electroencephalography (EEG) data are valuable for healthcare research and for developing artificial intelligence (AI)-based clinical decision-support systems, but EEG recordings and derived features may contain sensitive patient-specific information. This creates privacy risks when data are reused, analyzed, or shared across clinical and research environments. Conventional anonymization methods are often insufficient for high-dimensional biomedical signals, since removing direct identifiers does not necessarily prevent re-identification, linkage, or inference risks. At the same time, strong privacy protection may distort clinically relevant signal characteristics and reduce data utility. This paper studies subject-level differential privacy for protecting clinical EEG-derived feature representations using Gaussian and Laplace perturbations. The proposed framework considers three deployment scenarios: client-side anonymization, centralized server-side anonymization, and decentralized local training. Following EEG preprocessing and feature extraction, Gaussian and Laplace perturbations are applied to the resulting patient-level EEG feature representations. The Laplace experiments evaluate the implemented noise scales, while the scales required for formal full-vector calibration are derived separately. The effects of both perturbations are assessed using statistical utility measures and a downstream machine-learning-based utility check. The results show that differentially private perturbation can be integrated into EEG processing workflows, but the selected mechanism, privacy parameters, and sensitivity calibration strongly influence data utility. The study highlights the practical privacy-utility trade-off in DP-based EEG feature anonymization and the challenges of preserving downstream utility in small and imbalanced clinical EEG datasets.

Software agents are beginning to shop and pay on a person's behalf. Agent payment protocols such as AP2 produce cryptographically valid signatures for completed purchases, yet do not constrain the decisions that lead to them. Consequently, ordinary product-description text can steer a shopping agent into forming a cart that passes every protocol check but no longer matches the user's request. In this paper, we show that this vulnerability enables three related attacks. In the first attack, the agent is steered into fetching another user's payment credentials. In the second, it assembles a cryptographically valid cart whose contents do not match what the user was shown. In the third, a single factual claim about stock or product lineage moves the agent from the cheaper displayed item to a more expensive one, while the resulting cart remains fully consistent with the listing. In experiments using the Gemini Flash-Lite models that AP2's sample agents specify by default, the three attacks succeeded at rates of 90%, 56%, and 73.3%, respectively. The same vulnerability appears across seventeen Google models, three unrelated agent frameworks, two cross-vendor anchors, and Google's own consumer assistant. To address this attack vector, we introduce A-VIP (AP2 Verified-Intent Protection), a protocol-layer defense that treats the signed intent as a capability grant rather than judging the merchant's description. The defense binds every credential lookup to the session that requested it and every cart line to the listing seen, while flagging unauthorized spending. The first two attacks leave structural traces that these bindings block with zero false positives. The third attack leaves no trace, so A-VIP surfaces unauthorized spending for user confirmation. Finally, we release the A-VIP code, machine-checked invariants, and AP2-WhisperBench, a suite of 1,544 evaluation scenarios.

A quantum classifier assigns labels by evolving an input quantum state and measuring the output, so repeated executions reveal only a distribution over labels. We study certified adversarial robustness for such classifiers under known-readout query access (KRQA), where an evaluator can prepare inputs, knows the quantum measurement, and observes finite-shot outcomes but cannot inspect the internal evolution, parameters, or gradients. We give a measurement-only framework that returns two complementary guarantees for each input: a lower bound ruling out untargeted errors within a radius, and an attack-independent upper bound witnessing an adversarial state within a radius. Both are estimable from the known readout measurement and sampled outcomes, require no tomography or circuit description, and admit finite-sample guarantees. The upper bound uses gap operators induced by the quantum measurement; the lower bound relaxes state-space search to an efficient optimization over outcome distributions with operator-spectrum constraints, yielding certificates that are never weaker than prior probability-only certificates and can be strictly stronger when the spectral constraints are active. Evaluations on multiple quantum classifiers show that the lower bound tracks exact optima on tractable instances, while the upper bound remains informative when standard attacks fail. We further demonstrate real-device feasibility on IBM Quantum hardware: from 40 executions of two 8-qubit quantum neural networks, our method computes both certificates, with the expected ordering between the lower and upper bounds on every tested input. Taken together, these results show that robustness claims for quantum classifiers can be audited directly from observable statistics under KRQA.

Fully Homomorphic Encryption (FHE) enables secure computation on encrypted data, making it a promising solution for privacy-preserving applications in the cloud. Among various FHE schemes, FHE over the Torus (TFHE) stands out due to its support for arbitrary operations. However, its high computation and communication overhead, particularly in the Fast Fourier Transform (FFT) operations required during bootstrapping, limits its practicality for real-world applications. Conventional electronic accelerators struggle to achieve sufficient throughput due to the limitations of technology scaling and the memory-wall problem. To address these challenges, we propose PHAT, a PHotonic Accelerator for TFHE leveraging Optically-addressed Phase-Change Memory (OPCM). OPCM-based processing-in-memory systems offer high computation and communication throughput, making them well-suited for accelerating FFT operations in TFHE. However, directly mapping FFT to OPCM presents challenges such as high-precision analog computation and the high latency and energy cost of programming OPCM cells. To overcome these challenges, we introduce a novel electro-photonic accelerator architecture optimized for TFHE, featuring OPCM-based FFT units, a twiddle-stationary dataflow tailored for OPCM, and a scheduling mechanism to maximize the utilization of the FFT units. PHAT delivers $2.14\times$--$5.10\times$ speedup across four real-world TFHE workloads against the state-of-the-art ASIC accelerator. Our approach significantly enhances the performance of TFHE applications, paving the way for practical and efficient homomorphic encryption in cloud computing.

AI agents increasingly propose actions with external consequences, including financial transfers, infrastructure changes, software deployments, disclosures, and physical actuation. Authorization engines, policy languages, runtime monitors, provenance mechanisms, and agent guardrails provide important foundations, but do not necessarily define a common semantic contract for the final transition from a particular candidate action to execution authority. We specify EBL-Core, an execution-boundary conformance profile for deciding whether one canonical, fully materialized AI-generated candidate may receive action-scoped execution authority under explicit conditions. It binds a structured intent object, Root and Operational Policies, evidence obligations, typed evidence, context, time, and a verifiable Decision Derivation through an Execution Release Contract (ERC). An ERC is not an authority-bearing token; a verified ALLOW ERC may support a separate Execution Grant governed by Redemption-time validation. EBL-Core specifies action binding, policy non-weakening, evidence handling, deterministic adjudication, derivation verification, and grant lifecycle behavior. An accompanying reference artifact provides schemas, adjudication, separate verification and Semantic Replay, and a linearizable in-memory grant store. In the retained run, 34 static vectors and 15 lifecycle checks matched expected outcomes. Across 100 trials, 32 concurrent Redemption attempts yielded exactly one successful Redemption and protected test effect per trial; 100 Revoke-Redeem races ended in valid terminal outcomes. These bounded results demonstrate executability of the specified subset, not human-intent correctness, evidence truth, complete mediation, production readiness, mechanized correctness, or deployment-level security.

We propose CHERI-D Reincarnate (Reinc), an architectural extension to CHERI for scalable and efficient temporal memory safety. Prior work CHERI-D has a finite-width generation ID stored at a fixed location, requiring an object to be quarantined when its ID is exhausted. Reinc further provides use-after-free mitigation while permitting immediate freed memory reuse for objects through allocation reincarnation: rather than quarantining an allocation slot upon ID exhaustion, Reinc dynamically assigns a new ID to that slot when its current ID is exhausted. Exhausted IDs are quarantined and later reclaimed, while the underlying memory remains available for immediate reuse. By quarantining IDs rather than memory, Reinc enables continuous reuse of memory in the common case, substantially reducing both memory-sweep frequency and quarantine memory overhead. Reinc further introduces coherent ID caching while retaining a fully decentralized ID organization. Temporal metadata remains colocated with the memory it protects, preserving locality while avoiding centralized metadata structures. To support multicore execution, Reinc connects physical coherence events to the virtually addressed ObjID buffer using lightweight reverse-map and filter-based mechanisms. We implement Reinc as a hardware-software co-design spanning CHERI-Toooba (superscalar FPGA softcore), QEMU, LLVM/Clang and CheriBSD. Across our evaluated workloads, Reinc substantially reduces memory-sweep frequency and memory quarantine while incurring low performance and hardware overhead.

Certificate Transparency (CT) aims to reduce the trust required in Certificate Authorities (CAs) within the TLS certificate ecosystem. It is supported by all major browsers. The protocol obliges all CAs to record the certificates they issue in a public log, which itself is monitored for compliance and consistency by third parties. Given this complex set of checks between the four roles-CA, loggers, monitor but also the end user's client-it is very hard to provide a precise account of how CT eliminates trust assumptions in exchange for complex infrastructure. Analyses both in the Dolev-Yao paradigm and the computational paradigm only regard a very simplified model and feature definitions adapted specifically to CAs, essentially capturing design features rather than the target property. The present paper posits accountability as the main goal of CT and presents a thorough analysis in the Dolev-Yao model. We start with the vanilla PKI and, step by step, move to CT, finally analyzing proposed extensions for SCT Auditing and Gossiping. We show that plain CT relies on an honest log, but provides accountability under this assumption. Furthermore, we show that the SCT Auditing extension can eliminate this assumption, while the Gossiping extension cannot.

Blockchains enable decentralized applications through smart contracts---interactive programs executed through consensus. However, the inherently asynchronous nature of blockchain transaction ordering introduces a class of vulnerabilities known as frontrunning attacks, which have caused millions of dollars in losses in major blockchains, such as Ethereum. Frontrunning attacks arise because users interact with smart contracts through transactions, which are added to the blockchain by designated nodes called miners. Miners can exploit their ability to reorder, delay, or insert transactions to gain an advantage over honest users, effectively frontrunning them. Yet, to date, the field lacks a rigorous definition of what it even means for a contract to resist such attacks. Worse, we show that existing dynamic detection approaches are fundamentally inadequate: in a large-scale study comprising 287 smart contract audits, 55% of the 393 reported vulnerabilities identified by leading smart contract auditors fall outside the scope of state-of-the-art detection criteria. To address this gap, we propose the first formal definition of frontrunning vulnerability for smart contracts. Our definition captures a key insight: resistance to frontrunning is not an intrinsic property of a contract alone, but depends critically on how honest users interact with it. Grounded in this observation, we develop a sound algorithm for synthesizing secure interaction conditions, alongside a prototype implementation that we apply to audited real-world contracts---revealing previously undiscovered vulnerabilities in two Ethereum contracts.

Static side-channel attacks, which exploit halted-clock conditions to extract sensitive information, pose an increasing threat to chip security. To counter these attacks, various defenses have been proposed that monitor for abnormal clock behavior and trigger the clearing of sensitive data when clock anomalies are detected. In this work, we demonstrate that exposing a chip to cryogenic temperatures interferes with on-chip mixed-signal components, responsible for signal sensing and generation. Based on this observation, we develop Chypothermia, an attack that, without any electrical tampering with the system, disables the target clock sensor, the clock generation circuit, and the voltage sensors, while preserving the secret data. While effective at halting the clock, cooling is a slow process and, on its own, is often insufficient against systems equipped with temperature sensors designed to detect thermal anomalies. To bypass these protections, we combine Chypothermia with Chypnosis (Mitard et al., IEEE SP 2026) and show that, even within a moderately low-temperature operating range, this combination can halt the clock while evading detection. We implement Chypothermia on multiple FPGA/SoC platforms and demonstrate successful disabling of both soft-IP and hard-IP sensor implementations. Finally, we apply Chypothermia to the alert handler of the OpenTitan root of trust, which incorporates a state-of-the-art clock sensor, and show that the attack evades detection and prevents key zeroization. Finally, we introduce and implement an FPGA-compatible self-heating sensor as a countermeasure and demonstrate its robustness against Chypothermia.

Solana is a rapidly growing high-throughput blockchain platform that has attracted substantial liquidity and user activity. However, this expansion has also drawn the attention of illicit actors, who frequently leverage cross-chain bridges to route illicit funds onto Solana to obfuscate transaction lineage. Unlike EVM-compatible platforms, Solana features distinct execution dynamics and lacks standard event logs, creating severe semantic gaps that prevent existing tracing methods from reliably correlating cross-ledger transactions. In this paper, we formalize four types of Solana-bound cross-chain transaction modes and propose a candidate-set selective decision-based tracing method called SolTracer. SolTracer maps disparate execution semantics into a unified event space and employs candidate-set selective decision-making to reliably associate target transactions while abstaining when valid targets are absent. Extensive experiments demonstrate that SolTracer outperforms state-of-the-art (SOTA) methods across three representative scenarios: closed-world association, open-world association, and cross-source-chain generalization. In particular, under the challenging open-world setting with a 50% TA ratio, SolTracer improves the F1 score by 20.16% over the strongest SOTA baseline. Utilizing SolTracer, we conduct an empirical analysis on real-world cross-chain transfers to investigate ecosystem dynamics. Our analysis explores the stark count-value divergence across bridge mechanisms, the prevalence of cross-asset shifts, and the decoupling between on-chain settlement and explorer visibility.

Trusted Execution Environments (TEEs) have become a cornerstone of modern cloud computing, providing strong confidentiality and integrity guarantees for both code and data. A critical component of this trust model is remote attestation, which enables external entities to verify the authenticity and integrity of code executing within a TEE through cryptographic measurements. However, the effectiveness of remote attestation fundamentally depends on the verifier's ability to trace the reported measurement back to the original source code - a property that can only be guaranteed through reproducible builds. In this paper, we investigate the reproducibility of TEE builds through a technical analysis of 115 TEE deployments. Our analysis spans popular TEEs such as Intel SGX, Intel TDX, and AMD SEV, and reveals that a striking 91% of those deployments were not reproducible, with 80% failing to provide both source code and a reference build, the two essential prerequisites for reproducibility. To explore the root causes, we contacted the maintainers of 50 SGX projects and managed to recruit 12 developers from industry and academia for interviews. Only one of our participants reported that reproducibility is a priority during development, effectively confirming our technical findings. Beyond technical barriers (e.g., timestamps included in the binary) that can be readily addressed, we identify broader ecosystem-level challenges, such as the lack of control over the build environment in projects involving multiple stakeholders. We argue that achieving reproducibility in TEEs requires a holistic development approach that extends beyond individual developers and calls for stronger commitments - rather than treating TEEs as a "security badge".