Skip to content

Commit a902caa

Browse files
toolCHAINZtoolCHAINZ
committed
Update readme
1 parent 117d295 commit a902caa

File tree

4 files changed

+160
-65
lines changed

4 files changed

+160
-65
lines changed

‎README.md‎

Lines changed: 64 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -52,24 +52,41 @@ A simple usage looks like the following:
5252

5353
```python
5454
import logging
55+
56+
from crackers.crackers import DecisionResult
57+
from crackers.jingle import ModeledBlock, State
58+
5559
logging.basicConfig(level=logging.INFO)
5660

57-
from z3 import BoolRef, BoolVal
61+
from z3 import BoolRef, BoolVal, simplify
5862

59-
from crackers import State, ModeledBlock
60-
from crackers.config import MetaConfig, LibraryConfig, SleighConfig,
61-
ReferenceProgramConfig, SynthesisConfig, ConstraintConfig, CrackersConfig
62-
from crackers.config.constraint import RegisterValuation,
63-
RegisterStringValuation, MemoryValuation, PointerRange,
64-
CustomStateConstraint, CustomTransitionConstraint, PointerRangeRole
63+
from crackers.config import (
64+
MetaConfig,
65+
LibraryConfig,
66+
SleighConfig,
67+
ReferenceProgramConfig,
68+
SynthesisConfig,
69+
ConstraintConfig,
70+
CrackersConfig,
71+
)
72+
from crackers.config.constraint import (
73+
RegisterValuation,
74+
RegisterStringValuation,
75+
MemoryValuation,
76+
PointerRange,
77+
CustomStateConstraint,
78+
CustomTransitionConstraint,
79+
PointerRangeRole,
80+
)
6581
from crackers.config.log_level import LogLevel
6682
from crackers.config.synthesis import SynthesisStrategy
6783

84+
6885
# Custom state constraint example
6986
def my_constraint(s: State, _addr: int) -> BoolRef:
7087
rdi = s.read_register("RDI")
7188
rcx = s.read_register("RCX")
72-
return rdi == (rcx ^ 0x5a5a5a5a5a5a5a5a)
89+
return rdi == (rcx ^ 0x5A5A5A5A5A5A5A5A)
7390

7491

7592
# Custom transition constraint example
@@ -79,29 +96,53 @@ def my_transition_constraint(block: ModeledBlock) -> BoolRef:
7996

8097

8198
meta = MetaConfig(log_level=LogLevel.INFO, seed=42)
82-
library = LibraryConfig(max_gadget_length=8, path="libz.so.1", sample_size=None,
83-
base_address=None)
99+
library = LibraryConfig(
100+
max_gadget_length=8, path="libz.so.1", sample_size=None, base_address=None
101+
)
84102
sleigh = SleighConfig(ghidra_path="/Applications/ghidra")
85-
reference_program = ReferenceProgramConfig(path="sample.o", max_instructions=8, base_address=library.base_address)
86-
synthesis = SynthesisConfig(strategy=SynthesisStrategy.SAT, max_candidates_per_slot=200, parallel=8, combine_instructions=True)
103+
reference_program = ReferenceProgramConfig(
104+
path="sample.o", max_instructions=8, base_address=library.base_address
105+
)
106+
synthesis = SynthesisConfig(
107+
strategy=SynthesisStrategy.SAT,
108+
max_candidates_per_slot=200,
109+
parallel=8,
110+
combine_instructions=True,
111+
)
112+
87113
constraint = ConstraintConfig(
88114
precondition=[
89-
RegisterValuation(name="rdi", value=0xdeadbeef),
115+
RegisterValuation(name="RDI", value=0xDEADBEEF),
90116
MemoryValuation(space="ram", address=0x1000, size=4, value=0x41),
91-
RegisterStringValuation(reg="rsi", value="/bin/sh"),
92-
CustomStateConstraint(code=my_constraint)
117+
RegisterStringValuation(reg="RSI", value="/bin/sh"),
118+
CustomStateConstraint.from_callable(my_constraint),
93119
],
94120
postcondition=[
95-
RegisterValuation(name="rax", value=0x1337),
96-
CustomStateConstraint(code=my_constraint)
121+
RegisterValuation(name="RBX", value=0x1337),
97122
],
98-
transition=[
99-
PointerRange(role=PointerRangeRole.READ, min=0x2000, max=0x3000),
100-
CustomTransitionConstraint(code=my_transition_constraint)
101-
]
123+
pointer=[
124+
PointerRange(role=PointerRangeRole.READ, min=0x80_0000, max=0x80_8000),
125+
CustomTransitionConstraint.from_callable(my_transition_constraint),
126+
],
127+
)
128+
config = CrackersConfig(
129+
meta=meta,
130+
library=library,
131+
sleigh=sleigh,
132+
specification=reference_program,
133+
synthesis=synthesis,
134+
constraint=constraint,
102135
)
103-
config = CrackersConfig(meta=meta, library=library, sleigh=sleigh, specification=reference_program, synthesis=synthesis, constraint=constraint)
104-
config.run()
136+
r = config.run()
137+
match r:
138+
case DecisionResult.AssignmentFound(a):
139+
for g in a.gadgets():
140+
for i in g.instructions:
141+
print(i.disassembly)
142+
print()
143+
for name, bv in a.input_summary(True):
144+
print(f"{name} = {simplify(bv)}")
145+
105146
```
106147

