arXiv subjects

Zhaoxuan Li

Publications and source records attributed to Zhaoxuan Li.

9 recordsLinked to original sources

arXiv2026

Scratchy: Visual-Scratchpad Multimodal Reasoning for Cryptographic Proof Generation in EasyCrypt

Large language models (LLMs) have recently made substantial progress in formal proof generation, yet presenting distinctive challenges in cryptographic area. Computational security arguments posit that a valid proof must coordinate probability, adversarial games, invariants, assumptions and bounds, which can be provided by a machine-checked framework named EasyCrypt. Although all objects may appear in available context, LLMs still struggle because proof-theoretic dependencies are typically implicit in a linear representation and distributed across multiple programs. So, this paper presents Scratchy, a visual-scratchpad approach that exposes these dependencies for multimodal generation. Given the natural-language security description, with formal context and target propositions, the proof objects can be normalized into a typed proof-relation graph. Then a structure-preserving visual compiler transforms the graph into the formula-rich visual proof state that guides a multimodal model in generating the EasyCrypt proof. Also, the Scratchy-eval, a 114-task dataset derived from reliable official EasyCrypt files, has been introduced. It contains 64 security-form proof generations and 50 multiple-choice knowledge tests. After a series of evaluations, covering semantic grounding, relational invariants, and game reductions, classical LLMs like GPT-5.6-Sol and Claude-Opus-5 have gained a clear advantage from Scratchy's structured visual proof states. This contrast suggests that explicit proof structure can make the improvement and multimodal proof-state representation as a promising direction for computer-aided cryptography.

cs.CR↗

arXiv2026

A Drop-in KEM Replacement for Client Signatures in Post-Quantum SSH

The transition to post-quantum cryptography is reshaping the Secure Shell (SSH) protocol for remote administration. Post-quantum key exchange has been deployed in OpenSSH and is being standardized, while SSH authentication largely remains a signature-replacement effort. This path preserves the familiar public-key credential model, but inherits the size and computation overhead of post-quantum signatures, which can increase latency, traffic, and server-side load. KEM-based authentication offers a natural alternative to this signature-centric path, and SSH makes this especially attractive at the user-authentication layer, which is method-extensible, separated from transport-layer key exchange and host-key authentication, and already protected by the established channel. We present a drop-in KEM-based user-authentication method for SSH that replaces client public-key signatures with a session-bound challenge-response proof. The method fits into SSH's existing user-authentication framework, preserving the public-key credential model and enabling incremental deployment alongside existing methods. We provide a reduction-based security argument in the post-quantum ACCE framework, implement the design in OpenSSH using liboqs, and evaluate it under representative RTTs, TCP initial-window settings, and post-quantum migration configurations. Our results show that KEM-based authentication is competitive with compact signature-based authentication under representative network settings, while reducing median handshake latency by up to about 10% against large-signature hybrid baselines. The advantages are clearer when post-quantum signatures stress transmission or computation: median latency under small TCP initial windows falls by up to 7.3% versus ML-DSA and 17.9% versus SLH-DSA, while server-side online cryptographic cost is 59.1% lower than that for ML-DSA in the same NIST category.

cs.CR↗

arXiv2026

Decision-Level Hijacking: Injecting Cognitive Bias into Large Language Models via Bit-Flip Attacks

Large Language Models (LLMs) have been widely applied in high-stakes decision-making scenarios such as corporate strategy, and users are increasingly relying on their outputs. However, the deep integration of open-source model sharing ecosystems with LLM-powered critical decision-making applications also introduces critical risks: if an attacker can manipulate the model's cognitive stance, they can indirectly influence the judgments and actions of downstream decision-makers. This paper defines such threats as decision-level hijacking. Existing attacks fail to achieve targeted cognitive manipulation without triggering prohibited content or degrading model functionality. To fill this gap, this paper reveals that Bit-Flip Attacks (BFAs) can serve as an attack vector for inducing decision-level hijacking, requiring no real-time interaction or control over the training process, and only a minimal number of weight bits need to be flipped after deployment to achieve stealthy, low-cost, and persistent cognitive manipulation. Therefore, we propose CogBias, a cognitive bias injection framework for LLMs. CogBias converts subjective preferences into optimization signals via a differentiable sentiment evaluator, uses a multi-objective loss to jointly constrain multiple dimensions, and constructs BitScout to locate critical bits, achieving targeted cognitive intervention under an ultra-sparse flip budget. Experiments on Llama-3.2-3B, Mistral-7B, and Qwen2.5-14B, as well as on the commercial recommendation and controversial factual topic scenarios, demonstrate that flipping only a small number of bits stably induces significant stance shifts on target topics, while the impact on non-target tasks and overall output distribution is limited. This work demonstrates that minute perturbations to low-level weight data suffice to undermine the high-level value alignment of LLMs.

