Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview

• URL: http://arxiv.org/abs/2503.10784v1
• Date: Thu, 13 Mar 2025 18:22:22 GMT
• Title: Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview
• Authors: Norbert Tihanyi, Tamas Bisztray, Mohamed Amine Ferrag, Bilel Cherif, Richard A. Dubniczky, Ridhi Jain, Lucas C. Cordeiro,
• Abstract summary: This paper focuses on state-of-the-art software testing and verification.<n>It focuses on three key approaches: classical formal methods, LLM-based analysis, and emerging hybrid techniques.<n>We analyze whether integrating formal rigor with LLM-driven insights can enhance the effectiveness and scalability of software verification.
• Score: 3.135279672650891
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Software testing and verification are critical for ensuring the reliability and security of modern software systems. Traditionally, formal verification techniques, such as model checking and theorem proving, have provided rigorous frameworks for detecting bugs and vulnerabilities. However, these methods often face scalability challenges when applied to complex, real-world programs. Recently, the advent of Large Language Models (LLMs) has introduced a new paradigm for software analysis, leveraging their ability to understand insecure coding practices. Although LLMs demonstrate promising capabilities in tasks such as bug prediction and invariant generation, they lack the formal guarantees of classical methods. This paper presents a comprehensive study of state-of-the-art software testing and verification, focusing on three key approaches: classical formal methods, LLM-based analysis, and emerging hybrid techniques, which combine their strengths. We explore each approach's strengths, limitations, and practical applications, highlighting the potential of hybrid systems to address the weaknesses of standalone methods. We analyze whether integrating formal rigor with LLM-driven insights can enhance the effectiveness and scalability of software verification, exploring their viability as a pathway toward more robust and adaptive testing frameworks.

Related papers

• White-Basilisk: A Hybrid Model for Code Vulnerability Detection [50.49233187721795]
  We introduce White-Basilisk, a novel approach to vulnerability detection that demonstrates superior performance.<n>White-Basilisk achieves results in vulnerability detection tasks with a parameter count of only 200M.<n>This research establishes new benchmarks in code security and provides empirical evidence that compact, efficiently designed models can outperform larger counterparts in specialized tasks.
  arXiv  Detail & Related papers  (2025-07-11T12:39:25Z)
• SV-LLM: An Agentic Approach for SoC Security Verification using Large Language Models [8.912091484067508]
  We introduce SV-LLM, a novel multi-agent assistant system designed to automate and enhance system-on-chip (SoC) security verification.<n>By integrating specialized agents for tasks like verification question answering, security asset identification, threat modeling, test plan and property generation, vulnerability detection, and simulation-based bug validation, SV-LLM streamlines the workflow.<n>The system aims to reduce manual intervention, improve accuracy, and accelerate security analysis, supporting proactive identification and mitigation of risks early in the design cycle.
  arXiv  Detail & Related papers  (2025-06-25T13:31:13Z)
