diff --git a/crates/flowproof-agent/src/spec.rs b/crates/flowproof-agent/src/spec.rs index 4532db2..92eac8f 100644 --- a/crates/flowproof-agent/src/spec.rs +++ b/crates/flowproof-agent/src/spec.rs @@ -619,6 +619,7 @@ impl FlowSpec { | SpecStep::AssertToolCall { .. } | SpecStep::AssertNoToolCall { .. } | SpecStep::AssertNoEgress + | SpecStep::AssertNoSideEffect { .. } ) }); @@ -1463,6 +1464,13 @@ pub enum SpecStep { /// phase, and a capability error on any platform where containment is /// not enforced. AssertNoEgress, + /// `app: agent`: assert the run OBSERVED no side effect of the named + /// kind (`fs_write` | `http_request`). Judged against the live + /// observation log of each phase, and a capability error on any + /// platform or driver where observation cannot run. + AssertNoSideEffect { + assert_no_side_effect: String, + }, /// `app: agent`: assert NO declared secret appeared in the run's output /// corpus. The named-selector form: one or more `${VAR}` names, each a /// secret that must never surface. The `${VAR}` values resolve at @@ -1570,6 +1578,7 @@ impl SpecStep { `assert_sql: {...}`, `assert_api: {...}`, `assert_screenshot: {...}`, \ `prompt: `, `assert_tool_call: `, \ `assert_no_tool_call: `, `assert_no_egress`, \ + `assert_no_side_effect: `, \ `assert_no_secret_leak: ${VAR}`, `repeat: {...}`, `when: ` with `steps:`, \ `in: ` with `steps:`, or `foreach: {...}`"; @@ -1639,6 +1648,39 @@ impl SpecStep { }), _ => Err("`assert_no_tool_call:` takes a string (a tool name)".into()), }, + // `assert_no_side_effect:` takes ONE capturable kind, + // read off the same list the capture mechanism emits, so + // grammar and mechanism cannot drift; the schema's + // reserved kinds earn their own message. + Some("assert_no_side_effect") => { + let kind = match inner { + Value::String(s) => s.trim().to_string(), + _ => { + return Err( + "`assert_no_side_effect:` takes one kind (`fs_write` or \ + `http_request`)" + .into(), + ) + } + }; + if ["db_change", "sap_transaction"].contains(&kind.as_str()) { + return Err(format!( + "`{kind}` is reserved for a later phase, not yet capturable; \ + `assert_no_side_effect:` takes `fs_write` or `http_request`" + )); + } + if !flowproof_trace::side_effect::capturable_kinds() + .contains(&kind.as_str()) + { + return Err(format!( + "`{kind}` is not a capturable side-effect kind; \ + `assert_no_side_effect:` takes `fs_write` or `http_request`" + )); + } + Ok(SpecStep::AssertNoSideEffect { + assert_no_side_effect: kind, + }) + } // `assert_no_secret_leak:` takes a single `${VAR}` // selector or a LIST of them. Each is validated to be // `${VAR}` syntax here, so a literal or a predicate is a @@ -1797,6 +1839,9 @@ impl Serialize for SpecStep { SpecStep::AssertNoToolCall { assert_no_tool_call, } => single(serializer, "assert_no_tool_call", assert_no_tool_call), + SpecStep::AssertNoSideEffect { + assert_no_side_effect, + } => single(serializer, "assert_no_side_effect", assert_no_side_effect), SpecStep::AssertSql { assert_sql } => single(serializer, "assert_sql", assert_sql), SpecStep::AssertApi { assert_api } => single(serializer, "assert_api", assert_api), SpecStep::AssertScreenshot { assert_screenshot } => { @@ -1978,6 +2023,9 @@ impl SpecStep { format!("assert_no_tool_call: {assert_no_tool_call}") } SpecStep::AssertNoEgress => "assert_no_egress".to_string(), + SpecStep::AssertNoSideEffect { + assert_no_side_effect, + } => format!("assert_no_side_effect: {assert_no_side_effect}"), SpecStep::AssertNoSecretLeak { assert_no_secret_leak, } => { @@ -3164,6 +3212,37 @@ steps: assert!(err.to_string().contains("assert_no_egress"), "{err}"); } + /// `assert_no_side_effect` takes only the CAPTURABLE kinds and + /// round-trips as its keyed mapping. A reserved kind is refused with + /// its own message - "reserved", never "unknown" - and the step is + /// agent-only like the rest of the agent vocabulary. + #[test] + fn assert_no_side_effect_takes_only_capturable_kinds() { + let flow = spec( + "name: n\napp: agent\nagent:\n command: x\nsteps:\n - prompt: hi\n - assert_no_side_effect: fs_write\n - assert_no_side_effect: http_request\n", + ) + .expect("parses"); + let yaml = serde_yaml::to_string(&flow.steps).expect("serializes"); + let back: Vec = serde_yaml::from_str(&yaml).expect("round-trips"); + assert_eq!(back, flow.steps); + + for (kind, why) in [ + ("db_change", "reserved for a later phase"), + ("exec", "not a capturable"), + ] { + let err = spec(&format!( + "name: n\napp: agent\nagent:\n command: x\nsteps:\n - prompt: hi\n - assert_no_side_effect: {kind}\n" + )) + .expect_err(why); + assert!(err.to_string().contains(why), "{err}"); + } + + let err = + spec("name: n\napp: calc\nsteps:\n - Type 5\n - assert_no_side_effect: fs_write\n") + .expect_err("assert_no_side_effect on calc"); + assert!(err.to_string().contains("agent step"), "{err}"); + } + /// A full `mcp:` block parses: servers, commands, and per-server tool /// mocks all land where the trace and stand-in expect them. #[test] diff --git a/crates/flowproof-cli/src/agent_flow.rs b/crates/flowproof-cli/src/agent_flow.rs index b8c234e..6bcb856 100644 --- a/crates/flowproof-cli/src/agent_flow.rs +++ b/crates/flowproof-cli/src/agent_flow.rs @@ -617,6 +617,11 @@ struct Plan { /// contained - identical in record and replay, so both install (or skip) /// the seccomp filter the same way. engages_egress: bool, + /// The kinds `assert_no_side_effect` steps forbid, in step order. + no_side_effects: Vec, + /// [`engages_observation`]: routes a Linux `command:` driver through + /// the supervised path. + observes: bool, /// The `assert_no_secret_leak` steps, each naming one or more `${VAR}` /// selectors and its 1-based position in the flow's `steps:` (for the /// failure message). Only the variable NAMES travel here - never a value. @@ -663,6 +668,20 @@ impl Plan { /* egress_engaged: */ true, ) .map_err(|e| e.to_string()), + // Observation-only supervision, Linux-gated BY CONSTRUCTION + // (seccomp exists nowhere else): elsewhere the flow takes the + // plain path below and the assertion fails "cannot certify". + Driver::Command(command) if cfg!(target_os = "linux") && self.observes => { + run_against_contained( + proxy, + command, + &self.env, + AGENT_TIMEOUT, + &AllowSet::allow_all(), + /* egress_engaged: */ false, + ) + .map_err(|e| e.to_string()) + } Driver::Command(command) => { run_against(proxy, command, &self.env, AGENT_TIMEOUT).map_err(|e| e.to_string()) } @@ -753,6 +772,7 @@ fn plan(spec: &FlowSpec) -> Result { let mut tool_calls = Vec::new(); let mut forbidden = Vec::new(); let mut reply_contains = Vec::new(); + let mut no_side_effects = Vec::new(); // The secret-leak assertions come from the shared spec accessor, the same // source web and api flows build their scan from. let secret_leaks = spec.secret_leak_assertions(); @@ -766,6 +786,9 @@ fn plan(spec: &FlowSpec) -> Result { } => { forbidden.push(parse_expectation(assert_no_tool_call)?); } + SpecStep::AssertNoSideEffect { + assert_no_side_effect, + } => no_side_effects.push(assert_no_side_effect.clone()), SpecStep::Assert { assert } => { // v1 reply assertion: `reply contains `. let trimmed = assert.trim(); @@ -799,6 +822,8 @@ fn plan(spec: &FlowSpec) -> Result { allow_unresolved, assert_no_egress, engages_egress: engages_egress(spec), + no_side_effects, + observes: engages_observation(spec), secret_leaks, }) } @@ -822,6 +847,17 @@ pub fn engages_egress(spec: &FlowSpec) -> bool { declares_allow || asserts_no_egress } +/// Whether a flow ENGAGES side-effect observation: it engages egress (one +/// filter contains and watches) or carries an `assert_no_side_effect` step. +/// PURE over the spec, like [`engages_egress`], for the same determinism. +pub fn engages_observation(spec: &FlowSpec) -> bool { + engages_egress(spec) + || spec + .steps + .iter() + .any(|s| matches!(s, SpecStep::AssertNoSideEffect { .. })) +} + /// The egress destinations containment DENIED during the recorded run, read /// from the trace's egress lane as value-free `destination (protocol)` /// descriptors. Empty for a flow with no egress lane, an unreadable trace, or @@ -852,6 +888,13 @@ pub fn egress_blocked(trace_path: &Path) -> Vec { /// egress installs no filter and claims no tier. pub fn containment(spec: &FlowSpec) -> Containment { if !engages_egress(spec) { + // An observation-only Linux `command:` flow WILL run supervised, so + // the prediction says what the run will: observed, not contained - + // never `enforced` for a wildcard policy nobody declared. + let command = spec.agent.as_ref().is_some_and(|a| a.command.is_some()); + if cfg!(target_os = "linux") && command && engages_observation(spec) { + return Containment::observation_only(); + } return Containment::not_engaged(); } match spec.agent.as_ref() { @@ -931,7 +974,9 @@ fn check_egress( // that never touches egress serializes byte-identical to today. This is // the SAME pure predicate that gated containment (`plan.engages_egress`); // `run.egress.blocked` can only be non-empty when it was already true, so - // the two decisions never disagree. + // the two decisions never disagree. Observation-only supervision keeps + // the claim: allow-all reaches no denied branch, so `blocked` stays + // empty and no egress lane is minted for a flow that engaged none. let engaged = plan.engages_egress || !run.egress.blocked.is_empty(); if !engaged { return Ok(None); @@ -1134,6 +1179,108 @@ fn side_effects_lane( }) } +/// Why observation did not run here, for the capability failure. +fn observation_unavailable_reason(plan: &Plan) -> &'static str { + match &plan.driver { + Driver::Http { .. } => "a url: service is not observed; flowproof does not own it", + Driver::Command(_) if cfg!(target_os = "linux") => { + "the seccomp observation mechanism did not run" + } + Driver::Command(_) => "side-effect observation is Linux-only (seccomp)", + } +} + +/// The `assert_no_side_effect` verdict, pure over platform-neutral data so +/// the falsifiability harness feeds fixture records through the SAME code +/// record and replay execute. Order copies `check_egress`: capability +/// honesty, then faults, then the set predicate. +pub fn side_effect_verdict( + asserted_kinds: &[String], + effects: &[SideEffect], + faults: &[String], + observed: bool, + reason: Option<&str>, +) -> Result<(), String> { + if asserted_kinds.is_empty() { + return Ok(()); + } + if !observed { + return Err(format!( + "side effects are not observable on this platform/driver ({}); \ + assert_no_side_effect cannot certify", + reason.unwrap_or("the observation mechanism did not run") + )); + } + // A blind supervisor makes an empty effects list silence, not evidence. + if !faults.is_empty() { + return Err(format!( + "side-effect observation ran but could not adjudicate {} trapped \ + syscall(s) ({}); assert_no_side_effect cannot certify", + faults.len(), + faults.join("; ") + )); + } + // Deduped by (kind, target). The message embeds the AGENT-chosen + // target, which is why it starts with the sentinel: classification + // hangs on a prefix only this function mints, never on target words. + let mut seen = std::collections::BTreeSet::new(); + let violations: Vec = effects + .iter() + .filter(|e| asserted_kinds.contains(&e.kind)) + .filter(|e| seen.insert((e.kind.clone(), e.target.clone()))) + .map(|e| { + format!( + "{} {} ({}) at {}ms", + e.kind, + e.target.as_deref().unwrap_or("[redacted]"), + e.op.as_deref().unwrap_or("?"), + e.at_ms + ) + }) + .collect(); + if violations.is_empty() { + return Ok(()); + } + Err(format!( + "{}{}; assert_no_side_effect: {} forbids it", + flowproof_replay::runrecord::SIDE_EFFECT_VIOLATION, + violations.join(", "), + asserted_kinds.join(", ") + )) +} + +/// Build the lane and judge THIS run's live log. Returns the lane whenever +/// the run was observed, assertion or not (the egress-lane precedent); a +/// failure means record mints no trace and replay fails the flow. +fn check_side_effects( + plan: &Plan, + run: &AgentRun, + workspace: &Path, +) -> Result, String> { + let lane = side_effects_lane(run, &plan.allow, workspace); + // Only faults RELEVANT to the asserted kinds can blind them. + let mut faults = Vec::new(); + if plan.no_side_effects.iter().any(|k| k == KIND_FS_WRITE) { + faults.extend(run.fs.distinct_faults()); + } + if plan.no_side_effects.iter().any(|k| k == KIND_HTTP_REQUEST) { + for fault in run.egress.distinct_faults() { + if !faults.contains(&fault) { + faults.push(fault); + } + } + } + let effects = lane.as_ref().map(|l| l.effects.as_slice()).unwrap_or(&[]); + side_effect_verdict( + &plan.no_side_effects, + effects, + &faults, + run.observed, + Some(observation_unavailable_reason(plan)), + )?; + Ok(lane) +} + /// The short containment tag stored in the trace lane (the parenthetical of /// the report line): `enforced (linux seccomp)` or `not contained ()`. /// The run record stores the SAME string, so the trace and the artifact an @@ -1572,11 +1719,11 @@ fn record_inner( report_fs(&run); *achieved = Some(achieved_tier(&run, &tier)); let egress = check_egress(&plan, &run, &tier)?; - // The side-effect lane, built whenever the run was observed (the - // workspace root is the agent's spawn cwd) and scanned WITH the - // cassette below, BEFORE the trace is minted - the same store-guard. + // The side-effect lane (workspace root = the agent's spawn cwd), built + // and JUDGED, then scanned with the cassette below BEFORE the trace is + // minted - a violating record mints no trace, the same store-guard. let workspace = std::env::current_dir().unwrap_or_default(); - let side_effects = side_effects_lane(&run, &plan.allow, &workspace); + let side_effects = check_side_effects(&plan, &run, &workspace)?; check_secret_leak(&plan, &cassette, &mcp_trace, side_effects.as_ref())?; let trace = AgentTrace { @@ -1655,6 +1802,9 @@ fn replay_inner( report_fs(&run); *achieved = Some(achieved_tier(&run, &tier)); check_egress(&plan, &run, &tier)?; + // The side-effect assertion judges THIS phase's LIVE log too; the + // recomputed lane is discarded - the lane is audit, never authority. + check_side_effects(&plan, &run, &std::env::current_dir().unwrap_or_default())?; // Re-scan the recorded corpus for declared secrets by the SAME mechanism // as record, so an unchanged system replays the same verdict. The corpus // is the recorded cassette + MCP lanes + side-effect lane (the proxy @@ -2263,6 +2413,8 @@ mod tests { engages_egress: !allow_unresolved.is_empty() || assert_no_egress, allow_unresolved, assert_no_egress, + no_side_effects: Vec::new(), + observes: false, secret_leaks: Vec::new(), } } @@ -2517,6 +2669,89 @@ mod tests { ); } + // ---- the side-effect assertion (cross-platform) ---- + + /// Capability and fault failures read `cannot certify`; a violation + /// classifies Fail even when its target spells a capability keyword. + #[test] + fn the_side_effect_verdict_is_honest_in_all_three_directions() { + use flowproof_replay::runrecord::is_capability_error; + let kinds = vec![KIND_FS_WRITE.to_string()]; + // Capability: not observed, no bypass, never a vacuous pass. + let err = side_effect_verdict(&kinds, &[], &[], false, Some("Linux-only")) + .expect_err("cannot certify unobserved"); + assert!( + err.contains("cannot certify") && err.contains("Linux-only"), + "{err}" + ); + assert!(is_capability_error(&err), "{err}"); + // Fault: an empty effects list under a blind supervisor is silence. + let err = side_effect_verdict(&kinds, &[], &["openat2: EPERM".into()], true, None) + .expect_err("a blind supervisor cannot certify"); + assert!( + err.contains("could not adjudicate") && err.contains("openat2"), + "{err}" + ); + assert!(is_capability_error(&err), "{err}"); + // Violation: named, and NEVER relabeled by its own target. + let unlink = SideEffect { + kind: KIND_FS_WRITE.into(), + target: Some("./cannot certify.txt".into()), + target_note: None, + op: Some("unlinkat".into()), + flags: None, + at_ms: 412, + before: None, + after: None, + diff: None, + }; + let err = + side_effect_verdict(&kinds, &[unlink], &[], true, None).expect_err("a violation fails"); + assert!( + err.contains("unlinkat") && err.contains("./cannot certify.txt"), + "{err}" + ); + assert!(!is_capability_error(&err), "the sentinel wins: {err}"); + // And falsifiable in the other direction: clean and observed passes. + side_effect_verdict(&kinds, &[], &[], true, None).expect("clean and observed"); + } + + /// Observation-only supervision mints NO egress lane: allow-all + /// reaches no denied branch, so the presence disjunct never fires. + #[test] + fn an_observation_only_run_mints_no_egress_lane() { + let plan = egress_plan(false, vec![]); + let mut run = egress_run(vec![]); + run.observed = true; + let lane = check_egress(&plan, &run, &Containment::observation_only()) + .expect("observation is not an egress verdict"); + assert!( + lane.is_none(), + "no egress lane for a flow that engaged none" + ); + } + + /// The tier-line pin: an observation-only flow's PREDICTION equals its + /// run's achieved tier, and neither ever says `enforced`. + #[test] + fn an_observation_only_flow_predicts_the_tier_its_run_achieves() { + let spec = FlowSpec::parse( + "name: n\napp: agent\nagent:\n command: x\nsteps:\n - prompt: hi\n - assert_no_side_effect: fs_write\n", + ) + .expect("parses"); + assert!(engages_observation(&spec) && !engages_egress(&spec)); + let predicted = containment(&spec); + assert!(!predicted.is_enforced(), "{predicted:?}"); + if cfg!(target_os = "linux") { + // The run constructor pins the same tier (adapters e2e). + assert_eq!(predicted, Containment::observation_only()); + } else { + assert_eq!(predicted, Containment::not_engaged()); + } + // An uncontained path decides no tier, so the prediction stands. + assert_eq!(achieved_tier(&egress_run(vec![]), &predicted), predicted); + } + /// A spec whose only shape that matters here is its tools/mcp blocks. fn tool_spec(yaml: &str) -> FlowSpec { FlowSpec::parse(yaml).expect("spec parses") diff --git a/crates/flowproof-cli/src/lib.rs b/crates/flowproof-cli/src/lib.rs index 91b51e4..8efba1e 100644 --- a/crates/flowproof-cli/src/lib.rs +++ b/crates/flowproof-cli/src/lib.rs @@ -1583,6 +1583,13 @@ fn build_control_record( if agent_flow::engages_egress(spec) { lanes.push("egress".to_string()); } + if spec + .steps + .iter() + .any(|s| matches!(s, flowproof_agent::SpecStep::AssertNoSideEffect { .. })) + { + lanes.push("side_effects".to_string()); + } if !secrets_checked.is_empty() { lanes.push("secret_leak".to_string()); } @@ -1945,7 +1952,8 @@ struct AuditControl { verdict: flowproof_replay::ControlVerdict, #[serde(skip_serializing_if = "Option::is_none")] reason: Option, - /// Which control lanes the flow asserted (`egress`, `secret_leak`). + /// Which control lanes the flow asserted (`egress`, `secret_leak`, + /// `side_effects`). #[serde(skip_serializing_if = "Vec::is_empty")] lanes: Vec, /// The containment tier the run actually ran under. An `egress` lane diff --git a/crates/flowproof-replay/src/runrecord.rs b/crates/flowproof-replay/src/runrecord.rs index 11771b8..26396c0 100644 --- a/crates/flowproof-replay/src/runrecord.rs +++ b/crates/flowproof-replay/src/runrecord.rs @@ -78,11 +78,24 @@ impl ControlVerdict { } } +/// The prefix every `assert_no_side_effect` VIOLATION message starts with. +/// A violation embeds the AGENT-chosen target - the first classified message +/// to carry free text an agent controls - so its class hangs on this prefix +/// at byte 0, which only the verdict builder mints, never on keywords the +/// target could spell. +pub const SIDE_EFFECT_VIOLATION: &str = "side effect observed: "; + /// Whether a replay failure is really a capability error (the lane could not /// be enforced or observed) rather than a control that failed. Mirrors the /// egress honesty wording so a "not contained" run reads as capability-error, /// and a missing trace (surfaced as "no trace recorded") likewise. pub fn is_capability_error(message: &str) -> bool { + // Precedence first: a side-effect violation is NEVER a capability error, + // whatever its target spells (`./cannot certify.txt`). Prefix-anchored, + // so a mid-message occurrence of the sentinel changes nothing. + if message.starts_with(SIDE_EFFECT_VIOLATION) { + return false; + } message.contains("not contained") || message.contains("cannot certify") || message.contains("not enforced") @@ -132,7 +145,8 @@ pub struct ControlRecord { pub verdict: ControlVerdict, #[serde(default, skip_serializing_if = "Option::is_none")] pub reason: Option, - /// Which control lanes the flow asserted (`egress`, `secret_leak`). + /// Which control lanes the flow asserted (`egress`, `secret_leak`, + /// `side_effects`). #[serde(default, skip_serializing_if = "Vec::is_empty")] pub lanes: Vec, /// The containment tier THIS run actually ran under, for a flow that @@ -509,6 +523,26 @@ mod tests { ); } + /// The sentinel beats every keyword scan: a violation whose agent-chosen + /// target quotes a capability phrase still classifies Fail, and a + /// capability message quoting the sentinel MID-message stays what it is. + #[test] + fn a_side_effect_violation_is_never_a_capability_error() { + let violation = + format!("{SIDE_EFFECT_VIOLATION}fs_write ./cannot certify.txt (unlinkat) at 12ms"); + assert!(!is_capability_error(&violation), "{violation}"); + assert_eq!( + ControlVerdict::from_outcome(&Err(violation)).0, + ControlVerdict::Fail + ); + let capability = + format!("egress is not enforced here; a file named `{SIDE_EFFECT_VIOLATION}` moved"); + assert!( + is_capability_error(&capability), + "prefix-anchored, not a scan: {capability}" + ); + } + #[test] fn diff_detects_added_removed_and_verdict_changed() { let base = record( diff --git a/docs/agent-testing.md b/docs/agent-testing.md index c689363..b45ee2a 100644 --- a/docs/agent-testing.md +++ b/docs/agent-testing.md @@ -914,13 +914,17 @@ warning is what it is, and the assertion is what makes it a control. ## Filesystem observation -**This is not a control.** It asserts nothing, fails nothing, and has no -spec surface at all - there is no step to add and no key to declare. It is a -report, and it exists because a `command:` agent is a black-box process that -can delete a file without asking anyone. +**The observation itself is not a control.** It prevents nothing, and it +began with no spec surface at all. Since #465 the observations can carry a +verdict - `assert_no_side_effect` is the step that turns them into one - +but without that step this remains what it always was: a report, +existing because a `command:` agent is a black-box process that can delete +a file without asking anyone. Any flow that already engages containment gets it for free, because it is the -same seccomp filter. On Linux the report prints to stderr when, and only +same seccomp filter; a flow carrying only `assert_no_side_effect` engages the +same filter in its observation-only form, under an allow-all policy that +contains nothing. On Linux the report prints to stderr when, and only when, a run destroyed something: ``` @@ -977,7 +981,8 @@ was not there reads exactly like one that removed a tree. `open(path, O_WRONLY)` without `O_TRUNC` followed by a write at offset 0 corrupts a file and fires nothing; catching it needs a trap on every `write`, which would put a supervisor round-trip on every log line. Nothing is observed on macOS or -Windows, or on a flow that engages no containment. The recorded lane +Windows, or on a flow that engages neither egress containment nor +side-effect observation. The recorded lane inherits every one of these limits plus one of its own: a kept `./` target is the NAME the syscall used, never a resolution claim - a symlinked component can carry the actual victim elsewhere. @@ -1079,7 +1084,7 @@ Built and tested, each independently: | `assert_tool_call` grammar | the prose form | | `app: agent` | the spec surface, process runner, record/replay orchestration and CLI dispatch, exercised end to end | | egress containment | `allow_egress` / `assert_no_egress`, enforced by a Linux seccomp supervisor (proven by the Linux CI E2E); "not contained" and honestly reported on macOS/Windows and for `url:` flows | -| filesystem observation | the same seccomp filter also traps the destructive filesystem syscalls, REPORTS them to stderr, and - since #465 - records them into the trace's `side_effects` lane, workspace-relative or hash-redacted, asserting nothing: no spec surface, no step, no verdict. Linux only, and only where containment is already engaged | +| filesystem observation | the same seccomp filter also traps the destructive filesystem syscalls, REPORTS them to stderr, and - since #465 - records them into the trace's `side_effects` lane, workspace-relative or hash-redacted. `assert_no_side_effect` turns the record into a verdict; without that step the lane asserts nothing. Linux only, and only where egress containment or side-effect observation is engaged | | MCP tool boundary | stdio (v3.1) and streamable-HTTP (v3.2): flowproof stands in as the server, records the JSON-RPC traffic once and replays it with no server running. A tool with a `result:` here is answered by the stand-in and never forwarded, in either phase - the one boundary that stops a tool executing | | Anthropic Messages | built and covered end to end, record leg included: a flow records against a Messages-dialect upstream and replays it with no model at all | | Streaming | built and covered end to end in both dialects, record leg included: a `stream: true` agent is served SSE at record and at replay, and the test asserts the FRAME BOUNDARIES, not the assembled text - a replay that collapsed the stream into one buffered body would still produce the same reply | diff --git a/docs/authoring.md b/docs/authoring.md index 0c5131e..395dc4a 100644 --- a/docs/authoring.md +++ b/docs/authoring.md @@ -1244,6 +1244,7 @@ LLM author. The step forms: | `prompt: ` | the task handed to the agent; several `prompt:` steps are joined into one turn | | `assert_tool_call: [where [and …]]` | a tool call the agent must make. Matchers: `equals` (alias `is`), `contains`, `matches` (regex), `exists`, `is absent` | | `assert_no_tool_call: [where …]` | a tool the agent must NOT call anywhere in the trajectory | +| `assert_no_side_effect: ` | the run OBSERVED no side effect of the kind (`fs_write` or `http_request`); anywhere observation cannot run it fails "cannot certify" rather than passing vacuously | | `assert: reply contains ` | the final assistant message contains `` | `agent:` (command/env), `tools:` (the boundary mocks), and `strict:` are @@ -1452,8 +1453,9 @@ without it would otherwise present another machine's blocks as evidence here. A flow that engages egress also carries `containment:` - the tier the run actually ran under (`enforced (linux seccomp)`, or the honest reason it was -not). `lanes` says what the flow ASSERTED; `containment` says what was -ENFORCED. On a host where the mechanism does not exist the flow can still +not). `lanes` says what the flow ASSERTED - `egress`, `secret_leak`, and +`side_effects` for a flow carrying `assert_no_side_effect`; `containment` +says what was ENFORCED. On a host where the mechanism does not exist the flow can still pass, so without this field a passing row would imply a certification the run never made.