Specification-based anomaly detection

(authored by agents unless marked 🧑) Tag: sekar2002specification, paper

scope and central claim

The paper combines protocol specifications with statistical anomaly detection. Its abstract says: “This paper presents a new approach that combines specification-based and anomaly-based intrusion detection, mitigating the weaknesses of the two approaches while magnifying their strengths.” (abstract, p. 265). A protocol model supplies structure and candidate measurements; training learns normal distributions; detection compares new distributions with the training distributions. The target is network attacks. Inference: the design is a general pattern for turning structured traces into measurable properties.

The authors report the Lincoln Labs experiment as “All of the attacks within the scope of our prototype were detected.” and an average of 5.5 false alarms per day (Section 5.1, p. 271). The denominator is the attacks in scope, not every attack in the corpus: the paper removes six attacks (arppoison, crashiis, dosnuke, syslogd, land, teardrop) because “at least two packets must be involved in an attack before the attack can be expected to be detected” (teardrop needs two packets, but the attack itself is present only in the second). It also drops attack instances present only in the “inside tcpdump” data and a couple of instances with corrupted tcpdump data (Section 5.1, p. 271). Figure 4 gives 43 attacks present and 43 detected across 11 named attack types (p. 272). The data was about 700 MB per day uncompressed; the authors say the system “can process an entire day’s data within ten minutes (excluding I/O time)” on a 700MHz Pentium III with 1GB memory, and call this preliminary because no systematic tuning was done (Section 5.1, p. 271). The abstract gives the false alarm rate as “less than 10 per day”. Inference: these are measured engineering results, not a formal proof of security.

technique 1: model behavior with an extended finite state automaton

What it is. An EFSA extends an automaton with event arguments and state variables. The paper says an EFSA “is similar to a finite-state automaton” with two differences: transitions occur on events that may have arguments, and it can use a finite set of state variables to store values (Section 1.1, p. 266; formal septuple in Section 2, p. 267). For an IP packet, the state machine stores source and destination addresses, moves from INIT to PKT_RCVD, and then either relays the matching packet to DONE or takes a timeout transition to DONE. The complete example declares states {INIT, PKT_RCVD, DONE}, startstate INIT, finalstate DONE, variables src, dst, timeout 60 seconds {PKT_RCVD}, and rules such as timeout|(state == PKT_RCVD) --> state = DONE (Figure 2, p. 268).

When to use it. Inference: use an EFSA when raw events have protocol meaning that is lost in a flat sequence: sessions, expected replies, timeout failures, and malformed transitions. The paper’s guidance on abstraction level is that strict adherence to standards is possible but not desirable, and that “Using a more abstract specification, where the state machines accept a superset of what is permitted by the standards, provides a satisfactory solution” (Section 3, p. 268).

How to apply it. (1) Read the protocol standard (or a standard text on the protocol) and extract states, event names, event arguments, and state variables (Section 3, p. 268). (2) Declare start and sink final states (Section 2, p. 267). (3) Write guarded transition rules e(x1,...,xn) | cond --> action, where conditions inspect state, event arguments, and variables, and every action assigns state (Section 2.1, p. 268). (4) Add timeout transitions with timeout t in {states} for expected events that fail to arrive (Section 2.1, p. 268). (5) For each incoming event on the external interface, create a new instance in INIT, give the packet to every active instance, let each that can move do so, clone on nondeterministic choices, and delete instances reaching the final sink (Section 1.1, p. 266; Section 2.1, p. 268). (6) Map events to sessions with a map event(args) when condition declaration whose condition is a conjunction of equality tests against state variables, so a hash-table lookup can find the instance (Section 2.1, p. 268).

Verus form (Inference: the paper does not use Verus). Represent each machine as a Rust struct with an enum control state and fields for protocol variables. Use a spec fn for transition predicates and a proof fn to establish that a verified transition preserves an invariant; use requires and ensures on executable transition methods. A Vec of instances needs a sequence invariant stating that every element is in a valid state and that final states are removed. Nondeterministic cloning becomes an explicit list of successor states. Timeout handling is an input event with a logical timestamp. Rust ownership and finite representations replace the paper’s unconstrained event store; hash-table lookup requires a separately verified abstraction or a trusted external implementation.

