pith. sign in

arxiv: 2606.10649 · v1 · pith:VFCJJTGJnew · submitted 2026-06-09 · 💻 cs.CR · cs.FL

Layer Order Semantics for Automata-Based Cybersecurity

Faruk Alpay , Taylan Alpay This is my paper

Pith reviewed 2026-06-27 12:33 UTC · model grok-4.3

classification 💻 cs.CR cs.FL
keywords layer order semanticsautomata-based cybersecurityedit automataHTTP request desynchronizationonline enforcementfinite-state semanticsevidence markersparser-pair semantics
0
0 comments X

The pith

Layer order in cybersecurity pipelines receives a finite-state semantics equivalent to finite-output deterministic edit automata while preserving marker invariants.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs a formal account of how the sequence of layers in a security pipeline determines which evidence markers become visible to later stages. It composes layer-order automata, sequential transducers, and decision automata to model transformations on traces such as HTTP requests. The central worked example is request desynchronization, where the same input trace triggers detection or evasion depending on whether framing evidence reaches the differential parser before commitment. The model separates completed-trace recognition from online editing and shows that only the regular prefix-closed fragment under causal visibility yields faithful enforcers. This matters because many deployed systems are layered, so order itself can create or eliminate blind spots without any change to the individual components.

Core claim

The framework is monolithically equivalent to finite-output deterministic edit automata while preserving layer-local invariants such as marker birth, marker survival, and reorder-sensitive visibility; faithful online enforcement is characterized as the regular prefix-closed case under causal visibility. A concrete parser-pair semantics identifies the forbidden marker factor with CL.TE, TE.CL, TE.TE, and HTTP/2-downgrade boundary disagreement, and a contextual reorder congruence classifies which component permutations induce the same decision language.

What carries the argument

Layer-order automaton composed with deterministic sequential security transducers, evidence markers, and a final decision automaton.

If this is right

  • Completed-trace recognition can be separated from online editing and decision synthesis.
  • Regular policies remain recognizable even when they lie outside the boundary of deployable enforcers.
  • Contextual reorder congruence supplies a decision procedure for comparing pipeline permutations.
  • Marker birth, survival, and visibility invariants are preserved under the equivalence to edit automata.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The equivalence could let results from edit-automata theory be imported directly into the analysis of layered security pipelines.
  • The model supplies a vocabulary for automatically auditing whether a proposed reordering of components preserves or alters the decision language.
  • Extension to other layered protocols might reveal similar order-sensitive failure modes once the marker factors are abstracted.
  • Testing the parser-pair abstraction against production HTTP/2 and HTTP/1.1 traces would check whether the identified forbidden factors match observed desynchronization attacks.

Load-bearing premise

The stated abstraction of parser-pair semantics correctly identifies the forbidden marker factor with the listed desynchronization patterns and that the contextual reorder congruence classifies permutations without loss of relevant security distinctions.

What would settle it

A concrete layer ordering whose induced decision language differs from the one predicted by the contextual reorder congruence, or an observed marker factor in real HTTP traces that falls outside the identified CL.TE, TE.CL, TE.TE, and downgrade cases.

read the original abstract

Layered cybersecurity pipelines transform evidence before they decide on it, and the order of those transformations determines which security facts become visible to which layer. This paper gives layer order a finite-state semantics built from a layer-order automaton, deterministic sequential security transducers, evidence markers, and a final decision automaton. The worked case is HTTP request desynchronization: front-end and back-end processors compute incompatible request boundaries, and the same trace is detected or missed according to whether framing evidence reaches the parser-differential layer before it commits. The results separate completed-trace recognition, online editing, decision synthesis, and faithful enforcement; characterize faithful online enforcement as the regular prefix-closed case under causal visibility; and show that regular policies beyond that boundary remain recognizable without becoming deployable enforcers. The framework is monolithically equivalent to finite-output deterministic edit automata, while preserving layer-local invariants such as marker birth, marker survival, and reorder-sensitive visibility. A concrete parser-pair semantics identifies the forbidden marker factor with CL.TE, TE.CL, TE.TE, and HTTP/2-downgrade boundary disagreement under the stated abstraction, and a contextual reorder congruence classifies which component permutations induce the same decision language. The result is an automata-theoretic account of order-sensitive security failures and a compositional vocabulary for auditing, synthesizing, and comparing layered enforcement pipelines.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper develops a finite-state semantics for order in layered cybersecurity pipelines via layer-order automata, deterministic sequential security transducers, evidence markers, and a decision automaton. Using HTTP request desynchronization as the worked example, it separates completed-trace recognition, online editing, decision synthesis, and faithful enforcement; characterizes faithful online enforcement as the regular prefix-closed case under causal visibility; proves monolithic equivalence to finite-output deterministic edit automata while preserving marker birth/survival and reorder-sensitive visibility; supplies a concrete parser-pair semantics mapping the forbidden marker factor to CL.TE/TE.CL/TE.TE/HTTP/2-downgrade cases; and defines a contextual reorder congruence over component permutations.

