Breaking the Triage Bottleneck: When GNAT SAS meets GNAT DAS

In the realm of high-integrity software, whether it is steering a vehicle, guiding an aircraft, or securing critical infrastructure, verification cannot be an afterthought. Standards such as ISO 26262, ISO/SAE 21434, DO-178C/ED-12C, and EN 50128/EN 50657 require rigorous safety and security postures. To meet these demands, development teams rely heavily on static analysis and formal verification (such as CodeSonar, GNAT Static Analysis, and SPARK) to catch vulnerabilities across millions of lines of code before a single binary is executed.

But static analysis, as powerful as it is, introduces a well-known challenge: the triage bottleneck.

The Cost of Validating Warnings

Static analysis excels at broad strokes, enforcing rules and highlighting potential vulnerabilities. However, because static analyzers must safely approximate complex, data-dependent runtime logic, they inevitably generate false positives.

In a high-integrity environment, you cannot simply ignore these warnings. Every single alarm flagged by a static analyzer must be manually investigated and dispositioned by an engineer. This triage process is notoriously time-consuming. Developers spend countless hours tracing data flows, debating execution paths, and trying to determine whether a flagged buffer overflow or range violation can actually occur, or if it is just a false positive.

When you have hundreds of warnings, you have a bottleneck that directly impacts your time-to-market.

Enter the GNATfuzz Hot-Spot Workflow

This is where dynamic analysis, specifically targeted fuzz testing, becomes an essential companion to your static analysis tools. While static analysis predicts where a vulnerability might exist, fuzzing can provide concrete, executable proof.

We recently introduced the GNATfuzz fuzz-everything workflow to help teams automatically apply dynamic testing across their entire codebase. But to solve the triage bottleneck, teams need surgical precision. They need to take the exact warnings flagged by their static analyzer and apply intense, concentrated dynamic pressure directly on the suspect code.

The new hot-spot workflow in GNATfuzz is designed for exactly this purpose and currently supports Ada and SPARK, with future support for C.

Instead of spending hours manually analyzing a cluster of complex warnings in a specific module, you can now use the Hot-Spot workflow to dedicate your fuzzing campaign to try verifying them. If the fuzzer can trigger the vulnerability, the debate is over. There are no false positives in fuzzing; if GNATfuzz detects a crash on the subprogram under test, you have a definitive runtime failure and a reproducible test case in hand. You stop triaging, and you start fixing. Automating the generation of these reproducible test cases saves your development teams time.

Interoperability via Interchange Formats

To simplify the interface and ensure future expandability with other Static Analysis solutions, Hot-Spot uses open-source, non-proprietary, de facto industry interchange formats for input and output specifications. At AdaCore, we believe that software tools should interact with each other openly and collaboratively. Interchange formats act as generic (tool-agnostic) glue between related technologies, and the best fit format for Static & Dynamic Analysis input and output is the Static Analysis Results Interchange Format (SARIF). SARIF is an open JSON-based specification that was originally developed to allow IDEs to view results across multiple Static Analysis tool executions, but has since become a good format for other tool results, such as fuzzing.

Surgical Precision in Practice

The Hot-Spot workflow abstracts away the tedious setup of custom test harnesses and automatically manages the entire verification lifecycle. The process is entirely intent-driven, starting with the exact warnings your static analyzer has already found. The warnings are exported and then passed to the Hot-Spot workflow, which drives fuzzing campaigns targeting the subprograms that can reach those warnings.

First, you run a comprehensive static analysis (using GNAT SAS) across your project to flag potential issues:

$ gnatsas analyze -P my_project.gpr --mode deep -j0 --force

Next, you export a standard SARIF report. For the most effective dynamic validation, it is best to filter this report specifically for runtime check failures, the exact class of findings a fuzzer can trigger:

$ gnatsas report sarif -P my_project.gpr --show=kind=check -o checks.sarif

With your static analysis findings exported, you launch the focused fuzzing campaign with a single command:

$ gnatfuzz hot-spot --sarif checks.sarif -P my_project.gpr

From here, GNATfuzz takes over completely. It parses the SARIF file, extracts the flagged locations, and cross-references them against your project's call graph to find the nearest automatically fuzzable subprograms. It then automatically generates the test harness, builds it, manages the starting corpus, and launches a time-bounded fuzzing campaign on those specific hot spots. It hunts relentlessly for the concrete inputs that make the static warnings a reality.

Closing the Verification Loop

To fundamentally reduce your triage time, the hot-spot workflow delivers actionable data integrated directly into your existing tools:

• Augmented SARIF with Reproducers: When GNATfuzz proves a static analysis warning is real, it outputs an augmented SARIF file containing the original warning, a confidence score, exact reproducer commands, decoded inputs, and stack traces.
• Verifiable Evidence via GNATcoverage: If the fuzzer doesn't trigger the warning, aggregated GNATcoverage reports reveal exactly how much of the flagged logic was exercised. High coverage without a crash provides the data-backed confidence needed to classify a warning as a false positive.

Ultimately, every targeted warning resolves into one of three states: Confirmed (proven true positive), Unconfirmed with High Confidence (likely false positive), or Inconclusive (requires manual review). These results are cleanly exported in three formats: an augmented SARIF file for IDEs and dashboards, a JSON summary for pipeline automation, and GNATcoverage reports for line-by-line inspection.

Conclusion

By integrating the Hot-Spot workflow into your pipeline, you unlock a highly efficient verification strategy that drastically reduces manual engineering effort:

1. Automated triage: Stop manually tracing complex execution paths. Use hot-spot to generate concrete reproducers for true positives, separating the signal from the static-analysis noise.
2. Guided resource allocation: Use static analysis to map the codebase and identify risky areas, then focus your intensive, CPU-heavy dynamic analysis precisely where it is needed most.

When turning ambiguous warnings into undeniable proof, hot-spot breaks the triage bottleneck and brings automated, surgical security to the most critical corners of high-integrity applications.

To learn more about how GNATfuzz and the GNAT Dynamic Analysis Suite can elevate your verification pipeline and save your team hours of manual review, visit our documentation or contact us for a demo. Not at this time; the underlying technology is open-source, but integration into a seamless solution is available only with the commercial GNAT Dynamic Analysis Suite.