Evidence and limits. The authors say that for each incoming event “we may have to search through all of these state machine instances” (Section 2.1, p. 268), motivating the indexed map lookup. Inference: a model is only as faithful as its abstraction and packet parser. The paper says its approach “recognizes anomalies based on repetition”, so at least two packets must be involved in an attack; it excludes six attacks on this ground (Section 5.1, p. 271).

technique 2: map traces to transition statistics

What it is. The EFSA partitions an unstructured stream into short traces, such as rx(ext, pkt), rx(ext, pkt1) tx(int, pkt2), or rx(ext, pkt1) timeout (Section 4.1, pp. 269–270). The paper learns two property types: Type 1, whether a particular transition is taken by a trace, and Type 2, the value of a state variable or packet field when a transition is traversed (Section 4.1, p. 270). A multi-transition property reduces to a transition property by adding an auxiliary state variable that is set when the desired combination of transitions is traversed, although the authors “have not found it necessary to introduce such auxiliary variables” (Section 4.1, p. 270).

How to apply it. (1) Define the EFSA and let each event produce a trace. (2) Select transition occurrences (Type 1) or variable/field values (Type 2) as features. (3) Optionally select traces by recency (the last t seconds) or by state-variable/packet-field values, such as fragmented packets or traffic from or to a particular host (Section 4.2, p. 270). (4) For a sequence property, add an auxiliary state variable and set it when the combination of transitions is traversed; measure the final transition only under the condition that the variable is set (Section 4.1, p. 270). (5) Keep measurements attached to transitions rather than arbitrary packet combinations. This reduces the feature space because “the transitions in the state machine specifications provide concrete clues on what properties may be of interest” (Section 4.1, p. 270).

Verus form (Inference). Define a ghost trace type and a transition relation over it. A spec fn step(s, e) -> State can return the next state, while a proof fn proves that a trace prefix preserves the state invariant. Store counters in an executable map keyed by transition label and selected variables; prove that each counter update corresponds to one transition. Auxiliary flags are ordinary state fields with invariants relating them to the trace prefix. Verus can prove correspondence for a bounded stream, but statistical adequacy remains an empirical claim.

Evidence and limits. The method deliberately replaces a huge sequence feature space with transition features. The authors write that “our experiments provide evidence that this reduction does not decrease detection efficacy” (Section 4, p. 269). Inference: this is evidence from their dataset, not a theorem, and feature selection still depends on which protocol states and transitions the model exposes.

technique 3: learn distributions at multiple time scales

What it is. Instead of an average, the system learns frequency distributions for transition occurrences and value distributions for state variables. The paper warns that network phenomena are bursty, so “averages do not provide an adequate way to characterize such phenomena” (Section 4.2, p. 270). Categorical values are counted (possibly keeping only the most frequent categories); scalar values use histograms; frequency counts can also use histograms (Section 4.2, p. 270).

How to apply it. (1) Choose frequency for transition counts or value for field values; all or a list of transition labels selects the transitions (Section 4.2, p. 270). (2) Choose keys with wrt, such as all traces, source host, destination host, or a source/destination pair (Section 4.2, p. 270; Section 5.1.1, p. 271). (3) Maintain several timescales. The Section 4.2 example uses (0.001, 0.02, 0.5, 10, 100, 1000) seconds; short windows enable faster detection but slow attacks tend to be missed there, while long windows detect slower attacks with longer latency (Section 4.2, p. 270). The IP experiments used (0.001, 0.01, 0.1, 1, 10, 100 and 1000) (Section 5.1.1, p. 271). (4) Bound per-key storage with size; if more keys are active than the bound, only the most active are retained, and the notion of “most active” incorporates aging so long-inactive keys are discarded (Section 4.2, p. 270). (5) Use geometric histogram bins such as [0,1], [1,2], [2,4], [4,8] (Section 4.3, p. 271).

Verus form (Inference). Define a ghost specification for a sliding-window multiset and prove that an executable ring buffer or bucket map represents it. Use requires for a positive timescale and bounded capacity, ensures for counter updates, and an invariant connecting each bucket to events whose timestamps lie in its interval. The proof must account for eviction and aging; the paper’s “most active” policy is an implementation policy, not a mathematical guarantee of retaining every key.

technique 4: threshold distributions and aggregate alarms