cs.CR↗

arXiv2026

Graph Neural Network-based Algorithm Selection for the Traveling Salesman Problem: A Systematic Study of Cost and Rank Losses under Distinct Budget Regimes

Automated Algorithm Selection (AS) aims to improve problem-solving performance by selecting, for each problem instance, the most suitable algorithm from a predefined portfolio. This is particularly relevant to the Traveling Salesman Problem (TSP), where solver performance is strongly instance-dependent. We introduce GNNAS-TSP, a Graph Neural Network (GNN)-based AS framework that learns TSP instance representations directly from raw graph data, avoiding manual feature engineering. GNNAS-TSP formulates AS as a joint cost-prediction and ranking task. We evaluate cost-based (mean squared error (MSE), mean absolute error (MAE), and Huber), rank-based (RankNet, ListNet, and LambdaRank), and hybrid learning objectives for a portfolio comprising Chained Lin-Kernighan, Edge Assembly Crossover, Lin-Kernighan-Helsgaun, Multiagent Optimization System, and Concorde. Experiments use fixed computational budgets of 10 and 60 seconds. On the held-out test set, the selected configurations improve on the Single Best Solver (SBS) in normalized solution cost at both budgets. For the 10s budget, AS achieves substantial and statistically significant cost improvement over SBS. Overall, the results suggest that GNNAS-TSP is a useful meta-solving strategy when exploitable variation exists across solver performance.

cs.LG↗

arXiv2026

CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes

Manual formal analysis of cryptographic schemes is labor-intensive and requires substantial expertise. While model-checking tools (e.g., Scyther and Tamarin) and computational-security tools (e.g., CryptoVerif and EasyCrypt) improve the automation of security proofs, they still rely on experts to abstract schemes and write tool-specific formal descriptions. Large language models (LLMs) are a promising alternative, but their effectiveness in this domain remains unexplored due to the absence of standardized evaluation methodologies. To fill this gap, we introduce CrypFormBench (C.F.B for short), a comprehensive benchmark jointly covering symbolic and computational security to evaluate five core LLM capabilities: interpretation, generation, completion, transformation, and correction. It comprises 700 instances spanning 677 schemes, 7 mainstream formal verifier languages, and 160 security properties. The evaluation of 9 state-of-the-art LLMs reveals that most of them perform well on interpretation and completion, given their code-awareness advantages, but struggle with generation, transformation, and correction. Overall, their performance remains limited, with Claude-3.5 achieving the highest score at 48.7 out of 100. We further provide practical guidance, e.g., few-shot prompting, Pass@K sampling, and lightweight fine-tuning, to mitigate the executability bottleneck and improve tool-usable outputs. Taken together, our benchmark and analyses offer a grounded view of current progress and concrete directions toward reliable LLM-assisted formal cryptographic analysis.

cs.CR↗

arXiv2025

Has the Two-Decade-Old Prophecy Come True? Artificial Bad Intelligence Triggered by Merely a Single-Bit Flip in Large Language Models

Recently, Bit-Flip Attack (BFA) has garnered widespread attention for its ability to compromise software system integrity remotely through hardware fault injection. With the widespread distillation and deployment of large language models (LLMs) into single file .gguf formats, their weight spaces have become exposed to an unprecedented hardware attack surface. This paper is the first to systematically discover and validate the existence of single-bit vulnerabilities in LLM weight files: in mainstream open-source models (e.g., DeepSeek and QWEN) using .gguf quantized formats, flipping just single bit can induce three types of targeted semantic level failures Artificial Flawed Intelligence (outputting factual errors), Artificial Weak Intelligence (degradation of logical reasoning capability), and Artificial Bad Intelligence (generating harmful content). By building an information theoretic weight sensitivity entropy model and a probabilistic heuristic scanning framework called BitSifter, we achieved efficient localization of critical vulnerable bits in models with hundreds of millions of parameters. Experiments show that vulnerabilities are significantly concentrated in the tensor data region, particularly in areas related to the attention mechanism and output layers, which are the most sensitive. A negative correlation was observed between model size and robustness, with smaller models being more susceptible to attacks. Furthermore, a remote BFA chain was designed, enabling semantic-level attacks in real-world environments: At an attack frequency of 464.3 times per second, a single bit can be flipped with 100% success in as little as 31.7 seconds. This causes the accuracy of LLM to plummet from 73.5% to 0%, without requiring high-cost equipment or complex prompt engineering.

