logicaffeine_verify/
security.rs

1//! Security Property Verification — Non-Interference
2//!
3//! Hardware non-interference: two executions differing only in secret inputs
4//! must produce identical public outputs. Encoded as:
5//! (init_1 == init_2 on public) AND (secret_1 != secret_2) AND T_1 AND T_2
6//! AND (public_out_1 != public_out_2) is UNSAT.
7
8use crate::ir::VerifyExpr;
9use crate::kinduction;
10use std::collections::HashMap;
11
12#[derive(Debug, Clone, PartialEq)]
13pub enum SecurityLabel { Public, Secret }
14
15#[derive(Debug, Clone)]
16pub struct TaintedSignal {
17    pub name: String,
18    pub label: SecurityLabel,
19}
20
21#[derive(Debug)]
22pub enum SecurityResult {
23    NonInterference,
24    InformationLeak { path: Vec<String> },
25    TimingLeak { condition: VerifyExpr },
26    Unknown,
27}
28
29/// Check non-interference: public outputs independent of secret inputs.
30pub fn check_non_interference(
31    transition: &VerifyExpr,
32    signals: &[TaintedSignal],
33) -> SecurityResult {
34
35    let public_inputs: Vec<&TaintedSignal> = signals.iter()
36        .filter(|s| s.label == SecurityLabel::Public)
37        .collect();
38    let secret_inputs: Vec<&TaintedSignal> = signals.iter()
39        .filter(|s| s.label == SecurityLabel::Secret)
40        .collect();
41
42    if secret_inputs.is_empty() {
43        return SecurityResult::NonInterference;
44    }
45
46    // Create two copies of the system: copy1 and copy2
47    // Public inputs are the same, secret inputs differ
48    let solver = crate::solver::new_solver();
49
50    // Assert public inputs are the same in both copies
51    for sig in &public_inputs {
52        let v1 = format!("{}@0_copy1", sig.name);
53        let v2 = format!("{}@0_copy2", sig.name);
54        let eq = VerifyExpr::iff(VerifyExpr::var(&v1), VerifyExpr::var(&v2));
55        solver.assert(&encode_bool(&eq));
56    }
57
58    // Assert at least one secret input differs
59    if !secret_inputs.is_empty() {
60        let first_secret = &secret_inputs[0];
61        let v1 = format!("{}@0_copy1", first_secret.name);
62        let v2 = format!("{}@0_copy2", first_secret.name);
63        let neq = VerifyExpr::not(VerifyExpr::iff(VerifyExpr::var(&v1), VerifyExpr::var(&v2)));
64        solver.assert(&encode_bool(&neq));
65    }
66
67    // Assert transitions for both copies
68    let t1 = rename_copy(transition, "copy1");
69    let t2 = rename_copy(transition, "copy2");
70    solver.assert(&encode_bool(&t1));
71    solver.assert(&encode_bool(&t2));
72
73    // Check if public outputs differ
74    // We check all variables that appear in the transition outputs
75    let mut output_diffs = Vec::new();
76    let mut transition_vars = std::collections::HashSet::new();
77    crate::equivalence::collect_vars_pub(&t1, &mut transition_vars);
78    for sig in &public_inputs {
79        // Check at step 0 (always — constrained by public equality)
80        let _o1_0 = format!("{}@0_copy1", sig.name);
81        let _o2_0 = format!("{}@0_copy2", sig.name);
82        // Only check step-1 if the transition actually mentions this signal at step 1
83        let step1_name = format!("{}@1_copy1", sig.name);
84        if transition_vars.contains(&step1_name) {
85            let o1_1 = format!("{}@1_copy1", sig.name);
86            let o2_1 = format!("{}@1_copy2", sig.name);
87            let diff_1 = VerifyExpr::not(VerifyExpr::iff(VerifyExpr::var(&o1_1), VerifyExpr::var(&o2_1)));
88            output_diffs.push(diff_1);
89        }
90    }
91
92    if output_diffs.is_empty() {
93        return SecurityResult::NonInterference;
94    }
95
96    // Check each output diff individually — ANY SAT means information leak
97    for diff in &output_diffs {
98        let check_solver = crate::solver::new_solver();
99
100        // Re-assert all base constraints
101        for sig in &public_inputs {
102            let v1 = format!("{}@0_copy1", sig.name);
103            let v2 = format!("{}@0_copy2", sig.name);
104            let eq = VerifyExpr::iff(VerifyExpr::var(&v1), VerifyExpr::var(&v2));
105            check_solver.assert(&encode_bool(&eq));
106        }
107        if !secret_inputs.is_empty() {
108            let first_secret = &secret_inputs[0];
109            let v1 = format!("{}@0_copy1", first_secret.name);
110            let v2 = format!("{}@0_copy2", first_secret.name);
111            let neq = VerifyExpr::not(VerifyExpr::iff(VerifyExpr::var(&v1), VerifyExpr::var(&v2)));
112            check_solver.assert(&encode_bool(&neq));
113        }
114        check_solver.assert(&encode_bool(&t1));
115        check_solver.assert(&encode_bool(&t2));
116        check_solver.assert(&encode_bool(diff));
117
118        match check_solver.check() {
119            z3::SatResult::Sat => {
120                let path = secret_inputs.iter().map(|s| s.name.clone()).collect();
121                return SecurityResult::InformationLeak { path };
122            }
123            z3::SatResult::Unknown => return SecurityResult::Unknown,
124            z3::SatResult::Unsat => {} // This output is safe, check next
125        }
126    }
127
128    SecurityResult::NonInterference
129}
130
131fn rename_copy(expr: &VerifyExpr, suffix: &str) -> VerifyExpr {
132    match expr {
133        VerifyExpr::Var(name) => {
134            // Insert suffix before @ if present: "sig@0" → "sig@0_copy1"
135            VerifyExpr::Var(format!("{}_{}", name, suffix))
136        }
137        VerifyExpr::Binary { op, left, right } => VerifyExpr::binary(
138            *op, rename_copy(left, suffix), rename_copy(right, suffix),
139        ),
140        VerifyExpr::Not(inner) => VerifyExpr::not(rename_copy(inner, suffix)),
141        VerifyExpr::Bool(b) => VerifyExpr::Bool(*b),
142        VerifyExpr::Int(n) => VerifyExpr::Int(*n),
143        VerifyExpr::Iff(l, r) => VerifyExpr::iff(rename_copy(l, suffix), rename_copy(r, suffix)),
144        _ => expr.clone(),
145    }
146}
147
148fn encode_bool(expr: &VerifyExpr) -> z3::ast::Bool {
149    let mut bool_vars = HashMap::new();
150    let mut int_vars = HashMap::new();
151    let mut all_vars = std::collections::HashSet::new();
152    crate::equivalence::collect_vars_pub(expr, &mut all_vars);
153    for name in &all_vars {
154        bool_vars.insert(name.clone(), z3::ast::Bool::new_const(name.as_str()));
155    }
156    crate::equivalence::collect_int_vars_pub(expr, &mut int_vars);
157    kinduction::encode_expr_bool(expr, &bool_vars, &int_vars)
158}
logicaffeine_verify/security.rs

logicaffeine_verify/
security.rs
