Skip to content

Commit f0258f4

Browse files
toolCHAINZtoolCHAINZ
authored
fix: tweak some schemas and serializations (#77)
* Initial cut * Initial cut * Initial cut * Fix non-serializable stuff * Update readme * Remove import
1 parent f2ef4cb commit f0258f4

File tree

7 files changed

+249
-105
lines changed

7 files changed

+249
-105
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/__init__.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
11
from z3 import z3 # necessary to ensure z3 is loaded on macOS # noqa
2-
from ._internal import jingle, crackers # noqa
2+
from ._internal import jingle, crackers # noqa

0 commit comments

Comments
 (0)