107148
### Rust CLI

‎crackers_python/PYTHON_README.md‎

Lines changed: 65 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -24,54 +24,96 @@ A simple usage looks like the following:
2424

2525
```python
2626
import logging
27+
28+
from crackers.crackers import DecisionResult
29+
from crackers.jingle import ModeledBlock, State
30+
2731
logging.basicConfig(level=logging.INFO)
2832

29-
from z3 import BoolRef, BoolVal
33+
from z3 import BoolRef, BoolVal, simplify
3034

31-
from crackers import State, ModeledBlock
32-
from crackers.config import MetaConfig, LibraryConfig, SleighConfig,
33-
ReferenceProgramConfig, SynthesisConfig, ConstraintConfig, CrackersConfig
34-
from crackers.config.constraint import RegisterValuation,
35-
RegisterStringValuation, MemoryValuation, PointerRange,
36-
CustomStateConstraint, CustomTransitionConstraint, PointerRangeRole
35+
from crackers.config import (
36+
MetaConfig,
37+
LibraryConfig,
38+
SleighConfig,
39+
ReferenceProgramConfig,
40+
SynthesisConfig,
41+
ConstraintConfig,
42+
CrackersConfig,
43+
)
44+
from crackers.config.constraint import (
45+
RegisterValuation,
46+
RegisterStringValuation,
47+
MemoryValuation,
48+
PointerRange,
49+
CustomStateConstraint,
50+
CustomTransitionConstraint,
51+
PointerRangeRole,
52+
)
3753
from crackers.config.log_level import LogLevel
3854
from crackers.config.synthesis import SynthesisStrategy
3955

56+
4057
# Custom state constraint example
4158
def my_constraint(s: State, _addr: int) -> BoolRef:
4259
rdi = s.read_register("RDI")
4360
rcx = s.read_register("RCX")
44-
return rdi == (rcx ^ 0x5a5a5a5a5a5a5a5a)
61+
return rdi == (rcx ^ 0x5A5A5A5A5A5A5A5A)
62+
4563

4664
# Custom transition constraint example
4765
def my_transition_constraint(block: ModeledBlock) -> BoolRef:
4866
# Dummy: always true
4967
return BoolVal(True)
5068

69+
5170
meta = MetaConfig(log_level=LogLevel.INFO, seed=42)
52-
library = LibraryConfig(max_gadget_length=8, path="libz.so.1", sample_size=None,
53-
base_address=None)
71+
library = LibraryConfig(
72+
max_gadget_length=8, path="libz.so.1", sample_size=None, base_address=None
73+
)
5474
sleigh = SleighConfig(ghidra_path="/Applications/ghidra")
55-
reference_program = ReferenceProgramConfig(path="sample.o", max_instructions=8, base_address=library.base_address)
56-
synthesis = SynthesisConfig(strategy=SynthesisStrategy.SAT, max_candidates_per_slot=200, parallel=8, combine_instructions=True)
75+
reference_program = ReferenceProgramConfig(
76+
path="sample.o", max_instructions=8, base_address=library.base_address
77+
)
78+
synthesis = SynthesisConfig(
79+
strategy=SynthesisStrategy.SAT,
80+
max_candidates_per_slot=200,
81+
parallel=8,
82+
combine_instructions=True,
83+
)
84+
5785
constraint = ConstraintConfig(
5886
precondition=[
59-
RegisterValuation(name="rdi", value=0xdeadbeef),
87+
RegisterValuation(name="RDI", value=0xDEADBEEF),
6088
MemoryValuation(space="ram", address=0x1000, size=4, value=0x41),
61-
RegisterStringValuation(reg="rsi", value="/bin/sh"),
62-
CustomStateConstraint(code=my_constraint)
89+
RegisterStringValuation(reg="RSI", value="/bin/sh"),
90+
CustomStateConstraint.from_callable(my_constraint),
6391
],
6492
postcondition=[
65-
RegisterValuation(name="rax", value=0x1337),
66-
CustomStateConstraint(code=my_constraint)
93+
RegisterValuation(name="RBX", value=0x1337),
94+
],
95+
pointer=[
96+
PointerRange(role=PointerRangeRole.READ, min=0x80_0000, max=0x80_8000),
97+
CustomTransitionConstraint.from_callable(my_transition_constraint),
6798
],
68-
transition=[
69-
PointerRange(role=PointerRangeRole.READ, min=0x2000, max=0x3000),
70-
CustomTransitionConstraint(code=my_transition_constraint)
71-
]
7299
)
73-
config = CrackersConfig(meta=meta, library=library, sleigh=sleigh, specification=reference_program, synthesis=synthesis, constraint=constraint)
74-
config.run()
100+
config = CrackersConfig(
101+
meta=meta,
102+
library=library,
103+
sleigh=sleigh,
104+
specification=reference_program,
105+
synthesis=synthesis,
106+
constraint=constraint,
107+
)
108+
r = config.run()
109+
match r:
110+
case DecisionResult.AssignmentFound(a):
111+
for g in a.gadgets():
112+
for i in g.instructions:
113+
print(i.disassembly)
114+
print()
115+
for name, bv in a.input_summary(True):
116+
print(f"{name} = {simplify(bv)}")
75117
```
76118

