Analyzer output validation

This page documents the validators that protect analysis.json before it becomes safety evidence or a diagram.

The ownership rule is:

the native analyzer must either emit one complete artifact or fail;
AnalysisResult.validate() owns strict schema and cross-reference semantics every Kotlin consumer relies on;
P6 owns exact agreement with the Gradle run plan and DSL; and
P7 and the appendix own projection and publication checks.

Severity alone does not make a HIGH problem an unconditional failure. HIGH and lower problems use StigProblemReporter.report()/reportAll(): they are recorded and processing continues unless the resolved failAt threshold is reached. Only a non-continuable condition classified as CRITICAL uses the dedicated fail()/failAll() path and stops unconditionally. Analyzer-output mismatches listed below as CRITICAL are in that category because they make the evidence unusable or contradictory. Neither path truncates the graph or synthesizes recovery evidence.

Supported schemas

The native analyzer emits schema v7. Kotlin accepts exactly v5, v6, and v7:

v7 stores facts, states, ordered payloads, RLE successor lists, delta-coded positional topology shapes, sparse labelled-template overrides, and provenance components once in a run-global evidence store; physical sinks reference owned component indices;
v6 uses solverExecutions[] plus canonical facts, states, ordered payloads, and isolated evidence components;
v5 is an explicit archived-artifact compatibility shape with flattened per-sink segments[] and edges[];
each version rejects tables belonging exclusively to another version; and
all other versions are rejected.

Strict Jackson unknown-field handling is enabled. A producer/consumer shape mismatch is an error, not an ignored extension point.

Schema-v7 semantic validator

P6 and P7 call:

AnalysisResultJson.parseAndValidate(text)

The validator checks:

Invariant group	Required condition
Schema and emit contract	Version is 5, 6, or 7; v6/v7 have explicit emit flags and positive capacities; data-flow evidence requires the shared ICFG.
Repository and IDs	Repository names and every global ID namespace are unique; prefixes match their owning table; node repository references resolve.
ICFG	Every edge endpoint is known; a non-empty ICFG has an explicit entry-point instruction; reached sinks are entry-point reachable.
Canonical facts	Every v6/v7 fact has a supported structural base kind/ID, ordered offsets, lifetime, zero marker, and over-approximation marker; canonical identities are unique. Display labels are not identity.
Canonical states	Every state references a known instruction and fact; `(instructionId, factId)` identities are unique.
Ordered payloads	Every payload is non-empty, references known states, and has a unique complete ordered state sequence.
Topology isolation	V6 segment instances/edges are component local. V7 successor runs, signed index deltas, and sparse payload overrides decode exactly; each shape has one empty-override base template. Positions remain distinct even for equal payloads. Materialized templates have no dangling, self, duplicate, or cyclic edges, and roots/terminals exactly match topology.
Component boundaries	Every root has one or more distinct explicit source-generation records; each source belongs to the component's solver source batch and each generated state is the root payload's first exact state. Every terminal contains the selected physical sink.
Run-global ownership	Every v7 evidence component (not the analyzed software component/activity) is referenced by exactly one physical sink, names that same sink, references one known template, and has unique `(solver execution, physical sink)` provenance. One solver execution may cover many sinks and one analyzer artifact contains many evidence components. Every retained fact, state, payload, successor list, shape, and template is transitively referenced. Foreign, duplicate, multiply owned, and orphan values are rejected.
Compaction statistics	Per-component offered/new counts agree with the exact component. Retained counts equal the serialized tables, decoded shape/template references, overrides, and edges; offered counts cover all component input and cannot claim impossible sharing. Section byte counts are non-negative.
Solver manifest	Source/sink batch indexes and capacities are valid; endpoints are unique and belong to the configured universes; every configured source/sink pair is covered exactly once.
Solver verdicts	Each execution has exactly one verdict per active logical sink; physical sink inventories agree; `reached` agrees with reached physical IDs.
OR aggregation	Logical and physical `sink.leaked` values equal the OR of all covering PhASAR solver verdicts. A negative cell has no positive component and never cancels another cell.
Evidence provenance	Every component names an existing solver execution that covered and reached that physical sink; its non-empty matched leak facts exactly equal its terminal sink-state facts.
Verdict/evidence consistency	When data-flow graph emission is enabled, every positive sink has component evidence and materialized source-to-sink reachability; negative sinks have no facts, states, payloads, or components.
Feasibility	`NO_CHECK` emits no feasibility results. V6/v7 paths name a covering solver and use ordered instruction IDs from a configured source to the physical sink; v5 paths use known flattened segment IDs. A feasible path implies a positive PhASAR verdict.

The leak verdict remains the authoritative PhASAR result. DAG reachability is a required evidence consistency check, not an independent mechanism that may turn a negative verdict positive.

P6 run-plan and DSL postconditions

stigAnalysisP6RunAnalyzer validates the durable command, generated sidecars, analyzer JSON, and resolved DSL together. The following mismatches are build-breaking:

