{"id":"d45c96de-a660-428f-8c83-2eeaeda497b5","arxiv_id":"2510.06420","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"A graph-based visual coordination language with formal execution semantics is used to automate and repeat adversary threat emulation and to produce proof-of-attack traces.","lead":"This paper introduces Effects Language (EL), a visual programming language that turns multi-step cyber-attack plans into executable graphs and formally defines how those graphs run. It reports faster, cheaper repeatable threat emulation against a Wizard Spider scenario and generates machine-readable proof-of-attack traces.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 2 is false as stated: paths ending inside a loop lose all active nodes when the loop count fires, so Theorem 2's reachability proof is unsupported.","rationale":"The reader identified Lemma 2's loop-exit claim as the weakest assumption and also flagged Algorithm 6's expiry-time expression. My independent reading agrees: the formal reachability theorem is not established because Lemma 2 is false, and the Algorithm 6 bug independently breaks the execution semantics for zero-delay loops. These are correctness risks in the paper's central formal contribution, not merely stylistic or consensus disagreements. However, the paper has substantive engineering content—a real graph-based coordination design, a concrete Wizard Spider translation, and an honest efficiency comparison—and both defects appear fixable without abandoning the architecture. The reader's CONDITIONAL verdict remains appropriate; my stress-test does not move the verdict because these are exactly the concerns the reader already weighed. I therefore recommend UNCHANGED, while noting that if the authors cannot correct Lemma 2 or Algorithm 6, the formal-semantics claim would need to be weakened or the verdict should move to REJECT.","tokens_in":33055,"tokens_out":8648,"duration_ms":75680,"concrete_test":"Implement or hand-execute Algorithms 1–9 on the minimal loop graph s→A1, A1→l, l→A1, l→x, x→goal, with l's counter 1 and no timeouts/delays. Simulate the round in which l fires: after Algorithm 6 lines 5 and 13, record D, A, F and check whether path s→A1 intersects D∪A. The published line 13 gives A1 expiry t*, so garbage collection removes it; if instead timeout semantics are used, A1 remains active but Lemma 2 still fails on path s→A1 after l fires with count 0. Either outcome falsifies the published Lemma 2/reachability claim.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central claim—that EL's execution semantics are formally defined and that important execution properties are proved—rests on Lemmas 1–3 and Theorem 2 in Section 4.5. Lemma 2 is not merely mis-proved; it is false. Using the loop shape of Fig. 8, let l be the loop count node, A1..Ak the internal loop nodes, and x the loop exit. Fix a path π from a start s to an internal node k = A_j (j ≤ k) that passes through l and then re-enters the loop: π = s⋯l A1⋯A_j. Suppose l is active and fires with counter 0. In Algorithm 6, line 3 resets R(l) = {A1..Ak} to inactive, line 5 activates x, and line 6 moves l to F. Since π ends at A_j and does not pass through x, after this line π∩(D∪A) is empty. This directly contradicts Lemma 2. The proof's assertion that \"if π passes through the loop count node, then π also passes through the loop exit node\" is only valid for paths that continue past the loop to a goal; it is not valid for paths whose endpoint lies inside the loop. Lemma 3 invokes Lemma 2 for arbitrary logic nodes, including nodes inside loops, so the induction in Lemma 3—and hence Theorem 2—is not established. A second, independent defect compounds this: Algorithm 6 line 13 places a zero-delay first loop node in A with expiry t*+delay(n)=t*, so Algorithm 9 removes it in the same round; loops cannot iterate under the published semantics. Both issues mean the paper's formal semantics as written does not deliver the claimed executable/provable loop behavior.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces Effects Language (EL), a visual, graph-based coordination language for adversary threat emulation. An EL graph is a directed graph of AGE (activation/guard/effect), logic, loop count, loop break, and loop exit nodes; the authors give a formal operational semantics (Algorithms 1–9) that maintains partitions into inactive, delayed, active, and fired nodes, and they prove in the appendix termination, liveness, and reachability properties (Lemmas 1–3 and Theorem 2). The paper also defines proof-of-attack traces, translates part of the Wizard Spider emulation plan into EL, and reports time and labor savings from using EL. The central claims are that EL makes attack graphs directly executable and repeatable and that its execution semantics are formally established.","tokens_in":33438,"tokens_out":10748,"duration_ms":92291,"significance":"EL addresses a real gap: most attack-graph notations are descriptive rather than executable, and automation tools generally lack formal execution semantics. The paper's separation of coordination semantics from watchpoint/effect details is a sound design, and the proof-of-attack trace is a useful idea. The manuscript includes the full pseudo-code specification, an appendix of proofs, a concrete ATT&CK-derived example, and self-reported efficiency data; it is not circular and does not rely on fitted parameters. If the semantic defects in §4.4/§4.5 are fixed, the formal framework would be a meaningful contribution to automated threat emulation and attack-graph research. At present, however, the correctness results are not established as written.","major_comments":[{"comment":"Lemma 2 is false as stated. In the loop structure of Fig. 8, let l be the loop count node, A1..Ak the internal nodes, and x the loop exit. Take a path π = s⋯l A1⋯Aj that ends at an internal node Aj (j≤k) and suppose l fires with counter 0. Algorithm 6 line 3 resets R(l) = {A1..Ak} to inactive, line 5 activates x, and line 6 moves l to F. Since π ends at Aj and does not contain x, after this round π∩(D∪A) is empty, contradicting the lemma. The proof's assertion that every path through l also passes through x is true only for paths that continue to the loop exit; paths ending inside the loop are valid instances of the lemma. Lemma 3 and hence Theorem 2 depend on Lemma 2, so the reachability theorem is not established.","section":"§4.5, Lemma 2; proof in Appendix A"},{"comment":"In the non-zero branch, the first loop node n is activated with expiry `t* + delay(n)`. For the default delay 0 this is `(n, t*)`. Algorithm 9, called from Algorithm 1 line 11 in the same round, removes every pair with t ≤ t*, so n is deactivated immediately and never executes. The no-delay case should pair n with `t* + timeout(n)`, matching Algorithm 5 line 5. As written, loops cannot iterate, contradicting the loop semantics described in §4.2.1 and assumed by Lemmas 1–3.","section":"§4.4, Algorithm 6, lines 10–13"},{"comment":"Definition 4 defines the proof-of-attack trace as the list E, but Algorithm 5 line 12 appends only watchpoint node names, and logic, loop count, and loop exit nodes are excluded. The trace example in §5.1, however, includes a timestamp (`2024-12-26T13:25:21...`) and a full `_EL_EXEC_RESP` payload, neither of which is recorded in E as defined. If proof-of-attack is claimed to be a chronological evidence trail, the semantics must either enrich E (or a separate evidence log) with timestamps and evidence, or the claim should be narrowed to 'ordered list of fired watchpoint nodes.'","section":"§5.1, Definition 4; trace example"},{"comment":"The efficiency claims are internally inconsistent. The text says EL gives a '7% reduction in labor' in initial execution, but Table 3a's People column drops from 27 to 18 (33%); even if 'labor' means person-months, the table gives 66 vs 55.25 person-months (16% reduction). The 7% figure matches only the time column (17 vs 15.75 months). No methodology is given for the month/person entries. The abstract's efficiency conclusion is therefore not supported by the data as presented.","section":"§6, Tables 3a/3b"}],"minor_comments":[{"comment":"Typo: 'CALDREA' should be 'CALDERA'.","section":"§7.2"},{"comment":"The ATT&CK identifier 'T10003_003_NTDSCredential-Dump' appears to have an extra zero; it should be consistent with identifiers such as 'T1003.002' used elsewhere.","section":"§5.1, trace example"},{"comment":"The statement 'The actual EL implementation is in Rust' would be more useful with an artifact/repository link or an availability statement, so that the semantics can be checked against the implementation.","section":"§4.4"},{"comment":"Node names mix spaces, underscores, and hyphens (e.g., 'T1105 IngressELRat', 'T1547 004 AutostartWinlogonPersistence'); consistent notation would improve readability.","section":"Fig. 2 and Table 2"}],"recommendation":"major_revision","confidential_remarks":"The two formal defects (Lemma 2 and Algorithm 6) are technical but fixable, and the efficiency table inconsistency should also be addressed. I recommend requesting a revision in which the authors correct the loop-activation timeout, repair or restrict Lemma 2 and its use in Theorem 2, and align the trace definition with the proof-of-attack example. The Wizard Spider example and the coordination-language idea are promising, but the paper should not be accepted in its current form."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The useful core here is a visual, directly executable attack-graph language with asynchronous watchpoints, delays, timeouts, and constrained loops, plus a proof-of-attack trace and a worked Wizard Spider example. The efficiency tables are plausible and the related work is honest about the Petri-net and coordination-language lineage. Section 8 openly says continuity and debugging are not covered, which is the right kind of scoping.\n\nBut the formal section, which is the paper's main selling point, is not sound as written. The stress-test note is right on both counts.\n\nFirst, Lemma 2 is false. Its proof claims that if a path passes through the loop count node then it also passes through the loop exit node. That is only true for paths that continue out of the loop. A path from the start to a node inside the loop, ending at A_j before the exit, will have all its loop-internal nodes reset when the count fires, and the path no longer contains any node in D∪A. Lemma 3 invokes Lemma 2 for arbitrary logic nodes, including those inside loops, so the induction—and therefore Theorem 2—is not established. This is a genuine gap, but it is likely repairable: the proof only needs the property for paths that eventually reach a goal, and those do pass through the exit. The lemma just needs to be restated and proved for that narrower use.\n\nSecond, Algorithm 6, line 13, activates the first loop node with expiry t*+delay(n) instead of t*+timeout(n). When delay is zero, the expiry is the current round's time, so garbage collection in Algorithm 9 deactivates it immediately. Loops cannot iterate under the published semantics. This looks like a simple typo—the right-hand side in the else branch should be timeout(n)—but it is load-bearing, and the reader's stress-test correctly flags it.\n\nMinor, proportionate note: the efficiency savings are self-reported with no code or data shipped, so they are not independently verifiable. That is common for this kind of paper, but it does mean the 58% repeating-execution savings should be read as anecdotal.\n\nOverall: the architecture is coherent, the writing is clear, and the authors seem to know what they are doing. The flaws are specific and fixable, not signs of sloppy thinking. The paper deserves a serious referee—send it to peer review—but the semantics section needs major revision before the claims about formally defined execution and proven reachability can be accepted. I would want to see a corrected Algorithm 6, a restored Lemma 2, and ideally a machine-checked version of the proofs, since the point of the paper is formal grounding.\n\nFor a reading group: maybe, as a case study in how small semantic bugs can sink a formalization. I would not cite it in its current form.","headline":"The paper's real contribution is a graph-based coordination language for APT emulation, but the published semantics has two concrete bugs that undermine the formal claims; as written, loops do not execute under Algorithm 6 and Lemma 2 is false.","tokens_in":33932,"tokens_out":2347,"would_cite":false,"duration_ms":17919,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"EL makes attack graphs directly executable: the visual plan is the program, with formal semantics and an automatic proof-of-attack trace.","keywords":["Effects Language","attack graphs","threat emulation","operational semantics","visual programming language","proof-of-attack","execution trace","formal methods"],"falsifier":"Run Algorithms 6 and 9 on a minimal loop with count 1 and a first node whose delay is 0: the node is added to the active set with expiry t* and then removed by garbage collection in the same round, so the loop body never executes — contradicting Lemmas 1 and Theorem 2. Equivalently, exhibit a path from a start node to the first loop node that contains the loop-count node but not the loop-exit node, which the Lemma 2 proof asserts cannot happen.","tokens_in":32908,"feed_emoji":"🔁","tokens_out":9228,"duration_ms":72589,"temperature":0.7,"pith_summary":"Effects Language (EL) is a visual programming language whose attack graphs are not just diagrams but executable specifications: the same graph an analyst draws is what runs against the target environment. The paper defines EL's operational semantics completely — a main loop that collects environment alerts, fires triggered watchpoint and logic nodes, manages delays, timeouts, loops, and garbage collection — and proves the properties an execution should have: node states always partition the graph, executions terminate when loops are finite, and goal nodes are reachable whenever a path exists and watchpoints eventually fire. Because the engine appends every fired node to a trace E, the run itself produces a proof-of-attack: a chronological, evidenced record of what the adversary did. Applying EL to steps from a published advanced-threat emulation plan, the authors report that repeat executions take 58% less time and require 63% less labor than the previous approach. If the semantics hold, EL would give red teams and tool evaluators a low-labor way to run the same multi-step campaign again and again with a verifiable log of what happened.","feed_headline":"Repeatable attack emulation drops 58% in time, 63% in labor","feed_subtitle":"Formal semantics lets the visual attack plan itself run, and the trace doubles as proof-of-attack.","key_machinery":"The load-bearing machinery is the four-state node model — inactive, delayed, active, fired — driven by a time-stamped main loop (Algorithms 1–9). Each watchpoint node carries a delay and a timeout; delays hold a node in D until a specified time, timeouts set its expiry in A, and garbage collection removes expired nodes. The constrained loop structure is what makes cycles tractable: a loop-count node has exactly two children, the loop's first node and a loop-exit node, and firing the exit node resets every node in the loop. The paper's proofs depend on these structural constraints to show that the D/A/F sets form a partition and that forward progress is never lost.","core_discovery":"The paper's central claim is that an attack graph can be the program itself. An EL graph — activation nodes with watchpoints, guarded effect nodes that run scripts, logic nodes expressing AND/OR joins, and strictly constrained loops — is given a graph-based operational semantics: Algorithm 1 polls the environment for alerts, activates delayed nodes, fires triggered nodes, processes loop-count and loop-exit nodes, and garbage-collects timeouts, with the full behavior specified by Algorithms 1–9. On that basis the paper proves Theorem 1 (the delayed, active, and fired sets partition the graph at every step), Lemma 1 (finite loop counts imply finite executions), Lemma 2 (every path that once co","pith_inferences":["If the semantics are made fully rigorous, EL graphs become objects that can be statically checked before execution — for example, to detect deadlocking watchpoints or unsatisfiable joins that would stall a campaign.","The proof-of-attack trace could be reused in reverse: align the adversary-side trace against defender alerts to score detection coverage automatically on every run.","A natural stress-test is to port the same emulation plan to other automation frameworks and compare time, labor, and fidelity on identical scenarios, something the paper does not attempt.","The gap between the published pseudocode and the proofs (loop activation and garbage-collection timing) suggests that machine-checked proofs of the state-partition invariant would be a worthwhile next step to catch subtle timing defects before they ship."],"forward_implications":["An EL graph is directly executable, so the visual plan needs no translation into another format, eliminating a whole class of human translation errors.","Every run accumulates a trace E of fired nodes with the alerts that triggered them, giving vendor evaluations a ready-made, timestamped proof-of-attack.","Because effects are opaque scripts attached to nodes, attack steps written in different languages can be coordinated in one graph without reimplementation.","The reported savings — 58% less time and 63% less labor on repeat runs — mean campaigns can be re-run frequently for training, what-if tests, and tool scoring at a fraction of current cost.","Under the theorem's conditions (finite loop counts, no finite timeouts, watchpoints eventually satisfied, at least one start-to-goal path), a goal node is guaranteed to be reached, so a well-formed EL plan will not stall for reasons intrinsic to the semantics."],"fun_headline_variants":["Attack graph runs itself: 58% faster, 63% less labor","Visual attack language proves its own execution traces","Repeatable adversary emulation cuts time 58%, labor 63%","Graph semantics turn attack plans into executable proof","Effects Language: formal semantics for automated attack emulation"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The reachability guarantee stands only if the loop semantics behave exactly as the proofs assume: the published proof claims every path through a loop-count node also passes through the loop-exit node, which is false for paths that end inside the loop, and the published activation rule sets a zero-delay loop node's expiry to the current time, so garbage collection can remove it in the same round.","fun_headline_variants_meta":{"raw":{"variants":["Attack graph runs itself: 58% faster, 63% less labor","Visual attack language proves its own execution traces","Repeatable adversary emulation cuts time 58%, labor 63%","Graph semantics turn attack plans into executable proof","Effects Language: formal semantics for automated attack emulation"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000696,"raw_usage":{"total_tokens":2941,"prompt_tokens":662,"completion_tokens":2279,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":406,"completion_tokens_details":{"reasoning_tokens":2198}},"tokens_in":406,"tokens_out":2279,"duration_ms":11618,"temperature":1.0,"reasoning_tokens":2198,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T11:10:32.260199+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run Algorithms 6 and 9 on a minimal loop with count 1 and a first node whose delay is 0: the node is added to the active set with expiry t* and then removed by garbage collection in the same round, so the loop body never executes — contradicting Lemmas 1 and Theorem 2. Equivalently, exhibit a path from a start node to the first loop node that contains the loop-count node but not the loop-exit node, which the Lemma 2 proof asserts cannot happen.","supporting_citations":[],"review_version":1}