chore: bump deps (#57)

toolCHAINZ · web-flow · commit 713c8462e98e · 2025-08-14T05:01:18.000Z
* bump z3 and jingle stuff

* clippy

* Update Cargo.toml

* fmt

* python

* fmt

* remove parallel flag

* fmt again

* Bump libs and update readme
diff --git a/README.md b/README.md
@@ -8,12 +8,29 @@
 # `crackers`: A Tool for Synthesizing Code-Reuse Attacks from `p-code` Programs
 
 This repo contains the source code of `crackers`, a procedure for synthesizing
-code-reuse attacks (e.g. ROP). `crackers` takes as input a specification computation, usually
+code-reuse attacks (e.g. ROP). `crackers` takes as input a "reference program", usually
 written in an assembly language, a binary (of the same architecture) in which to look
 for gadgets, and user-provided constraints to enforce on synthesized chains. It will always
 return an answer (though there is no strict bound to runtime), reporting either that the problem
 is UNSAT, or providing an assignment of gadgets that meet all constraints, and a model
-of the memory state of the PCODE virtual machine at every stage of the comptuation.
+of the memory state of the PCODE virtual machine at every stage of the computation.
+
+`crackers` will assume that _all_ system state is usable unless the user prohibits it by providing a constraint.
+This approach, while requiring more human guidance, allows it to minimize the assumptions it makes about the
+arrangement and roles of memory in an exploit.
+
+To validate chains, `crackers` builds a mathematical model of the trace through the gadgets. This model, along
+with user-provided constraints, is verified against a model of the "reference program". When this verification
+returns SAT, `crackers` returns the Z3 model of the memory state of the chain at every point of its execution. This
+memory model may be used to derive the contents of memory needed to invoke the chain, and transitively the input needed to
+provide to the program to realize it.
+
+Note that the provided CLI of crackers currently only prints the selected gadgets to the command line.
+To make use of the logical memory model it must be used through the programmatic API.
+
+There is also an experimental Python binding for `crackers`, allowing for basic configuration, execution, and model
+inspection from python. These bindings also feature cross-FFI support with the python z3 bindings, allowing
+constraints to be expressed as python functions or `lambda` expressions returning Python Z3 `BoolRef` instances.
 
 ### This software is still in alpha and may change at any time
 
diff --git a/crackers/Cargo.toml b/crackers/Cargo.toml
@@ -24,8 +24,8 @@ toml = ["dep:toml_edit"]
 z3-gh-release = ["z3/gh-release"]
 
 [dependencies]
-jingle = { version = "0.2.0", features = ["gimli"] }
-z3 = "0.14.0"
+jingle = { version = "0.2.2", features = ["gimli"] }
+z3 = "0.14.1"
 serde = { version = "1.0.203", features = ["derive"] }
 thiserror = "2.0"
 tracing = "0.1"
diff --git a/crackers/src/gadget/library/mod.rs b/crackers/src/gadget/library/mod.rs
@@ -1,6 +1,6 @@
 use jingle::modeling::ModeledInstruction;
 use jingle::sleigh::context::loaded::LoadedSleighContext;
-use jingle::sleigh::{ArchInfoProvider, Instruction, SpaceInfo, VarNode};
+use jingle::sleigh::{ArchInfoProvider, Instruction, SleighArchInfo, SpaceInfo, VarNode};
 use jingle::{JingleContext, JingleError};
 use rand::SeedableRng;
 use rand::rngs::StdRng;
@@ -27,6 +27,13 @@ impl GadgetLibrary {
         self.gadgets.len()
     }
 
+    pub(crate) fn arch_info(&self) -> SleighArchInfo {
+        SleighArchInfo::new(
+            self.get_registers(),
+            self.get_all_space_info(),
+            self.default_code_space_index,
+        )
+    }
     pub fn get_random_candidates_for_trace<'a>(
         &'a self,
         jingle: &JingleContext,
diff --git a/crackers/src/synthesis/assignment_model/builder.rs b/crackers/src/synthesis/assignment_model/builder.rs
@@ -1,75 +1,24 @@
 use crate::error::CrackersError;
 use crate::gadget::Gadget;
-use crate::gadget::library::GadgetLibrary;
 use crate::reference_program::ReferenceProgram;
 use crate::synthesis::assignment_model::AssignmentModel;
 use crate::synthesis::builder::{StateConstraintGenerator, TransitionConstraintGenerator};
 use crate::synthesis::pcode_theory::pcode_assignment::PcodeAssignment;
 use jingle::JingleContext;
 use jingle::modeling::{ModeledBlock, ModeledInstruction};
-use jingle::sleigh::{ArchInfoProvider, SpaceInfo, VarNode};
+use jingle::sleigh::SleighArchInfo;
 use std::fmt::{Debug, Formatter};
 use std::sync::Arc;
 use z3::{Context, Solver};
 
-// todo: this should probably just be a struct in Jingle and we can stop with this trait nonsense
-#[derive(Clone, Debug)]
-pub struct ArchInfo {
-    spaces: Vec<SpaceInfo>,
-    default_code_space_index: usize,
-    registers: Vec<(VarNode, String)>,
-}
-
-impl From<&GadgetLibrary> for ArchInfo {
-    fn from(value: &GadgetLibrary) -> Self {
-        Self {
-            default_code_space_index: value.get_code_space_idx(),
-            registers: value
-                .get_registers()
-                .map(|(a, b)| (a.clone(), b.to_string()))
-                .collect(),
-            spaces: value.get_all_space_info().cloned().collect(),
-        }
-    }
-}
-
-impl ArchInfoProvider for ArchInfo {
-    fn get_space_info(&self, idx: usize) -> Option<&SpaceInfo> {
-        self.spaces.get(idx)
-    }
-
-    fn get_all_space_info(&self) -> impl Iterator<Item = &SpaceInfo> {
-        self.spaces.iter()
-    }
-
-    fn get_code_space_idx(&self) -> usize {
-        self.default_code_space_index
-    }
-
-    fn get_register(&self, name: &str) -> Option<&VarNode> {
-        self.registers.iter().find(|f| f.1 == name).map(|f| &f.0)
-    }
-
-    fn get_register_name(&self, location: &VarNode) -> Option<&str> {
-        self.registers
-            .iter()
-            .find(|f| f.0 == *location)
-            .map(|f| f.1.as_str())
-    }
-
-    fn get_registers(&self) -> impl Iterator<Item = (&VarNode, &str)> {
-        self.registers.iter().map(|(f, v)| (f, v.as_str()))
-    }
-}
-
 #[derive(Clone)]
 pub struct AssignmentModelBuilder {
     pub templates: ReferenceProgram,
     pub gadgets: Vec<Gadget>,
     pub preconditions: Vec<Arc<StateConstraintGenerator>>,
     pub postconditions: Vec<Arc<StateConstraintGenerator>>,
     pub pointer_invariants: Vec<Arc<TransitionConstraintGenerator>>,
-    pub arch_info: ArchInfo,
+    pub arch_info: SleighArchInfo,
 }
 
 impl Debug for AssignmentModelBuilder {
diff --git a/crackers/src/synthesis/assignment_model/mod.rs b/crackers/src/synthesis/assignment_model/mod.rs
@@ -3,7 +3,7 @@ pub mod builder;
 use std::fmt::{Display, Formatter};
 
 use jingle::modeling::{ModelingContext, State};
-use jingle::sleigh::{ArchInfoProvider, GeneralizedVarNode};
+use jingle::sleigh::{ArchInfoProvider, GeneralizedVarNode, SleighArchInfo};
 use jingle::varnode::ResolvedVarnode;
 use z3::Model;
 use z3::ast::BV;
@@ -12,11 +12,16 @@ use z3::ast::BV;
 pub struct AssignmentModel<T: ModelingContext> {
     model: Model,
     pub gadgets: Vec<T>,
+    pub arch_info: SleighArchInfo,
 }
 
 impl<T: ModelingContext> AssignmentModel<T> {
-    pub fn new(model: Model, gadgets: Vec<T>) -> Self {
-        Self { model, gadgets }
+    pub fn new(model: Model, gadgets: Vec<T>, arch_info: SleighArchInfo) -> Self {
+        Self {
+            model,
+            gadgets,
+            arch_info,
+        }
     }
 
     pub fn model(&self) -> &Model {
@@ -61,6 +66,14 @@ impl<T: ModelingContext> AssignmentModel<T> {
             .unwrap();
         self.model.eval(&val, false)
     }
+
+    pub fn inputs(&self) -> impl Iterator<Item = ResolvedVarnode> {
+        self.gadgets.iter().flat_map(|gadget| gadget.get_inputs())
+    }
+
+    pub fn outputs(&self) -> impl Iterator<Item = ResolvedVarnode> {
+        self.gadgets.iter().flat_map(|gadget| gadget.get_outputs())
+    }
 }
 
 impl<T: ModelingContext + Display> Display for AssignmentModel<T> {
diff --git a/crackers/src/synthesis/mod.rs b/crackers/src/synthesis/mod.rs
@@ -10,7 +10,7 @@ use crate::error::CrackersError::EmptySpecification;
 use crate::gadget::candidates::{CandidateBuilder, Candidates};
 use crate::gadget::library::GadgetLibrary;
 use crate::reference_program::ReferenceProgram;
-use crate::synthesis::assignment_model::builder::{ArchInfo, AssignmentModelBuilder};
+use crate::synthesis::assignment_model::builder::AssignmentModelBuilder;
 use crate::synthesis::builder::{
     StateConstraintGenerator, SynthesisParams, SynthesisSelectionStrategy,
     TransitionConstraintGenerator,
@@ -112,7 +112,7 @@ impl AssignmentSynthesis {
             preconditions: self.preconditions.clone(),
             postconditions: self.postconditions.clone(),
             pointer_invariants: self.pointer_invariants.clone(),
-            arch_info: ArchInfo::from(self.library.as_ref()),
+            arch_info: self.library.arch_info(),
         }
     }
 
diff --git a/crackers/src/synthesis/pcode_theory/pcode_assignment.rs b/crackers/src/synthesis/pcode_theory/pcode_assignment.rs
@@ -75,7 +75,11 @@ impl PcodeAssignment {
                 let model = solver
                     .get_model()
                     .ok_or(CrackersError::ModelGenerationError)?;
-                Ok(AssignmentModel::new(model, self.eval_trace.to_vec()))
+                Ok(AssignmentModel::new(
+                    model,
+                    self.eval_trace.to_vec(),
+                    jingle.info.clone(),
+                ))
             }
         }
     }
diff --git a/crackers_python/Cargo.toml b/crackers_python/Cargo.toml
@@ -12,7 +12,7 @@ crate-type = ["cdylib"]
 [dependencies]
 pyo3 = { version = "0.25", features = ["extension-module", "py-clone"] }
 crackers = {path = "../crackers", features = ["pyo3"], version = "0.3.0" }
-jingle = {version = "0.2.0", features = ["pyo3"]}
+jingle = {version = "0.2.2", features = ["pyo3"]}
 toml_edit = "0.22.22"
 z3 = "0.14.0"
 serde_json = "1.0.140"
diff --git a/crackers_python/src/decision/assignment_model/mod.rs b/crackers_python/src/decision/assignment_model/mod.rs
@@ -4,11 +4,11 @@ use crate::decision::assignment_model::model_varnode_iterator::ModelVarNodeItera
 use crackers::synthesis::assignment_model::AssignmentModel;
 use jingle::modeling::{ModeledBlock, ModelingContext, State};
 use jingle::python::modeled_block::PythonModeledBlock;
-use jingle::python::resolved_varnode::PythonResolvedVarNode;
+use jingle::python::resolved_varnode::{PythonResolvedVarNode, PythonResolvedVarNodeInner};
 use jingle::python::state::PythonState;
 use jingle::python::varode_iterator::VarNodeIterator;
 use jingle::python::z3::ast::{TryFromPythonZ3, TryIntoPythonZ3};
-use jingle::sleigh::{SpaceType, VarNode, VarNodeDisplay};
+use jingle::sleigh::{ArchInfoProvider, SpaceType};
 use jingle::varnode::{ResolvedIndirectVarNode, ResolvedVarnode};
 use pyo3::exceptions::PyRuntimeError;
 use pyo3::{Py, PyAny, PyResult, pyclass, pymethods};
@@ -28,23 +28,29 @@ impl PythonAssignmentModel {
         vn: PythonResolvedVarNode,
         completion: bool,
     ) -> Option<(String, BV)> {
-        match vn {
-            PythonResolvedVarNode::Direct(a) => {
-                let bv = state.read_varnode(&VarNode::from(a.clone())).ok()?;
+        match vn.inner {
+            PythonResolvedVarNodeInner::Direct(a) => {
+                let bv = state.read_varnode(a.inner()).ok()?;
                 let val = self.inner.model().eval(&bv, completion)?;
                 Some((format!("{a}"), val))
             }
-            PythonResolvedVarNode::Indirect(i) => {
-                let pointer_value = self.inner.model().eval(&i.inner.pointer, completion)?;
-                let space_name = i.inner.pointer_space_info.name.clone();
-                let access_size = i.inner.access_size_bytes;
+            PythonResolvedVarNodeInner::Indirect(i) => {
+                let info = i.info();
+                let i = i.inner();
+                let pointer_value = self.inner.model().eval(&i.pointer, completion)?;
+                let space_name = info
+                    .get_space_info(i.pointer_space_idx)
+                    .unwrap()
+                    .name
+                    .clone();
+                let access_size = i.access_size_bytes;
                 let pointed_value = self.inner.model().eval(
                     &state
                         .read_resolved(&ResolvedVarnode::Indirect(ResolvedIndirectVarNode {
-                            access_size_bytes: i.inner.access_size_bytes,
-                            pointer_location: i.inner.pointer_location,
-                            pointer: i.inner.pointer,
-                            pointer_space_idx: i.inner.pointer_space_info.index,
+                            access_size_bytes: i.access_size_bytes,
+                            pointer_location: i.pointer_location.clone(),
+                            pointer: i.pointer.clone(),
+                            pointer_space_idx: i.pointer_space_idx,
                         }))
                         .ok()?,
                     completion,
@@ -100,8 +106,15 @@ impl PythonAssignmentModel {
             .flat_map(|g| g.get_input_vns().ok())
             .flatten()
             .filter(|a| {
-                if let PythonResolvedVarNode::Direct(VarNodeDisplay::Raw(r)) = a {
-                    r.space_info._type == SpaceType::IPTR_PROCESSOR
+                if let PythonResolvedVarNode {
+                    inner: PythonResolvedVarNodeInner::Direct(a),
+                } = a
+                {
+                    a.info()
+                        .get_space_info(a.inner().space_index)
+                        .unwrap()
+                        ._type
+                        == SpaceType::IPTR_PROCESSOR
                 } else {
                     true
                 }
@@ -116,8 +129,15 @@ impl PythonAssignmentModel {
             .flat_map(|g| g.get_output_vns().ok())
             .flatten()
             .filter(|a| {
-                if let PythonResolvedVarNode::Direct(VarNodeDisplay::Raw(r)) = a {
-                    r.space_info._type == SpaceType::IPTR_PROCESSOR
+                if let PythonResolvedVarNode {
+                    inner: PythonResolvedVarNodeInner::Direct(a),
+                } = a
+                {
+                    a.info()
+                        .get_space_info(a.inner().space_index)
+                        .unwrap()
+                        ._type
+                        == SpaceType::IPTR_PROCESSOR
                 } else {
                     true
                 }

Original file line number	Diff line number	Diff line change
`@@ -75,7 +75,11 @@ impl PcodeAssignment {`
`75`	`75`	`let model = solver`
`76`	`76`	`.get_model()`
`77`	`77`	`.ok_or(CrackersError::ModelGenerationError)?;`
`78`		`- Ok(AssignmentModel::new(model, self.eval_trace.to_vec()))`
	`78`	`+ Ok(AssignmentModel::new(`
	`79`	`+ model,`
	`80`	`+ self.eval_trace.to_vec(),`
	`81`	`+ jingle.info.clone(),`
	`82`	`+ ))`
`79`	`83`	`}`
`80`	`84`	`}`
`81`	`85`	`}`