feat(agent): record observed fs writes into the side-effect lane (#465 Phase A, 2/5)

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),

crates/flowproof-adapters/src/egress_linux.rs

@@ -1175,25 +1175,29 @@ 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
         // case where we cannot say whether anything was destroyed, which is
         // 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<String> = 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.

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/<pid>/...` 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<String>,
-    /// 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<String>,
+    /// 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<String>,
     /// 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("<path unknown>");
+        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("<path unknown>").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());

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