.. role:: bash(code)
:language: bash
********
Z3 Armor
********
|ci-docs| |ci-lint| |ci-tests| |pypi| |versions| |discord| |license|
.. |ci-docs| image:: https://github.com/Dashstrom/z3-armor/actions/workflows/docs.yml/badge.svg
:target: https://github.com/Dashstrom/z3-armor/actions/workflows/docs.yml
:alt: CI : Docs
.. |ci-lint| image:: https://github.com/Dashstrom/z3-armor/actions/workflows/lint.yml/badge.svg
:target: https://github.com/Dashstrom/z3-armor/actions/workflows/lint.yml
:alt: CI : Lint
.. |ci-tests| image:: https://github.com/Dashstrom/z3-armor/actions/workflows/tests.yml/badge.svg
:target: https://github.com/Dashstrom/z3-armor/actions/workflows/tests.yml
:alt: CI : Tests
.. |pypi| image:: https://img.shields.io/pypi/v/z3-armor.svg
:target: https://pypi.org/project/z3-armor
:alt: PyPI : z3-armor
.. |versions| image:: https://img.shields.io/pypi/pyversions/z3-armor.svg
:target: https://pypi.org/project/z3-armor
:alt: Python : versions
.. |discord| image:: https://img.shields.io/badge/Discord-dashstrom-5865F2?style=flat&logo=discord&logoColor=white
:target: https://dsc.gg/dashstrom
:alt: Discord
.. |license| image:: https://img.shields.io/badge/license-MIT-green.svg
:target: https://github.com/Dashstrom/z3-armor/blob/main/LICENSE
:alt: License : MIT
Description
###########
Constraint-based obfuscation using z3.
Documentation
#############
Documentation is available on https://dashstrom.github.io/z3-armor
Installation
############
You can install :bash:`z3-armor` using `pipx <https://pipx.pypa.io/stable/>`_
from `PyPI <https://pypi.org/project>`_
.. code-block:: bash
pip install pipx
pipx ensurepath
pipx install z3-armor
Usage
#####
Generate C challenge
********************
.. code-block:: bash
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 ┬─┬ ~( º-º~)
.. code-block:: c
#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
************************
.. code-block:: bash
z3-armor --template solver.py -p 'CTF{flag}' -s 0 -o solve.py
python3 solve.py
b'CTF{flag}'
.. code-block:: python
"""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 :bash:`poe check`, please
ensure the coverage at least stays the same before you submit a pull request.
Setup
*****
You need to install `Poetry <https://python-poetry.org/docs/#installation>`_
and `Git <https://git-scm.com/book/en/v2/Getting-Started-Installing-Git>`_
for work with this project.
.. code-block:: bash
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.
.. code-block:: text
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 :
.. code-block:: bash
git commit --no-verify -m 'MESSAGE'
Commit with commitizen
**********************
To respect commit conventions, this repository uses
`Commitizen <https://github.com/commitizen-tools/commitizen?tab=readme-ov-file>`_.
.. code-block:: bash
cz c
How to add dependency
*********************
.. code-block:: bash
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
#########
.. code-block:: bash
pipx uninstall z3-armor
License
#######
This work is licensed under `MIT <https://github.com/Dashstrom/z3-armor/blob/main/LICENSE>`_.
Raw data
{
"_id": null,
"home_page": "https://github.com/Dashstrom/z3-armor",
"name": "z3-armor",
"maintainer": "Dashstrom",
"docs_url": null,
"requires_python": ">=3.8",
"maintainer_email": "dashstrom.pro@gmail.com",
"keywords": "python",
"author": "Dashstrom",
"author_email": "dashstrom.pro@gmail.com",
"download_url": "https://files.pythonhosted.org/packages/5f/38/a33c86d9ff0808bbc5e09290b8a3a5ceafa7f3dc0dc53a953dc119c5a7b2/z3_armor-0.0.1.tar.gz",
"platform": null,
"description": ".. role:: bash(code)\n :language: bash\n\n********\nZ3 Armor\n********\n\n|ci-docs| |ci-lint| |ci-tests| |pypi| |versions| |discord| |license|\n\n.. |ci-docs| image:: https://github.com/Dashstrom/z3-armor/actions/workflows/docs.yml/badge.svg\n :target: https://github.com/Dashstrom/z3-armor/actions/workflows/docs.yml\n :alt: CI : Docs\n\n.. |ci-lint| image:: https://github.com/Dashstrom/z3-armor/actions/workflows/lint.yml/badge.svg\n :target: https://github.com/Dashstrom/z3-armor/actions/workflows/lint.yml\n :alt: CI : Lint\n\n.. |ci-tests| image:: https://github.com/Dashstrom/z3-armor/actions/workflows/tests.yml/badge.svg\n :target: https://github.com/Dashstrom/z3-armor/actions/workflows/tests.yml\n :alt: CI : Tests\n\n.. |pypi| image:: https://img.shields.io/pypi/v/z3-armor.svg\n :target: https://pypi.org/project/z3-armor\n :alt: PyPI : z3-armor\n\n.. |versions| image:: https://img.shields.io/pypi/pyversions/z3-armor.svg\n :target: https://pypi.org/project/z3-armor\n :alt: Python : versions\n\n.. |discord| image:: https://img.shields.io/badge/Discord-dashstrom-5865F2?style=flat&logo=discord&logoColor=white\n :target: https://dsc.gg/dashstrom\n :alt: Discord\n\n.. |license| image:: https://img.shields.io/badge/license-MIT-green.svg\n :target: https://github.com/Dashstrom/z3-armor/blob/main/LICENSE\n :alt: License : MIT\n\nDescription\n###########\n\nConstraint-based obfuscation using z3.\n\nDocumentation\n#############\n\nDocumentation is available on https://dashstrom.github.io/z3-armor\n\nInstallation\n############\n\nYou can install :bash:`z3-armor` using `pipx <https://pipx.pypa.io/stable/>`_\nfrom `PyPI <https://pypi.org/project>`_\n\n.. code-block:: bash\n\n pip install pipx\n pipx ensurepath\n pipx install z3-armor\n\nUsage\n#####\n\nGenerate C challenge\n********************\n\n.. code-block:: bash\n\n z3-armor --template crackme.c -p 'CTF{flag}' -s 0 -o chall.c\n gcc -o chall -fno-stack-protector -O0 chall.c\n ./chall\n password: CTF{flag}\n Valid password \u252c\u2500\u252c ~( \u00ba-\u00ba~)\n\n.. code-block:: c\n\n #include <stdio.h>\n #include <stdlib.h>\n #include <sys/types.h>\n #include <string.h>\n\n #define SIZE 9\n\n typedef unsigned char uc;\n static const char INVALID_PASSWORD[] = \"Invalid password (\\u256f\\u00b0\\u25a1\\u00b0)\\u256f \\u253b\\u2501\\u253b\\n\";\n static const char VALID_PASSWORD[] = \"Valid password \\u252c\\u2500\\u252c ~( \\u00ba-\\u00ba~)\\n\";\n\n int main();\n\n int main() {\n char secret[SIZE + 1];\n printf(\"password: \");\n fgets(secret, SIZE + 1, stdin);\n secret[strcspn(secret, \"\\r\\n\")] = 0;\n size_t length = strlen(secret);\n if (length != SIZE) {\n printf(INVALID_PASSWORD);\n return 1;\n }\n if (\n (uc)(secret[1] ^ secret[4]) == 50\n && (uc)(secret[5] * secret[3]) == 228\n && secret[6] == (uc)(secret[3] + 230)\n && secret[7] == (uc)(secret[2] - 223)\n && (uc)(secret[7] - secret[8]) == 234\n && secret[7] == (uc)(secret[0] - 220)\n && (uc)(secret[8] ^ secret[1]) == 41\n && secret[6] == (uc)(secret[2] - 229)\n && (uc)(secret[4] + secret[0]) == 169\n && secret[8] == (uc)(secret[5] + 17)\n ) {\n printf(VALID_PASSWORD);\n } else {\n printf(INVALID_PASSWORD);\n }\n return 0;\n }\n\nGenerate Python Solution\n************************\n\n.. code-block:: bash\n\n z3-armor --template solver.py -p 'CTF{flag}' -s 0 -o solve.py\n python3 solve.py\n b'CTF{flag}'\n\n.. code-block:: python\n\n \"\"\"Solver for challenge.\"\"\"\n from z3 import BitVec, Solver, sat\n\n\n def solve() -> None:\n \"\"\"Solve challenge using z3.\"\"\"\n p = [BitVec(f\"p[{i}]\", 8) for i in range(9)]\n s = Solver()\n s.add((p[1] ^ p[4]) == 50)\n s.add((p[5] * p[3]) == 228)\n s.add(p[6] == (p[3] + 230))\n s.add(p[7] == (p[2] - 223))\n s.add((p[7] - p[8]) == 234)\n s.add(p[7] == (p[0] - 220))\n s.add((p[8] ^ p[1]) == 41)\n s.add(p[6] == (p[2] - 229))\n s.add((p[4] + p[0]) == 169)\n s.add(p[8] == (p[5] + 17))\n if s.check() != sat:\n print(\"Cannot find secret.\")\n return\n model = s.model()\n solutions = [model[c] for c in p]\n flag = bytes(s.as_long() for s in solutions)\n print(flag)\n\n if __name__ == \"__main__\":\n solve()\n\nDevelopment\n###########\n\nContributing\n************\n\nContributions are very welcome. Tests can be run with :bash:`poe check`, please\nensure the coverage at least stays the same before you submit a pull request.\n\nSetup\n*****\n\nYou need to install `Poetry <https://python-poetry.org/docs/#installation>`_\nand `Git <https://git-scm.com/book/en/v2/Getting-Started-Installing-Git>`_\nfor work with this project.\n\n.. code-block:: bash\n\n git clone https://github.com/Dashstrom/z3-armor\n cd z3-armor\n poetry install --all-extras\n poetry run poe setup\n poetry shell\n\nPoe\n********\n\nPoe is available for help you to run tasks.\n\n.. code-block:: text\n\n test Run test suite.\n lint Run linters: ruff linter, ruff formatter and mypy.\n format Run linters in fix mode.\n check Run all checks: lint, test and docs.\n cov Run coverage for generate report and html.\n open-cov Open html coverage report in webbrowser.\n docs Build documentation.\n open-docs Open documentation in webbrowser.\n setup Setup pre-commit.\n pre-commit Run pre-commit.\n clean Clean cache files\n\nSkip commit verification\n************************\n\nIf the linting is not successful, you can't commit.\nFor forcing the commit you can use the next command :\n\n.. code-block:: bash\n\n git commit --no-verify -m 'MESSAGE'\n\nCommit with commitizen\n**********************\n\nTo respect commit conventions, this repository uses\n`Commitizen <https://github.com/commitizen-tools/commitizen?tab=readme-ov-file>`_.\n\n.. code-block:: bash\n\n cz c\n\nHow to add dependency\n*********************\n\n.. code-block:: bash\n\n poetry add 'PACKAGE'\n\nIgnore illegitimate warnings\n****************************\n\nTo ignore illegitimate warnings you can add :\n\n- **# noqa: ERROR_CODE** on the same line for ruff.\n- **# type: ignore[ERROR_CODE]** on the same line for mypy.\n- **# pragma: no cover** on the same line to ignore line for coverage.\n- **# doctest: +SKIP** on the same line for doctest.\n\nUninstall\n#########\n\n.. code-block:: bash\n\n pipx uninstall z3-armor\n\nLicense\n#######\n\nThis work is licensed under `MIT <https://github.com/Dashstrom/z3-armor/blob/main/LICENSE>`_.\n\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "Constraint-based obfuscation using z3.",
"version": "0.0.1",
"project_urls": {
"Documentation": "https://dashstrom.github.io/z3-armor",
"Homepage": "https://github.com/Dashstrom/z3-armor",
"Repository": "https://github.com/Dashstrom/z3-armor"
},
"split_keywords": [
"python"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "4710f7cb7bb04c40d1860d15b893a2981db697120c50542374fc5400f92ba2bc",
"md5": "2fd898f4e0ba36ae68c21969ddccd106",
"sha256": "e937601e0513bcc51b5e29977364b6c5480dca3edc0a2832fd59501df56d9745"
},
"downloads": -1,
"filename": "z3_armor-0.0.1-py3-none-any.whl",
"has_sig": false,
"md5_digest": "2fd898f4e0ba36ae68c21969ddccd106",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.8",
"size": 12469,
"upload_time": "2024-07-13T22:39:26",
"upload_time_iso_8601": "2024-07-13T22:39:26.965504Z",
"url": "https://files.pythonhosted.org/packages/47/10/f7cb7bb04c40d1860d15b893a2981db697120c50542374fc5400f92ba2bc/z3_armor-0.0.1-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "5f38a33c86d9ff0808bbc5e09290b8a3a5ceafa7f3dc0dc53a953dc119c5a7b2",
"md5": "a8d6e933d30a61a5bd1abfa3d0e5ba1d",
"sha256": "f0a07565e07eec6ec04072944ee71cc7bc37bca9e0fd3dbb191eb5ded3085897"
},
"downloads": -1,
"filename": "z3_armor-0.0.1.tar.gz",
"has_sig": false,
"md5_digest": "a8d6e933d30a61a5bd1abfa3d0e5ba1d",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.8",
"size": 14228,
"upload_time": "2024-07-13T22:39:28",
"upload_time_iso_8601": "2024-07-13T22:39:28.521058Z",
"url": "https://files.pythonhosted.org/packages/5f/38/a33c86d9ff0808bbc5e09290b8a3a5ceafa7f3dc0dc53a953dc119c5a7b2/z3_armor-0.0.1.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-07-13 22:39:28",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "Dashstrom",
"github_project": "z3-armor",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"lcname": "z3-armor"
}
JSON
