diff --git a/Cargo.lock b/Cargo.lock index 1dd297c..6906e1e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -894,6 +894,7 @@ dependencies = [ "serde", "serde_json", "serde_yaml", + "sha2 0.10.9", "tiny_http", ] diff --git a/crates/flowproof-adapters/src/agent_runner.rs b/crates/flowproof-adapters/src/agent_runner.rs index 0c29c04..ea6743c 100644 --- a/crates/flowproof-adapters/src/agent_runner.rs +++ b/crates/flowproof-adapters/src/agent_runner.rs @@ -151,6 +151,12 @@ pub struct AgentRun { /// mechanism, which is everywhere the egress log is empty for the same /// reason: the traps are installed together or not at all. pub fs: FsLog, + /// Whether the seccomp observation mechanism ran: true only on the + /// Linux contained path. Distinct from `containment` - observing side + /// effects is not containing egress - and load-bearing for the trace's + /// side-effect lane, ABSENT when this is false: an unobserved run's + /// empty `fs` is silence, not evidence. + pub observed: bool, /// The containment tier this RUN achieved, when the run itself is what /// decides it. /// @@ -385,6 +391,7 @@ pub fn run_http( upstream_error: log.upstream_error.clone(), egress: EgressLog::default(), fs: FsLog::default(), + observed: false, containment: None, }; drop(log); @@ -647,6 +654,7 @@ pub fn run_against( upstream_error: log.upstream_error.clone(), egress: EgressLog::default(), fs: FsLog::default(), + observed: false, containment: None, }; drop(log); @@ -711,6 +719,9 @@ pub fn run_against_contained( upstream_error: log.upstream_error.clone(), egress, fs, + // The filter that enforced is the filter that watched, so `fs` + // above is evidence here and silence everywhere else. + observed: true, // Reaching here means the filter installed: it goes in via `pre_exec` // and a failure aborts the spawn, so there is no path to a finished // run with no filter behind it. @@ -766,6 +777,7 @@ pub fn run_against_contained( }, // Filesystem observation is a seccomp mechanism; Windows has none. fs: FsLog::default(), + observed: false, containment: Some(match outcome.not_contained { None => Containment::Enforced, Some(why) => Containment::NotContained(why), diff --git a/crates/flowproof-adapters/src/egress_linux.rs b/crates/flowproof-adapters/src/egress_linux.rs index f4f410f..6d922e6 100644 --- a/crates/flowproof-adapters/src/egress_linux.rs +++ b/crates/flowproof-adapters/src/egress_linux.rs @@ -1175,17 +1175,21 @@ fn observe( let (a, pid) = (req.data.args, req.pid); // Where each call keeps the thing it destroys. Wrong indices make a wrong // REPORT, never a wrong verdict - the trap already happened. - let (subject, flags) = match op { - "unlink" | "rmdir" | "truncate" | "creat" => (at(pid, None, a[0]), None), - "open" => (at(pid, None, a[0]), open_flags(a[1])), - "openat" => (at(pid, Some(a[0]), a[1]), open_flags(a[2])), - "unlinkat" => (at(pid, Some(a[0]), a[1]), at_flags(a[2])), - "rename" => (pair(at(pid, None, a[0]), at(pid, None, a[1])), None), + let (subject, subject2, flags) = match op { + "unlink" | "rmdir" | "truncate" | "creat" => (at(pid, None, a[0]), None, None), + "open" => (at(pid, None, a[0]), None, open_flags(a[1])), + "openat" => (at(pid, Some(a[0]), a[1]), None, open_flags(a[2])), + "unlinkat" => (at(pid, Some(a[0]), a[1]), None, at_flags(a[2])), + // The rename family keeps its two subjects STRUCTURED (`path2`): + // ` -> ` is a legal filename substring nothing could split back + // safely; `FsEvent::line` joins for the report. + "rename" => (at(pid, None, a[0]), Some(at(pid, None, a[1])), None), "renameat" | "renameat2" => ( - pair(at(pid, Some(a[0]), a[1]), at(pid, Some(a[2]), a[3])), + at(pid, Some(a[0]), a[1]), + Some(at(pid, Some(a[2]), a[3])), None, ), - "ftruncate" => (fd_subject(pid, a[0] as RawFd), None), + "ftruncate" => (fd_subject(pid, a[0] as RawFd), None, None), // `openat2` hides its flags in a pointed-to `open_how` that cBPF // cannot see, so the filter trapped it unconditionally and the // destructiveness test lands here. An unreadable struct is the one @@ -1193,7 +1197,7 @@ fn observe( // what a FAULT means; a bad pointer from the child is not, because the // syscall was going to fail anyway. "openat2" => match open_how_flags(pid, a[2], a[3] as usize) { - Ok(Some(flags)) => (at(pid, Some(a[0]), a[1]), Some(flags)), + Ok(Some(flags)) => (at(pid, Some(a[0]), a[1]), None, Some(flags)), Ok(None) => return continue_resp(), Err(e) if !is_supervisor_fault(&e) => return continue_resp(), Err(e) => return fs_fault(fs, &format!("openat2: could not read open_how: {e}")), @@ -1203,13 +1207,24 @@ fn observe( // reads as a clean run - which is what makes it a fault. _ => return fs_fault(fs, &format!("no handler for trapped syscall {op}")), }; - let (path, path_note) = subject; + let (path, note) = subject; + let (path2, path_note) = match subject2 { + // A rename's one note field carries both sides, attributed by prefix. + Some((path2, note2)) => { + let src = note.map(|n| format!("src: {n}")); + let dst = note2.map(|n| format!("dst: {n}")); + let merged: Vec = src.into_iter().chain(dst).collect(); + (path2, (!merged.is_empty()).then(|| merged.join("; "))) + } + None => (None, note), + }; fs.lock() .unwrap_or_else(|e| e.into_inner()) .destructive .push(FsEvent { op: op.to_string(), path, + path2, path_note, flags, at_ms: spawn.elapsed().as_millis() as u64, @@ -1249,13 +1264,6 @@ fn fd_subject(pid: u32, fd: RawFd) -> Subject { } } -/// The rename family clobbers its DESTINATION and moves its source: name both. -fn pair(from: Subject, to: Subject) -> Subject { - let note = from.1.clone().or_else(|| to.1.clone()); - let show = |s: &Subject| s.0.clone().unwrap_or_else(|| "?".to_string()); - (Some(format!("{} -> {}", show(&from), show(&to))), note) -} - /// The `O_*` bits worth naming, or `None` when `O_TRUNC` is absent - which is /// the whole destructiveness test for the open family. `open`/`openat` were /// gated on that bit in-kernel; `openat2` is tested only here. diff --git a/crates/flowproof-adapters/src/fs_observe.rs b/crates/flowproof-adapters/src/fs_observe.rs index 698a5c2..cf01d68 100644 --- a/crates/flowproof-adapters/src/fs_observe.rs +++ b/crates/flowproof-adapters/src/fs_observe.rs @@ -12,16 +12,27 @@ use std::collections::BTreeSet; /// One destructive filesystem syscall the supervisor watched go past. +/// +/// CAPTURE CONTRACT: `path` and `path2` carry only the bare path string; +/// every qualifier goes to `path_note`. One named kernel exception: a +/// subject readlinked out of `/proc//...` carries the kernel's +/// ` (deleted)` suffix - trailing for an unlinked target, MID-path under +/// an unlinked cwd. NOT stripped: the same bytes are a legal filename +/// ending, and munging a real name would break "the name the syscall used". #[derive(Debug, Clone, PartialEq, Eq)] pub struct FsEvent { /// The syscall by name: `unlinkat`, `truncate`, `openat`. pub op: String, - /// What it acted on, absolute where the supervisor could resolve one. The - /// rename family names both, `source -> destination`. + /// What it acted on, absolute where the supervisor could resolve one. + /// For the rename family, the SOURCE. pub path: Option, - /// Why `path` is missing or unresolved. Weaker evidence, labelled as - /// such: the TRAP is what proves the syscall happened, and traps fire on - /// syscall number, which nothing can race. + /// The rename family's destination; `None` for every non-rename op. + /// Structured, never pre-joined: ` -> ` is a legal filename substring. + pub path2: Option, + /// Why `path` (or `path2`, prefixed `src:`/`dst:` for a rename) is + /// missing or unresolved. Weaker evidence, labelled as such: the TRAP is + /// what proves the syscall happened, and traps fire on syscall number, + /// which nothing can race. pub path_note: Option, /// The flags worth naming, for the calls that carry them: /// `O_WRONLY|O_TRUNC`, `AT_REMOVEDIR`. @@ -30,7 +41,8 @@ pub struct FsEvent { } impl FsEvent { - /// The one-line rendering used in the report. + /// The one-line rendering used in the report; the rename family's + /// `source -> destination` join happens HERE, unchanged on stderr. pub fn line(&self) -> String { let flags = match &self.flags { Some(f) => format!(" [{f}]"), @@ -40,7 +52,15 @@ impl FsEvent { Some(n) => format!(" ({n})"), None => String::new(), }; - let path = self.path.as_deref().unwrap_or(""); + let path = if self.op.starts_with("rename") { + format!( + "{} -> {}", + self.path.as_deref().unwrap_or("?"), + self.path2.as_deref().unwrap_or("?") + ) + } else { + self.path.as_deref().unwrap_or("").to_string() + }; format!("{}{flags} {path}{note} at {}ms", self.op, self.at_ms) } } @@ -124,12 +144,21 @@ mod tests { FsEvent { op: op.into(), path: path.map(Into::into), + path2: None, path_note: None, flags: None, at_ms: 412, } } + /// The stderr rendering must not have moved when the rename join did. + #[test] + fn a_rename_renders_its_two_subjects_joined() { + let mut e = event("renameat2", Some("/x/a")); + e.path2 = Some("/x/b".into()); + assert_eq!(e.line(), "renameat2 /x/a -> /x/b at 412ms"); + } + #[test] fn a_run_that_destroyed_nothing_says_nothing() { assert!(FsLog::default().is_clean()); diff --git a/crates/flowproof-cli/Cargo.toml b/crates/flowproof-cli/Cargo.toml index 95bd56e..d25e044 100644 --- a/crates/flowproof-cli/Cargo.toml +++ b/crates/flowproof-cli/Cargo.toml @@ -31,6 +31,9 @@ serde = { workspace = true } serde_json = { workspace = true } # The `audit` report renders as YAML (default) or JSON. serde_yaml = { workspace = true } +# Side-effect path redaction hashes what it will not store. Already in the +# build graph via pdf-extract, so no new crate compiles. +sha2 = "0.10" [lints] workspace = true diff --git a/crates/flowproof-cli/src/agent_flow.rs b/crates/flowproof-cli/src/agent_flow.rs index 87e8c60..455ee47 100644 --- a/crates/flowproof-cli/src/agent_flow.rs +++ b/crates/flowproof-cli/src/agent_flow.rs @@ -23,10 +23,11 @@ use flowproof_adapters::agent_runner::{run_against, run_against_contained, run_h use flowproof_adapters::egress::{AllowSet, Containment}; use flowproof_adapters::mcp_http::McpHttpServer; use flowproof_adapters::mcp_stdio::{McpCall, McpOut, McpPlan, McpServerEvent}; +use flowproof_adapters::FsEvent; use flowproof_agent::{FlowSpec, SpecStep}; use flowproof_trace::cassette::Cassette; use flowproof_trace::egress::EgressEvent; -use flowproof_trace::side_effect::SideEffect; +use flowproof_trace::side_effect::{SideEffect, KIND_FS_WRITE}; use flowproof_trace::substitution::Mocks; use flowproof_trace::toolcalls::{self, ToolCallExpectation}; @@ -974,6 +975,116 @@ fn report_fs(run: &AgentRun) { } } +/// The first 12 hex of sha256 over the raw captured path: stable, so "the +/// same file every run" correlates without literal disclosure. +fn short_hash(raw: &str) -> String { + use sha2::{Digest, Sha256}; + let digest = Sha256::digest(raw.as_bytes()); + digest.iter().take(6).map(|b| format!("{b:02x}")).collect() +} + +/// TOTAL over any capture-side subject: `(target fragment, note)`, the one +/// constructor of a trace-side fs target. Property-tested POSTCONDITION: a +/// `Some` target is `./`-prefixed, `..`-free, never absolute, byte-for-byte +/// the captured path minus workspace prefix and `.` components; every +/// other input redacts. +fn hygiene( + raw: Option<&str>, + capture_note: Option<&str>, + workspace: &Path, +) -> (Option, Option) { + use std::path::Component; + // No path at all: the trap proved the syscall; there is no claim to clean. + let Some(raw) = raw else { + return (None, capture_note.map(str::to_string)); + }; + let path = Path::new(raw); + // Not absolute (the unreadable-cwd fallback): neither provably inside + // nor outside the workspace, so never kept. + if !path.is_absolute() { + let hash = short_hash(raw); + let extra = capture_note.map(|n| format!("; {n}")).unwrap_or_default(); + let note = format!("unanchored relative path (sha256:{hash}){extra}"); + return (None, Some(note)); + } + // REDACT on traversal, never normalize-and-keep: popping `a/..` is only + // valid when `a` is not a symlink, which lexical processing cannot know + // (`.` components, dropped by `components()` below, are lexically safe). + if path.components().any(|c| matches!(c, Component::ParentDir)) { + let note = format!("traversal path (sha256:{})", short_hash(raw)); + return (None, Some(note)); + } + // Component-wise strip, never a string prefix, so `/ws-evil` cannot + // match `/ws`; a non-absolute root (unreadable cwd) vouches for nothing. + let cleaned: PathBuf = path.components().collect(); + match cleaned.strip_prefix(workspace) { + Ok(rel) if workspace.is_absolute() => ( + Some(format!("./{}", rel.display())), + capture_note.map(str::to_string), + ), + _ => { + let note = format!("outside workspace (sha256:{})", short_hash(raw)); + (None, Some(note)) + } + } +} + +/// One captured [`FsEvent`] as the trace record, every path through +/// [`hygiene`]. A rename runs it per side and joins only the OUTPUTS - a +/// redacted side renders `[redacted]`, both redacted leaves no target. +fn fs_effect(event: &FsEvent, workspace: &Path) -> SideEffect { + let (target, target_note) = if event.op.starts_with("rename") { + let (src, src_note) = hygiene(event.path.as_deref(), None, workspace); + let (dst, dst_note) = hygiene(event.path2.as_deref(), None, workspace); + let target = (src.is_some() || dst.is_some()).then(|| { + format!( + "{} -> {}", + src.as_deref().unwrap_or("[redacted]"), + dst.as_deref().unwrap_or("[redacted]") + ) + }); + let notes: Vec = (event.path_note.clone().into_iter()) + .chain(src_note.map(|n| format!("src: {n}"))) + .chain(dst_note.map(|n| format!("dst: {n}"))) + .collect(); + (target, (!notes.is_empty()).then(|| notes.join("; "))) + } else { + hygiene(event.path.as_deref(), event.path_note.as_deref(), workspace) + }; + SideEffect { + kind: KIND_FS_WRITE.into(), + target, + target_note, + op: Some(event.op.clone()), + flags: event.flags.clone(), + at_ms: event.at_ms, + before: None, + after: None, + diff: None, + } +} + +/// The trace's side-effect lane, or `None` when the observation mechanism +/// never ran - absence keeps meaning "not observed", and a present lane +/// with no effects stays positive evidence: observed, and clean. +fn side_effects_lane(run: &AgentRun, workspace: &Path) -> Option { + if !run.observed { + return None; + } + // Canonicalized once, so a symlinked cwd still prefix-matches the + // `/proc`-resolved absolutes; a chdir'd-away agent's paths redact. + let root = workspace + .canonicalize() + .unwrap_or_else(|_| workspace.to_path_buf()); + Some(SideEffectsTrace { + observation: "observed (linux seccomp)".into(), + effects: (run.fs.destructive.iter()) + .map(|e| fs_effect(e, &root)) + .collect(), + faults: run.fs.distinct_faults(), + }) +} + /// 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 @@ -1009,6 +1120,7 @@ fn egress_failure_message(undeclared: &[EgressEvent]) -> String { fn secret_corpus( cassette: &Cassette, mcp: &BTreeMap, + side_effects: Option<&SideEffectsTrace>, ) -> Vec<(String, String)> { let mut corpus = Vec::new(); // The cassette element is always present on an agent flow (a run with an @@ -1025,6 +1137,13 @@ fn secret_corpus( serde_json::to_string(lane).unwrap_or_default(), )); } + // And the side-effect lane, when the run minted one. + if let Some(lane) = side_effects { + corpus.push(( + "the side-effects lane".to_string(), + serde_json::to_string(lane).unwrap_or_default(), + )); + } corpus } @@ -1038,11 +1157,12 @@ fn check_secret_leak( plan: &Plan, cassette: &Cassette, mcp: &BTreeMap, + side_effects: Option<&SideEffectsTrace>, ) -> Result<(), String> { if plan.secret_leaks.is_empty() { return Ok(()); } - let corpus = secret_corpus(cassette, mcp); + let corpus = secret_corpus(cassette, mcp, side_effects); flowproof_trace::secret_scan::scan_corpus(&plan.secret_leaks, &corpus) } @@ -1403,10 +1523,11 @@ fn record_inner( report_fs(&run); *achieved = Some(achieved_tier(&run, &tier)); let egress = check_egress(&plan, &run, &tier)?; - // The secret-leak scan runs BEFORE the trace is minted: a leak fails the - // run so NO trace is written. That doubles as a store-guard - a secret - // leaked into a cassette body never reaches disk. - check_secret_leak(&plan, &cassette, &mcp_trace)?; + // 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. + let side_effects = side_effects_lane(&run, &std::env::current_dir().unwrap_or_default()); + check_secret_leak(&plan, &cassette, &mcp_trace, side_effects.as_ref())?; let trace = AgentTrace { app: "agent".into(), @@ -1414,9 +1535,7 @@ 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, + side_effects, }; 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()))?; @@ -1488,8 +1607,14 @@ fn replay_inner( check_egress(&plan, &run, &tier)?; // 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 (the proxy consumed the live one). - check_secret_leak(&plan, &trace.cassette, &trace.mcp)?; + // is the recorded cassette + MCP lanes + side-effect lane (the proxy + // consumed the live cassette, and the recorded lane is the one on disk). + check_secret_leak( + &plan, + &trace.cassette, + &trace.mcp, + trace.side_effects.as_ref(), + )?; Ok(()) } @@ -1908,6 +2033,120 @@ mod tests { ); } + // ---- path hygiene and the side-effect lane (unix-gated: capture is + // a Linux mechanism, so every input is a Unix path) ---- + + #[cfg(unix)] + fn ws() -> &'static Path { + Path::new("/ws") + } + + /// The kept form is `./`-prefixed, byte-for-byte the captured name + /// minus the workspace prefix and `.` components - the kernel's + /// ` (deleted)` marker included, anywhere it sits - and the workspace + /// root itself is `./` (pinned: "empty target" and "no target" must not + /// blur). Everything doubtful redacts to a hash of the RAW string, + /// saying why - `/ws/a/../b` is NEVER normalized to a kept `./b`. + #[cfg(unix)] + #[test] + fn workspace_names_are_kept_and_everything_doubtful_redacts() { + for (raw, kept) in [ + ("/ws/./exports/./2025.csv", "./exports/2025.csv"), + ("/ws", "./"), + ("/ws/tmp.csv (deleted)", "./tmp.csv (deleted)"), + ("/ws/dir (deleted)/f.csv", "./dir (deleted)/f.csv"), + ] { + assert_eq!(hygiene(Some(raw), None, ws()), (Some(kept.into()), None)); + } + // A capture-side note travels with a kept target untouched. + assert_eq!( + hygiene(Some("/ws/a"), Some("weak evidence"), ws()), + (Some("./a".into()), Some("weak evidence".into())) + ); + for (raw, why) in [ + ("/home/alice/tokens.csv", "outside workspace (sha256:"), + ("/ws/a/../b", "traversal path (sha256:"), + ("gone.txt", "unanchored relative path (sha256:"), + ] { + let (target, note) = hygiene(Some(raw), None, ws()); + assert_eq!(target, None, "{raw}"); + assert!(note.expect("says why").starts_with(why), "{raw}"); + } + } + + /// The postconditions over generated inputs: ANY `..` input yields no + /// target; a kept target is `./`-prefixed, never absolute, `..`-free, + /// and rejoins to the captured path modulo dropped `.` components. + #[cfg(unix)] + #[test] + fn hygiene_postconditions_hold_over_generated_paths() { + use std::path::Component; + const PARTS: [&str; 7] = ["ws", "a", "..", ".", "exports", "x (deleted)", "ws-evil"]; + let mut state: u64 = 0x9E37_79B9_7F4A_7C15; + let mut next = move |bound: usize| { + state = state.wrapping_mul(0x5851_F42D_4C95_7F2D).wrapping_add(1); + (state >> 33) as usize % bound + }; + for _ in 0..4000 { + let parts: Vec<&str> = (0..next(6)).map(|_| PARTS[next(7)]).collect(); + let raw = format!("{}{}", ["", "/"][usize::from(next(4) > 0)], parts.join("/")); + let Some(target) = hygiene(Some(&raw), None, ws()).0 else { + continue; + }; + assert!(!parts.contains(&".."), "`..` in {raw:?} must redact"); + let rel = target + .strip_prefix("./") + .expect("a kept target is ./-prefixed"); + let clean = !rel.starts_with('/') + && !Path::new(rel) + .components() + .any(|c| matches!(c, Component::ParentDir)); + assert!(clean, "{target:?} from {raw:?}"); + let cleaned: PathBuf = Path::new(&raw).components().collect(); + assert_eq!(ws().join(rel), cleaned, "{target:?} rejoins to {raw:?}"); + } + } + + /// The lane: absent unobserved (silence, never laundered into "clean"), + /// faults deduped, every path in it a hygiene OUTPUT - a rename joining + /// the two outputs, `[redacted]` standing in for a redacted side. + #[cfg(unix)] + #[test] + fn the_lane_records_hygiene_outputs_never_raw_paths() { + let mut run = egress_run(vec![]); + assert!(side_effects_lane(&run, ws()).is_none(), "not observed"); + + run.observed = true; + run.fs.faults = vec!["openat2: EPERM".into(), "openat2: EPERM".into()]; + let event = |op: &str, path: &str, path2: Option<&str>| flowproof_adapters::FsEvent { + op: op.into(), + path: Some(path.into()), + path2: path2.map(Into::into), + path_note: None, + flags: None, + at_ms: 412, + }; + run.fs.destructive = vec![ + event("unlinkat", "/ws/gone.csv", None), + event("renameat2", "/ws/a", Some("/home/u/b.csv")), + event("rename", "/home/u/a", Some("/home/u/b")), + ]; + let lane = side_effects_lane(&run, ws()).expect("observed mints the lane"); + assert_eq!(lane.observation, "observed (linux seccomp)"); + assert_eq!(lane.faults.len(), 1, "one mechanism, one finding"); + assert_eq!(lane.effects[0].target.as_deref(), Some("./gone.csv")); + assert_eq!(lane.effects[1].target.as_deref(), Some("./a -> [redacted]")); + assert_eq!(lane.effects[2].target, None, "both sides redacted"); + let note = lane.effects[1].target_note.as_deref().expect("says why"); + assert!(note.starts_with("dst: outside workspace"), "{note}"); + let json = serde_json::to_string(&lane).expect("serialize"); + assert!(!json.contains("/home"), "no raw path in the lane: {json}"); + + // The store-guard scans the lane, as a named corpus element. + let corpus = secret_corpus(&neutral_cassette("hi", "x"), &BTreeMap::new(), Some(&lane)); + assert!(corpus.iter().any(|(n, _)| n == "the side-effects lane")); + } + // ---- egress containment verdict (cross-platform) ---- /// A minimal `command:` Plan for exercising `check_egress` directly. @@ -1947,6 +2186,7 @@ mod tests { upstream_error: None, egress: flowproof_adapters::egress::EgressLog { blocked, faults }, fs: flowproof_adapters::FsLog::default(), + observed: false, containment: None, } } @@ -1964,6 +2204,7 @@ mod tests { run.fs.destructive.push(flowproof_adapters::FsEvent { op: "unlinkat".into(), path: Some("/home/u/prod.db".into()), + path2: None, path_note: None, flags: None, at_ms: 12, @@ -2273,6 +2514,7 @@ mod tests { upstream_error: None, egress: Default::default(), fs: Default::default(), + observed: false, divergence: None, timed_out: false, containment: None, diff --git a/crates/flowproof-cli/src/lib.rs b/crates/flowproof-cli/src/lib.rs index 2760a8f..91b51e4 100644 --- a/crates/flowproof-cli/src/lib.rs +++ b/crates/flowproof-cli/src/lib.rs @@ -2005,6 +2005,7 @@ fn secret_scan_corpus_report(app: &str) -> (Vec, Vec) { vec![ "model-boundary trajectory (cassette request and response bodies)".to_string(), "MCP lanes".to_string(), + "the side-effects lane, when the run was observed".to_string(), ], vec!["channels the engine never observed (server logs, third-party sinks)".to_string()], ), diff --git a/docs/agent-testing.md b/docs/agent-testing.md index cadb7b5..c689363 100644 --- a/docs/agent-testing.md +++ b/docs/agent-testing.md @@ -950,14 +950,26 @@ dropped, since the trap already proved the syscall happened. Only a syscall whose *destructiveness* could not be adjudicated - an `openat2` whose `open_how` was unreadable - is a fault. -**It prints, and it is not recorded.** There is no `fs` lane in the trace, -by decision rather than by omission: the report goes to stderr and nothing -survives the run. A lane was designed and declined, because a trace is a -COMMITTED artifact and these paths are absolute - `/home/alice/exports/ -acme-corp-2025.csv` would be baked into a file that is reviewed and diffed -forever. That is the same argument that keeps `execve` out of the trap set -for its argv. So this answers "what did that run destroy", never "what has -this flow destroyed since March". +**It prints, and - since issue #465 - it is also recorded, redacted.** A +lane was designed once before and declined, and the objection deserves +keeping in its original words: a trace is a COMMITTED artifact and these +paths are absolute - `/home/alice/exports/acme-corp-2025.csv` would be +baked into a file that is reviewed and diffed forever. That is the same +argument that keeps `execve` out of the trap set for its argv. Issue #465 +is the human act that reversed the decline - the lane's availability, not +the judgment about paths, which still holds: an absolute path never enters +a trace. An observed run now writes a `side_effects` lane whose records +keep a path only when it is workspace-relative by construction - +`./`-prefixed, the name the syscall used minus the workspace prefix and +any bare `.` components, no component rewritten - and redact everything +else (traversal forms included, never normalized-and-kept) to a +`sha256:` fragment of the captured path; the exact rules and the +confirmation-oracle residual are in +[trace-format.md](trace-format.md#side-effect-lane-app-agent). The lane is +scanned by the `assert_no_secret_leak` store-guard before the trace is +minted, and the stderr report above keeps full absolute-path fidelity +either way. So "what has this flow destroyed since March" finally has an +answer: names inside the workspace, hashes outside it. **Punts, and they are real.** These are ATTEMPTS, not outcomes: the reply goes out before the kernel runs the call, so an `rmdir` of a directory that @@ -965,7 +977,10 @@ 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. +Windows, or on a flow that engages no containment. 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. ## Secret-leak control (`assert_no_secret_leak`) @@ -1064,7 +1079,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 and REPORTS them, 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, asserting nothing: no spec surface, no step, no verdict. Linux only, and only where containment is already 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 |