77119
# Research Paper

‎crackers_python/crackers/config/constraint.py‎

Lines changed: 16 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -162,12 +162,12 @@ class ConstraintConfig(BaseModel):
162162
Attributes:
163163
precondition (list[StateConstraint] | None): Constraints on the initial state.
164164
postcondition (list[StateConstraint] | None): Constraints on the final state.
165-
transition (list[TransitionConstraint] | None): Constraints on the transitions between states.
165+
pointer (list[TransitionConstraint] | None): Constraints on the transitions between states (named 'pointer' for compatibility reasons, but can express any transition constraint)
166166
"""
167167

168168
precondition: list[StateConstraint] | None = None
169169
postcondition: list[StateConstraint] | None = None
170-
transition: list[TransitionConstraint] | None = None
170+
pointer: list[TransitionConstraint] | None = None
171171

172172
@field_serializer("precondition", "postcondition")
173173
def serialize_state_constraints(value, _info):
@@ -190,7 +190,7 @@ def serialize_state_constraints(value, _info):
190190
"size": mem.size,
191191
"value": mem.value,
192192
}
193-
transformed: StateEqualityConstraint = {
193+
transformed = {
194194
"register": {
195195
v.name: v.value for v in filtered if isinstance(v, RegisterValuation)
196196
},
@@ -203,8 +203,18 @@ def serialize_state_constraints(value, _info):
203203
}
204204
return transformed
205205

206-
@field_serializer("transition")
207-
def skip_custom_transition_constraints(value, _info):
208-
return [
206+
@field_serializer("pointer")
207+
def serialize_transition_constraints(value, _info):
208+
filtered = [
209209
v for v in value or [] if getattr(v, "type", None) != "custom_transition"
210210
]
211+
read_ranges = []
212+
write_ranges = []
213+
for v in filtered:
214+
if isinstance(v, PointerRange):
215+
range_dict = {"min": v.min, "max": v.max}
216+
if v.role == PointerRangeRole.READ:
217+
read_ranges.append(range_dict)
218+
elif v.role == PointerRangeRole.WRITE:
219+
write_ranges.append(range_dict)
220+
return {"read": read_ranges, "write": write_ranges}

‎crackers_python/crackers/config/crackers.py‎

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,13 @@
11
from pydantic import BaseModel
2-
from crackers.config.constraint import ConstraintConfig
2+
from crackers.config.constraint import ConstraintConfig, CustomStateConstraint, \
3+
CustomTransitionConstraint
34
from crackers.config.library import LibraryConfig
45
from crackers.config.meta import MetaConfig
56
from crackers.config.sleigh import SleighConfig
67
from crackers.config.specification import ReferenceProgramConfig
78
from crackers.config.synthesis import SynthesisConfig
89
from crackers import _internal
10+
from crackers.crackers import DecisionResult
911

1012

1113
class CrackersConfig(BaseModel):
@@ -28,40 +30,40 @@ class CrackersConfig(BaseModel):
2830
synthesis: SynthesisConfig
2931
constraint: ConstraintConfig
3032

31-
def run(self):
33+
def run(self) -> DecisionResult:
3234
j = self.model_dump_json()
3335
config = _internal.crackers.CrackersConfig.from_json(j)
3436
resolved = config.resolve_config()
3537

3638
# Separate custom state constraints into precondition and postcondition
37-
precondition_state_constraints = []
38-
postcondition_state_constraints = []
39+
precondition_state_constraints: list[CustomStateConstraint] = []
40+
postcondition_state_constraints: list[CustomStateConstraint] = []
3941
if self.constraint.precondition:
4042
precondition_state_constraints = [
41-
c
43+
c # type: ignore
4244
for c in self.constraint.precondition
4345
if getattr(c, "type", None) == "custom_state"
4446
]
4547
if self.constraint.postcondition:
4648
postcondition_state_constraints = [
47-
c
49+
c # type: ignore
4850
for c in self.constraint.postcondition
4951
if getattr(c, "type", None) == "custom_state"
5052
]
5153

52-
custom_transition_constraints = []
53-
if self.constraint.transition:
54+
custom_transition_constraints: list[CustomTransitionConstraint] = []
55+
if self.constraint.pointer:
5456
custom_transition_constraints = [
55-
c
56-
for c in self.constraint.transition
57+
c # type: ignore
58+
for c in self.constraint.pointer
5759
if getattr(c, "type", None) == "custom_transition"
5860
]
5961

6062
for c in precondition_state_constraints:
6163
resolved.add_precondition(c._code)
6264
for c in postcondition_state_constraints:
6365
resolved.add_postcondition(c._code)
64-
for c in custom_transition_constraints:
65-
resolved.add_transition_constraint(c._code)
66+
for d in custom_transition_constraints:
67+
resolved.add_transition_constraint(d._code)
6668

67-
print(resolved.run())
69+
return resolved.run()

0 commit comments

Comments
 (0)