D3.1: Static Code Analysers and Formal Verification Methods (first version)

D3.1: Static Code Analysers and Formal Verification Methods (first version) PROJECT Project Number 101120962 Project Acronym RESCALE Project Title Revolutionised Enhanced Supply Chain Automation with Limited Threats Exposure Start Date 01.10.2023 Programme HORIZON-CL3-2022-CS-01-02 DELIVERABLE Deliverable Type R - Document Report Workpackage WP3 Deliverable Lead PST Editors Sascha Kattelmann, M´at´e Lajk´o Contributors UPRC, UNSPMF Dissemination Level PU - Public Abstract This deliverable outlines the foundational structure and early implementation of the static code analysis and formal verification framework under Task T3.1. The framework, bundled into the Static Code Analysis Module, employs advanced Machine Learning (ML) and Deep Learning (DL) techniques to improve vulnerability detection accuracy while minimizing false positives across diverse programming environments. Formal verification methods test software against modeled safety properties, validating critical behavioral requirements, especially in concurrent and functional systems. Together with symbolic execution for comprehensive path analysis, these methods culminate in the Static Supply Chain component Guarantee (SSCG), which consolidates all testing efforts into a structured report that integrates into the RESCALE platform as a first step to the creation of a Trusted Bill of Materials (TBOM). Disclaimer The information in this document is provided “as is”, and no guarantee or warranty is given that the information is fit for any particular purpose. The content of this document reflects only the author’s view – the European Commission is not responsible for any use that may be made of the information it contains. The users use the information at their sole risk and liability. This project has received funding from the European Union’s Horizon Europe research and innovation programme under grant agreement No 101120962 D3.1: Static Code Analysers and Formal Verification Methods (first version) Document Revision & Quality Assurance Internal Reviewers 1. Daniel Asztalos - (CC) 2. Konstantinos Latanis - (S5) Revisions Version Date Partner Overview 0.1 15/09/2024 PST ToC 0.2 15/11/2024 PST, UPRC, UNSPMF First draft 0.3 21/11/2024 CC, S5 Reviewer comments 0.4 26/11/2024 PST, UPRC, UNSPMF Comments addressed 08.0 27/11/2024 PST Final version 0.9 31/11/2024 ISI, AEGIS Final comments 1.0 13/12/2024 PST Final version RESCALE – PU - Public – Page 2 / 86 Table of Contents 1 Introduction 8 1.1 Scope&Contribution............................... 8 1.2 Relation to Work Packages, Deliverables, and Activities . . . . . . . . . . . . . 8 1.3 Contribution to WP3 and Project Objectives . . . . . . . . . . . . . . . . . . . 8 1.4 DocumentStructure................................ 10 2 State of the Art Analysis 11 2.1 Erlang....................................... 11 2.2 Python....................................... 11 2.3 C/C++....................................... 12 2.4 SymbolicExecution................................ 12 2.4.1 Symbolic Execution Techniques . . . . . . . . . . . . . . . . . . . . . 12 2.4.1.1 Path Exploration . . . . . . . . . . . . . . . . . . . . . . . . 13 2.4.1.2 Constraint Handling and Optimization . . . . . . . . . . . . . 14 2.4.1.3 State Management . . . . . . . . . . . . . . . . . . . . . . . 15 2.4.1.4 Execution Strategies . . . . . . . . . . . . . . . . . . . . . . 15 2.4.1.5 Abstraction........................... 16 2.4.1.6 Path Explosion Mitigation . . . . . . . . . . . . . . . . . . . 17 2.4.1.7 Memory Modeling . . . . . . . . . . . . . . . . . . . . . . . 17 2.4.1.8 Path Prioritization and Heuristics . . . . . . . . . . . . . . . 18 2.4.2 Symbolic Execution Tools . . . . . . . . . . . . . . . . . . . . . . . . 18 3 Static Code Analysis Module 20 3.1 Architecture.................................... 20 3.2 Utilization..................................... 22 3.3 ToolboxOverview................................. 23 4 Development of Static Code Analysers 24 4.1 SAVE-ME: Large Language Models for Static Code Vulnerability Analysis . . 24 4.1.1 CodeBERT ................................ 24 4.1.2 SAVE-ME................................. 27 4.1.3 Integration Into the Static Analysis Module . . . . . . . . . . . . . . . 29 4.1.4 Enhancements over Existing Solutions . . . . . . . . . . . . . . . . . . 30 4.2 SASTer: Static Application Security Tester . . . . . . . . . . . . . . . . . . . . 30 4.2.1 SASTer-GUI ............................... 30 4.2.1.1 Architecture .......................... 31 4.2.1.2 ML/DL Integration . . . . . . . . . . . . . . . . . . . . . . . 33 4.2.1.3 Evaluation Results . . . . . . . . . . . . . . . . . . . . . . . 33 4.2.2 SASTer-CLI................................ 35 4.2.2.1 Architecture .......................... 36 4.2.2.2 Evaluation Results . . . . . . . . . . . . . . . . . . . . . . . 36 4.2.3 Integration Into the Static Analysis Module . . . . . . . . . . . . . . . 37 4.2.4 Enhancements over Existing Solutions . . . . . . . . . . . . . . . . . . 38 4.2.5 Limitations and Future Enhancements . . . . . . . . . . . . . . . . . . 39 4.3 Intelligent Vulnerabilities Exposure Engine (IVEE) . . . . . . . . . . . . . . . 39 4.3.1 Core Components and Functionality . . . . . . . . . . . . . . . . . . . 40 4.3.2 Considerations and Enhancements . . . . . . . . . . . . . . . . . . . . 41 3 D3.1: Static Code Analysers and Formal Verification Methods (first version) 4.4 Efforts Related to RefactorERL . . . . . . . . . . . . . . . . . . . . . . . . . . 41 5 Formal Verification 43 5.1 DetectEr...................................... 43 5.1.1 Hennessy–Milner Logic and Safety Properties . . . . . . . . . . . . . . 44 5.1.2 Application to a Software Update Mechanism . . . . . . . . . . . . . . 45 6 SSCG Design and Generation 47 6.1 Requirements ................................... 47 6.1.1 Test Reporting Format . . . . . . . . . . . . . . . . . . . . . . . . . . 48 6.1.2 Reproducible Testing . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 6.1.3 Classification of Artifacts . . . . . . . . . . . . . . . . . . . . . . . . . 48 6.1.4 Classification of Vulnerabilities and Weaknesses . . . . . . . . . . . . 49 6.2 InitialDesign ................................... 49 6.3 Unification of Test Reports . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 6.4 SARIF....................................... 53 6.4.1 Overview ................................. 53 6.4.2 FormatDetails .............................. 54 6.4.3 ContextinRESCALE........................... 55 6.4.4 SARIFValidation............................. 56 6.4.5 Challenges in Using SARIF for SSCG . . . . . . . . . . . . . . . . . . 56 6.5 SSCGGenerator.................................. 57 7 Main Innovations & Conclusion 59 7.1 MainInnovations ................................. 59 7.2 Conclusion .................................... 59 7.3 FutureWork.................................... 60 7.3.1 Identified Challenges . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 7.3.2 Possible Mitigations & Improvements . . . . . . . . . . . . . . . . . . 61 Appendices 62 A SSCG Example 63 B SARIF Examples 66 B.1 SimpleExample.................................. 66 B.2 SAVE-MEExample................................ 67 B.3 BanditExample.................................. 68 RESCALE – PU - Public – Page 4 / 86 List of Figures 1 RESCALE Components Architecture . . . . . . . . . . . . . . . . . . . . . . . . 9 2 Static Code Analysis Module Architecture . . . . . . . . . . . . . . . . . . . . . . 21 3 Static Code Analysis Module Utilization . . . . . . . . . . . . . . . . . . . . . . . 22 4 An illustration about the replaced token detection objective. Source: [20]. . . . . . 26 5 Overview of the SAVE-ME architecture with pipeline . . . . . . . . . . . . . . . . 28 6 SASTerDashboard .................................. 34 7 SASTerAnalysis ................................... 34 8 SASTerResults .................................... 35 9 SASTerCLI...................................... 37 10 SSCGConcept .................................... 50 11 CycloneDX Attestations Overview . . . . . . . . . . . . . . . . . . . . . . . . . . 51 12 Unification of Analyzer Reports with an Example Set of Analyzers . . . . . . . . . 53 5 D3.1: Static Code Analysers and Formal Verification Methods (first version) List of Abbreviations API Application Programming Interface. 19, 20, 32 BERT Bidirectional Encoder Representations from Transformers. 24 BOM Bill of Materials. 10, 49 CD Continuous Development. 32, 37, 38, 52, 54, 56, 59 CDX CycloneDX. 10, 22, 49–52, 57 CEGAR Counterexample-Guided Abstraction Refinement. 16 CFG Control Flow Graph. 39, 40 CI Continuous Integration. 20, 22, 32, 37, 38, 52, 54, 56, 59 CLI Command Line Interface. 20, 22, 35–38, 56, 57 CVE Common Vulnerabilities and Exposures. 49, 60, 61 CWE Common Weakness Enumeration. 49, 60, 61 DL Deep Learning. 1, 8–11, 14, 20, 23, 33, 38, 39, 41, 42, 52, 53, 59 DSCG Dynamic Supply Chain component Guarantee. 9 ELF Executable and Linkable Format. 40 GUI Graphical User Interface. 30, 35, 38 HML Hennessy–Milner Logic. 23, 44 IoT Internet of Things. 45, 46 IVEE Intelligent Vulnerabilities Exposure Engine. 9, 23, 39–41, 59 JSF JSON Signature Format. 52 JSON JavaScript Object Notation. 21, 32, 36, 48, 51, 53, 54, 56, 57 LLM Large Language Model. 10, 24 LLVM Low-Level Virtual Machine. 19 ML Machine Learning. 1, 8–11, 20, 23, 33, 38, 39, 41, 42, 52, 53, 59 MLM Masked Language Modeling. 25 MVP Minimum Viable Product. 49 RESCALE – PU - Public – Page 6 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) NIST National Institute of Standards and Technology. 56 NLP Natural language processing. 24 NVD National Vulnerability Database. 49 PE Portable Executable. 40 PKI Public Key Infrastructure. 52 RTD Replaced Token Detection. 25 SARIF Static Analysis Results Interchange Format. 31–33, 36–38, 48, 52–57, 59–61 SAST Static Application Security Testing. 30–32, 39 SAVE-ME Static Analysis of Vulnerabilities – Machine Learning Enhancements. 5, 24, 26–30 SBOM Software Bill of Materials. 9, 20, 22, 57, 59, 60 sHML safe Hennessy–Milner Logic. 43–45 SMT Satisfiability Modulo Theories. 14, 19 SotA State of the Art. 11, 12, 20 SSCG Static Supply Chain component Guarantee. 1, 8–10, 20–22, 47–52, 56–59 TBOM Trusted Bill of Materials. 1, 8, 9, 21, 22, 47, 49, 57–59 VM Virtual Machine. 20 XML Extensible Markup Language. 32, 36, 48 RESCALE – PU - Public – Page 7 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) 1 Introduction One of the primary goals of RESCALE is to improve static code analysis and formal verification methods. This includes developing advanced static code analyzers using Machine Learning (ML) and Deep Learning (DL) techniques to enhance accuracy and reduce false positives. The respective task T3.1 also explores formal verification approaches to ensure software security, delivering a comprehensive framework - the RESCALE Static Code Analysis Module - for detecting vulnerabilities effectively. The outcome of the Static Code Analysis Module is then packaged as a Static Supply Chain component Guarantee (SSCG) and sent to other RESCALE infrastructure components which aggregate all information about a software artifact into a Trusted Bill of Materials (TBOM). 1.1 Scope & Contribution This document outlines the results of the first phase of task T3.1 ”Static Code Analysis and Formal Verification”. This phase involves in particular the initial design and prototypical implementation of static code analyzers, exploration of formal verification approaches, as well as the SSCG Generator and the overall construction and usability of the Static Code Analysis Module. 1.2 Relation to Work Packages, Deliverables, and Activities Deliverable D3.1 represents the first outcome of Task 3.1 within Work Package 3 (WP3) and is also pertinent to Work Packages 4 (WP4) and 5 (WP5). This deliverable describes the architecture and tooling associated with the Static Code Analysis Module, with specific integration aspects linked to WP5. Additionally, Task 3.1 defines the SSCG report, which is a first building block towards producing a TBOM in WP4. 1.3 Contribution to WP3 and Project Objectives The RESCALE workflow consists of essentially three major steps leading to the creation of a TBOM. The very first step of the workflow is about an entity statically testing source code of a software project and assembling results and findings into a document called SSCG. This entity is called the ’Producer’ in the context of RESCALE roles (see D2.5). Typically the Producer is in some way the ‘owner’ of the respective software project, for example a commercial organization which distributes the software as compiled package or the maintainer of an open source project. The static testing of source code happens within the Static Code Analysis Module which incorporates sets of different tools for different technology stacks. Based on a certain configuration these tools are executed on the source code of the software project. While many tools are generically executable on any source code of a specific programming language, there are also tools which need project specific configuration as further information is needed to test for certain characteristics of the software. RESCALE – PU - Public – Page 8 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) The resulting SSCG can be published by the Producer along a Software Bill of Materials (SBOM) to the RESCALE infrastructure. Here it can be picked up by a different entity called the ‘Consumer’ (D2.5) of the software project for the second step of the RESCALE workflow, the dynamic testing (D3.3) which can also involve specific hardware testing (D3.5) and even interactions with operating system kernels (D3.7). Results of the dynamic testing are assembled into a Dynamic Supply Chain component Guarantee (DSCG) and also sent to the RESCALE infrastructure where finally the TBOM (D4.1) is created as the third and last step of the RESCALE workflow. In D2.5 a high level architecture was presented to reflect on this workflow (see figure 1). Dynamic Testing module Management module TrustOR Communication mechanisms Trust Storage Repositories Low Level Hardware Assessment Dynamic HW Analyzer Static code analysis module Static Code Analyzer Formal Verifier Standardization Guidelines (CVE/CWE) Security Assurance TBOM Generator TBOM Validator Dashboard External git Repositories SSCG Dynamic Software Testing Ledger Infrastructure SSCG Generator DSCG Generator Auth / IAM State manager Ledger Adapter DSCG TBOM Assessment Domain Security & Trust Domain Management Domain Figure 1: RESCALE Components Architecture T3.1 incorporates a range of Machine Learning (ML)/Deep Learning (DL) tools to enhance the accuracy and efficiency of vulnerability detection for software projects. Key tools include CodeBERT, which applies transformer-based models for source code analysis, and SAVE-ME, which fine-tunes CodeBERT for detecting specific vulnerabilities in Erlang code. Additionally, the SASTer tool combines ML-enhanced static analysis for Python and C/C++, reducing false positives and providing more precise insights into potential security issues. Within RESCALE, formal verification is used in two different flavors, in the context of verification of execution traces and in the context of symbolic execution. For the verification of traces, the tool DetectEr is used. However, the main focus here is to create formal models which can be used for the actual verification of traces for the Erlang programming language. Regarding symbolic execution, a new tool based on the angr platform [70], the Intelligent Vulnerabilities Exposure Engine (IVEE), will be presented. RESCALE – PU - Public – Page 9 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) •Dynamic Symbolic Execution: Also known as dynamic symbolic testing, this approach combines symbolic execution with runtime information to handle dynamic behaviors and external interactions. By adapting to the runtime context, it improves path coverage and uncovers complex bugs. Concolic execution or hybrid execution is a specific form of dynamic symbolic execution. It runs the program with concrete inputs while simultaneously performing symbolic analysis. This hybrid method is particularly effective for generating inputs that expose subtle bugs. The work by Yun et al. [84], introduces QSYM, an optimized concolic execution engine designed for hybrid fuzzing, addressing performance bottlenecks in traditional concolic execution. Another study by Jaffar et al. [33], presents a novel system that uses interpolation techniques to tackle the path explosion problem, enhancing the scalability of dynamic symbolic execution. Lastly, Vishnyakov et al. [79] highlights performance improvements in dynamic symbolic execution by optimizing symbolic formula simplification and skipping non-symbolic instructions, demonstrating superior efficiency. •Selective Symbolic Execution: This strategy focuses symbolic execution on specific parts of the program, such as functions or modules that are critical or prone to errors. By narrowing the scope, it reduces computational overhead and enhances scalability. The study by He et al. presents a technique for selective symbolic execution, targeting specific program components to improve efficiency [28]. Execution strategies are critical for balancing the thoroughness of analysis with computational efficiency. These strategies tailor symbolic execution to prioritize paths most likely to reveal significant insights. 2.4.1.5 Abstraction Abstraction techniques are employed to simplify complex program structures and data, making analysis more tractable. By abstracting certain elements, these techniques reduce the state space and computational overhead, enhancing the efficiency of symbolic execution. Some abstraction techniques are explained below in detail: •Predicate Abstraction: This method abstracts program states by mapping them to a finite set of boolean expressions, known as predicates. By focusing on these predicates, the analysis becomes more manageable. The work by Jon´ aˇ s et al. [35] introduces a technique that combines symbolic execution with predicate abstraction and CounterexampleGuided Abstraction Refinement (CEGAR) to improve the effectiveness of symbolic execution in proving unreachability. •Symbolic Summarization: Symbolic summarization involves creating concise representations of program components, such as functions or loops, capturing their behavior without delving into detailed execution paths. This technique allows symbolic execution to handle complex programs more efficiently by focusing on high-level summaries. The study by Boudhiba et al. [7] presents a method for symbolic execution of transition systems using function summaries, which are logical formulas built from concrete values describing representative input and output data tuples of the function. RESCALE – PU - Public – Page 16 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) •Interpolant Generation: Interpolant generation is used to derive intermediate assertions, known as interpolants, that summarize the effect of a sequence of program statements. These interpolants help in refining abstractions and guiding the symbolic execution process. The study by Jaffar et al., mentioned in subsection 2.4.1.4 [33], which introduced TracerX, was build using interpolation to address the path explosion problem. Abstraction techniques simplify complex program behaviors, improving both the precision and performance of symbolic execution. This allows for a broader application of symbolic execution in complex system analysis. 2.4.1.6 Path Explosion Mitigation The path explosion problem arises when the number of execution paths grows exponentially due to program complexity, loops and conditionals. This rapid growth can overwhelm computational resources, making exhaustive analysis impractical. Several mitigation techniques have been developed designed to tackle this specific issue faced in symbolic execution: •Parallel Path Exploration: This technique involves distributing the exploration of execution paths across multiple processors or machines. By parallelizing the workload, symbolic execution can handle a larger number of paths simultaneously, reducing the time required for analysis. The work by Karna et al. [37] introduces a parallel symbolic execution framework that effectively distributes path exploration tasks, enhancing scalability. Additionally, Ryan et al., [65] propose a modular approach where independent components of hardware designs are explored separately and reused, effectively addressing path explosion through parallel composition strategies. •Work Stealing: In dynamic parallel execution environments, work stealing allows idle processors to take over tasks from busy processors. This load-balancing strategy ensures efficient utilization of computational resources during symbolic execution. The study by Wen et al. [81] presents a work-stealing scheduler designed for parallel symbolic execution, demonstrating significant performance improvements. Tackling path explosion is vital for symbolic execution’s success in real-world scenarios. Techniques like selective exploration ensure that computational resources are allocated efficiently without compromising analysis depth. 2.4.1.7 Memory Modeling Accurately modeling memory in symbolic execution is crucial for analyzing programs that utilize complex data structures and pointer manipulations. Effective memory modeling ensures that symbolic execution can handle various memory operations, including dynamic allocations and pointer arithmetic. Some techniques are analyzed below: •Precise Memory Modeling: This approach aims to accurately represent the program’s memory state, including complex data structures and pointer relationships. By maintaining a detailed model of memory, symbolic execution can precisely track variable values RESCALE – PU - Public – Page 17 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) and detect subtle errors. Borzacchiello et al., [6] discuss key ideas and new thoughts on memory models in symbolic execution, highlighting the importance of precise memory modeling. •Simplified Memory Models: To improve performance, some symbolic execution tools use simplified memory models that abstract certain details of the memory state. While this can enhance scalability, it may reduce the precision of the analysis. Kapus et al., [36] presented a segmented memory model for symbolic execution, which reduces forking due to symbolic pointer dereferences, often completely, thereby decreasing execution time and memory usage. Effective memory modeling enables symbolic execution to handle dynamic data structures and low-level operations. This extends the applicability of symbolic execution to programs with complex memory interactions, ensuring thorough analysis. 2.4.1.8 Path Prioritization and Heuristics Efficiently exploring the vast number of possible execution paths is crucial. Path prioritization and heuristics guide the exploration process, focusing on paths that are more likely to uncover errors or achieve higher code coverage. Key strategies include: •Coverage-Guided Execution: This approach prioritizes paths that are expected to increase code coverage, ensuring that untested parts of the program are explored. By focusing on less-explored paths, this heuristic enhances the thoroughness of testing. The study by Cha et al. [13] introduces a technique that automatically generates search heuristics for dynamic symbolic execution, improving coverage by learning from previous explorations. •Bug-Focused Heuristics: These heuristics prioritize paths that are more likely to contain bugs, such as those involving complex conditions or known vulnerable patterns. By directing exploration towards these paths, the efficiency of bug detection is enhanced. The research by Ruaro et al. [64] presents SyML, a system that guides symbolic execution toward vulnerable states through pattern learning, effectively focusing on bug-prone paths. Guided by heuristics, path prioritization enhances symbolic execution by targeting paths likely to reveal vulnerabilities. This approach streamlines the analysis and accelerates vulnerability detection. 2.4.2 Symbolic Execution Tools Symbolic execution has led to the development of various tools designed to analyze and test software systems. These tools differ in their capabilities, target platforms and applications. Below is an overview of some prominent symbolic execution tools: RESCALE – PU - Public – Page 18 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) •KLEE: Built on the Low-Level Virtual Machine (LLVM) compiler infrastructure, KLEE is an open-source symbolic execution engine that automatically generates high-coverage tests for complex systems programs [10]. It has been instrumental in detecting bugs and verifying software correctness. •Manticore: Developed by Trail of Bits [55], Manticore is a symbolic execution tool capable of analyzing smart contracts and binaries [53]. It offers features like program exploration, input generation, error discovery and a programmatic interface via a Python API. •Maat: Also from Trail of Bits [55], Maat is an open-source dynamic symbolic execution and binary analysis framework [54]. It provides functionalities such as symbolic execution, taint analysis, constraint solving, binary loading and environment simulation. Maat leverages Ghidra’s SLEIGH library for assembly lifting. •Triton: Triton is a dynamic binary analysis framework that provides robust symbolic execution capabilities [66]. It supports taint analysis, dynamic symbolic execution and program analysis for binary-level programs. •Angr: Angr is a powerful binary analysis platform that combines symbolic execution with other analysis techniques like CFG recovery, taint analysis and more [21]. It’s widely used for vulnerability discovery in complex binaries. •CrossHair: CrossHair is an analysis tool for Python that blurs the line between testing and type systems [75]. It works by repeatedly calling functions with symbolic inputs, using an SMT solver to explore viable execution paths and find counterexamples. CrossHair supports symbolic reasoning for built-in types, user-defined classes and much of the standard library, making it a comprehensive tool for Python code analysis. •Sydr: Sydr is a dynamic symbolic execution tool that combines DynamoRIO dynamic binary instrumentation with the Triton symbolic engine. It introduces performance and accuracy improvements, such as skipping non-symbolic instructions and path predicate slicing, to enhance symbolic execution efficiency. •Symbooglix: Symbooglix is a symbolic execution tool for Boogie programs, facilitating the analysis and verification of programs written in the Boogie intermediate verification language [43]. •OSS-Sydr-Fuzz: OSS-Sydr-Fuzz is a hybrid fuzzing tool for open-source software that combines symbolic execution with fuzzing techniques to improve vulnerability detection [76]. These tools exemplify the diverse applications of symbolic execution in software analysis, testing and verification. They cater to various programming languages, platforms and analysis needs, contributing significantly to the advancement of software reliability and security. RESCALE – PU - Public – Page 19 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) 3 Static Code Analysis Module The RESCALE static code analysis module processes software projects, specifically their source code and the SBOM associated with it, to identify and assess potential security vulnerabilities and weaknesses. It employs advanced ML and DL enhanced static code analyzers, which go beyond traditional methods to detect issues more effectively. The ML/DL components play a crucial role in reducing false positives, enhancing the accuracy of the analysis compared to traditional static analysis tools. A key benefit of this module is that it aggregates these analyzers in a unified way. In the current State of the Art (SotA), every static code analysis tool typically needs to be handled uniquely since there is no standardized Application Programming Interface (API), which complicates the evaluation process. By providing a streamlined interface, the RESCALE module simplifies interaction with various analyzers, enhancing user experience and efficiency. Reflecting on the envisioned workflows from D2.5, RESCALE will initially design this module as a container, making it compatible with common Continuous Integration (CI) systems. Within these CI systems, source code typically gets injected at runtime, allowing the module to automatically assess the code as part of the development pipeline. While the module is designed to be containerized for easy integration, its architecture remains independent of the containerized approach, ensuring flexibility and adaptability for various deployment environments (for example using a Virtual Machine (VM) based approach). The outcome of the analysis is the SSCG, a detailed report that includes the types of tests performed, their results, the identity of the evaluator, the version of the assessed asset etc. The SSCG is generated using a newly developed piece of software, the SSCG Generator, and it can be published to the management module for further processing or just stored locally for inspection without exposing information to the public. 3.1 Architecture Figure 2 outlines the architecture of the RESCALE static code analysis module, highlighting its self-contained design and integration with key components. The process starts with the Software Repository, containing the source code and the SBOM. Configuration Management sets up the container runtime environment based on specified settings, and the Execution Engine initiates the static code analysis using the configured analyzers. A key feature of this module is its ability to aggregate multiple static analyzers. Each analyzer is enclosed in a RESCALE Wrapper, which provides a standardized interface. In its simplest form, the RESCALE Wrapper might just be a shell script that carries the name of the targeted static code analyzer, offering a Command Line Interface (CLI) to start the analyzer with a default set of options. This approach addresses the common issue of handling each static analysis tool uniquely due to the lack of standardized APIs. It might be of interest later on to augment this API with additional capabilities to stop the analysis or track its progress. While RESCALE hasn’t yet settled on a specific test output format, the wrapper must transform the analyzer’s output to include how the analyzer was invoked, ensuring reproducibility of RESCALE – PU - Public – Page 20 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) Figure 2: Static Code Analysis Module Architecture findings. It also needs to detail the vulnerabilities and weaknesses identified, which is crucial for supporting the TBOM lifecycle as explained in D4.1, where a score-based process is used to evaluate the status of an asset with a TBOM. Additionally, the wrapper should attach a more detailed report about the code locations and how different findings might relate to each other, enhancing the depth of analysis. The wrapper output is expected to be in JavaScript Object Notation (JSON) format, aligning with the SSCG’s design as a JSON document. This consistency in format simplifies the integration of outputs into the overall analysis process and facilitates further processing. The module uses an initial set of configuration parameters (given as environment variables) to manage the analysis process. These parameters are likely subject to change during WP5 integration activities. •USER ACCESS TOKEN: A user access token for secure communication with the RESCALE Management Module (e.g., “abc123token”). This token is processed by the SSCG Generator, which acts as a client of the management module, ensuring that only authorized users can publish analysis results. •LANG INFO: Specifies the programming languages used in the source code (e.g., “Python 3.10, Erlang 24, C11”). The Execution Engine maintains a mapping between this information and the respective analyzers, ensuring that the correct tools are used for each language (or technology) specified in the configuration. •SRC PATH: A list of source code file locations (e.g., “./src/*”). This parameter guides the module to the directories where the source code is located, allowing it to identify the files to be analyzed. •DRY RUN: A flag to control whether the analysis is a “dry run” (e.g., “true” or “false”). When set to “true,” the analysis results are stored locally without publishing to the RESCALE Management Module. When set to “false,” the module can publish the results, depending on the configuration. RESCALE – PU - Public – Page 21 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) •SBOM PATH: The location of the SBOM file (e.g., “/path/to/sbom”). This path provides the necessary input for the analysis, allowing the module to use the SBOM in conjunction with the source code for a comprehensive evaluation. After executing the static analysis, the results are sent to the SSCG Generator, where the SSCG, formatted as a CDX document (as discussed in D4.1), is compiled. Afterwards, the CycloneDX CLI tool [56] validates the SSCG to ensure its compliance with the CycloneDX specification. Depending on the module configuration, the SSCG Generator will either publish the SSCG to the RESCALE Management Module or store it locally as a CI artifact during a dry run, preserving privacy and control over the information. 3.2 Utilization Figure 3 illustrates the utilization of the RESCALE static code analysis module within a producer test infrastructure, showing how various components interact to enable the analysis of source code and the generation of an SSCG. The process begins with the download or update of the static code analysis module from the module repository, ensuring it is up-to-date with the latest analyzer updates. Then, configuration settings are ingested to define parameters for the analysis, such as programming language settings. The source code, optional other assets subject to static testing (like compiled binaries), and the SBOM which is stored in the code repository, are injected into the static code analysis module, which processes these inputs to identify vulnerabilities and weaknesses and generates the SSCG with relevant details. Once the SSCG is generated, it can be published to the management module for further processing towards the TBOM. In the case of a dry run, the SSCG can be kept locally within the producer’s test infrastructure without being published. Figure 3: Static Code Analysis Module Utilization This approach offers several advantages. First, it allows for the use of a generic static code analysis module that can be applied to any software under test, regardless of the programming language or its version. While it may still be beneficial to create specialized modules for different programming languages to optimize the analysis, the generic module provides a flexible and versatile solution. Additionally, the module is compatible with existing CI infrastructure, RESCALE – PU - Public – Page 22 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) enabling seamless integration into current development workflows without the need for extensive changes or adaptations. An approach involving static code analysis modules specific to the software being tested is not feasible, as it would require the RESCALE infrastructure to generate such modules on demand for each software project. 3.3 Toolbox Overview The Static Code Analysis Module incorporates several tools to deliver security insights across multiple programming languages, enhanced with ML/DL capabilities to reduce false positives, prioritize findings, and improve code coverage. SASTer, a bundle of static analysis tools, is tailored for Python and C/C++. It leverages machine learning to identify security issues and other problems in the codebase under analysis. Further RESCALE project leverages CodeBERT, a transformer-based language model adapted to code, to enhance vulnerability detection by understanding complex code structures and relationships. SAVE-ME, a new tool developed in RESCALE, builds upon CodeBERT, fine-tuning it specifically for identifying vulnerabilities in Erlang code. DetectEr is a runtime verification tool for Erlang, designed to monitor system behaviors and detect concurrency issues like race conditions. Utilizing Hennessy–Milner Logic (HML), DetectEr specifies safety properties and validates system actions against these properties in realtime, without the need for exhaustive formal verification, offering a pragmatic way of error detection under real-world conditions. Within RESCALE there will be safety properties developed for e.g., a software update mechanism. The Intelligent Vulnerabilities Exposure Engine (IVEE) in RESCALE leverages symbolic execution to provide a thorough assessment of software components, going beyond standard syntactical analysis. By systematically exploring all possible execution paths with symbolic inputs, IVEE verifies code against specified properties, identifying vulnerabilities that conventional tools may overlook. Built on the angr platform, IVEE benefits from angr’s capabilities for analyzing binary code and navigating complex control flows, making it effective in assessing compiled applications and low-level vulnerabilities. Each of these tools is described in greater detail in their respective sections later in the document. RESCALE – PU - Public – Page 23 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) 4 Development of Static Code Analysers Traditional static analysis tools for detecting vulnerabilities in source code often rely on rulebased approaches or pattern matching. While these methods can identify certain types of vulnerabilities – here broadly referring to weaknesses, deficiencies, or other issues in code – they are limited by their predefined rules and struggle with the complexity and evolving nature of modern programming languages. Additionally, static analysis tools often fail to capture subtle issues that arise from context-dependent code behavior, which is particularly important in functional and concurrent programming languages like Erlang. This section describes two approaches for static analysis within RESCALE: Static Analysis of Vulnerabilities – Machine Learning Enhancements (SAVE-ME) based on Large Language Models (LLMs) (Section 4.1), and Static Application Security Tester (SASTer), a modular extensible platform for streamlining the process of analyzing source code (Section 4.2). In addition, our initial efforts regarding RefactorERL, an advanced tool designed for static analysis and refactoring of Erlang code, are discussed in Section 4.4. 4.1 SAVE-ME: Large Language Models for Static Code Vulnerability Analysis Large Language Models (LLMs) such as CodeBERT [20] offer a powerful alternative and enhancement to traditional static code analysis tools. LLMs can be pretrained on large amounts of source code to learn both syntax and semantic structures, allowing them to recognize a broader range of vulnerabilities and patterns that go beyond simple rule-based detection. By fine-tuning these models on specific datasets, we can enhance their ability to identify security vulnerabilities in a given language. For this part of the Static Code Analysis Module, we focus on classifying vulnerabilities in Erlang source code. Erlang’s unique features introduce specific security challenges that are not as prevalent in other languages. Traditional static analysis tools may not be fully equipped to handle these challenges, making a machine learning-based approach like CodeBERT particularly valuable. Our tool, called Static Analysis of Vulnerabilities – Machine Learning Enhancements (SAVE-ME), is based on an LLM architecture, specifically CodeBERT. 4.1.1 CodeBERT CodeBERT is a transformer-based model designed specifically for source code understanding. It is based on the Bidirectional Encoder Representations from Transformers (BERT) [17] architecture, which was originally designed for natural language processing (NLP). The transformer architecture forms the backbone of CodeBERT and is highly suited for processing structured data like source code because of its ability to model long-range dependencies and capture contextual information in a bidirectional manner. Key components of the transformer architecture are the following: RESCALE – PU - Public – Page 24 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) • At the heart of the transformer is the self-attention mechanism, which allows the model to weigh the importance of each token (word or code token) relative to the others in the input sequence. A token is a unit of text, such as a word, symbol, or code element, that the model uses as its smallest building block for analysis. For source code, tokens include keywords (e.g., if, else), operators, identifiers, and even special characters or delimiters. The process of tokenization involves breaking down the input code into these discrete components, allowing the model to systematically process and analyze the sequence. This is important for understanding source code because dependencies between variables or function calls can occur at different parts of the code, often far apart. The self-attention mechanism allows CodeBERT to capture these dependencies and contextual relationships effectively. • CodeBERT’s transformer model is bidirectional, meaning it processes the entire input sequence in both directions (left-to-right and right-to-left). For code understanding, this is particularly beneficial because it enables the model to understand the relationships between code tokens, function names, arguments, and control flow structures, leading to more robust representations of code. • CodeBERT breaks down source code into tokens and embeds them into high-dimensional vectors. This embedding captures both syntactic and semantic information, allowing the model to learn the relationships between keywords, variables, and operations. The choice of a transformer architecture is motivated by its ability to process complex, structured data efficiently. CodeBERT employs two pre-training objectives, the Masked Language Modeling (MLM) and the Replaced Token Detection (RTD): • Masked Language Modeling (MLM): In this objective, a random subset of token positions is selected in both natural language (NL, e.g., code documentation) and programming language (PL) sequences. These positions are replaced with a special mask token. The model is then trained to predict the original tokens that were masked, enabling it to learn contextual representations of the input sequences. • Masked Language Modeling (MLM): For this objective, some tokens in the original NL and PL sequences are randomly masked. A generator model, which is similar to an ngram probabilistic model, replaces the masked tokens with predictions. Subsequently, a discriminator model is trained to identify whether a given token is the original token or a replacement. This task is framed as a binary classification problem. Both NL and code generators are language models, which generate plausible tokens for masked positions based on surrounding contexts. NL-Code discriminator is the targeted pre-trained model, which is trained via detecting plausible alternatives tokens sampled from NL and PL generators. NL-Code discriminator is used for producing general-purpose representations in the fine-tuning step. Both NL and code generators are are thrown out in the fine-tuning step [20]. An illustration of RTD is shown in Figure 4. CodeBERT’s architecture is particularly suited for downstream tasks like vulnerability classification because of its pre-training objectives and modular design. During pre-training, CodeBERT learns to predict masked tokens and identify relationships between code snippets, equipping it with a deep understanding of syntax and semantics across multiple languages. This RESCALE – PU - Public – Page 25 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) •Backend System: The Backend System manages the core logic and operations of the platform, acting as the processing layer between the Web Interface and the Analysis Modules. Built using Flask [62] and Flask-SQLAlchemy [63], it is responsible for the following: –User Authentication and session management: Verifies user credentials, manages secure login/logout workflows and maintains active user sessions. –Project Orchestration: Manages project uploads, triggers analysis jobs and coordinates results processing with the analysis modules. –Database Management: Stores user credentials, project metadata and tool configurations in a relational database using Flask-SQLAlchemy [63]. –RESTful API Services: Provides endpoints to facilitate communication between the Web Interface and the backend, ensuring smooth data exchange. •Modules: Each SAST tool or module, as is called inside SASTer, is encapsulated within its own Docker container, ensuring isolation since tools run independently and avoiding conflicts or interference. Moreover, the dockerization ensures consistency since tool environments are standardized and reproducible. Each tool is integrated through a consistent modular structure comprised of the following components: –Dockerfile: Defines the containerized environment for the tool, including its dependencies, configurations and execution commands. –Loader Script: Initializes and dynamically loads the tool into the system. –Analysis Script: Executes static analysis using environment-specific parameters. –Result Handler: Retrieves and processes the output, converting it to SARIF if necessary. •Result Standardization: Results are standardized into SARIF, either natively or through custom conversion mechanisms, such as scripts that transform JSON or XML output to SARIF. Most if not all static code analyzers support either JSON or XML output format. This ensures compatibility with external tools and CI/CD pipelines. The process of analyzing source code with SASTer is designed to be intuitive and efficient. Below, we outline the key steps (workflow) users follow to interact with the platform and conduct their code analysis: 1. Logging In: Users begin by logging into SASTer using their credentials. If they don’t have an account, they must create one. 2. Creating a Project: After logging in, users create a project where their code files will be analyzed. 3. Uploading Code Files: Users upload their source code files to the created project through the web-based interface. 4. Automatic Tool Selection and Execution: Based on the uploaded file types (e.g., .py, .c, .js), SASTer automatically identifies the appropriate analyzers for the programming languages detected. The system then spawns the necessary Docker containers to execute these tools. RESCALE – PU - Public – Page 32 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) 5. Processing and Standardizing Results: Once the analysis is complete, SASTer retrieves the results from each tool. If required, custom scripts are used to convert the output into the standardized SARIF format. 6. Reviewing Results: The processed results are displayed on the user’s dashboard, providing clear insights into identified vulnerabilities and enabling users to address potential issues effectively. This structured process ensures that users can efficiently analyze their code for vulnerabilities with minimal effort. 4.2.1.2 ML/DL Integration SASTer plans to incorporate ML and DL techniques to further enhance the accuracy and efficiency of its static analysis processes. These planned advancements aim to reduce false positives, eliminate duplicate results and provide actionable guidance to users for addressing vulnerabilities. Once implemented, the ML/DL modules will parse analyzer outputs post-processing, identifying redundant findings and suppressing less critical issues to present users with a prioritized and refined list of vulnerabilities. This will ensure that developers can focus on resolving the most significant security concerns efficiently. Additionally, code recommendations will be generated, assisting users in fixing vulnerabilities. By integrating ML/DL methods into SASTer, the tool will streamline the analysis process and empower developers with precise and actionable insights, marking a significant step forward in static application security testing. 4.2.1.3 Evaluation Results SASTer has undergone thorough evaluation to ensure its robustness, efficiency and accuracy in performing static application security testing. The tool has been rigorously tested across a diverse range of source code files, encompassing programming languages such as Python, C, C++ and JavaScript. This comprehensive testing process has demonstrated SASTer’s ability to seamlessly integrate and execute a variety of static code analyzers, consistently delivering actionable and standardized results. The evaluation process has confirmed the tool’s capability to accurately detect security vulnerabilities, ensuring developers can trust the results provided. Each supported analyzer has been validated in its dockerized environment to guarantee reliable and consistent performance across supported languages. Additionally, SASTer’s automated workflows and SARIF standardization have been shown to significantly streamline the analysis process, reducing manual effort and improving the overall efficiency of software security assessments. To provide a clearer understanding of SASTer’s functionality and user experience, the figures below showcase key components of the platform. RESCALE – PU - Public – Page 33 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) Figure 6: SASTer Dashboard Figure 6 highlights the SASTer dashboard, which provides users with an overview of their projects. This interface includes information about created projects and the status of ongoing or completed analyses. Figure 7: SASTer Analysis Figure 7 shows the page users encounter after starting the analysis of their code. Here, users can monitor the execution of selected tools on their uploaded files. This screen provides updates on the status of the analysis, ensuring transparency and allowing users to track the progress of their static code analysis. RESCALE – PU - Public – Page 34 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) Figure 8: SASTer Results Figure 8 presents the results interface, where users can view identified vulnerabilities after an analysis is completed. This screen organizes results in a structured format, presenting the severity and type of vulnerabilities. 4.2.2 SASTer-CLI The SASTer CLI tool provides a streamlined and flexible alternative to the GUI version, allowing users to perform static code analysis directly from the terminal. Designed for both automation and efficiency, the CLI tool offers SASTer’s capabilities to users who prefer or require command-line workflows. The tool supports online and offline modes. The online mode, still under development, will connect in the future to a SASTer live instance, leveraging most of the tools features, such as containerized static analyzers, etc. It simply provides a way to access SASTer’s full capabilities without using the GUI, relying instead on command-line operations for flexibility, automation and integration on existing workflows. On the other hand, the offline mode, which is currently operational, enables direct integration of static analyzers within a user’s environment, focusing on essential functionality such as running supported tools and generating standardized outputs. The offline mode works locally, without the need to connect to the live service or even go online. The only requirement is that the static code analyzers are already installed on the user’s system. The offline mode shares many of the core advantages of the SASTer GUI version, such as a modular architecture and the ability to easily incorporate additional analyzers. However, the offline mode is more lightweight by design, omitting some of the advanced features of the GUI version. For instance, while the GUI version includes containerized analyzers for streamlined deployment, the CLI tool’s offline mode relies on direct integration of the analyzers within the RESCALE – PU - Public – Page 35 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) user’s environment, offering a more manual but flexible approach. 4.2.2.1 Architecture This section describes the architecture of the offline mode of the SASTer CLI tool, as it is the currently operational mode. It details the structural design and components that enable the tool to integrate static analyzers, execute scans and produce standardized outputs locally within a user’s environment. The architecture of the SASTer CLI tool’s offline mode is designed to provide a modular and efficient framework for static code analysis. The core components that interact to perform static code analysis are described below: •Command Processing: The CLI acts as the primary interface, interpreting user commands to initiate actions, such as scanning code files. SASTer-CLI uses “argparse” to handle commands (e.g., scan, version), a Python library used for parsing command-line arguments, thus ensuring appropriate workflows are executed. •Configuration Management: The CLI tool manages runtime settings through a structured configuration mechanism. These configurations define parameters such as logging levels and output preferences. The configuration is loaded via the “config.ini” file (and falls back to defaults if the file is absent). •Logging Mechanism: The CLI tool includes a robust logging mechanism to provide detailed feedback on execution processes. It supports multiple severity levels (e.g., informational, warning, error) to ensure users are well-informed about operations and any potential issues. This is handled by the The “logger” module. •Static Analyzer Integration: The SASTer CLI tool’s offline mode uses a modular approach for integrating static code analyzers. Static analyzers are integrated as independent modules, each responsible for its own initialization and execution. While not formalized under a strict interface, this design ensures flexibility in supporting different analyzers. The approach simplifies the addition of new analyzers and provides support for diverse programming languages. •Execution Engine: The execution engine coordinates the scanning process by invoking analyzers on the source code provided by the user. It ensures that analyzers are executed efficiently and their outputs are collected for further processing. •Result Generation: Results can be generated in various formats, including SARIF. For analyzers that do not natively support SARIF, the offline mode employs parsers to convert JSON or XML outputs that many analyzers support into SARIF, maintaining uniformity. 4.2.2.2 Evaluation Results The evaluation of the SASTer CLI tool focused on its offline mode, assessing its effectiveness in executing static code analysis. The tool was tested across diverse codebases using its currently RESCALE – PU - Public – Page 36 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) supported analyzers. At this moment, the offline mode supports Flawfinder, Bandit, Semgrep, Bearer, Horusec and Cppcheck, thus it can scan python and C/C++ codebases. The lightweight design and command-line-driven workflow proved effective for integration into automated environments, such as CI/CD pipelines, with minimal setup. To run a scan using the offline mode, the command is: python3 saster - cli.py scan --offline \ -m Bandit , Flawfinder , Semgrep , Horusec \ -o results . sarif project -- verbose Figure 9: SASTer CLI Figure 9 shows the SASTer CLI tool performing a scan in offline mode, utilizing multiple static analyzers, including Horusec, Bandit, Flawfinder and Semgrep. The respective versions and configurations of the analyzers are logged for transparency. The tool processes the provided project directory and outputs SARIF-compliant results for each analyzer. One of the SARIF outputs can be found in B.3. The verbose mode enhances visibility into the execution process, confirming successful initialization, execution and result generation for all modules. 4.2.3 Integration Into the Static Analysis Module The SASTer CLI tool, along with its dependencies and analyzers, is packaged in a lightweight container image based on a Debian slim distribution, ensuring minimal overhead while maintaining functionality. RESCALE – PU - Public – Page 37 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) The Docker-based integration automates the setup of the required environment, including the installation of static analyzers such as Flawfinder, Semgrep, Bandit, Horusec, Bearer and Cppcheck. These analyzers are installed alongside the code of the SASTer CLI, enabling the execution of comprehensive static code analysis within the container. To integrate the tool, the source code is included as part of the Docker build process and placed in a dedicated directory within the container. This containerized approach allows the SASTer CLI to be integrated into the Static Code Analysis Module with minimal configuration. The SASTer container can be invoked using the following command: sudo docker run \ -v $(pwd)/ project :/ saster - tool / project \ -v $(pwd)/ results :/ saster - tool / results \ saster -cli: latest \ saster -cli scan --offline -m Bandit , Flawfinder , Semgrep ,Horusec -o / saster - tool / results / results . sarif --verbose This command mounts the project folder in the current directory into the container’s /sastertool/project directory, which contains the source code to be analyzed. Similarly, it mounts the results folder into the container’s /saster-tool/results directory, where the output files will be saved. The “saster-cli:latest” image specifies the Docker image to run. Inside the container, the “saster-cli” command is executed in offline mode, using the analyzers Bandit, Flawfinder, Semgrep and Horusec. 4.2.4 Enhancements over Existing Solutions SASTer represents a significant advancement over traditional static code analysis solutions by addressing their limitations and introducing innovative features designed to enhance usability, accuracy and extensibility. One of the primary innovations of SASTer is its modular architecture, both for the GUI and CLI version which allows seamless integration of multiple analyzers. The architecture simplifies the incorporation of more analyzers while also making updates to existing ones easy. Another key detail is the adoption of SARIF for output standardization. By converting the diverse outputs of integrated tools into SARIF, SASTer ensures that results are presented in a consistent and actionable format, making it easier for developers to interpret findings and integrate them into CI/CD pipelines. This innovation addresses a common problem in traditional solutions, where inconsistent result formats hinder automation and scalability. Moreover, planned enhancements, such as the integration of ML/DL for post-processing results, aim to reduce false positives, eliminate duplicate findings and provide recommendations to users. These upcoming features position SASTer as a forward-looking tool designed to adapt to evolving security challenges. Additionally, SASTer simplifies the developer experience by offering a web-based interface for centralized management and a CLI tool for local execution. This dual approach ensures that SASTer is accessible to a wide range of users, from individual developers to enterprise teams, while maintaining flexibility and control. RESCALE – PU - Public – Page 38 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) By combining modularity, standardization, security and extensibility, SASTer sets a new standard for static code analysis solutions. Its ability to address the limitations of traditional tools while incorporating cutting-edge technologies makes it a transformative platform for software security. 4.2.5 Limitations and Future Enhancements SASTer, while offering a modular and extensible way for integrating multiple SAST analyzers, has certain limitations that will be addressed in future iterations. One limitation is its current reliance on existing static analyzers, which means the tool’s performance is inherently dependent on the capabilities of the integrated analyzers. As a result, SASTer at this moment cannot directly address the limitations of these tools, such as their false positive rates or inability to detect certain advanced vulnerabilities. Additionally, SASTer doesn’t currently support scanning binary code which is often used. The absence of advanced ML/DL modules post-processing for tool outputs is another area that limits SASTer’s ability to provide deeper insights, such as vulnerability prioritization and intelligent recommendations. Planned future enhancements for SASTer include the integration of ML/DL capabilities to reduce false positives, detect duplicate results and provide actionable recommendations. Moreover, future iterations of SASTer could provide support for binary code analysis. These improvements will ensure that SASTer continues to evolve as a robust and versatile tool for secure software development. 4.3 Intelligent Vulnerabilities Exposure Engine (IVEE) The Intelligent Vulnerabilities Exposure Engine (IVEE) in RESCALE is designed to address critical gaps in static code analysis by leveraging symbolic execution. Unlike traditional static analyzers, which rely on syntactic and semantic analysis, the IVEE introduces a another layer to assess code comprehensively. This tool focuses primarily on symbolic execution to detect vulnerabilities in compiled binary files. The symbolic execution capabilities of the IVEE systematically explore all feasible execution paths using symbolic inputs, ensuring that property violations (e.g., assertion failures) are detected across various execution paths. The IVEE achieves this by combining symbolic execution with static analysis features like Control Flow Graph (CFG) generation. This approach allows for an exhaustive assessment of a software component’s behavior under diverse scenarios, helping to identify vulnerabilities that might be missed by conventional tools. By using symbolic execution, the IVEE provides concrete counterexamples when properties are violated, helping developers pinpoint the exact inputs that lead to failure. RESCALE – PU - Public – Page 39 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) 4.3.1 Core Components and Functionality The backbone of the IVEE is the Angr framework [21], which enables the symbolic execution of binary executables. Symbolic execution allows the IVEE to explore multiple execution paths in a program by treating inputs as symbolic variables instead of concrete values. This approach allows the tool to detect vulnerabilities that depend on specific execution paths, such as buffer overflows, use-after-free, integer overflows and other critical security issues. Angr’s symbolic execution engine handles path exploration, constraint solving and counterexample generation to identify flaws in the software’s behavior. The core symbolic execution component in the IVEE is based on “angr.simulation manager”, a Python class in the Angr framework responsible for orchestrating the management of execution paths. It provides functions for branching, pruning and evaluating constraints to identify property violations such as assertion failures or security checks. The IVEE is able to scan several types of compiled binary files, such as Executable and Linkable Format (ELF) for Linux and Portable Executable (PE) for Windows. These formats are ideal for symbolic analysis because they contain the binary code that the symbolic execution engine needs to analyze. By focusing on compiled binary code, the IVEE eliminates the need for handling source code, making it an efficient tool for post-compilation vulnerability detection. One of the IVEE’s key features is the ability to automatically explore feasible execution paths using Angr’s “ExplorationTechnique”. This process involves searching for paths that may lead to vulnerabilities, focusing on areas of the code where such issues are most likely to arise. The IVEE will embed specific properties as assertions or constraints and use symbolic execution to verify whether these properties hold true across different execution paths. If a property violation occurs, Angr’s solver will provide counterexamples, which are concrete inputs that trigger the violation, helping developers understand the conditions under which vulnerabilities can be exploited. To better understand the structure of binaries, the IVEE will also generate different CFGs using “angr.analyses.CFGFast”. These graphs visualize the flow of execution through the binary, helping the analysis engine identify key areas of interest, such as loops, conditionals and function calls. By visualizing the control flow, the IVEE can prioritize regions of code that are more likely to contain vulnerabilities, allowing it to focus the symbolic execution on critical sections. The IVEE will use symbolic execution to detect property violations, such as assertion failures, buffer overflows and other security vulnerabilities. Angr’s symbolic execution engine enables the detection of these violations by exploring multiple execution paths and generating path constraints. When a violation is detected, IVEE will use Angr’s solver to generate concrete inputs, known as counterexamples, which can reproduce the failure. These counterexamples provide valuable insight into the input conditions that cause the vulnerability, enabling developers to patch or mitigate the issue. Initially, the IVEE will focus on supporting C/C++ and Python-generated binaries. This decision is driven by the prevalence of these languages in system-level programming and the fact that many vulnerabilities (e.g., buffer overflows, uninitialized variables) are most commonly found in C/C++ applications. The IVEE will analyze these compiled binaries to detect vulnerabilities that are specific to these languages. RESCALE – PU - Public – Page 40 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) 4.3.2 Considerations and Enhancements While Angr provides a robust symbolic execution engine, there are a few considerations and potential enhancements for the IVEE’s initial version: •Path Explosion: As with any symbolic execution tool, the IVEE may encounter the path explosion problem when analyzing large or complex codebases. This occurs when the number of feasible execution paths grows exponentially, leading to significant computational overhead. To mitigate this, the IVEE will incorporate various path exploration optimizations, such as path pruning and state merging, to reduce the number of paths explored and improve performance. •Dynamic Features and Limitations: Although Angr is highly effective for static code analysis, it might miss certain vulnerabilities that rely on runtime behavior. To address this, the IVEE will eventually integrate dynamic analysis techniques, allowing for a more comprehensive analysis that captures runtime behavior and dynamic vulnerabilities. •Integration with Traditional Static Code Analyzers: To further enhance its capabilities, the IVEE could integrate with other static analysis tools like Bandit or Semgrep for static analysis, helping to prioritize potentially vulnerable code regions before running symbolic execution. •Machine Learning (ML) Enhancements: Incorporating ML models could improve the prioritization of execution paths based on historical vulnerability data, making the tool more adaptive and intelligent. The IVEE represents a powerful tool for static code analysis, focusing on symbolic execution to identify vulnerabilities in binary code. By leveraging Angr’s symbolic execution capabilities, the IVEE offers automated, high-coverage analysis of binaries, including support for C/C++ and Python executables. With its ability to detect property violations and provide counterexamples, the IVEE plays a critical role in enhancing software security. Future improvements, will further strengthen the IVEE’s ability to identify and mitigate vulnerabilities across a wide range of software applications. 4.4 Efforts Related to RefactorERL RefactorERL [8] is an advanced tool designed for static analysis and refactoring of Erlang code, helping developers ensure code quality and maintainability through automated analysis techniques. With capabilities to analyze code structure, detect potential issues, and suggest improvements, RefactorERL serves as a critical asset for projects relying on the Erlang ecosystem to refine their applications. RefactorERL’s potential contribution to RESCALE, particularly in the integration of ML/DL techniques for Erlang-specific static analysis, is significant. However, an assessment led by PST revealed several obstacles related to RefactorERL’s current state as a software project. Currently hosted in a private repository at ELTE University, RefactorERL lacks the visibility and collaborative framework offered by platforms like GitHub, which has introduced challenges in both maintenance and community engagement. Notable issues include: RESCALE – PU - Public – Page 41 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) 9. Comparability: The SSCG should be structured in a way that allows for easy comparison with other SSCGs, enabling stakeholders to evaluate different components or systems side by side based on the tests performed, vulnerabilities identified, and compliance with standards. 10. Authenticity and Integrity: The SSCG must include mechanisms to ensure the authenticity and integrity of the test reports and it’s metadata. It should be emphasized here that the SSCG contains a multitude of test reports, each generated by different tools with possibly different configurations, environments and requirements towards ensuring their authenticity and integrity. Hence each single test report will also contain such a specific set of descriptions. The above list also touches related topics which are elaborated on in the following. 6.1.1 Test Reporting Format Static analysis tools are effectively, as of today, not guided by an official standard regarding their output format. This means in practice that every tool follows a different output format ranging from plain shell output of newline separated findings to complex folder structures including Extensible Markup Language (XML) or JavaScript Object Notation (JSON) reports following different schemas. To tackle this problem of having comparable and interoperable outputs of static analysis tools the Static Analysis Results Interchange Format (SARIF) [67] was developed as an OASIS approved (JSON-based) industry standard without any significant competition. Within RESCALE it is desirable to honor this format when possible. 6.1.2 Reproducible Testing Since static testing might result in uncovering security findings it is desirable to repeat the testing effort after fixing an issue, or at least provide transparency to other parties to enable them to repeat the test. The latter requirement is in particular important for open source projects where this degree of transparency is not only appreciated but for widely used software projects in the light of the recent XZ Utils backdoor (CVE-2024-3094 [15]) also expected. RESCALE test definitions/descriptions should therefore be sufficiently rich in details to allow different parties to evaluate the tests themselves. Here it appears to be desirable to use a definition language that allows the automation of testing efforts including the hardware and operating system setup. There exist different automation technologies like Ansible [61] and Puppet [57] which allow the description of workflows such that a test can be defined in a machine processable manner. RESCALE will allow a wide range of test definitions starting from plain human readable text to comprehensive machine readable definitions of setups and workflows. 6.1.3 Classification of Artifacts Further, the SSCG could be able to contain information to classify the state of the respective software artifact according to a defined compliance requirement or standard. This allows a producer to elaborate further on his motivations and testing effort. Such a requirement could RESCALE – PU - Public – Page 48 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) be “The maximum CVSS score of a vulnerability of the tested artifact is not higher than 2” or more technology related like “The static analysis tool RefactorErl was not able to identify any issues which could potentially halt the Erlang Virtual Machine and therefore stop the program execution”. Such requirements can hence be very generic or really technology dependent but also be totally different between organizations that want to ensure to only deploy viable software artifacts. 6.1.4 Classification of Vulnerabilities and Weaknesses To make static analysis results actionable, they must be categorized using standardized systems that ensure consistent interpretation and processing. Two key frameworks widely adopted for this purpose are Common Vulnerabilities and Exposures (CVE) [77] and Common Weakness Enumeration (CWE) [78], both maintained by MITRE and commonly integrated into static analysis tools. CVE provides unique identifiers for publicly disclosed vulnerabilities, allowing organizations to track specific issues consistently. Each CVE entry includes a description of the vulnerability and its potential impact, making it easier to prioritize responses. Static analysis tools often map their findings to CVE entries, enabling organizations to align with global standards and track vulnerabilities across systems. CVE integration allows for streamlined communication and remediation by linking vulnerabilities to well-documented references in databases like the NVD [51]. CWE categorizes common software and hardware weaknesses that could lead to vulnerabilities. While CVE identifies specific vulnerabilities, CWE focuses on the underlying coding flaws (e.g., buffer overflows, improper input validation) that allow these vulnerabilities to exist. Static analysis tools regularly use CWE categories to classify findings, providing deeper insight into the root causes of weaknesses. It must be emphasized here that a processable classification of findings is necessary to enable an automated TBOM lifecycle, specifically an automated generation of its vulnerability document. 6.2 Initial Design As outlined in D4.1, CycloneDX (CDX) is a suitable BOM standard in the scope of RESCALE. CDX follows an abstract high-level specification encompassing a variety of metadata, dependencies of the artifact and even workflows that affect its processing like its compilation. While it was initially designed as a relatively simple BOM standard for software artifacts to capture vulnerabilities, it has grown to cover complex use cases involving whole service architectures, hardware components and environment descriptions. One of the most recent updates (in CycloneDX 1.6 [12]) is the addition of attestations which enables CDX to even incorporate testing data with respect to a test target. This addition is crucial since the output of the static code analysis module needs to be part of the SSCG, together with a definition of the actual test and other elements that were mentioned in section 6.1. An initial specification of the SSCG using CDX serves two key purposes. First, it provides a usable specification for the Minimum Viable Product (MVP), ensuring the project starts with RESCALE – PU - Public – Page 49 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) something functional and testable. CDX offers a well-supported structure, making it an ideal starting point for this integration. Second, this approach allows for practical learning and improvement. By starting with a partially implemented SSCG in CDX, the project can gain insights from real-world use, informing necessary adjustments and refinements as development progresses. While this initial implementation focuses on CDX, transitioning to a neutral format for SSCG specification is under consideration for later stages, as well as adjustments to the CDX standard based on the project’s experience. Figure 10 illustrates the conceptual structure of the SSCG’s initial design, as it can be defined using CDX. The SSCG has a core part which contains the all relevant meta data, configuration and tool invocation details with respect to e.g. the static code analysis module, and of course the test output itself. This core part is meant to be the usual output of the static code analysis module. Further, CDX offers the possibility to extend this core part with rather producer specific content in case the he has a set of requirements on the software he wants to verify and also wants to capture the compliance with these requirements in the SSCG as explained in section 6.1.3. Figure 10: SSCG Concept Appendix A contains an SSCG example in CDX format, following the structure laid out in figure 10. While a large chunk of the content is self-explanatory there are some parts, especially the “declarations” and “definitions” fields, which need further explanation. As illustrated by figure 11 the “definitions” field contains a list of standards which again allow the definition of a list of “requirements”. These requirements can be used to express software qualities and RESCALE – PU - Public – Page 50 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) the testing effort that needs to be covered in the static analysis testing. Further, the RESCALE workflow can be elaborated here as a principal guideline for processing the software artifact. The example in appendix A includes fictional examples of those standards and requirements to showcase this approach. Please note again, that those definitions are optional as they are part of the extended SSCG. Figure 11: CycloneDX Attestations Overview The “declarations” field then contains the actual evidence to support compliance or mismatches with the standards and their requirements. This is done using the definition of “claims” which function as a hypothesis towards a requirement. Such a claim can express that a requirement was violated to a certain degree or on the other side that a requirement is fulfilled. Each claim is carried by “evidence” which is a piece of data to support the hypothesis (e.g., the claim). Note that the SSCG makes heavy use of so called CDX “bom-ref” elements to refer to objects defined in other places; for example, a claim uses the bom-ref of a piece of evidence to refer to the evidence itself. It is possible to attach arbitrary text as evidence here, together with its format identifier such that e.g. JSON can be attached and consumed in a programmatic way. In the scope of the SSCG, the evidence contains test report data, i.e. output from static code analyzers. An example of a claim could be “Memory vulnerabilities related to CVE-202144228 were found” (which violates a requirement) while the evidence shows the respective output of a single or even multiple static analyzer tools. In case no standards and requirements are defined, a claim could simply be that a specific static code analyzer found issues, with the respective test output as evidence. Given a sufficiently elaborated standards and requirements catalog (which is out of scope of this document), it is conceivable that e.g., a standard identifier is given to the static code analysis module (as a configuration option) which then executes tests against its set of requirements. Further, CDX actually allows the above approach of capturing and interpreting test data for multiple test targets at once. The SSCG is specific for a single software artifact and hence the list of test targets will always contain exactly one element. On top of that, CDX allows to add various metadata like information about the “assessor” (the RESCALE Producer subentity, that executes actual tests) and even environment and configuration information to a high degree. Also the involved tooling (“tools”) like containers and the SSCG Generator itself can be specified, including invocation information (again, see appendix A). RESCALE – PU - Public – Page 51 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) It should also be mentioned that CDX supports signatures using JSON Signature Format (JSF). This way basically every part of the SSCG document, specifically the attestations related fields, can be signed by the Producer entity using a Public Key Infrastructure (PKI). 6.3 Unification of Test Reports Unifying the output from multiple static code analysis tools is essential for improving efficiency and simplifying the management of analysis results. One effective approach is to adopt standardized formats, such as SARIF (see also section 6.1.1). SARIF provides a common structure for the output of different tools, ensuring consistency and making it easier to integrate into automated processes like CI/CD pipelines. This standardization reduces complexity by presenting all results in a uniform format. Another approach is to use consolidation frameworks like SonarQube [72] or DefectDojo [16], which are designed to merge and present reports from various static analysis tools in a single, centralized dashboard. By normalizing the data from different sources, these platforms help eliminate duplication and provide a clear, comprehensive overview of all detected issues. This centralized view enables teams to prioritize and track vulnerabilities or code issues more effectively. In the specific context of the RESCALE static code analysis module it could be valuable to build custom aggregators to unify outputs from different tools. Custom solutions can parse the outputs of various analysis tools, converting them into a common format fit for further local processing. This would effectively mean that test reports in the SSCG, despite being able to contain detailed reports of single tools, could also be aggregated in a way that the overall sum of executed tests appears as the test result of the static code analysis module in a unified and value added way. Machine Learning (ML) and Deep Learning (DL) methods can play a transformative role in enhancing custom aggregators for static code analysis by intelligently processing and interpreting large volumes of data generated by multiple tools. Traditional aggregators focus on collecting and normalizing outputs, but with ML/DL integration, aggregators can go beyond simple data merging. ML/DL models could analyze the relationships between different code modules and respective findings and evaluate them in a way that static analysis tools individually might not be capable of. Figure 12 depicts a possible workflow of aggregation in combination with ML/DL methods. Multiple static code analyzers generate output from a single software project, then their output undergoes tooling specific pre-processing and finally the findings of the specific tools are mapped to code locations in a unified way. This allows an aggregation of finding on a per code location basis such that further processing can be applied to each code location. This code location specific aggregation could be done using ML/DL methods which technically transforms a matrix of tool specific results into a vector of code location specific interpreted findings. There is also another more subtle element to the usage of ML/DL methods in figure 12. The final vector of interpreted findings and their locations need to be mapped back to the source code in a meaningful and actionable way. Here ML/DL might again become useful, especially since different findings on different code locations can be dependent. Hence a single finding might RESCALE – PU - Public – Page 52 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) Figure 12: Unification of Analyzer Reports with an Example Set of Analyzers be related to multiple code locations and can be accompanied by suitable meta information. While WP3 focuses rather on analyzers in the context of ML/DL methods, it is under consideration to develop the idea of such an aggregation mechanism further. 6.4 SARIF The Static Analysis Results Interchange Format (SARIF) [67] is an open standard designed to unify the output of static analysis tools, facilitating the integration of diverse tools into cohesive development workflows. Standardized by OASIS [52], SARIF addresses the challenges posed by the varied and often incompatible output formats of static analysis tools, which can hinder effective integration and analysis. SARIF plays a crucial role in RESCALE by enabling a consistent and interoperable way to report static analysis results across multiple tools in the ‘evidence’ section of a SSCG (see section 6.2 and figure 10). This ensures a streamlined process for aggregating, analyzing, and sharing vulnerability reports within the project. 6.4.1 Overview SARIF employs a JSON-based schema to represent static analysis results, ensuring both human readability and machine processability. This design choice enhances interoperability among tools and platforms, enabling developers to aggregate and analyze results from multiple sources efficiently. In RESCALE, this is particularly valuable for unifying outputs from a diverse set of static analysis tools. A key advantage of SARIF is its ability to encapsulate comprehensive information about analRESCALE – PU - Public – Page 53 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) ysis results, including details about the tool that generated the results, the rules applied during analysis and the specific locations in the code where issues were detected. This rich metadata supports advanced scenarios such as automated bug filing, trend analysis and integration with CI/CD pipelines, which are integral to the RESCALE workflow. The adoption of SARIF has been bolstered by its support from major industry players and its integration into widely used development tools. For instance, Microsoft’s Visual Studio and GitHub’s code scanning features utilize SARIF [25] [46] to present static analysis results, demonstrating the format’s practical applicability and industry acceptance. This widespread adoption underscores SARIF’s role in promoting best practices in static analysis and enhancing software development processes. SARIF represents a significant advancement in static analysis by providing a standardized, extensible, and interoperable format for analysis results. Its adoption within RESCALE facilitates the integration of diverse analysis tools, improves workflow efficiency, and enhances the overall quality and security of software components in the supply chain. 6.4.2 Format Details SARIF is structured as a JSON-based format that encapsulates the results of static analysis in a standardized and extensible way. It organizes data hierarchically, ensuring clarity and ease of integration across diverse tools and platforms. The SARIF schema comprises several key components, each serving a specific role in accurately conveying the results of static analysis. These components are described below in detail: •version: Identifies the version of the SARIF specification used in the report to ensure proper interpretation. •runs: Represents one or more analysis executions, allowing the consolidation of outputs from different tools or repeated runs of the same tool. •tool: Provides metadata about the analysis tool, including its name, version and information about its execution. •results: Contains the findings from the analysis, the attributes of each result are explained below: –ruleId: Links the issue to a specific rule. –message: Describes the detected problem. –locations: Points to the precise code location or locations, including file path and line numbers. –severity: Classifies the importance of the finding (e.g, error, warning, etc.). •rules: Lists the set of rules applied during the analysis, the attributes of each result are explained below: –id: The unique identifier for the rule. –shortDescription: A brief explanation of the rule. RESCALE – PU - Public – Page 54 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) –fullDescription: A detailed account of what the rule checks for. –helpUri: A link to external documentation for further context. •invocations: Captures details about the execution of the analysis tool, including start and end times, command-line arguments and environment variables. •artifacts: Represents the files analyzed or produced during the analysis, detailing their locations, contents and roles. •logicalLocations: Describes program elements like namespaces, classes or functions, aiding in pinpointing issues within the code structure. •taxonomies: Defines classifications or categorizations used in the analysis, such as security vulnerability types or coding standards. This structured approach enables SARIF to comprehensively represent static analysis results while maintaining flexibility for future extensions, ensuring its relevance in evolving software development workflows. To further illustrate the structure and application of SARIF, two examples are provided in the appendices. The first is a simple SARIF file sourced from Microsoft’s SARIF tutorials [47], showcasing the core components and their basic structure. This example serves as a foundational reference for understanding SARIF’s standardized schema. The second example demonstrates a SARIF file generated from the Bandit tool, which includes additional metadata and detailed analysis results. This example highlights how SARIF is used in practice within RESCALE, providing a more comprehensive view of how static analysis findings are reported and integrated into the project. These examples provide a clear and practical demonstration of SARIF’s capabilities, highlighting its role in standardizing static analysis outputs and facilitating seamless integration across diverse tools and workflows. 6.4.3 Context in RESCALE In the RESCALE framework, SARIF is instrumental in standardizing the outputs of various static code analysis tools. Given the diverse range of analyzers employed across different programming languages and environments, SARIF offers a unified, machine-readable format that facilitates the seamless aggregation and processing of analysis results within RESCALE. Many static analyzers integrated into RESCALE, such as bandit, flawfinder, bearer, natively support SARIF, enabling direct and consistent reporting of vulnerabilities, code quality issues and other findings. This native compatibility ensures efficient interpretation and consolidation of results across the project. For the static code analyzers that do not inherently support SARIF, custom scripts are developed to transform the output of the tools to SARIF-compliant formats. These scripts, written mainly in Python, leverage powerful libraries such as “sarif-om” and “sarif-tools” to simplify the conversion process: •sarif-om: This library provides an object model for creating and manipulating SARIF data, ensuring that the transformed outputs adhere strictly to the SARIF schema [59]. RESCALE – PU - Public – Page 55 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) •sarif-tools: Offers utilities for validating and managing SARIF files, allowing for efficient handling of large and complex analysis outputs. sarif-tools serves a dual purpose, providing both a CLI and a library for handling SARIF files [60]. Together, these libraries enable a robust and automated workflow for converting diverse static analysis results into SARIF. This approach ensures that all static analysis data adheres to a uniform schema, promoting consistency and enhancing interoperability within the Static Code Analysis Module. By adopting SARIF, RESCALE benefits from improved toolchain compatibility and streamlined integration. SARIF’s rich metadata capabilities; including information on tool configurations, analysis rules and specific code locations, provide the necessary context for generating comprehensive reports and facilitating effective communication. 6.4.4 SARIF Validation Ensuring the validity of SARIF files is crucial for maintaining consistency and reliability in static analysis reporting. To achieve this, we employ several validation methods described below: •Microsoft’s SARIF Validator: This web-based tool allows users to upload and validate SARIF files against the official SARIF schema, ensuring compliance and correctness [45]. •NIST’s SARIF Validator: Offered by the National Institute of Standards and Technology (NIST), this validator checks SARIF files for adherence to the SARIF standard, providing an additional layer of verification [49]. •Custom Validation Script: We have also developed a custom Python script utilizing the “json schema” library. This script automates the validation process by comparing SARIF files against the official SARIF JSON schema, which defines the structure and rules for valid SARIF files. The script can be seamlessly integrated into CI/CD pipelines, enabling automated SARIF validation as part of the development workflow. Moreover, the script provides detailed error reports, including specific line numbers and descriptions of validation failures. By integrating these validation methods, we maintain the integrity and consistency of our static analysis reports, facilitating seamless integration and accurate reporting within our development workflow. 6.4.5 Challenges in Using SARIF for SSCG While SARIF is effective for standardizing the reporting of static analysis findings, its application as an SSCG itself (and not just as ‘evidence’ in the SSCG) within RESCALE presents several challenges explained below: RESCALE – PU - Public – Page 56 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) •Limited Scope of Analysis: SARIF is designed specifically for static analysis results, focusing on issues such as vulnerabilities and code quality concerns. However an SSCG, requires broader assurance beyond just static analysis, including aspects like comprehensive reporting of static security guarantees, which SARIF alone cannot fulfill. •Lack of Standardized Vulnerability Classification: SARIF does not enforce a uniform taxonomy for categorizing vulnerabilities. This can lead to discrepancies in how issues are classified and reported, complicating the process of assessing and comparing vulnerabilities across different components of the supply chain. •Integration with Other Assurance Mechanisms: SSCG requires the integration of multiple assurance mechanisms, such as compliance checks, certification statuses and historical vulnerability data. SARIF, focused solely on static analysis, lacks inherent support for incorporating these diverse data types, limiting its ability to serve as a holistic SSCG solution. •Scalability Concerns: As the size and complexity of software projects that need to be scanned increases, SARIF files can become large and unwieldy. Efficiently managing and processing these extensive reports is essential to maintain the effectiveness of SSCG within large-scale projects. In summary, while SARIF provides a standardized format for static analysis reporting, its limitations in scope, vulnerability classification, integration with other assurance mechanisms and scalability present challenges for its use as a comprehensive SSCG within RESCALE. 6.5 SSCG Generator The SSCG Generator, developed in Erlang for the RESCALE project, is a CLI tool designed for generating and managing SSCGs. It provides two primary subcommands: generate for creating SSCGs and publish for transmitting them. Note that the publish command is not fully implemented, as the overall flow of TBOM creation is currently under revision in the scope of WP4 and WP5. The generate command uses an SBOM and associated test results to create an SSCG in a CDX JSON structure, as outlined in section 6.2. Additionally, the --authors argument captures basic producer information (name and email) in line with RESCALE’s workflow requirements, with potential for adding more detailed metadata about the producer in future updates. Currently, the tool expects test reports to be simple text files. However, it is desirable to adopt a standardized, machine-processable format such as SARIF and the SSCG Generator will support it in the future. The following shows the help texts of the tool which illustrate the usage: Main Help % sscg_generator --help usage: sscg_generator {generate|publish} [-v] [--verbose] RESCALE – PU - Public – Page 57 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) } } } ], " hashes ": [ { " alg ": " SHA -1" , " content ": "35 d1c8f259129dc800ec8e073bb68f995424619c " } ] } ] } }, "definitions": { " standards ": [ { "bom - ref ": " https :// rescale - project .eu/ standard /1.0.0" , " name ": " The ReSCALE Standard ", " description ": " The ReSCALE Standard describes a workflow to create a Trusted BOM (TBOM)", " version ": "1.0.0" , "requirements": [ { "bom - ref ": " https :// rescale - project .eu/ standard /1.0.0/ conformance / complete ", " identifier ": " rescale /1.0.0/ conformance / complete ", " title ": " Full conformance with ReSCALEs ’complete ’ profile , e.g. complete absence of findings " } ] } ] }, "declarations": { "targets": { " components ": [ { " type ": " library ", "name ": "A Very Nice Library which was tested by the ReSCALE Static Code Analysis Module ", "bom -ref ": " pkg:hex/a-very -nice - library@1 .0.0" , " version ": "1.0.0" , " description ": " Such a good piece of software , but it has security issues ..." , "purl ": "pkg:hex /a-very -nice - library@1 .0.0" , " hashes ": [ { " alg ": " SHA -1" , " content ": "53 ab2f0f92e87ea4874c8c6997335c211d81e636 " } ] } ] }, " assessors ": [ { "bom - ref ": " Producer Reference ", RESCALE – PU - Public – Page 64 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) " thirdParty ": false , "organization": { "bom - ref ": " Producer Entity ", "name ": " Some Company that wants to generate a SSCG for their library ", "contact": [ { " email ": " some@company . com" } ] } } ], "attestations": [ { " assessor ": " Producer Reference ", " summary ": " Mapping of Requirements to Claims ", "map ": [ { "requirement": " https :// rescale - project .eu/ standard /1.0.0/ conformance / complete ", " counterClaims ": [ " Claim : ReSCALE Test Suite XY found something !" ] } ] } ], " claims ": [ { "bom - ref ": " Claim : ReSCALE Test Suite XY found something !" , " target ": " pkg:hex/a-very -nice - library@1 .0.0" , " evidence ": [ " Evidence : memory error " ] } ], " evidence ": [ { "bom - ref ": " Evidence : memory error", " description ": " Exploitable memory error found ", "data ": [ { " name ": " ReSCALE Test Suite XY Output ", " contents ": { " attachment ": { " content ": " Test Suite XY found : \n\ tmemory corruption in file main .c at line 23" } } } ] } ] } } RESCALE – PU - Public – Page 65 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) B SARIF Examples B.1 Simple Example { " version ": "2.1.0" , "$schema ": "http :// json. schemastore . org/sarif -2.1.0 - rtm .4" , "runs ": [ { "tool ": { " driver ": { " name ": " ESLint ", " informationUri ": "https :// eslint .org", " rules ": [ { "id ": "no - unused - vars ", "shortDescription": { "text ": " disallow unused variables " }, "helpUri": " https :// eslint .org/ docs / rules /no - unused - vars ", " properties ": { " category ": " Variables " } } ] } }, " artifacts ": [ { " location ": { "uri ": " file :/// C:/ dev / sarif / sarif - tutorials / samples / Introduction / simple - example .js " } } ], "results": [ { " level ": " error ", "message": { "text ": "’x’ is assigned a value but never used ." }, " locations ": [ { "physicalLocation": { "artifactLocation": { "uri ": " file :/// C :/ dev / sarif / sarif - tutorials / samples / Introduction / simple - example . js", " index ": 0 }, " region ": { " startLine ": 1, "startColumn": 5 } } } RESCALE – PU - Public – Page 66 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) ], " ruleId ": "no - unused - vars ", " ruleIndex ": 0 } ] } ] } B.2 SAVE-ME Example { "$schema ": " https :// json. schemastore . org /sarif -2.1.0" , " version ": "2.1.0" , "runs ": [ { "tool ": { " driver ": { " name ": " Erlang Analyzer ", " fullName ": " Erlang Vulnerability Analyzer ", " version ": "1.0.0" , " informationUri ": " https :// sample_site . com", " rules ": [ { "id ": " vulnerability - detection ", " name ": " Vulnerability Detection ", " fullDescription ": { " text ": " Detects vulnerabilities in Erlang functions " } } ] } }, "results": [ { " ruleId ": " vulnerability - detection ", "message": { "text ": "No vulnerability detected with confidence 3.59. Confidence for potential vulnerability : -3.28." }, " locations ": [ { "physicalLocation": { "artifactLocation": { " uri ": " file :/// Users / Shared / Files From d. localized / Materijali / _RESCALE / save - me/ test_dir / sample_erlang_module_n . erl" }, " region ": { " startLine ": 19, " endLine ": 19 } } } ], " properties ": { RESCALE – PU - Public – Page 67 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) " confidence ": 3.586867332458496 } }, { " ruleId ": " vulnerability - detection ", "message": { "text ": "No vulnerability detected with confidence 3.59. Confidence for potential vulnerability : -3.30." }, " locations ": [ { "physicalLocation": { "artifactLocation": { " uri ": " file :/// Users / Shared / Files From d. localized / Materijali / _RESCALE / save - me/ test_dir / sample_erlang_module_n . erl" }, " region ": { " startLine ": 26, " endLine ": 26 } } } ], " properties ": { " confidence ": 3.591543436050415 } } ] } ] } B.3 Bandit Example { "$schema ": " https :// json. schemastore . org /sarif -2.1.0. json", " version ": "2.1.0" , "runs ": [ { "tool ": { " driver ": { " name ": " Bandit ", " organization ": " PyCQA ", " rules ": [ { "id ": " B404 ", " name ": " blacklist ", " properties ": { "tags ": [ " security ", " external /cwe/cwe -78" ], " precision ": " high " }, RESCALE – PU - Public – Page 68 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) "helpUri": " https :// bandit . readthedocs .io /en /1.7.10/ blacklists / blacklist_imports . html #b404 - import - subprocess " }, { "id ": " B602 ", "name ": " subprocess_popen_with_shell_equals_true ", " properties ": { "tags ": [ " security ", " external /cwe/cwe -78" ], " precision ": " high " }, "helpUri": " https :// bandit . readthedocs . io/ en /1.7.10/ plugins / b602_subprocess_popen_with_shell_equals_true . html " }, { "id ": " B608 ", "name": "hardcoded_sql_expressions", " properties ": { "tags ": [ " security ", " external /cwe/cwe -89" ], " precision ": "low " }, "helpUri": " https :// bandit . readthedocs . io/ en /1.7.10/ plugins / b608_hardcoded_sql_expressions . html" }, { "id ": " B201 ", " name ": " flask_debug_true ", " properties ": { "tags ": [ " security ", " external /cwe/cwe -94" ], " precision ": " medium " }, "helpUri": " https :// bandit . readthedocs . io/ en /1.7.10/ plugins / b201_flask_debug_true . html " }, { "id ": " B403 ", " name ": " blacklist ", " properties ": { "tags ": [ " security ", " external /cwe/cwe -502" ], " precision ": " high " }, "helpUri": " https :// bandit . readthedocs . io /en /1.7.10/ blacklists / blacklist_imports . html# b403 - import - pickle " }, { "id ": " B324 ", " name ": " hashlib ", RESCALE – PU - Public – Page 69 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) " properties ": { "tags ": [ " security ", " external /cwe/cwe -327" ], " precision ": " high " }, "helpUri": " https :// bandit . readthedocs . io/ en /1.7.10/ plugins / b324_hashlib .html" }, { "id ": " B105 ", "name": "hardcoded_password_string", " properties ": { "tags ": [ " security ", " external /cwe/cwe -259" ], " precision ": " medium " }, "helpUri": " https :// bandit . readthedocs . io/ en /1.7.10/ plugins / b105_hardcoded_password_string . html" }, { "id ": " B301 ", " name ": " blacklist ", " properties ": { "tags ": [ " security ", " external /cwe/cwe -502" ], " precision ": " high " }, "helpUri": " https :// bandit . readthedocs . io /en /1.7.10/ blacklists / blacklist_calls . html #b301 - pickle " }, { "id ": " B113 ", " name ": " request_without_timeout ", " properties ": { "tags ": [ " security ", " external /cwe/cwe -400" ], " precision ": "low " }, "helpUri": " https :// bandit . readthedocs . io/ en /1.7.10/ plugins / b113_request_without_timeout . html " } ], " version ": "1.7.10" , " semanticVersion ": "1.7.10" } }, "invocations": [ { "executionSuccessful": true, " endTimeUtc ": "2024 -10 -01 T08 :35:40 Z", RESCALE – PU - Public – Page 70 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) "toolConfigurationNotifications": [ { "message": { " text ": " syntax error while parsing AST from file" }, " level ": " error ", " locations ": [ { "physicalLocation": { "artifactLocation": { "uri ": " file :/// data / uploads / user_1 / project_1 / files / python_example_1 . py " } } } ] } ] } ], " properties ": { "metrics": { "_totals": { " loc ": 139 , " nosec ": 0, " skipped_tests ": 0, " SEVERITY . UNDEFINED ": 0, " CONFIDENCE . UNDEFINED ": 0, " SEVERITY .LOW ": 4, " CONFIDENCE .LOW ": 2, " SEVERITY . MEDIUM ": 3, " CONFIDENCE . MEDIUM ": 2, " SEVERITY .HIGH ": 4, " CONFIDENCE .HIGH ": 7 }, "/ data / uploads / user_1 / project_1 / files / python_example_1 . py ": { "loc ": 56 , " nosec ": 0, " skipped_tests ": 0 }, "/ data / uploads / user_1 / project_1 / files / python_example_2 . py ": { "loc ": 14 , " nosec ": 0, " skipped_tests ": 0, " SEVERITY . UNDEFINED ": 0, " SEVERITY .LOW ": 1, " SEVERITY . MEDIUM ": 0, " SEVERITY .HIGH ": 1, " CONFIDENCE . UNDEFINED ": 0, " CONFIDENCE .LOW ": 0, " CONFIDENCE . MEDIUM ": 0, " CONFIDENCE .HIGH ": 2 }, "/ data / uploads / user_1 / project_1 / files / python_example_3 . py ": { "loc ": 28 , " nosec ": 0, " skipped_tests ": 0, " SEVERITY . UNDEFINED ": 0, RESCALE – PU - Public – Page 71 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) " SEVERITY .LOW ": 0, " SEVERITY . MEDIUM ": 1, " SEVERITY .HIGH ": 1, " CONFIDENCE . UNDEFINED ": 0, " CONFIDENCE .LOW ": 1, " CONFIDENCE . MEDIUM ": 1, " CONFIDENCE .HIGH ": 0 }, "/ data / uploads / user_1 / project_1 / files / python_example_4 . py ": { "loc ": 22 , " nosec ": 0, " skipped_tests ": 0, " SEVERITY . UNDEFINED ": 0, " SEVERITY .LOW ": 3, " SEVERITY . MEDIUM ": 1, " SEVERITY .HIGH ": 2, " CONFIDENCE . UNDEFINED ": 0, " CONFIDENCE .LOW ": 0, " CONFIDENCE . MEDIUM ": 1, " CONFIDENCE .HIGH ": 5 }, "/ data / uploads / user_1 / project_1 / files / python_example_5 . py ": { "loc ": 19 , " nosec ": 0, " skipped_tests ": 0, " SEVERITY . UNDEFINED ": 0, " SEVERITY .LOW ": 0, " SEVERITY . MEDIUM ": 1, " SEVERITY .HIGH ": 0, " CONFIDENCE . UNDEFINED ": 0, " CONFIDENCE .LOW ": 1, " CONFIDENCE . MEDIUM ": 0, " CONFIDENCE .HIGH ": 0 } } }, "results": [ { "message": { "text ": " Consider possible security implications associated with the subprocess module ." }, " level ": " note ", " locations ": [ { "physicalLocation": { " region ": { "snippet": { " text ": " import subprocess \n" }, " endColumn ": 18, " endLine ": 1, " startColumn ": 1, " startLine ": 1 }, "artifactLocation": { "uri ": " file :/// data / uploads / user_1 / project_1 / files / python_example_2 . py " RESCALE – PU - Public – Page 72 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) }, " contextRegion ": { "snippet": { " text ": " import subprocess \n\ ndef list_files ( directory ) :\ n" }, " endLine ": 3, " startLine ": 1 } } } ], " properties ": { " issue_confidence ": "HIGH", "issue_severity": "LOW" }, " ruleId ": " B404 ", " ruleIndex ": 0 }, { "message": { "text ": " subprocess call with shell= True identified , security issue ." }, " level ": " error ", " locations ": [ { "physicalLocation": { " region ": { "snippet": { "text ": " result = subprocess . check_output ( command , shell = True )\n" }, " endColumn ": 62, " endLine ": 8, " startColumn ": 18, " startLine ": 8 }, "artifactLocation": { "uri ": " file :/// data / uploads / user_1 / project_1 / files / python_example_2 . py " }, " contextRegion ": { "snippet": { " text ": " command = \" ls {}\". format ( directory )\n result = subprocess . check_output ( command , shell = True )\n print ( result . decode () )\n" }, " endLine ": 9, " startLine ": 7 } } } ], " properties ": { " issue_confidence ": "HIGH", "issue_severity": "HIGH" RESCALE – PU - Public – Page 73 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) "uri ": " file :/// data / uploads / user_1 / project_1 / files / python_example_5 . py " }, " contextRegion ": { "snippet": { " text ": " def send_data ( data ):\n response = requests. post (\" http :// insecure - server .com/api /data\", json = data )\n return response \n" }, " endLine ": 16 , " startLine ": 14 } } } ], " properties ": { "issue_confidence": "LOW", "issue_severity": "MEDIUM" }, " ruleId ": " B113 ", " ruleIndex ": 8 } ] } ] } RESCALE – PU - Public – Page 80 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) References [1] Ericsson AB. dialyzer. https://www.erlang.org/doc/apps/dialyzer/dialyzer. html. [2] Ericsson AB. xref. https://www.erlang.org/doc/apps/tools/xref.html. [3] Saswat Anand, Corina S P˘ as˘ areanu, and Willem Visser. Symbolic execution with abstract subsumption checking. In International SPIN Workshop on Model Checking of Software, pages 163–181. Springer, 2006. [4] Duncan Paul Attard and Adrian Francalanza. A monitoring tool for a branching-time logic. In Yli` es Falcone and C´ esar S´ anchez, editors, Runtime Verification, pages 473–481, Cham, 2016. Springer International Publishing. [5] Roberto Baldoni, Emilio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR), 51(3):1–39, 2018. [6] Luca Borzacchiello, Emilio Coppa, Daniele Cono D’Elia, and Camil Demetrescu. Memory models in symbolic execution: key ideas and new thoughts. Software Testing, Verification and Reliability, 29(8):e1722, 2019. [7] Imen Boudhiba, Christophe Gaston, Pascale Le Gall, and Virgile Prevosto. Symbolic execution of transition systems with function summaries. In Sebastian Gabmeyer and Einar Broch Johnsen, editors, Tests and Proofs, pages 41–58, Cham, 2017. Springer International Publishing. [8] I. Boz´ o, D. Horp´ acsi, Z. Horv´ ath, R. Kitlei, J. K¨ oszegi, Tejfel. M., and M T´ oth. Refactorerl - source code analysis and refactoring in erlang. In Proceedings of the 12th Symposium on Programming Languages and Software Tools, ISBN 978-9949-23-178-2, pages 138– 148, Tallin, Estonia, October 2011. [9] Pietro Braione, Giovanni Denaro, and Mauro Pezz` e. Symbolic execution of programs with heap inputs. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pages 602–613, 2015. [10] Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. klee-se.org, 2008. [11] Georgiana Caltais, Mohammad Reza Mousavi, and Hargurbir Singh. Causal reasoning for safety in hennessy milner logic. Fundamenta informaticae, 173(2-3):217–251, 2020. Publisher Copyright: © 2020 - IOS Press and the authors. All rights reserved. [12] CycloneDX v1.6 JSON Reference. https://cyclonedx.org/docs/1.6/json/, April 2024. [13] Sooyoung Cha, Seongjoon Hong, Jiseong Bak, Jingyoung Kim, Junhee Lee, and Hakjoo Oh. Enhancing dynamic symbolic execution by automatically learning search heuristics. IEEE Transactions on Software Engineering, 48(9):3640–3663, 2021. RESCALE – PU - Public – Page 81 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) [14] Ying-Shen Chen, Wei-Ning Chen, Che-Yu Wu, Hsu-Chun Hsiao, and Shih-Kun Huang. Dynamic path pruning in symbolic execution. In 2018 IEEE Conference on Dependable and Secure Computing (DSC), pages 1–8. IEEE, 2018. [15] CVE-2024-3094. https://www.cve.org/CVERecord?id=CVE-2024-3094. [16] DefectDojo, Inc. DefectDojo. https://www.defectdojo.org/. [17] Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding, 2019. [18] Inc. Docker. Docker: Empowering app development for developers. https://www. docker.com/, 2024. [19] Ecma International. CycloneDX Bill of materials specification, 2024. [20] Zhangyin Feng, Daya Guo, Duyu Tang, Nan Duan, Xiaocheng Feng, Ming Gong, Linjun Shou, Bing Qin, Ting Liu, and et al. Jiang, Daxin. Codebert: A pre-trained model for programming and natural languages. arXiv preprint arXiv:2002.08155, 2020. [21] Evan Fish et al. Angr: Binary analysis platform. https://angr.io/, 2017. [22] OpenJS Foundation. Eslint: Find and fix problems in your javascript code. https: //eslint.org/, 2024. [23] Python Software Foundation. Python programming language. https://www.python. org/, 2024. [24] Lars- ˚ Ake Fredlund and H. Svensson. McErlang: a model checker for a distributed functional programming language. ACM SIGPLAN Notices, 42(9):125–136, 2007. [25] GitHub. SARIF support for code scanning. https://docs.github.com/ en/code-security/code-scanning/integrating-with-code-scanning/ sarif-support-for-code-scanning, 2023. [26] Alkis Gotovos, Maria Christakis, and Konstantinos Sagonas. Test-driven development of concurrent programs using concuerror. In Proceedings of the 10th ACM SIGPLAN Workshop on Erlang, Erlang ’11, page 51–61, New York, NY, USA, 2011. Association for Computing Machinery. [27] ´ Akos Hajdu, Matteo Marescotti, Thibault Suzanne, Ke Mao, Radu Grigore, Per Gustafsson, and Dino Distefano. Inferl: scalable and extensible erlang static analysis. In Proceedings of the 21st ACM SIGPLAN International Workshop on Erlang, Erlang 2022, page 33–39, New York, NY, USA, 2022. Association for Computing Machinery. [28] Jingxuan He, Gishor Sivanrupan, Petar Tsankov, and Martin Vechev. Learning to explore paths for symbolic execution. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, pages 2526–2540, 2021. [29] Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In Proceedings of the 7th Colloquium on Automata, Languages and Programming, page 299–309, Berlin, Heidelberg, 1980. Springer-Verlag. RESCALE – PU - Public – Page 82 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) [30] Carl Hewitt, Peter Bishop, and Richard Steiger. A universal modular actor formalism for artificial intelligence. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence, IJCAI’73, page 235–245, San Francisco, CA, USA, 1973. Morgan Kaufmann Publishers Inc. [31] S¨ oren Holmstr¨ om. Hennessy-milner logic with recursion as a specification language, and a refinement calculus based on it. In C. Rattray, editor, Specification and Verification of Concurrent Systems, pages 294–330, London, 1990. Springer London. [32] Inaka. elvis. https://github.com/inaka/elvis. [33] Joxan Jaffar, Rasool Maghareh, Sangharatna Godboley, and Xuan-Linh Ha. Tracerx: Dynamic symbolic execution with interpolation (competition contribution). Fundamental Approaches to Software Engineering, 12076:530, 2020. [34] Joxan Jaffar, Jorge A Navas, and Andrew E Santosa. Unbounded symbolic execution for program verification. In Runtime Verification: Second International Conference, RV 2011, San Francisco, CA, USA, September 27-30, 2011, Revised Selected Papers 2, pages 396–411. Springer, 2012. [35] Martin Jon´ aˇ s, Jan Strejcek, and Alberto Griggio. Combining symbolic execution with predicate abstraction and cegar. In # PLACEHOLDER PARENT METADATA VALUE#, pages 272–280. TU Wien Academic Press, 2024. [36] Timotej Kapus and Cristian Cadar. A segmented memory model for symbolic execution. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 774–784, 2019. [37] Anil Kumar Karna, Jinbo Du, Haihao Shen, Hao Zhong, Jiong Gong, Haibo Yu, Xiangning Ma, and Jianjun Zhao. Tuning parallel symbolic execution engine for better performance. Frontiers of Computer Science, 12:86–100, 2018. [38] Brian W. Kernighan and Dennis M. Ritchie. The C Programming Language. Prentice Hall, 1988. [39] Dexter Kozen. Results on the propositional µ-calculus. In Mogens Nielsen and Erik Meineche Schmidt, editors, Automata, Languages and Programming, pages 348– 359, Berlin, Heidelberg, 1982. Springer Berlin Heidelberg. [40] Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, and George Candea. Efficient state merging in symbolic execution. Acm Sigplan Notices, 47(6):193–204, 2012. [41] Raymond Li, Loubna Ben Allal, Yangtian Zi, Niklas Muennighoff, Denis Kocetkov, Chenghao Mou, Marc Marone, Christopher Akiki, Jia Li, and et al. Chim, Jenny. Starcoder: May the source be with you! arXiv preprint arXiv:2305.06161, 2023. [42] Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, and Marsha Chechik. Symbolic optimization with smt solvers. ACM SIGPLAN Notices, 49(1):607–618, 2014. [43] K. S. Luckow. Symbooglix: Symbolic execution for boogie programs. https://github. com/boogie-org/symbooglix, 2015. RESCALE – PU - Public – Page 83 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) [44] Sicheng Luo, Hui Xu, Yanxiang Bi, Xin Wang, and Yangfan Zhou. Boosting symbolic execution via constraint solving time prediction (experience paper). In Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 336–347, 2021. [45] Microsoft. SARIF Validator. https://sarifweb.azurewebsites.net/Validation. Accessed: November 16, 2024. [46] Microsoft. SARIF Viewer for Visual Studio Code. https://github.com/microsoft/ sarif-vscode-extension, 2023. [47] Microsoft. SARIF Tutorials. https://github.com/microsoft/sarif-tutorials, 2024. [48] Facundo Molina, Pablo Ponzio, Nazareno Aguirre, and Marcelo Frias. Learning to prune infeasible paths in generalized symbolic execution. In 2022 IEEE 33rd International Symposium on Software Reliability Engineering (ISSRE), pages 494–504. IEEE, 2022. [49] National Institute of Standards and Technology. NIST SARIF Validator. https: //samate.nist.gov/SARD/sarif-validator. Accessed: November 16, 2024. [50] Mozilla Developer Network. Javascript programming language. https://developer. mozilla.org/en-US/docs/Web/JavaScript, 2024. [51] National Vulnerability Database. https://nvd.nist.gov/. [52] OASIS. OASIS Open. https://www.oasis-open.org/, 2024. [53] Trail of Bits. Manticore: Symbolic execution tool for smart contracts and binaries. https://github.com/trailofbits/manticore, 2019. [54] Trail of Bits. Maat: Dynamic symbolic execution framework. https://github.com/ trailofbits/maat, 2020. [55] Trail of Bits. Trail of bits: Security engineering firm. https://www.trailofbits.com/, 2023. [56] OWASP Foundation. cyclonedx-cli. https://github.com/CycloneDX/ cyclonedx-cli. [57] Perforce Software. puppet. https://github.com/puppetlabs/puppet. [58] PyCQA. Bandit: Security linter for python code. https://bandit.readthedocs.io/, 2024. [59] Python Package Index (PyPI). sarif-om: SARIF Object Model. https://pypi.org/ project/sarif-om/, 2024. [60] Python Package Index (PyPI). sarif-tools: SARIF Command-line Tools. https://pypi. org/project/sarif-tools/, 2024. [61] Red Hat, Inc. Ansible. https://github.com/ansible/ansible. [62] Armin Ronacher. Flask: A microframework for python. https://flask. palletsprojects.com/, 2024. RESCALE – PU - Public – Page 84 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) [63] Armin Ronacher and Others. Flask-sqlalchemy: Flask extension for sqlalchemy. https: //flask-sqlalchemy.palletsprojects.com/, 2024. [64] Nicola Ruaro, Kyle Zeng, Lukas Dresel, Mario Polino, Tiffany Bao, Andrea Continella, Stefano Zanero, Christopher Kruegel, and Giovanni Vigna. Syml: Guiding symbolic execution toward vulnerable states through pattern learning. In Proceedings of the 24th International Symposium on Research in Attacks, Intrusions and Defenses, pages 456– 468, 2021. [65] Kaki Ryan and Cynthia Sturton. Countering the path explosion problem in the symbolic execution of hardware designs. arXiv preprint arXiv:2304.05445, 2023. [66] Jonathan Salwan. Triton: Dynamic binary analysis framework. https:// triton-library.github.io/, 2015. [67] Static analysis results interchange format (SARIF) version 2.1.0 plus errata 01. https://docs.oasis-open.org/sarif/sarif/v2.1.0/errata01/os/sarif-v2. 1.0-errata01-os-complete.html, August 2023. OASIS Standard incorporating Approved Errata. [68] Inc. Semgrep. Semgrep: Lightweight static analysis for many languages. https:// semgrep.dev/, 2024. [69] Koushik Sen, George Necula, Liang Gong, and Wontae Choi. Multise: Multi-path symbolic execution using value summaries. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pages 842–853, 2015. [70] Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Audrey Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna. SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis. In IEEE Symposium on Security and Privacy, 2016. [71] S Singh and S Khurshid. Distributed symbolic execution using test-depth partitioning. corr abs/2106.02179 (2021). URL https://arxiv. org/abs/2106.02179, 2021. [72] SonarSource SA. SonarQube. https://www.sonarsource.com/products/ sonarqube/. [73] Bjarne Stroustrup. The C++ Programming Language. Addison-Wesley, 2013. [74] Cppcheck Team. Cppcheck: A tool for static c/c++ code analysis. http://cppcheck. sourceforge.net/, 2024. [75] CrossHair Team. Crosshair: Symbolic execution for python. https://github.com/ pschanely/CrossHair, 2023. [76] Oss-Sydr-Fuzz Team. Oss-sydr-fuzz: Hybrid fuzzing for open source software. https: //github.com/ispras/oss-sydr-fuzz, 2021. [77] The MITRE Corporation. CVE Program. https://www.cve.org/About/Overview. [78] The MITRE Corporation. CWE Program. https://cwe.mitre.org/about/index. html. RESCALE – PU - Public – Page 85 / 86 D3.1: Static Code Analysers and Formal Verification Methods (first version) [79] Alexey Vishnyakov, Andrey Fedotov, Daniil Kuts, Alexander Novikov, Darya Parygina, Eli Kobrin, Vlada Logunova, Pavel Belecky, and Shamil Kurmangaleev. Sydr: Cutting edge dynamic symbolic execution. In 2020 Ivannikov ISPRAS Open Conference (ISPRAS), pages 46–54. IEEE, 2020. [80] Junye Wen, Mujahid Khan, Meiru Che, Yan Yan, and Guowei Yang. Constraint solving with deep learning for symbolic execution. arXiv preprint arXiv:2003.08350, 2020. [81] SH Wen, WL Mow, WN Chen, CY Wang, and HC Hsiao. Enhancing symbolic execution by machine learning based solver selection (01 2019). DOI: https://doi. org/10.14722/bar, 2019. [82] David A. Wheeler. Flawfinder: Examining c/c++ code for security weaknesses. https: //dwheeler.com/flawfinder/, 2024. [83] Guowei Yang, Antonio Filieri, Mateus Borges, Donato Clun, and Junye Wen. Advances in symbolic execution. Advances in Computers, 113:225–287, 2019. [84] Insu Yun, Sangho Lee, Meng Xu, Yeongjin Jang, and Taesoo Kim. {QSYM}: A practical concolic execution engine tailored for hybrid fuzzing. In 27th USENIX Security Symposium (USENIX Security 18), pages 745–761, 2018. RESCALE – PU - Public – Page 86 / 86