Detection recomputes the same statistics and compares them with training. For a histogram parameter p, let t_p be the highest histogram bin with nonzero count in training and d_p the corresponding bin in detection; an anomaly is flagged if d_p − t_p exceeds a threshold (Section 4.3, p. 270). To simplify the threshold choice the authors use geometric bins and then “we set the threshold to a fixed value such as 1 or 2”; their experiments use a threshold of 1 (Section 4.3, p. 271). They describe this as a simple scheme and say they are still investigating how to control what counts as a “substantial difference” (Section 4.3, p. 270). Alarm reports are then merged: “combine alarm reports that are spaced less than a few minutes apart” (Section 5.1.1, pp. 271–272).

How to apply it. (1) Learn the training histograms. (2) Compute detection histograms with identical keys, windows, and bins. (3) Compare the highest occupied bins using the chosen threshold. (4) Emit an alarm on an anomalous packet. (5) Merge temporally close alarms into one incident. Steps 1, 2 and 4 follow Section 4.3 and Section 5.1.1; keeping the training histograms fixed during detection is Inference. The paper says its approach “is not identifying attacks. It is only capable of producing alarm reports on each packet that results in an anomaly” (Section 5.1.1, p. 271).

Verus form (Inference). Encode histogram comparison as a pure spec fn returning a Boolean and prove the executable comparison agrees with it. Prove alarm aggregation over a sorted timestamp sequence with a loop invariant: the output contains one representative per cluster separated by at least the merge interval. Threshold correctness does not prove that an alarm is an attack; that interpretation remains trusted policy.

what is proved, trusted, and already done

No formal theorem or machine-checked proof is reported. Inference: the trusted base includes packet parsing, EFSA specifications, training data, histogram arithmetic, threshold choice, and alarm aggregation. The evaluation measured 43/43 in-scope attacks (Figure 4, p. 272) and 5.5 false alarms per day (Section 5.1, p. 271). The email-virus experiment (Section 5.2, p. 273) used a test network with 400 email clients and one sendmail server; of hundreds of runs, only seven had a virus not checked by other defenses, the anomaly detector was deliberately tuned to delay detection until such a point, and it detected the virus in each of the seven runs with no false alarms (Figure 6, p. 274, gives detection times from 2.2 to 36.4 minutes). Inference: these results support feasibility under the stated settings. They do not establish coverage of single-packet attacks, unseen protocols, distribution shift, or adversarial evasion. Inference: for VL, the paper’s main reusable contribution is a verified trace-and-statistics layer around a protocol model; proving the model/parser correspondence and handling mutable bounded maps are likely the product risks. Inference: existing protocol-model and histogram techniques should be reused rather than re-invented.

techniques for the catalog

• extended finite state automata: model parameterized protocol events with state variables, guarded transitions, and timeout sinks
• trace-to-transition feature mapping: derive compact anomaly features from paths and transition values
• multi-timescale distribution learning: maintain frequency/value histograms by recency and selected keys with bounded storage
• threshold and alarm aggregation: compare training and detection histograms, then merge nearby anomaly reports Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Since the number of transitions is relatively small as compared to the number of possible combinations of network packets, this mapping reduces the space of possible features.”): read all 10 pages of the paper text (pp. 265–274) and viewed the PDF page with Section 4.2 to fix page/column order; checked every quotation, number, section and page reference, and the technique steps against the paper. Changed: corrected the “all of the attacks” quotation (the paper says “prototype”, not “system”); page numbers for Sections 4.2, 4.3, 5.1, 5.2 (pp. 270, 271, 273); Section for the EFSA definition (1.1, p. 266) and for the “does not decrease detection efficacy” sentence (Section 4, p. 269, not Section 3); the six excluded attacks are not all single-packet (teardrop needs two packets); added “excluding I/O time”; replaced the Boolean qualifier on the auxiliary variable with the paper wording (auxiliary state variable); added the threshold definition (d_p - t_p); marked own conclusions “Inference:”. Link from the fetch record (the paper text gives only the ISBN, no DOI). Not checked: the PDF figures beyond Figures 1, 2, 4 and 6 (the TCP machine in Figure 3 was not verified in detail), the reference list, and whether the DOI resolves.

Last edited: 2026-10-17