Significance. If the equivalence, characterizations, and parser-pair mapping hold with the claimed invariants, the framework supplies a compositional automata-theoretic vocabulary for auditing, synthesizing, and comparing order-sensitive enforcement pipelines—an area where existing edit-automaton models lack explicit layer-order structure. The separation of recognition from deployable enforcement and the regular prefix-closed characterization are potentially useful for practical pipeline design.

major comments (2)
  1. [parser-pair semantics] Abstract and § on parser-pair semantics: the claim that the abstraction 'correctly identifies the forbidden marker factor with CL.TE, TE.CL, TE.TE, and HTTP/2-downgrade boundary disagreement' is load-bearing for transferring the automata results to concrete security; the manuscript must exhibit an explicit check that timing of marker survival relative to commit points and non-regular visibility constraints are not elided, otherwise the security characterization does not transfer even if the formal equivalence holds.
  2. [contextual reorder congruence] Section on contextual reorder congruence: the congruence is asserted to classify permutations without loss of relevant security distinctions; the manuscript must demonstrate (via the HTTP desync case or a counter-example) that the congruence does not identify permutations that differ on reorder-sensitive visibility or marker survival, as this is required for the 'preserving layer-local invariants' claim to support the central equivalence.
minor comments (2)
  1. [faithful enforcement characterization] Notation for 'causal visibility' and 'regular prefix-closed case' should be defined before the characterization theorem to avoid forward references.
  2. [equivalence theorem] The abstract states the framework is 'monolithically equivalent' to finite-output deterministic edit automata; the corresponding theorem statement should explicitly list which layer-order components map to which edit-automaton components.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments on the parser-pair semantics and contextual reorder congruence. Both points identify places where the manuscript's transfer arguments to concrete security can be strengthened with explicit verification. We will revise the manuscript to address them directly.

read point-by-point responses

  1. Referee: Abstract and § on parser-pair semantics: the claim that the abstraction 'correctly identifies the forbidden marker factor with CL.TE, TE.CL, TE.TE, and HTTP/2-downgrade boundary disagreement' is load-bearing for transferring the automata results to concrete security; the manuscript must exhibit an explicit check that timing of marker survival relative to commit points and non-regular visibility constraints are not elided, otherwise the security characterization does not transfer even if the formal equivalence holds.

    Authors: We agree that an explicit check is required for the security transfer claim. The current parser-pair section defines the abstraction but does not walk through marker survival timing against commit points or non-regular visibility. In the revision we will add a dedicated verification subsection that uses the HTTP desync traces to confirm (i) marker birth occurs before the relevant commit point in each CL.TE/TE.CL/TE.TE case, (ii) survival is preserved exactly when the layer-order automaton accepts, and (iii) no non-regular visibility is introduced by the abstraction. This will be placed immediately after the definition of the forbidden marker factor. revision: yes

  2. Referee: Section on contextual reorder congruence: the congruence is asserted to classify permutations without loss of relevant security distinctions; the manuscript must demonstrate (via the HTTP desync case or a counter-example) that the congruence does not identify permutations that differ on reorder-sensitive visibility or marker survival, as this is required for the 'preserving layer-local invariants' claim to support the central equivalence.

    Authors: We accept that the manuscript currently asserts the congruence preserves distinctions without supplying the required demonstration. In the revision we will insert a short subsection that applies the congruence to the HTTP desync parser-pair permutations. For each pair we will exhibit (a) the reorder-sensitive visibility sets before and after congruence, (b) the marker survival intervals, and (c) that no two permutations differing on either property are identified. If any pair collapses a distinction we will note it as a limitation; otherwise the example will serve as the required witness. revision: yes

Circularity Check

0 steps flagged

No significant circularity; framework reduces to known edit automata with independent invariants

full rationale

The abstract presents the layer-order framework as monolithically equivalent to finite-output deterministic edit automata while preserving additional layer-local invariants (marker birth, survival, reorder-sensitive visibility). This equivalence is stated as a derived property rather than a definitional identity. No load-bearing steps reduce by construction to inputs, no fitted parameters are renamed as predictions, and no self-citations or uniqueness theorems from prior author work are invoked to justify central claims. The parser-pair semantics and contextual reorder congruence are described as concrete identifications under the stated abstraction, but the provided text shows no explicit reduction where the output is forced by the input definitions themselves. The derivation chain therefore remains self-contained against external automata-theoretic benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only; no free parameters, axioms, or invented entities can be extracted or audited. The central claim rests on unstated modeling assumptions about what constitutes causal visibility and marker survival.

pith-pipeline@v0.9.1-grok · 5755 in / 1237 out tokens · 14816 ms · 2026-06-27T12:33:42.226053+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

