crackers 0.9.0

A tool for synthesizing Code Reuse Attacks (ROP chains) using Ghidra's p-code and Z3
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62

use z3::ast::Bool;

use crate::synthesis::Decision;
use crate::synthesis::pcode_theory::conflict_clause::ConflictClause;

#[derive(Debug, Copy, Clone, PartialEq, Eq)]
pub enum TheoryStage {
    CombinedSemantics,
    Consistency,
    Branch,
    Precondition,
    Postcondition,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ConjunctiveConstraint {
    pub decisions: Vec<Decision>,
    boolean: Bool,
    constraint_type: TheoryStage,
}

impl ConjunctiveConstraint {
    pub fn new(decisions: &[Decision], boolean: Bool, t: TheoryStage) -> Self {
        Self {
            decisions: decisions.to_vec(),
            boolean,
            constraint_type: t,
        }
    }
    pub fn get_bool(&self) -> &Bool {
        &self.boolean
    }

    pub fn gen_conflict_clause(&self) -> ConflictClause {
        let mut clause = ConflictClause::from(self.decisions.iter());
        clause.precondition = matches!(self.constraint_type, TheoryStage::Precondition);
        clause.postcondition = matches!(self.constraint_type, TheoryStage::Postcondition);
        clause
    }
}

pub(crate) fn gen_conflict_clauses(
    constraints: &[&ConjunctiveConstraint],
) -> Option<ConflictClause> {
    let mut result = Vec::new();
    let mut semantics = Vec::new();
    for x in constraints {
        result.push(x.gen_conflict_clause());
        match x.constraint_type {
            TheoryStage::CombinedSemantics | TheoryStage::Branch => {
                semantics.push(x.gen_conflict_clause());
            }
            _ => {}
        }
    }
    if result.is_empty() {
        None
    } else if !semantics.is_empty() {
        Some(ConflictClause::combine(semantics.as_slice()))
    } else {
        Some(ConflictClause::combine(result.as_slice()))
    }
}