vyre_libs/security/
taint_kill.rs

1//! `taint_kill`  -  one-Region set-difference dataflow primitive.
2//!
3//! Given a `frontier_in` bitset of currently-tainted nodes and a
4//! `kill_set` bitset of nodes whose taint must be dropped (e.g.
5//! sanitizer-tagged nodes, or nodes covered by an explicit guard),
6//! emit a Program that writes `frontier_out = frontier_in & !kill_set`.
7//!
8//! This is the symmetric counterpart to `bitset_or_into`'s "merge
9//! reach" pattern: where `bitset_or_into` accumulates positives,
10//! `taint_kill` removes negatives. Downstream analyzer's `sanitized_by` uses this
11//! as its first stage; the iterated taint-fixpoint loop applies it
12//! after each step to guarantee sanitizer nodes never re-enter the
13//! frontier.
14//!
15//! Soundness: ``Exact``. The set difference
16//! is bit-precise on every word; no over- or under-approximation.
17
18use vyre_foundation::ir::Program;
19use vyre_primitives::bitset::and_not::bitset_and_not;
20use vyre_primitives::graph::csr_forward_traverse::bitset_words;
21
22pub(crate) const OP_ID: &str = "vyre-libs::security::taint_kill";
23
24/// Emit `frontier_out = frontier_in & !kill_set`.
25///
26/// `node_count` defines how many bits the bitset covers; the emitted
27/// Program iterates one thread per bit (rounded up to the next 32-bit
28/// word boundary). Backends that prefer word-level dispatch can rely
29/// on `bitset_words(node_count)` to size their workgroup grid.
30#[must_use]
31pub fn taint_kill(
32    node_count: u32,
33    frontier_in: &str,
34    kill_set: &str,
35    frontier_out: &str,
36) -> Program {
37    let words = bitset_words(node_count);
38    let primitive = bitset_and_not(frontier_in, kill_set, frontier_out, words);
39    Program::wrapped(
40        primitive.buffers().to_vec(),
41        primitive.workgroup_size(),
42        crate::region::reparent_program_children(&primitive, OP_ID),
43    )
44}
45
46/// CPU oracle. Mirrors the per-word semantic exactly.
47#[must_use]
48#[cfg(test)]
49pub(crate) fn cpu_ref(frontier_in: &[u32], kill_set: &[u32]) -> Vec<u32> {
50    vyre_primitives::bitset::and_not::cpu_ref(frontier_in, kill_set)
51}
52
53/// Marker type for the taint_kill dataflow primitive.
54pub struct TaintKill;
55
56impl vyre_spec::soundness::SoundnessTagged for TaintKill {
57    fn soundness(&self) -> vyre_spec::soundness::Soundness {
58        vyre_spec::soundness::Soundness::Exact
59    }
60}
61
62#[cfg(test)]
63mod tests {
64    use super::*;
65
66    #[test]
67    fn empty_kill_set_passes_frontier_through() {
68        assert_eq!(cpu_ref(&[0xFFFF_FFFF], &[0]), vec![0xFFFF_FFFF]);
69    }
70
71    #[test]
72    fn full_kill_set_zeros_frontier() {
73        assert_eq!(cpu_ref(&[0xFFFF_FFFF], &[0xFFFF_FFFF]), vec![0]);
74    }
75
76    #[test]
77    fn partial_kill_set_drops_specific_bits() {
78        // Frontier covers bits 0-15; kill set covers bits 8-15.
79        // Result: only bits 0-7 remain.
80        let frontier = [0x0000_FFFFu32];
81        let kill = [0x0000_FF00u32];
82        assert_eq!(cpu_ref(&frontier, &kill), vec![0x0000_00FF]);
83    }
84
85    #[test]
86    fn idempotent_under_repeated_application() {
87        let frontier = [0xDEAD_BEEFu32];
88        let kill = [0xF0F0_F0F0u32];
89        let after_one = cpu_ref(&frontier, &kill);
90        let after_two = cpu_ref(&after_one, &kill);
91        assert_eq!(after_one, after_two);
92    }
93
94    #[test]
95    fn taint_kill_program_emits_and_not_region() {
96        let program = taint_kill(64, "fin", "kill", "fout");
97        let buffer_names: Vec<&str> = program.buffers().iter().map(|b| b.name()).collect();
98        assert!(buffer_names.contains(&"fin"));
99        assert!(buffer_names.contains(&"kill"));
100        assert!(buffer_names.contains(&"fout"));
101    }
102}
vyre_libs/security/taint_kill.rs

vyre_libs/security/
taint_kill.rs