data-and-control-flow sources are not exactly all recognized sources with ASIL greater than or equal to the sink ASIL;
cascading-fault sources are not exactly all recognized sources below the sink ASIL;
the two enabled partitions overlap or fail to cover the recognized source universe;
sourceASILs, run-plan sources, endpoint sidecar sources, generated analyzer cfg sources, and analyzer codeAnalysisConfiguration.configuredSources disagree;
run-plan sinks, endpoint sidecar sinks, and analyzer codeAnalysisConfiguration.configuredSinks disagree;
the emitted analysisKind or configPath differs from the durable run-plan entry;
the resolved analyzerExecution.maxSinksPerSolver, durable --max-sinks-per-solver=<n> option, task input, and metadata disagree; or
the analyzer process fails, times out, runs out of memory, reports an unknown fact encoding, or fails its native compaction round trip.

maxSinksPerSolver = null means all configured sinks and therefore deliberately omits the CLI capacity option. A positive value is serialized exactly. The current source capacity is one and is recorded as codeAnalysisConfiguration.maxSourcesPerSolver.

Run-plan generation first checks the ASIL policy and all generated representations. P6 independently repeats the endpoint/ASIL/sidecar checks against the actual run-plan entry and the analyzer artifact that was just produced. P6 publishes staged output only after every analyzer invocation and postcondition succeeds. It never publishes a successful subset of a failed invocation. These unusable-output checks are CRITICAL hard failures and therefore do not use the configurable safety-problem threshold.

Safety problems remain distinct from structural validity. For example, a valid cascading-fault result that reports a lower-ASIL source reaching a higher-ASIL sink is a HIGH safety problem: it is reported and continues by default, but fails when failAt is configured to HIGH or lower. A malformed solver manifest or component is a CRITICAL tool-output error and stops unconditionally.

P7 and appendix checks

After validation, P7 projects the compact artifact into all-sinks and one-sink Vista graphs. It checks:

Check	Severity / behavior
Analyzer JSON cannot be validated or materialized	`CRITICAL`; no diagrams are accepted.
An enabled non-empty diagram cell loses all renderable nodes	`CRITICAL`.
Data-flow endpoint scope differs from the selected run/sink projection	`CRITICAL`.
Presentation creates an invalid endpoint cycle or a foreign source/sink marker	`CRITICAL`.
Source line or source browse URL is unavailable	Diagnostic severity; the graph can fall back to IR labels.
Propagated ASIL is higher than the configured element ASIL	`CRITICAL`.
Propagated ASIL is lower than the configured element ASIL	`MODERATE`; conservative rating review.

Vista retains native evidenceComponentIds[] and solverExecutionIds[] on segment presentation nodes and edges. Presentation-only coalescing may combine those lists, but it does not alter the validated analyzer object or serialize a new authoritative graph.

The one-logical-sink object used while building Vista is an in-memory projection, not a second analyzer artifact. Projection remaps every retained global index, rebases the selected template used as each shape's payload base, rebuilds sparse overrides, and recomputes retained counters and canonical-key sizes. Offered counters and serialized-section byte counts remain origin telemetry from the validated native artifact; they must not be read as a new projection compaction ratio or projection file size.

stigGenerateDiagramAppendix copies enabled assets into the report, validates Markdown references, renders a no-data message for truly empty cells, and keeps summarized all-sinks previews enabled independently of detailed all-sinks configuration. An artifact-size policy may omit a particular rendered file; it does not truncate native evidence.

Failure and scale rules

There is no valid success mode based on a segment-count or evidence-depth cutoff. In particular, 65,536 segments is not a 65 MB file-size limit and is not a permitted truncation boundary. The former segment-count rejection has been removed: a component with more than 65,536 segments must serialize completely or the analyzer invocation must fail. There is likewise no configured byte cap for native analysis.json; operational exhaustion of memory, disk, heap, or time fails the invocation rather than accepting partial evidence.

The independent diagramOutputs.maxArtifactSizeMiB setting applies only when P7 diagram/source-index artifacts become report publication assets. It does not constrain analyzer evidence or generation of the complete P7 build artifact used by metrics and postconditions. The appendix retains raw P7 Cytoscape .cyjson and creates a lossless .cyjson.gz inside its declared docsOutputDir; the limit is evaluated on that compressed publication size. Other formats are evaluated on their stored size. An oversized publication asset is omitted and reported as HIGH; the complete source artifact remains under build/.

Wall-clock timings and RSS are operational log diagnostics, not canonical evidence fields. They identify whether cost was in solver construction, solve(), leak collection, reconstruction, minimization, normalization/interning, validation, or serialization without making otherwise equal JSON differ by runtime. Deterministic schema-v7 storageStatistics and compaction counts are evidence fields: they cover offered/retained values and topology plus actual serialized evidence-section bytes. Canonical-key byte counts describe logical identity encodings, not retained string lookup maps; JSON syntax outside those sections, allocator overhead, and the ICFG are excluded. The serialization log's bytes counter is the exact complete artifact size.