Skip to content

verdicts.md

Latest commit

 

History

History
201 lines (158 loc) · 10 KB

verdicts.md

File metadata and controls

201 lines (158 loc) · 10 KB
Raw

How verdicts are reached

This is the document to read if you disagree with a verdict.

The lattice

Every leaf predicate in a rule evaluates to one of four values, ordered:

UNSAT  <  UNKNOWN  <  WEAK  <  SAT
Value Meaning
SAT The field exists and a value satisfying the predicate was observed in the supplied data.
WEAK The field exists, but the required value was never observed, or the field is too sparsely populated to rely on. The rule could still fire in production.
UNKNOWN Undecidable by static analysis: a regular expression, a field-to-field comparison, an unresolved placeholder, or a value set we stopped collecting because it hit the cardinality cap.
UNSAT The field does not appear anywhere in the observed schema, so no event in this shape can satisfy it.

Three values would not be enough. "I proved this cannot match", "I could not decide", and "this could match but I saw no evidence" are three genuinely different states; collapsing any two produces either false confidence or useless output.

The connectives

AND  =  min      OR  =  max

Those two lines carry most of Nullfire's reasoning, and the useful properties fall out rather than being special-cased:

  • An absent optional OR branch cannot sink a healthy rule. max(UNSAT, SAT) is SAT.
  • One unsatisfiable conjunct is enough. min(SAT, SAT, UNSAT) is UNSAT.
  • Uncertainty propagates instead of being rounded away. min(SAT, UNKNOWN) is UNKNOWN, so a rule with one undecidable predicate is never reported MATCHABLE.

NOT is asymmetric, deliberately

Sigma NOT branches are filters. They subtract matches; they essentially never make a rule impossible. selection and not filter asks for an event matching the selection that does not match the filter — and unless the filter demands the very value the selection demands, you can always pick an event that avoids it.

So negation never returns UNSAT, with one exception below. Two consequences worth knowing:

  • NOT UNSAT → SAT, plus a note that the filter is inert against this schema. An exclusion that can never match filters nothing, which makes the rule easier to satisfy.
  • Everything else → SAT, with the limitation recorded in the rule's notes.

Declaring a rule dead because of a filter would be the worst false positive this tool could produce. Filters are the most-edited part of a rule, and an engineer told their rule was dead because of an exclusion clause would rightly stop trusting the output.

The exception: provable contradiction. If a conjunction requires F == V and simultaneously excludes exactly F == V, no event can satisfy both. Nullfire reports that as UNSAT. The check is narrow on purpose:

  • Conjunctions are flattened first, because pySigma nests each named selection in its own AND — selection and not filter arrives as AND[ AND[F=V, …], NOT(F=V) ], and the two halves are never siblings.
  • A negated conjunction teaches us nothing. not (a and b) is satisfied by a and not b, so it does not exclude a. Only a negated single-field equality counts.
  • The field must have exactly one required value. With two, the rule is already unsatisfiable for a different reason.

Per-predicate behaviour

Sigma construct Field absent Field present
field: value UNSAT SAT if a matching value was observed; WEAK if the value set is complete and the value is missing; UNKNOWN if the cardinality cap was hit
field|contains, startswith, endswith UNSAT as above, matched with the wildcard matcher
field|all expanded by pySigma into a real AND
field|base64offset|contains UNSAT pySigma has already encoded the literal, so it evaluates as an ordinary containment and gets a real verdict
field: null SAT — trivially satisfied SAT if occupancy < 100%; WEAK if the field is populated in every event
field|exists: true UNSAT SAT, or WEAK if sparse
field|exists: false SAT SAT if occupancy < 100%, else WEAK
field|cidr UNSAT decided exactly using ipaddress
field|lt/lte/gt/gte/neq UNSAT decided numerically
field|re UNSAT UNKNOWN — no rule-supplied regex is ever compiled
field|fieldref UNSAT UNKNOWN — depends on per-event values
keyword (no field) n/a SAT if observed; WEAK if not; never UNSAT
unresolved %placeholder% UNKNOWN — needs a pipeline to expand it

