vyre_libs/security/
integer_overflow_arith.rs1use 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#[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#[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
86pub 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 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}