20 extracted references · 7 canonical work pages

  1. [1]

    Certified share-alike public-release record

    Faruk Alpay. Certified share-alike public-release record. Preprint record 2606.07884, 2026. https://arxiv.org/abs/2606.07884

    Pith/arXiv arXiv 2026

  2. [2]

    Schneider

    Bowen Alpern and Fred B. Schneider. Defining liveness.Information Processing Letters, 21(4):181–185, 1985. doi:10.1016/0020-0190(85)90056-0

    work page doi:10.1016/0020-0190(85)90056-0 1985

  3. [3]

    Rule-based runtime verification

    Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik Sen. Rule-based runtime verification. InVerification, Model Checking, and Abstract Interpretation, pages44–57.Springer, 2004. 20

    2004

  4. [4]

    Runtime verification for LTL and TLTL.ACM Transactions on Software Engineering and Methodology, 20(4):14:1–14:64, 2011

    Andreas Bauer, Martin Leucker, and Christian Schallhart. Runtime verification for LTL and TLTL.ACM Transactions on Software Engineering and Methodology, 20(4):14:1–14:64, 2011. doi:10.1145/2000799.2000800

    work page doi:10.1145/2000799.2000800 2011

  5. [5]

    Fielding, Mark Nottingham, and Julian Reschke

    Roy T. Fielding, Mark Nottingham, and Julian Reschke. RFC 9112: HTTP/1.1. RFC Editor, 2022.https://www.rfc-editor.org/rfc/rfc9112

    2022

  6. [6]

    Hamlen, Greg Morrisett, and Fred B

    Kevin W. Hamlen, Greg Morrisett, and Fred B. Schneider. Computability classes for enforce- ment mechanisms.ACM Transactions on Programming Languages and Systems, 28(1):175–205,

  7. [7]

    doi:10.1145/1111596.1111601

    work page doi:10.1145/1111596.1111601

  8. [8]

    Rewriting-based techniques for runtime verification

    Klaus Havelund and Grigore Rosu. Rewriting-based techniques for runtime verification. Automated Software Engineering, 12(2):151–197, 2005. doi:10.1007/s10515-005-6205-y

    work page doi:10.1007/s10515-005-6205-y 2005

  9. [9]

    HTTP desync attacks: Request smuggling reborn

    James Kettle. HTTP desync attacks: Request smuggling reborn. PortSwigger Re- search, presented at Black Hat USA 2019. https://portswigger.net/research/ http-desync-attacks-request-smuggling-reborn

    2019

  10. [10]

    HTTP/2: The sequel is always worse

    James Kettle. HTTP/2: The sequel is always worse. PortSwigger Research, presented at Black Hat USA 2021.https://portswigger.net/research/http2

    2021

  11. [11]

    Browser-powered desync attacks: A new frontier in HTTP request smug- gling

    James Kettle. Browser-powered desync attacks: A new frontier in HTTP request smug- gling. PortSwigger Research, presented at Black Hat USA 2022.https://portswigger.net/ research/browser-powered-desync-attacks

    2022

  12. [12]

    HTTP/2 request smuggling

    Emil Lerner. HTTP/2 request smuggling. Technical presentation, 2021

    2021

  13. [13]

    A brief account of runtime verification.Journal of Logic and Algebraic Programming, 78(5):293–303, 2009

    Martin Leucker and Christian Schallhart. A brief account of runtime verification.Journal of Logic and Algebraic Programming, 78(5):293–303, 2009. doi:10.1016/j.jlap.2008.08.004

    work page doi:10.1016/j.jlap.2008.08.004 2009

  14. [14]

    Edit automata: Enforcement mechanisms for run-time security policies.International Journal of Information Security, 4(1–2):2–16, 2005

    Jay Ligatti, Lujo Bauer, and David Walker. Edit automata: Enforcement mechanisms for run-time security policies.International Journal of Information Security, 4(1–2):2–16, 2005. doi:10.1007/s10207-004-0046-8

    work page doi:10.1007/s10207-004-0046-8 2005

  15. [15]

    HTTP request smuggling

    Chaim Linhart, Amit Klein, Ronen Heled, and Steve Orrin. HTTP request smuggling. Watchfire whitepaper, 2005

    2005

  16. [16]

    CWE-444: Inconsistent interpretation of HTTP requests

    MITRE. CWE-444: Inconsistent interpretation of HTTP requests. Accessed 2026.https: //cwe.mitre.org/data/definitions/444.html

    2026

  17. [17]

    MITRE ATT&CK

    MITRE. MITRE ATT&CK. Accessed 2026.https://attack.mitre.org/

    2026

  18. [18]

    Credential stuffing, sub-technique T1110.004

    MITRE. Credential stuffing, sub-technique T1110.004. Accessed 2026. https://attack. mitre.org/techniques/T1110/004/

    2026

  19. [19]

    Testing for HTTP request smuggling

    OWASP Foundation. Testing for HTTP request smuggling. Accessed 2026.https://owasp. org/www-project-web-security-testing-guide/

    2026

  20. [20]

    Schneider

    Fred B. Schneider. Enforceable security policies.ACM Transactions on Information and System Security, 3(1):30–50, 2000. doi:10.1145/353323.353382. 21

    work page doi:10.1145/353323.353382 2000