Constraint-based obfuscation using z3.
Project description
Description
Constraint-based obfuscation using z3.
Documentation
Documentation is available on https://dashstrom.github.io/z3-armor
Installation
You can install z3-armor
using pipx
from PyPI
pip install pipx
pipx ensurepath
pipx install z3-armor
Usage
Generate C challenge
z3-armor --template crackme.c -p 'CTF{flag}' -s 0 -o chall.c
gcc -o chall -fno-stack-protector -O0 chall.c
./chall
password: CTF{flag}
Valid password ┬─┬ ~( º-º~)
#include <stdio.h>
#include <stdlib.h>
#include <sys/types.h>
#include <string.h>
#define SIZE 9
typedef unsigned char uc;
static const char INVALID_PASSWORD[] = "Invalid password (\u256f\u00b0\u25a1\u00b0)\u256f \u253b\u2501\u253b\n";
static const char VALID_PASSWORD[] = "Valid password \u252c\u2500\u252c ~( \u00ba-\u00ba~)\n";
int main();
int main() {
char secret[SIZE + 1];
printf("password: ");
fgets(secret, SIZE + 1, stdin);
secret[strcspn(secret, "\r\n")] = 0;
size_t length = strlen(secret);
if (length != SIZE) {
printf(INVALID_PASSWORD);
return 1;
}
if (
(uc)(secret[1] ^ secret[4]) == 50
&& (uc)(secret[5] * secret[3]) == 228
&& secret[6] == (uc)(secret[3] + 230)
&& secret[7] == (uc)(secret[2] - 223)
&& (uc)(secret[7] - secret[8]) == 234
&& secret[7] == (uc)(secret[0] - 220)
&& (uc)(secret[8] ^ secret[1]) == 41
&& secret[6] == (uc)(secret[2] - 229)
&& (uc)(secret[4] + secret[0]) == 169
&& secret[8] == (uc)(secret[5] + 17)
) {
printf(VALID_PASSWORD);
} else {
printf(INVALID_PASSWORD);
}
return 0;
}
Generate Python Solution
z3-armor --template solver.py -p 'CTF{flag}' -s 0 -o solve.py
python3 solve.py
b'CTF{flag}'
"""Solver for challenge."""
from z3 import BitVec, Solver, sat
def solve() -> None:
"""Solve challenge using z3."""
p = [BitVec(f"p[{i}]", 8) for i in range(9)]
s = Solver()
s.add((p[1] ^ p[4]) == 50)
s.add((p[5] * p[3]) == 228)
s.add(p[6] == (p[3] + 230))
s.add(p[7] == (p[2] - 223))
s.add((p[7] - p[8]) == 234)
s.add(p[7] == (p[0] - 220))
s.add((p[8] ^ p[1]) == 41)
s.add(p[6] == (p[2] - 229))
s.add((p[4] + p[0]) == 169)
s.add(p[8] == (p[5] + 17))
if s.check() != sat:
print("Cannot find secret.")
return
model = s.model()
solutions = [model[c] for c in p]
flag = bytes(s.as_long() for s in solutions)
print(flag)
if __name__ == "__main__":
solve()
Development
Contributing
Contributions are very welcome. Tests can be run with poe check
, please
ensure the coverage at least stays the same before you submit a pull request.
Setup
You need to install Poetry and Git for work with this project.
git clone https://github.com/Dashstrom/z3-armor
cd z3-armor
poetry install --all-extras
poetry run poe setup
poetry shell
Poe
Poe is available for help you to run tasks.
test Run test suite.
lint Run linters: ruff linter, ruff formatter and mypy.
format Run linters in fix mode.
check Run all checks: lint, test and docs.
cov Run coverage for generate report and html.
open-cov Open html coverage report in webbrowser.
docs Build documentation.
open-docs Open documentation in webbrowser.
setup Setup pre-commit.
pre-commit Run pre-commit.
clean Clean cache files
Skip commit verification
If the linting is not successful, you can’t commit. For forcing the commit you can use the next command :
git commit --no-verify -m 'MESSAGE'
Commit with commitizen
To respect commit conventions, this repository uses Commitizen.
cz c
How to add dependency
poetry add 'PACKAGE'
Ignore illegitimate warnings
To ignore illegitimate warnings you can add :
# noqa: ERROR_CODE on the same line for ruff.
# type: ignore[ERROR_CODE] on the same line for mypy.
# pragma: no cover on the same line to ignore line for coverage.
# doctest: +SKIP on the same line for doctest.
Uninstall
pipx uninstall z3-armor
License
This work is licensed under MIT.
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
File details
Details for the file z3_armor-0.0.1.tar.gz
.
File metadata
- Download URL: z3_armor-0.0.1.tar.gz
- Upload date:
- Size: 14.2 kB
- Tags: Source
- Uploaded using Trusted Publishing? Yes
- Uploaded via: twine/5.1.0 CPython/3.12.4
File hashes
Algorithm | Hash digest | |
---|---|---|
SHA256 | f0a07565e07eec6ec04072944ee71cc7bc37bca9e0fd3dbb191eb5ded3085897 |
|
MD5 | a8d6e933d30a61a5bd1abfa3d0e5ba1d |
|
BLAKE2b-256 | 5f38a33c86d9ff0808bbc5e09290b8a3a5ceafa7f3dc0dc53a953dc119c5a7b2 |
File details
Details for the file z3_armor-0.0.1-py3-none-any.whl
.
File metadata
- Download URL: z3_armor-0.0.1-py3-none-any.whl
- Upload date:
- Size: 12.5 kB
- Tags: Python 3
- Uploaded using Trusted Publishing? Yes
- Uploaded via: twine/5.1.0 CPython/3.12.4
File hashes
Algorithm | Hash digest | |
---|---|---|
SHA256 | e937601e0513bcc51b5e29977364b6c5480dca3edc0a2832fd59501df56d9745 |
|
MD5 | 2fd898f4e0ba36ae68c21969ddccd106 |
|
BLAKE2b-256 | 4710f7cb7bb04c40d1860d15b893a2981db697120c50542374fc5400f92ba2bc |