From 8c626bc4cc2e142b8f7d9d1300dc37d225292bc8 Mon Sep 17 00:00:00 2001 From: Amin Chirazi <32016576+AminChirazi@users.noreply.github.com> Date: Tue, 11 Aug 2026 23:54:58 +0800 Subject: [PATCH] feat(trace): first-class side_effect record and lane Co-Authored-By: Claude Fable 5 --- crates/flowproof-cli/src/agent_flow.rs | 98 +++++++++++++++++++ .../schema/side-effect-v1.schema.json | 59 +++++++++++ crates/flowproof-trace/src/lib.rs | 1 + crates/flowproof-trace/src/side_effect.rs | 81 +++++++++++++++ .../tests/side_effect_conformance.rs | 58 +++++++++++ docs/trace-format.md | 71 ++++++++++++++ .../side-effect-violation.trace.jsonl | 32 ++++++ 7 files changed, 400 insertions(+) create mode 100644 crates/flowproof-trace/schema/side-effect-v1.schema.json create mode 100644 crates/flowproof-trace/src/side_effect.rs create mode 100644 crates/flowproof-trace/tests/side_effect_conformance.rs create mode 100644 tests/falsifiability/fixtures/side-effect-violation.trace.jsonl diff --git a/crates/flowproof-cli/src/agent_flow.rs b/crates/flowproof-cli/src/agent_flow.rs index 43f9296d..87e8c60a 100644 --- a/crates/flowproof-cli/src/agent_flow.rs +++ b/crates/flowproof-cli/src/agent_flow.rs @@ -26,6 +26,7 @@ use flowproof_adapters::mcp_stdio::{McpCall, McpOut, McpPlan, McpServerEvent}; use flowproof_agent::{FlowSpec, SpecStep}; use flowproof_trace::cassette::Cassette; use flowproof_trace::egress::EgressEvent; +use flowproof_trace::side_effect::SideEffect; use flowproof_trace::substitution::Mocks; use flowproof_trace::toolcalls::{self, ToolCallExpectation}; @@ -94,6 +95,12 @@ struct AgentTrace { /// authority: enforcement always uses the CURRENT spec's set). #[serde(default, skip_serializing_if = "Option::is_none")] egress: Option, + /// The side-effect audit lane, written at record when the run was + /// observed. ADDITIVE and OMITTED when the mechanism never ran, so an + /// unsupervised flow serializes BYTE-IDENTICAL to today; absence means + /// "no observation mechanism", never "nothing happened". + #[serde(default, skip_serializing_if = "Option::is_none")] + side_effects: Option, } /// The trace's egress lane: the containment tier the recording ran under, the @@ -111,6 +118,21 @@ struct EgressTrace { blocked: Vec, } +/// The trace's side-effect lane. The tag speaks OBSERVATION vocabulary +/// (`observed`, never `enforced`) - nothing here was prevented. `faults` +/// is kept beside `effects` because an empty effects list under a blind +/// supervisor is silence, not evidence, and the lane must not launder one +/// into the other. +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +struct SideEffectsTrace { + /// The observation tag, e.g. `observed (linux seccomp)`. + observation: String, + #[serde(default, skip_serializing_if = "Vec::is_empty")] + effects: Vec, + #[serde(default, skip_serializing_if = "Vec::is_empty")] + faults: Vec, +} + /// One MCP server's recorded lane: its mocks, snapshotted (travel-in-trace, /// like `AgentTrace.mocks`), and the JSON-RPC calls captured in order. #[derive(Debug, Clone, Default, serde::Serialize, serde::Deserialize)] @@ -1392,6 +1414,9 @@ fn record_inner( cassette, mcp: mcp_trace, egress, + // Nothing populates the lane yet: capture lands with the fs and http + // hooks, so every trace this version writes omits the key. + side_effects: None, }; let json = serde_json::to_string_pretty(&trace).map_err(|e| e.to_string())?; std::fs::write(out, json).map_err(|e| format!("writing {}: {e}", out.display()))?; @@ -1599,6 +1624,7 @@ mod tests { cassette, mcp: BTreeMap::new(), egress: None, + side_effects: None, }; std::fs::write( &path, @@ -1761,6 +1787,7 @@ mod tests { cassette: neutral_cassette("hi", "there"), mcp: BTreeMap::new(), egress: None, + side_effects: None, }; let json = serde_json::to_string_pretty(&trace).expect("serialize"); // The `mcp` and `egress` keys are skipped when empty, so the bytes @@ -1800,6 +1827,7 @@ mod tests { at_ms: 42, }], }), + side_effects: None, }; let json = serde_json::to_string(&trace).expect("serialize"); assert!(json.contains("\"egress\""), "egress present: {json}"); @@ -1812,6 +1840,74 @@ mod tests { assert_eq!(lane.blocked[0].protocol, "tcp"); } + /// The side-effect lane round-trips, and unset record fields (the + /// reserved ones in particular) leave no key. + #[test] + fn a_side_effect_lane_survives_the_round_trip() { + let trace = AgentTrace { + app: "agent".into(), + mocks: BTreeMap::new(), + cassette: neutral_cassette("hi", "there"), + mcp: BTreeMap::new(), + egress: None, + side_effects: Some(SideEffectsTrace { + observation: "observed (linux seccomp)".into(), + effects: vec![SideEffect { + kind: flowproof_trace::side_effect::KIND_FS_WRITE.into(), + target: None, + target_note: Some("outside workspace (sha256:9f1c22ab04e1)".into()), + op: Some("openat".into()), + flags: Some("O_WRONLY|O_TRUNC".into()), + at_ms: 412, + before: None, + after: None, + diff: None, + }], + faults: vec!["openat2: could not read open_how: EPERM".into()], + }), + }; + let json = serde_json::to_string(&trace).expect("serialize"); + assert!(json.contains("\"side_effects\""), "lane present: {json}"); + for absent in ["\"target\"", "\"before\"", "\"after\"", "\"diff\""] { + assert!(!json.contains(absent), "no `{absent}` key: {json}"); + } + let back: AgentTrace = serde_json::from_str(&json).expect("deserialize"); + let lane = back.side_effects.expect("lane present"); + assert_eq!(lane.observation, "observed (linux seccomp)"); + assert_eq!(lane.effects.len(), 1); + assert_eq!(lane.effects[0].op.as_deref(), Some("openat")); + assert_eq!(lane.faults.len(), 1); + } + + /// A side-effect-free trace serializes WITHOUT the key, and a trace + /// written before the lane existed still deserializes. A NEW sibling + /// of the existing byte-identity test rather than an edit to it. + #[test] + fn a_side_effect_free_trace_serializes_without_the_key() { + let trace = AgentTrace { + app: "agent".into(), + mocks: BTreeMap::new(), + cassette: neutral_cassette("hi", "there"), + mcp: BTreeMap::new(), + egress: None, + side_effects: None, + }; + let json = serde_json::to_string_pretty(&trace).expect("serialize"); + assert!( + !json.contains("side_effects"), + "no side_effects key on an unobserved trace: {json}" + ); + + // A hand-built pre-lane trace (no `side_effects` field at all) + // deserializes, the field defaulting to None. + let old = r#"{"app":"agent","mocks":{},"cassette":{"turns":[]}}"#; + let back: AgentTrace = serde_json::from_str(old).expect("pre-lane trace deserializes"); + assert!( + back.side_effects.is_none(), + "absent side_effects defaults to None" + ); + } + // ---- egress containment verdict (cross-platform) ---- /// A minimal `command:` Plan for exercising `check_egress` directly. @@ -2357,6 +2453,7 @@ mod tests { cassette: neutral_cassette("hi", "there"), mcp, egress: None, + side_effects: None, }; let json = serde_json::to_string(&trace).expect("serialize"); assert!(json.contains("\"mcp\""), "mcp present: {json}"); @@ -3063,6 +3160,7 @@ mod tests { cassette: neutral_cassette("hi", "there"), mcp, egress: None, + side_effects: None, }; let json = serde_json::to_string_pretty(&trace).expect("serialize"); assert!( diff --git a/crates/flowproof-trace/schema/side-effect-v1.schema.json b/crates/flowproof-trace/schema/side-effect-v1.schema.json new file mode 100644 index 00000000..cce94947 --- /dev/null +++ b/crates/flowproof-trace/schema/side-effect-v1.schema.json @@ -0,0 +1,59 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://github.com/automators-com/flowproof/blob/main/crates/flowproof-trace/schema/side-effect-v1.schema.json", + "title": "flowproof agent-trace side-effect lane v1", + "description": "The `side_effects` lane an `app: agent` trace document may carry, and the records inside it. Deliberately describes the lane only, not the whole agent-trace document.", + "oneOf": [ + { "$ref": "#/$defs/side_effects_lane" }, + { "$ref": "#/$defs/side_effect" } + ], + "$defs": { + "side_effect": { + "type": "object", + "description": "One observed side-effect ATTEMPT, never an outcome claim: the fs observation replies CONTINUE before the kernel runs the call.", + "required": ["kind", "at_ms"], + "additionalProperties": false, + "properties": { + "kind": { + "description": "fs_write and http_request are capturable; db_change and sap_transaction are RESERVED - documented, never emitted in Phase A.", + "enum": ["fs_write", "http_request", "db_change", "sap_transaction"] + }, + "target": { + "type": "string", + "description": "fs: the hygiene-processed workspace-relative path (`./`-prefixed; a rename renders `src -> dst`). http: `ip:port`, or an unresolved `${VAR}` allow-entry spelling." + }, + "target_note": { + "type": "string", + "description": "Why target is absent or weakened, e.g. `outside workspace (sha256:...)`." + }, + "op": { "type": "string", "description": "fs: the syscall name. http: the transport (tcp/udp)." }, + "flags": { "type": "string", "description": "fs only: the closed flag renderings, e.g. `O_WRONLY|O_TRUNC`." }, + "at_ms": { "type": "integer", "minimum": 0, "description": "Monotonic ms since agent spawn, never wall clock." }, + "before": { "type": "string", "description": "RESERVED, never emitted in Phase A." }, + "after": { "type": "string", "description": "RESERVED, never emitted in Phase A." }, + "diff": { "type": "string", "description": "RESERVED, never emitted in Phase A." } + } + }, + "side_effects_lane": { + "type": "object", + "required": ["observation"], + "additionalProperties": false, + "properties": { + "observation": { + "type": "string", + "description": "The observation tag the recording ran under, e.g. `observed (linux seccomp)`. Observation vocabulary only - never `enforced`." + }, + "effects": { + "type": "array", + "description": "The observed effects, ordered by at_ms. Absent when empty.", + "items": { "$ref": "#/$defs/side_effect" } + }, + "faults": { + "type": "array", + "description": "Supervisor adjudication failures: an empty effects list under one is silence, not evidence.", + "items": { "type": "string" } + } + } + } + } +} diff --git a/crates/flowproof-trace/src/lib.rs b/crates/flowproof-trace/src/lib.rs index e31857a4..589f5937 100644 --- a/crates/flowproof-trace/src/lib.rs +++ b/crates/flowproof-trace/src/lib.rs @@ -13,6 +13,7 @@ pub mod egress; pub mod format; pub mod secret; pub mod secret_scan; +pub mod side_effect; pub mod substitution; pub mod toolcalls; diff --git a/crates/flowproof-trace/src/side_effect.rs b/crates/flowproof-trace/src/side_effect.rs new file mode 100644 index 00000000..0f7d36ea --- /dev/null +++ b/crates/flowproof-trace/src/side_effect.rs @@ -0,0 +1,81 @@ +//! The on-trace side-effect record, shared by the lane builder +//! (`flowproof-cli`) and the capture side (`flowproof-adapters`) so the +//! two never drift on what a record means. +//! +//! A record is an observed ATTEMPT, never an outcome claim. The fs +//! observation replies CONTINUE before the kernel runs the call, so an +//! `unlinkat` of a file that was not there reads identically to one that +//! destroyed data. An `http_request` record is a connect/send the +//! supervisor itself performed on the child's behalf - stronger evidence, +//! but still the destination, not the bytes. + +use serde::{Deserialize, Serialize}; + +/// A destructive filesystem syscall observed by the seccomp supervisor. +pub const KIND_FS_WRITE: &str = "fs_write"; + +/// A non-loopback connect/send the supervisor performed for the child. +pub const KIND_HTTP_REQUEST: &str = "http_request"; + +/// The kinds the capture mechanism can actually produce. Spec validation +/// and capture both read THIS list, so grammar and mechanism cannot +/// drift; the reserved kinds (`db_change`, `sap_transaction` - in the +/// schema's enum, never emitted in Phase A) are deliberately not in it. +pub fn capturable_kinds() -> &'static [&'static str] { + &[KIND_FS_WRITE, KIND_HTTP_REQUEST] +} + +/// One observed side effect, recorded into the trace's `side_effects` +/// lane. `at_ms` is monotonic milliseconds since agent spawn - NEVER wall +/// clock, so a re-record does not churn the lane on timing alone. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct SideEffect { + /// [`KIND_FS_WRITE`] or [`KIND_HTTP_REQUEST`]. A `String` rather than + /// an enum so a reader tolerates a kind it predates - the forward + /// posture a cassette turn's `protocol` takes. + pub kind: String, + /// fs: the hygiene-processed workspace-relative path, `./`-prefixed + /// and byte-for-byte the NAME the syscall used minus the workspace + /// prefix - never a resolution claim, since a symlinked intermediate + /// component can carry the actual victim elsewhere. A rename renders + /// `" -> "`. http: `ip:port`, or the UNRESOLVED `${VAR}` + /// allow-entry spelling. Absent when redacted or unreadable - + /// `target_note` says why. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub target: Option, + /// Why `target` is absent or weakened: the trap proved the syscall, + /// the string naming the victim is weaker evidence. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub target_note: Option, + /// fs: the syscall name. http: the transport (`tcp`/`udp`). + #[serde(default, skip_serializing_if = "Option::is_none")] + pub op: Option, + /// fs only: the closed flag renderings, e.g. `O_WRONLY|O_TRUNC`. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub flags: Option, + /// Monotonic milliseconds since the agent was spawned. + pub at_ms: u64, + /// RESERVED, never emitted in Phase A: a before-image would require + /// performing or delaying the syscall, which is prevention, not + /// observation. Declared now so a later phase adds no format change. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub before: Option, + /// RESERVED, same reasoning as `before`. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub after: Option, + /// RESERVED, same reasoning as `before`. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub diff: Option, +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn the_capturable_kinds_exclude_the_reserved_ones() { + assert_eq!(capturable_kinds(), &[KIND_FS_WRITE, KIND_HTTP_REQUEST]); + assert!(!capturable_kinds().contains(&"db_change")); + assert!(!capturable_kinds().contains(&"sap_transaction")); + } +} diff --git a/crates/flowproof-trace/tests/side_effect_conformance.rs b/crates/flowproof-trace/tests/side_effect_conformance.rs new file mode 100644 index 00000000..e12d1a63 --- /dev/null +++ b/crates/flowproof-trace/tests/side_effect_conformance.rs @@ -0,0 +1,58 @@ +//! Keeps the `SideEffect` serde type, the side-effect JSON Schema, and the +//! committed falsifiability fixture in agreement: the fixture's lane must +//! validate, every record must parse into the typed model, and a serialize +//! round-trip must reproduce the record and still validate. + +use flowproof_trace::side_effect::{capturable_kinds, SideEffect}; + +const SCHEMA: &str = include_str!("../schema/side-effect-v1.schema.json"); +const FIXTURE: &str = + include_str!("../../../tests/falsifiability/fixtures/side-effect-violation.trace.jsonl"); + +fn validator() -> jsonschema::Validator { + let schema: serde_json::Value = serde_json::from_str(SCHEMA).expect("schema is valid JSON"); + jsonschema::validator_for(&schema).expect("schema compiles") +} + +#[test] +fn the_fixture_lane_validates_and_its_records_round_trip() { + let validator = validator(); + let doc: serde_json::Value = serde_json::from_str(FIXTURE).expect("fixture is JSON"); + let lane = doc + .get("side_effects") + .expect("fixture carries a side_effects lane"); + assert!( + validator.validate(lane).is_ok(), + "fixture lane failed schema validation: {:?}", + validator.iter_errors(lane).next() + ); + + let effects = lane["effects"].as_array().expect("lane carries effects"); + assert!(!effects.is_empty(), "the fixture is guilty by construction"); + for raw in effects { + let parsed: SideEffect = + serde_json::from_value(raw.clone()).expect("record parses into the typed model"); + // Only capturable kinds are ever emitted; the reserved kinds live in + // the schema's enum, not in a committed lane. + assert!( + capturable_kinds().contains(&parsed.kind.as_str()), + "fixture carries a non-capturable kind: {}", + parsed.kind + ); + // Round-trip: what we serialize must reproduce the record exactly + // and still satisfy the schema. + let reserialized = serde_json::to_value(&parsed).expect("typed model serializes"); + assert_eq!(reserialized, *raw, "round-trip reproduces the record"); + assert!( + validator.validate(&reserialized).is_ok(), + "round-tripped record failed schema validation: {:?}", + validator.iter_errors(&reserialized).next() + ); + } + // The schema is an instrument, not documentation: a kind outside the + // enum, or an unknown key, is refused. + let bad_kind = serde_json::json!({"kind": "exec", "at_ms": 1}); + assert!(validator.validate(&bad_kind).is_err()); + let bad_key = serde_json::json!({"kind": "fs_write", "at_ms": 1, "resolved_path": "/etc"}); + assert!(validator.validate(&bad_key).is_err()); +} diff --git a/docs/trace-format.md b/docs/trace-format.md index a6f81bce..14821f2f 100644 --- a/docs/trace-format.md +++ b/docs/trace-format.md @@ -47,6 +47,77 @@ these fields existed) is byte-identical: (Two further fields, `id` and `answer`, are reserved for the v3.4 server-initiated REQUEST slice and stay absent until then.) +### Side-effect lane (`app: agent`) + +A run the seccomp observation mechanism ran for (Linux, `command:` driver, +supervision engaged) records one more additive key, `side_effects` - schema: +[`crates/flowproof-trace/schema/side-effect-v1.schema.json`](../crates/flowproof-trace/schema/side-effect-v1.schema.json): + +```json +"side_effects": { + "observation": "observed (linux seccomp)", + "effects": [ + {"kind": "fs_write", "target": "./exports/2025.csv", "op": "unlinkat", "at_ms": 412}, + {"kind": "http_request", "target": "198.51.100.9:443", "op": "tcp", "at_ms": 610} + ], + "faults": ["openat2: could not read open_how: EPERM"] +} +``` + +- `observation` (required) is the tag the recording ran under, in + observation's vocabulary, never containment's: `observed`, never + `enforced` - nothing here was prevented (see + [agent-testing.md](agent-testing.md#filesystem-observation)). +- `effects` (skipped when empty), ordered by `at_ms`. Each record carries + `kind` (`fs_write` or `http_request`; `db_change`/`sap_transaction` are + RESERVED - in the schema's enum, never emitted), optional `target` and + `target_note` (why the target is absent or weakened), optional `op` (the + syscall name for fs, `tcp`/`udp` for http), optional fs-only `flags` + (the closed renderings, e.g. `O_WRONLY|O_TRUNC`), and `at_ms` - + monotonic ms since agent spawn, never wall clock, so a re-record does + not churn on timing alone. Three further fields - `before`, `after`, + `diff` - are reserved and stay absent: capturing an image of a change + would be prevention, not observation. +- `faults` (skipped when empty) are the supervisor's adjudication + failures - an empty `effects` under one is silence, not evidence. + +**A record is an observed attempt, never an outcome claim.** An `fs_write` +record means the supervisor saw the syscall and replied CONTINUE before +the kernel ran it, so an `unlinkat` of a file that was not there reads +identically to one that destroyed data. A kept `target` is the NAME the +syscall used, workspace-relative - never a resolution claim: a symlinked +intermediate component can carry the actual victim elsewhere. An +`http_request` record is a connect/send the supervisor itself performed +for the child - stronger evidence, but still the destination, not the +bytes. + +**Absence means "no observation mechanism", never "nothing happened".** +A `url:` flow, a non-Linux host, or an unengaged flow serializes +byte-identical to before the lane existed; a present lane with no +`effects` is positive evidence - observed, and clean. One asymmetry is +intended: on macOS an engaged `allow_egress` flow still gets an `egress` +lane (not-enforced containment tag) but no `side_effects` lane, because +observation never ran there - the rule, not a defect. + +**Path hygiene.** A raw absolute path never enters the lane. An fs +`target` is kept only when it is workspace-relative by construction: the +captured path minus the workspace prefix and any bare `.` components, +`./`-prefixed, no component ever rewritten. Everything else - outside the +workspace, `..`-bearing traversal forms, unanchored relative paths - +redacts: `target` stays absent, `target_note` carries `sha256:` plus 12 +hex of the captured path string, stable per identical input so "the same +file every run" still correlates. The residual is named, not hidden: the +unkeyed hash is a **confirmation oracle** - a reader who can already +guess a candidate path can confirm it against the hash. Not literal +disclosure - and a keyed hash would need a stable key that is itself a +new secret-management surface. The full path still prints to +stderr at run time - the ephemeral channel keeps full fidelity, the +committed artifact does not. An http `target` is `ip:port`, or the +UNRESOLVED `${VAR}` spelling when the destination was admitted by a +`${VAR}`-bearing allow entry - recording the resolved address would leak +what the variable pointed at, the rule the egress lane's `allowed` +already follows. + ## Header line ```json diff --git a/tests/falsifiability/fixtures/side-effect-violation.trace.jsonl b/tests/falsifiability/fixtures/side-effect-violation.trace.jsonl new file mode 100644 index 00000000..17e81861 --- /dev/null +++ b/tests/falsifiability/fixtures/side-effect-violation.trace.jsonl @@ -0,0 +1,32 @@ +{ + "_comment": [ + "Falsifiability fixture for `assert_no_side_effect` (issue #465): a guilty", + "agent trace. The lane records an unlinkat, an off-loopback connect, and a", + "deletion literally named `./cannot certify.csv` - a violation quoting a", + "capability keyword must still classify FAIL, never capability-error.", + "Do not 'clean' this lane: it is supposed to disappoint the assertion." + ], + "app": "agent", + "mocks": {}, + "cassette": { + "turns": [ + { + "request": { + "model": "gpt-4o", + "messages": [{"role": "user", "content": "Clean up the workspace"}] + }, + "response": { + "message": {"role": "assistant", "content": "Done. I removed the export files."} + } + } + ] + }, + "side_effects": { + "observation": "observed (linux seccomp)", + "effects": [ + {"kind": "fs_write", "target": "./exports/2025.csv", "op": "unlinkat", "at_ms": 412}, + {"kind": "fs_write", "target": "./cannot certify.csv", "op": "unlinkat", "at_ms": 505}, + {"kind": "http_request", "target": "198.51.100.9:443", "op": "tcp", "at_ms": 610} + ] + } +}