• OpenUnlearning: Accelerating LLM Unlearning via Unified Benchmarking of Methods and Metrics [101.78963920333342]
  We introduce OpenUnlearning, a standardized framework for benchmarking large language models (LLMs) unlearning methods and metrics.<n>OpenUnlearning integrates 9 unlearning algorithms and 16 diverse evaluations across 3 leading benchmarks.<n>We also benchmark diverse unlearning methods and provide a comparative analysis against an extensive evaluation suite.
  arXiv  Detail & Related papers  (2025-06-14T20:16:37Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• LLMpatronous: Harnessing the Power of LLMs For Vulnerability Detection [0.0]
  Large Language Models (LLMs) for vulnerability detection presents unique challenges. Previous attempts employing machine learning models for vulnerability detection have proven ineffective. We propose a robust AI-driven approach focused on mitigating these limitations.
  arXiv  Detail & Related papers  (2025-04-25T15:30:40Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  We propose a unified Test-Time Compute scaling framework that leverages increased inference-time instead of larger models. Our framework incorporates two complementary strategies: internal TTC and external TTC. We demonstrate our textbf32B model achieves a 46% issue resolution rate, surpassing significantly larger models such as DeepSeek R1 671B and OpenAI o1.
  arXiv  Detail & Related papers  (2025-03-31T07:31:32Z)
• LLMs in Software Security: A Survey of Vulnerability Detection Techniques and Insights [12.424610893030353]
  Large Language Models (LLMs) are emerging as transformative tools for software vulnerability detection.<n>This paper provides a detailed survey of LLMs in vulnerability detection.<n>We address challenges such as cross-language vulnerability detection, multimodal data integration, and repository-level analysis.
  arXiv  Detail & Related papers  (2025-02-10T21:33:38Z)
• Causality can systematically address the monsters under the bench(marks) [64.36592889550431]
  Benchmarks are plagued by various biases, artifacts, or leakage.<n>Models may behave unreliably due to poorly explored failure modes.<n> causality offers an ideal framework to systematically address these challenges.
  arXiv  Detail & Related papers  (2025-02-07T17:01:37Z)
• FaithEval: Can Your Language Model Stay Faithful to Context, Even If "The Moon is Made of Marshmallows" [74.7488607599921]
  FaithEval is a benchmark to evaluate the faithfulness of large language models (LLMs) in contextual scenarios. FaithEval comprises 4.9K high-quality problems in total, validated through a rigorous four-stage context construction and validation framework.
  arXiv  Detail & Related papers  (2024-09-30T06:27:53Z)
• Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
  Uncertainty quantification is a key element of machine learning applications.<n>We introduce a novel benchmark that implements a collection of state-of-the-art UQ baselines.<n>We conduct a large-scale empirical investigation of UQ and normalization techniques across eleven tasks, identifying the most effective approaches.
  arXiv  Detail & Related papers  (2024-06-21T20:06:31Z)
• Probabilistic ML Verification via Weighted Model Integration [11.812078181471634]
  Probability formal verification (PFV) of machine learning models is in its infancy. We propose a unifying framework for the PFV of ML systems based on Weighted Model Integration (WMI) We show how successful scaling techniques in the ML verification literature can be generalized beyond their original scope.
  arXiv  Detail & Related papers  (2024-02-07T14:24:04Z)
• LLbezpeky: Leveraging Large Language Models for Vulnerability Detection [10.330063887545398]
  Large Language Models (LLMs) have shown tremendous potential in understanding semnatics in human as well as programming languages. We focus on building an AI-driven workflow to assist developers in identifying and rectifying vulnerabilities.
  arXiv  Detail & Related papers  (2024-01-02T16:14:30Z)
• Testing learning-enabled cyber-physical systems with Large-Language Models: A Formal Approach [32.15663640443728]
  The integration of machine learning (ML) into cyber-physical systems (CPS) offers significant benefits. Existing verification and validation techniques are often inadequate for these new paradigms. We propose a roadmap to transition from foundational probabilistic testing to a more rigorous approach capable of delivering formal assurance.
  arXiv  Detail & Related papers  (2023-11-13T14:56:14Z)
• CodeLMSec Benchmark: Systematically Evaluating and Finding Security Vulnerabilities in Black-Box Code Language Models [58.27254444280376]
  Large language models (LLMs) for automatic code generation have achieved breakthroughs in several programming tasks. Training data for these models is usually collected from the Internet (e.g., from open-source repositories) and is likely to contain faults and security vulnerabilities. This unsanitized training data can cause the language models to learn these vulnerabilities and propagate them during the code generation procedure.
  arXiv  Detail & Related papers  (2023-02-08T11:54:07Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)
• Practical Machine Learning Safety: A Survey and Primer [81.73857913779534]
  Open-world deployment of Machine Learning algorithms in safety-critical applications such as autonomous vehicles needs to address a variety of ML vulnerabilities. New models and training techniques to reduce generalization error, achieve domain adaptation, and detect outlier examples and adversarial attacks. Our organization maps state-of-the-art ML techniques to safety strategies in order to enhance the dependability of the ML algorithm from different aspects.
  arXiv  Detail & Related papers  (2021-06-09T05:56:42Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.