Two entries in that table are where a naive "required fields" analysis goes wrong:

  • field: null inverts. An absent field makes an equality predicate unsatisfiable but makes a null check trivially satisfiable.
  • Keywords cannot be ruled out. A keyword searches the whole event, so there is no field whose absence could exclude it. The strongest negative available is "not observed in the supplied data".

Sparsity applies on top: if a field's occupancy is at or below sparse_field_threshold, a SAT leaf is downgraded to WEAK with a reason naming the actual occupancy.

String matching is case-insensitive by default, per the Sigma specification. |cased is respected.

From lattice to status

                        ┌─────────────────────────────┐
                        │ total_events == 0?          │──yes──▶ UNASSESSED
                        └─────────────┬───────────────┘
                                      │ no
                        ┌─────────────▼───────────────┐
                        │ self-contradictory rule?    │──yes──▶ NULLFIRE
                        └─────────────┬───────────────┘         (data-independent)
                                      │ no
                        ┌─────────────▼───────────────┐
                        │ SOURCE_MISSING?             │──yes──▶ UNASSESSED
                        └─────────────┬───────────────┘
                                      │ no
                        ┌─────────────▼───────────────┐
                        │ no declaration AND zero     │──yes──▶ UNASSESSED
                        │ field overlap?              │
                        └─────────────┬───────────────┘
                                      │ no
                        ┌─────────────▼───────────────┐
                        │ lattice result              │
                        │   SAT     → MATCHABLE       │
                        │   WEAK    → DEGRADED        │
                        │   UNKNOWN → DEGRADED        │
                        │   UNSAT   → NULLFIRE*       │
                        └─────────────────────────────┘
                          * subject to both interlocks

Log-source gating

A rule's logsource is compared against each declared data source. Per dimension (product, category, service):

  • The rule does not specify it → skip.
  • The rule specifies it and the declaration matches → confirmed.
  • The rule specifies it and the declaration omits it → unconfirmed.
  • The rule specifies it and the declaration says something else → conflict.

Any conflict rules that declared source out. All-confirmed and no unconfirmed gives SOURCE_MATCH. Unconfirmed dimensions give SOURCE_UNKNOWN. If every declared source conflicts, SOURCE_MISSING → UNASSESSED.

An omitted dimension means unspecified, not wildcard. Declaring only product: windows therefore does not license NULLFIRE for every Windows rule — a registry-event rule judged against process-creation data would otherwise be mislabelled.

If nothing is declared at all, every rule is SOURCE_UNKNOWN.

The two interlocks on NULLFIRE

1. A declared source is required. Without one, verdicts cap at DEGRADED. Rationale: a rule requiring EventID against event.code-only data is indistinguishable from a rule for the wrong log source; both present as total field absence, and only the operator can break the tie.

2. The sample must reach min_sample_size. Below it, verdicts cap at DEGRADED.

Both only ever downgrade, and every downgrade is recorded in the rule's notes so the report explains why a dead-looking rule reads DEGRADED.

The contradiction case bypasses both, because its conclusion is a property of the rule rather than a claim about the data.

Statuses vs operational errors

PARSE_ERROR, PIPELINE_ERROR, VERIFICATION_ERROR, CONFIG_ERROR and DATA_ERROR are not statuses. A rule that fails to parse gets no verdict at all; it is counted in its own bucket. The summary reports five numbers (four statuses plus errors) that sum to the corpus size.

The invariant is enforced in code, not by convention: RuleResult.validate() raises if a result carries both a verdict and a blocking issue, or neither.

Reading a verdict

Every assessed rule carries:

  • status — one of the four
  • satisfiability — the underlying lattice value
  • source_match — SOURCE_MATCH / SOURCE_UNKNOWN / SOURCE_MISSING
  • reason — one precise sentence about why
  • dependent_fields, observed_fields, missing_fields — post-pipeline
  • evidence — per-leaf findings, worst-first, with observed occupancy
  • notes — limitations, downgrades and undecidable constructs
  • fixture or fixture_unavailable_reason

If a verdict looks wrong, evidence is where the answer is: it names the field, the expected value, the occupancy, and what was actually observed.