Foundation models have achieved remarkable success across diverse tasks, but they remain vulnerable. To investigate such vulnerabilities, semantic-shift jailbreaks have recently emerged as a promising attack paradigm. They bypass explicit safety mechanisms by replacing harmful terms in original harmful questions with benign alternatives and leveraging contextual information to induce the target model to reinterpret these alternatives as their corresponding harmful concepts. However, existing semantic-shift jailbreaks often achieve limited effectiveness. In this work, we reveal that this limitation arises from overlooking the semantic-shift capability of contexts. Through systematic analysis, we find that contexts exhibit substantially different abilities in inducing semantic shifts: contexts with stronger semantic-shift capabilities are more likely to guide models toward recovering harmful meanings and achieving successful jailbreaks. Based on this finding, we systematically identify and distill the characteristics of effective contexts and propose a black-box context-aware semantic-shift jailbreak framework with Iterative Context Optimization (ICO). In each iteration, ICO leverages these characteristics and feedback from the target model to optimize contexts. Extensive experiments on three datasets and eight target foundation models demonstrate that ICO consistently outperforms eight state-of-the-art baselines, achieving an average attack success rate of 74.6%.
Hujian Zhu, Yihao Huang, Felix Juefei-Xu et al.· 0 citations
Program verification tools often rely on specific intermediate representations and analysis backends, limiting the reuse of verification algorithms and model checkers across frameworks. In contrast, hardware model checking has developed a mature backend ecosystem, where standard formats such as BTOR2 support reusable algorithms for counterexample search and inductive safety proving. Applying these capabilities to C requires translating assertion-based programs into transition systems that hardware model checkers can directly process. We present C2Btor, a method for encoding such verification tasks into BTOR2 models. C2Btor uses a program counter to capture control transfers, represents data states and memory objects with bit-vectors and arrays, and maps assumptions and assertion checks into BTOR2 constraints and bad-state properties. We evaluate C2Btor on SV-COMP C ReachSafety benchmarks and a curated assertion-category benchmark suite, comparing it with representative program verification tools. C2Btor correctly solves 263 tasks, 101 more than CBMC configured with bounded model checking, and is especially effective on bit-vector benchmarks, where it solves 75.5% of the tasks with no wrong verdicts. These results show that the BTOR2 route allows C program verification to benefit from advances in hardware model-checking backends, expanding the available capability for counterexample search, inductive safety proving, and word-level transition-system reasoning.
Xinyu Zhang, Runxuan Fang, Ziqun Bao et al.· 0 citations
Deep learning (DL) compilers such as Apache TVM translate high-level models into optimized low-level code through multi-stage compilation pipelines. While recent testing efforts have improved fuzzing of optimization stages, they still face two key challenges: (i) the lack of semantics-preserving test models, leading to low validity, and (ii) coarse-grained input generation that fails to trigger hard-to-reach compiler components. To address these limitations, we propose CovCraft, a unified testing framework that integrates constraint-driven model generation with large language model (LLM)-guided input adaptation. CovCraft constructs diverse and valid ONNX models via symbolic constraint encoding and SMT solving, and then iteratively refines inputs using LLM-guided prompts to target uncovered functions, enabling the activation of rarely executed code paths. We evaluate CovCraft on TVM and observe consistent improvements over state-of-the-art techniques: it increases branch and function coverage by 8.9% and 7.0%, respectively, and detects 8 bugs. Moreover, the LLM-guided component achieves an 83.75% success rate in covering designated target functions, demonstrating the effectiveness of combining constraint-based generation with adaptive LLM reasoning for DL compiler testing. The prototype implementation of CovCraft is publicly available at: https://github.com/duduhedangdang/CovCraft.
Yifei He, Fangyu Yang, Ting Su et al.· Annual International Compute...· 0 citations
