Z3 Armor

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.