Skip to main content

vyre_libs/security/
integer_overflow_arith.rs

1//! `integer_overflow_arith`  -  does this binary op overflow on
2//! attacker input? CWE-190 supporting predicate.
3//!
4//! Per node `n`, write 1 iff `n` is a binary arithmetic node
5//! (mul / add / shl) AND at least one operand is reachable from
6//! `@http_input_family` AND there is no dominating overflow check.
7
8use std::sync::Arc;
9
10use vyre::ir::model::expr::Ident;
11use vyre::ir::{BufferAccess, BufferDecl, DataType, Expr, Node, Program};
12use vyre_primitives::graph::csr_forward_traverse::bitset_words;
13
14pub(crate) const OP_ID: &str = "vyre-libs::security::integer_overflow_arith";
15
16/// Build an overflow-check Program: arith_set AND attacker_reach
17/// AND NOT overflow_check_dominates.
18#[must_use]
19pub fn integer_overflow_arith(
20    node_count: u32,
21    arith_set: &str,
22    attacker_reach: &str,
23    overflow_check_dominates: &str,
24    intermediate: &str,
25    out: &str,
26) -> Program {
27    let words = bitset_words(node_count);
28    let t = Expr::InvocationId { axis: 0 };
29    let attacker_arith = Expr::bitand(
30        Expr::load(arith_set, t.clone()),
31        Expr::load(attacker_reach, t.clone()),
32    );
33    let body = vec![
34        Node::let_bind("attacker_arith", attacker_arith),
35        Node::store(intermediate, t.clone(), Expr::var("attacker_arith")),
36        Node::store(
37            out,
38            t.clone(),
39            Expr::bitand(
40                Expr::var("attacker_arith"),
41                Expr::bitnot(Expr::load(overflow_check_dominates, t.clone())),
42            ),
43        ),
44    ];
45    Program::wrapped(
46        vec![
47            BufferDecl::storage(arith_set, 0, BufferAccess::ReadOnly, DataType::U32)
48                .with_count(words),
49            BufferDecl::storage(attacker_reach, 1, BufferAccess::ReadOnly, DataType::U32)
50                .with_count(words),
51            BufferDecl::storage(
52                overflow_check_dominates,
53                2,
54                BufferAccess::ReadOnly,
55                DataType::U32,
56            )
57            .with_count(words),
58            BufferDecl::storage(intermediate, 3, BufferAccess::ReadWrite, DataType::U32)
59                .with_count(words),
60            BufferDecl::output(out, 4, DataType::U32).with_count(words),
61        ],
62        [256, 1, 1],
63        vec![Node::Region {
64            generator: Ident::from(OP_ID),
65            source_region: None,
66            body: Arc::new(vec![Node::if_then(
67                Expr::lt(t.clone(), Expr::u32(words)),
68                body,
69            )]),
70        }],
71    )
72}
73
74/// CPU oracle.
75#[must_use]
76#[cfg(test)]
77pub(crate) fn cpu_ref(
78    arith_set: &[u32],
79    attacker_reach: &[u32],
80    overflow_check_dominates: &[u32],
81) -> Vec<u32> {
82    let inter = vyre_primitives::bitset::and::cpu_ref(arith_set, attacker_reach);
83    vyre_primitives::bitset::and_not::cpu_ref(&inter, overflow_check_dominates)
84}
85
86/// Soundness marker for [`integer_overflow_arith`].
87pub struct IntegerOverflowArith;
88impl vyre::soundness::SoundnessTagged for IntegerOverflowArith {
89    fn soundness(&self) -> vyre::soundness::Soundness {
90        vyre::soundness::Soundness::Exact
91    }
92}
93
94#[cfg(test)]
95mod tests {
96    use super::*;
97
98    #[test]
99    fn unguarded_attacker_arith_fires() {
100        // arith {0,1,2,3}, attacker {1,2}, no checks.
101        assert_eq!(cpu_ref(&[0b1111], &[0b0110], &[0]), vec![0b0110]);
102    }
103
104    #[test]
105    fn guarded_does_not_fire() {
106        assert_eq!(cpu_ref(&[0b1111], &[0b0110], &[0b0010]), vec![0b0100]);
107    }
108
109    #[test]
110    fn no_attacker_means_no_finding() {
111        assert_eq!(cpu_ref(&[0b1111], &[0], &[0]), vec![0]);
112    }
113
114    #[test]
115    fn no_arith_means_no_finding() {
116        assert_eq!(cpu_ref(&[0], &[0xFFFF], &[0]), vec![0]);
117    }
118}