cs.CR↗

arXiv2025

A.S.E: A Repository-Level Benchmark for Evaluating Security in AI-Generated Code

The increasing adoption of large language models (LLMs) in software engineering necessitates rigorous security evaluation of their generated code. However, existing benchmarks often lack relevance to real-world AI-assisted programming scenarios, making them inadequate for assessing the practical security risks associated with AI-generated code in production environments. To address this gap, we introduce A.S.E (AI Code Generation Security Evaluation), a repository-level evaluation benchmark designed to closely mirror real-world AI programming tasks, offering a comprehensive and reliable framework for assessing the security of AI-generated code. Our evaluation of leading LLMs on A.S.E reveals several key findings. In particular, current LLMs still struggle with secure coding. The complexity in repository-level scenarios presents challenges for LLMs that typically perform well on snippet-level tasks. Moreover, a larger reasoning budget does not necessarily lead to better code generation. These observations offer valuable insights into the current state of AI code generation and help developers identify the most suitable models for practical tasks. They also lay the groundwork for refining LLMs to generate secure and efficient code in real-world applications.

cs.SE↗

arXiv2024

Magnifier: Detecting Network Access via Lightweight Traffic-based Fingerprints

Network access detection plays a crucial role in global network management, enabling efficient network monitoring and topology measurement by identifying unauthorized network access and gathering detailed information about mobile devices. Existing methods for endpoint-based detection primarily rely on deploying monitoring software to recognize network connections. However, the challenges associated with developing and maintaining such systems have limited their universality and coverage in practical deployments, especially given the cost implications of covering a wide array of devices with heterogeneous operating systems. To tackle the issues, we propose Magnifier for mobile device network access detection that, for the first time, passively infers access patterns from backbone traffic at the gateway level. Magnifier's foundation is the creation of device-specific access patterns using the innovative Domain Name Forest (dnForest) fingerprints. We then employ a two-stage distillation algorithm to fine-tune the weights of individual Domain Name Trees (dnTree) within each dnForest, emphasizing the unique device fingerprints. With these meticulously crafted fingerprints, Magnifier efficiently infers network access from backbone traffic using a lightweight fingerprint matching algorithm. Our experimental results, conducted in real-world scenarios, demonstrate that Magnifier exhibits exceptional universality and coverage in both initial and repetitive network access detection in real-time. To facilitate further research, we have thoughtfully curated the NetCess2023 dataset, comprising network access data from 26 different models across 7 brands, covering the majority of mainstream mobile devices. We have also made both the Magnifier prototype and the NetCess2023 dataset publicly available\footnote{https://github.com/SecTeamPolaris/Magnifier}.

cs.NI↗

arXiv2017

Buildings-to-Grid Integration Framework

This paper puts forth a mathematical framework for Buildings-to-Grid (BtG) integration in smart cities. The framework explicitly couples power grid and building's control actions and operational decisions, and can be utilized by buildings and power grids operators to simultaneously optimize their performance. Simplified dynamics of building clusters and building-integrated power networks with algebraic equations are presented---both operating at different time-scales. A model predictive control (MPC)-based algorithm that formulates the BtG integration and accounts for the time-scale discrepancy is developed. The formulation captures dynamic and algebraic power flow constraints of power networks and is shown to be numerically advantageous. The paper analytically establishes that the BtG integration yields a reduced total system cost in comparison with decoupled designs where grid and building operators determine their controls separately. The developed framework is tested on standard power networks that include thousands of buildings modeled using industrial data. Case studies demonstrate building energy savings and significant frequency regulation, while these findings carry over in network simulations with nonlinear power flows and mismatch in building model parameters. Finally, simulations indicate that the performance does not significantly worsen when there is uncertainty in the forecasted weather and base load conditions.

math.OC↗