Dieses Kapitel befasst sich mit der Integration des Frameworks zur statischen Wertflussanalyse (SVF) in den Software Verification Competition (SV-COMP) und stellt den ersten Versuch dar, die Fähigkeiten des SVF in diesem Wettbewerbsbereich zu nutzen. SVF, bekannt für seine skalierbare und präzise interprozedurale statische Analyse für LLVM-basierte Sprachen, setzt spärliche und bedarfsgerechte Analysen ein, um Pointer-Alias-Analysen, Speicher-SSA-Formularkonstruktion, Wertflussverfolgung und abstrakte Ausführung durchzuführen. Das Kapitel beschreibt die notwendigen Anpassungen, um SVF mit SV-COMP kompatibel zu machen, einschließlich der Entwicklung eines Adapters, um SV-COMP-Programme und -Eigenschaften in SVF-kompatible Formate zu übersetzen. Es werden auch die dabei aufgetretenen Herausforderungen wie Formatierung und Input- / Output-Probleme sowie die zu ihrer Bewältigung angewandten Strategien diskutiert. Die Bewertung von SVF-SVC in SV-COMP 25 zeigt eine anfängliche vernünftige Leistung bei der Überprüfung echter Eigenschaften, zeigt aber auch Bereiche auf, die verbesserungswürdig sind, insbesondere bei der Behauptung von Unrichtigkeiten und der Handhabung komplexer Schleifen. Das Kapitel schließt mit einer Roadmap für zukünftige Verbesserungen, die sich auf die Verbesserung der Kompatibilität, Präzision und die Generierung umfangreicher Zeugen konzentriert, um eine bessere Validierung und Leistung in späteren Wettbewerben sicherzustellen.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
The Static Value-Flow Analysis Framework (SVF) is a tool that enables interprocedural static value-flow analysis for LLVM-based languages by leveraging sparse and on-demand analysis. This work, SVF-SVC, presents an adaptation of SVF for its debut in SV-COMP 2025. We detail our development which uses SVF as a library to correctly parse SV-COMP program specifications and produce witnesses statements for C programs in the ReachSafety, MemSafety and SoftwareSystems categories. We evaluate SVF-SVC’s performance in SV-COMP 2025 and pave the way for its participation in future editions.
1 Verification Approach
The Static Value-Flow Analysis Framework (SVF) [10] is a tool that enables scalable and precise interprocedural static analysis for LLVM-based languages [6] by leveraging sparse [13] and on-demand analysis. SVF is capable of performing pointer alias analysis [4], memory SSA form construction [11], value-flow tracking [9] and abstract execution for program understanding and memory error checking. SVF performs its analysis by reasoning about properties on a set of graph representations of code. In this value-flow analysis, SVF uses the points-to information generated by Andersen’s pointer analysis [1] to construct an interprocedural memory SSA form, in which the defuse chains of both top-level and address-taken variables are captured. Sparse static analysis on this offers a more scalable solution compared to its non-sparse counterpart. SVF achieves this by first conducting fast pointer analysis that over-approximates value-flows and propagates data-flow facts sparsely along only the pre-computed value-flows instead of all control flow points. SVF also incorporates cross-domain sparse abstract execution [3] that interweaves correlations between values across multiple abstract domains (e.g., memory address and interval domains) by establishing implications of values from one domain to another. This allows SVF to refine spurious alias relations using interval domain information to enhance the precision of interval analysis with refined alias results.
These value-flow results can then be exploited to evaluate the reachability of code sections in the ReachSafety category. Furthermore, memory leak detection can be formulated as a source-sink problem of whether memory allocation will reach a free site across every execution path. By identifying memory allocations as sources and frees as sinks SVF can detect memory leaks in the MemSafety category using its reachability capabilities. Similarly, buffer-overflow errors can be detected by combining reasoning about the reachability of untrusted user input (the source) to array accesses (the sink) and evaluation of the array accesses at this point via abstract execution. This work represents the first attempt to incorporate SVF into the verification competition, despite numerous challenges related to formatting and input/output that needed to be addressed. Fig. 1 contains a high level overview of how SVF operates.
Before our work, the program input formats accepted by SVF were incompatible with the specifications defined in SV-COMP. SVF also did not provide any witness formats which could be validated by an approved validator in SV-COMP. SVF-SVC performs the role of an adapter which correctly translates SV-COMP programs and category properties into an SVF compatible program with appropriate arguments. It then takes the output from SVF and generates format version 1.0 witness statements for SV-COMP. The whole process is shown in Fig. 2.
SVF-SVC performs the adaptation by inspecting input files for non-determinate function declarations and inserting appropriate translations for each function at the start of the C file. After compilation to LLVM-IR using Clang [5], SVF then analyses the LLVM-IR file and produces an SVF verdict to be interpreted by SVF-SVC to generate a valid witness.
Fig. 2.
Program flow of SVF-SVC.
2.1 Reach Safety
Reach safety analysis is performed by wrapping the main function with an assert ensuring a global variable is in its initial state. The reach_error function is overwritten to put the global variable into the error state when reached so that the SVF assert will correctly capture the error. The wrapping technique is summarised in Fig. 3.
Fig. 3.
Wrapper used for reach safety.
2.2 Memory Checks
Memory leaks and double-free checking are done using the SABER [12] component of SVF and by passing the "-leak" and "-dfree" options respectively. SVF-SVC can also test for buffer overflows with abstract execution by passing the "-overflow" flag into SVF. SVF-SVC does not currently support other memory checks in this competition submission.
Anzeige
2.3 Software Systems
This category is simply real-world applications of the other categories. As such, there are no special handlers needed for this category beyond those previously mentioned besides ensuring that SVF-SVC ignores unsupported properties. The aforementioned formatting challenges prevented SVF-SVC from scoring any points in this category.
Whilst SVF-SVC was not the strongest competitor in its debut, a reasonable initial performance was achieved in the verification of true properties. In contrast, SVF-SVC performed weakly in asserting falsities with less than 60% of its claims being correct. The reason behind this is likely due to the conservative over-approximations performed by SVF under the hood. The over-estimation of values produced by abstract execution in theory ensures that if a property is still not violated by the conservative upperbound provided, then it will not be violated by real-world conditions either. However, there could be cases where the over-estimation violates the required properties even though the actual bounds are smaller and non-violating.
Another issue faced was that majority of our correct false claims were unconfirmed due to SVF-SVC not specifying exactly which property was violated, leading to errors with the validators. In a significant portion of test cases SVF-SVC reported UNKNOWN, to some extent due to limitations with the current functionality of SVF but largely due to compatibility issues with SVF-SVC’s wrapper for certain test cases in SV-COMP. In theory SVF-SVC’s approach should be accurate when reporting false statements, however SVF does not currently have the capability to correctly reason about loops with complex conditions as the widening and narrowing rules used to effectively analyse them only work on monotonic conditions. This leads to many incorrect results in the reachability and memory safety categories. Beyond implementing strategies in SVF to handle such cases, accurately identifying these cases for separate handling would reduce the number of erroneous claims made by SVF-SVC.
The largest areas for improvement in future editions would be furthering SVF-SVC’s compatibility in existing categories to support the full functionality of SVF which should reduce the number of UNKNOWN responses of SVF-SVC. Utilising internal representations in SVF to output more extensive witnesses would assist in ensuring the confirmation of correct outputs by validators. A tuning of the efficiency precision tradeoff in SVF for greater precision at the cost of speed would improve results by reducing the numerous incorrect false claims SVF-SVC makes and minimising the high penalties associated with them. Improvements to SVF’s internal implementation to more accurately detect cases where a precise answer is UNKNOWN rather than incorrectly claiming that properties are true or false would also significantly improve SVF-SVC’s score in future editions of SV-COMP.
In the process, it would be hoped that options for greater precision in SVF would allow for stronger real-world performance in cases where users want a low number of false positives in vulnerability detection at the cost of reduced speed and efficiency. In our initial attempt at this year’s SV-COMP, we did not modify the internal implementation of SVF for precision tuning (due to time limitations); however, we plan to enhance SVF for future competitions.
4 Software Project and Contributors
SVF-SVC is available on GitHub [7], and is released under the GNU Affero General Public License version 3. The exact version (1.4) used in the competition is available as a Zenodo archive [8] and can run on Ubuntu 24.04 LTS. The execution of SVF-SVC is as follows:
Where c_file is the program to be tested in the format applicable to SV-COMP. The contributors who adapted SVF for SV-COMP 2025 are the authors of this paper.
Disclosure of Interests
The authors have no competing interests to declare that are relevant to the content of this article.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
