Skip to content
KitploitKITPLOIT
ToolsBlog
Einreichen
ToolsBlog
Einreichen

Hacking-, PenTest- und Cybersicherheits-Tools für Ihr Sicherheitsarsenal!

Kitploit ist ein Verzeichnis von Hacking-, Cybersicherheits- und Pentesting-Tools. Entdecken Sie die neuesten Projekt-Updates, um Schwachstellen zu finden, Systeme zu analysieren, Tests zu automatisieren und Ihre Sicherheit zu stärken.

··Feeds·Kontakt·Datenschutz·© 2026 Kitploit

Tool-Verzeichnis

Kategorien

Alle Kategorien anzeigen
Loading categories
Tools/GitHubGitHub/z3prover/z3
Statische AnalyseKryptographieBinäranalysePapers & ForschungLernen & Bildung
GitHubz3prover/z3

z3

Hochleistungs-SMT-Löser für automatisiertes Theorembeweisen, Constraint-Lösen und Programmverifikation. Unterstützt mehrere Theorien und Sprachbindungen für formale Analysen.

Repository anzeigen
12.5k1.7k84vor 1h 46mVon Kitploit geprüft

Beliebteste

Alle anzeigen →

Entdecken Sie die meistgenutzten Tools unserer Community.

Alle Tools erkunden

Durchsuchen Sie unsere Tool-Sammlung

Alle Tools anzeigen →
Teilen

Z3

Z3 ist ein Theorembeweiser von Microsoft Research. Es ist unter der MIT-Lizenz lizenziert. Windows-Binärverteilungen enthalten C++-Laufzeit-Redistributables

Wenn Sie mit Z3 nicht vertraut sind, können Sie hier beginnen.

Vorgefertigte Binärdateien für stabile und nächtliche Versionen sind hier verfügbar.

Z3 kann mit Visual Studio, einem Makefile, mit CMake, mit vcpkg oder mit Bazel erstellt werden. Es bietet Bindings für mehrere Programmiersprachen.

Siehe die Versionshinweise für Hinweise zu verschiedenen stabilen Versionen von Z3.

Try the online Z3 Guide

Build-Status

Pull Request & Push Workflows

WASM-BuildWindows-BuildCIOCaml-Binding
WASM BuildWindowsCIOCaml Binding CI

Geplante Workflows

Offene FehlerAndroid-BuildPyodide Wheel (PyPI)Nächtlicher BuildCross-Build
Open IssuesAndroid BuildPyodide Wheel (PyPI)Nightly BuildRISC V and PowerPC 64
MSVC StaticMSVC Clang-CLBuild Z3 CacheSpeichersicherheitPRs als bereit markieren
MSVC Static BuildMSVC Clang-CL Static BuildBuild and Cache Z3Memory Safety AnalysisMark PRs Ready for Review

Manuelle & Release-Workflows

DokumentationRelease-BuildWASM-ReleaseNuGet-Build
DocumentationRelease BuildWebAssembly PublishBuild NuGet Package

Spezialisierte Workflows

Nächtliche ValidierungCopilot-EinrichtungAgentik-Wartung
Nightly Build ValidationCopilot Setup StepsAgentics Maintenance

Agentische Workflows

API-KohärenzCode-VereinfacherVersionshinweiseWorkflow-VorschlagAkademische Zitation
API Coherence CheckerCode SimplifierRelease Notes UpdaterWorkflow Suggestion AgentAcademic Citation Tracker
Issue BacklogSpeichersicherheitsberichtQF-S-BenchmarkSpecbot-Crash-AnalyzerSMTLIB-Benchmark-Finder
Issue Backlog ProcessorMemory Safety ReportZIPT String Solver BenchmarkSpecbot Crash AnalyzerSMTLIB Benchmark Finder
TPTP-Benchmark
TPTP Front-End Benchmark

Erstellen von Z3 unter Windows mit der Visual Studio-Eingabeaufforderung

Für 32-Bit-Builds beginnen Sie mit:

root@kitploit:~
python scripts/mk_make.py

oder stattdessen für einen 64-Bit-Build:

root@kitploit:~
python scripts/mk_make.py -x

führen Sie dann aus:

root@kitploit:~
cd build
nmake

Z3 verwendet C++20. Die empfohlene Version von Visual Studio ist daher VS2019 oder neuer.

Sicherheitsfunktionen (MSVC): Beim Erstellen mit Visual Studio/MSVC sind standardmäßig einige Sicherheitsfunktionen für Z3 aktiviert:

  • Control Flow Guard (/guard:cf) – standardmäßig aktiviert, um Versuche zu erkennen, Ihren Code zu kompromittieren, indem Aufrufe an andere Stellen als Funktions-Einstiegspunkte verhindert werden, was es Angreifern erschwert, durch Umleitung des Kontrollflusses beliebigen Code auszuführen.
  • Address Space Layout Randomization (/DYNAMICBASE) – standardmäßig aktiviert für die Randomisierung des Speicherlayouts, erforderlich durch die /GUARD:CF-Linkeroption.
  • Diese können bei Bedarf mit python scripts/mk_make.py --no-guardcf (Python-Build) oder cmake -DZ3_ENABLE_CFG=OFF (CMake-Build) deaktiviert werden.

Erstellen von Z3 mit make und GCC/Clang

Führen Sie aus:

root@kitploit:~
python scripts/mk_make.py
cd build
make
sudo make install

Beachten Sie, dass standardmäßig g++ als C++-Compiler verwendet wird, falls verfügbar. Wenn Sie Clang bevorzugen, ändern Sie den Aufruf von mk_make.py in:

root@kitploit:~
CXX=clang++ CC=clang python scripts/mk_make.py

Beachten Sie, dass Clang < 3.7 OpenMP nicht unterstützt.

Sie können Z3 auch für Windows mit Cygwin und dem Mingw-w64-Cross-Compiler erstellen. Stellen Sie in diesem Fall sicher, dass Sie Cygwins eigenes Python und keine Windows-Installation von Python verwenden.

Für einen 64-Bit-Build (von Cygwin64) konfigurieren Sie die Z3-Quellen mit

root@kitploit:~
CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.py

Ein 32-Bit-Build sollte ähnlich funktionieren (ist aber ungetestet); dasselbe gilt für 32/64-Bit-Builds innerhalb von Cygwin32.

Standardmäßig installiert es Z3-Executables in PREFIX/bin, Bibliotheken in PREFIX/lib und Include-Dateien in PREFIX/include, wobei das PREFIX-Installationspräfix vom Skript mk_make.py abgeleitet wird. Es ist normalerweise /usr für die meisten Linux-Distributionen und /usr/local für FreeBSD und macOS. Verwenden Sie die Befehlszeilenoption --prefix=, um das Installationspräfix zu ändern. Zum Beispiel:

root@kitploit:~
python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install

Um Z3 zu deinstallieren, verwenden Sie

root@kitploit:~
sudo make uninstall

Um Z3 zu bereinigen, können Sie das Build-Verzeichnis löschen und das Skript mk_make.py erneut ausführen.

Erstellen von Z3 mit CMake

Z3 hat ein Build-System mit CMake. Lesen Sie die Datei README-CMake.md für Details. Es wird für die meisten Build-Aufgaben empfohlen, mit Ausnahme des Erstellens von OCaml-Bindungen.

Erstellen von Z3 mit vcpkg

vcpkg ist ein vollständiger Plattform-Paketmanager. Um Z3 mit vcpkg zu installieren, führen Sie aus:

root@kitploit:~
git clone https://github.com/microsoft/vcpkg.git
./bootstrap-vcpkg.bat # For powershell
./bootstrap-vcpkg.sh # For bash
./vcpkg install z3

Erstellen von Z3 mit Bazel

Z3 kann mit Bazel erstellt werden. Dies funktioniert bekanntermaßen unter Ubuntu mit Clang (kann aber auch anderswo mit anderen Compilern funktionieren):

root@kitploit:~
bazel build //...

Abhängigkeiten

Z3 selbst hat nur wenige Abhängigkeiten. Es verwendet C++-Laufzeitbibliotheken, einschließlich pthreads für Multithreading. Optional kann GMP für mehrfache Genauigkeit bei Ganzzahlen verwendet werden, aber Z3 enthält eine eigene in sich geschlossene Mehrfachgenauigkeitsfunktionalität. Python ist erforderlich, um Z3 zu erstellen. Das Erstellen von Java-, .NET-, OCaml- und Julia-APIs erfordert die Installation relevanter Toolchains.

Z3-Bindungen

Z3 hat Bindungen für verschiedene Programmiersprachen.

.NET

Sie können ein NuGet-Paket für die neueste Z3-Version von nuget.org installieren.

Verwenden Sie das Befehlszeilen-Flag --dotnet mit mk_make.py, um das Erstellen dieser zu aktivieren.

Siehe examples/dotnet für Beispiele.

C

Diese sind immer aktiviert.

Siehe examples/c für Beispiele.

C++

Diese sind immer aktiviert.

Siehe examples/c++ für Beispiele.

Java

Verwenden Sie das Befehlszeilen-Flag --java mit mk_make.py, um das Erstellen dieser zu aktivieren.

Anleitungen zur IDE-Einrichtung (Eclipse, IntelliJ IDEA, Visual Studio Code) und Fehlerbehebung finden Sie im Java IDE Setup Guide.

Siehe examples/java für Beispiele.

Go

Verwenden Sie das Befehlszeilen-Flag --go mit mk_make.py, um das Erstellen dieser zu aktivieren. Beachten Sie, dass Go-Bindungen CGO verwenden und eine Go-Toolchain (Go 1.20 oder neuer) zum Erstellen benötigen.

Verwenden Sie mit CMake die Option -DZ3_BUILD_GO_BINDINGS=ON.

Siehe examples/go für Beispiele und src/api/go/README.md für die vollständige API-Dokumentation.

OCaml

Verwenden Sie das Befehlszeilen-Flag --ml mit mk_make.py, um das Erstellen dieser zu aktivieren.

Siehe examples/ml für Beispiele.

Python

Sie können den Python-Wrapper für Z3 für die neueste Version von pypi mit dem folgenden Befehl installieren:

root@kitploit:~
   pip install z3-solver

Verwenden Sie das Befehlszeilen-Flag --python mit mk_make.py, um das Erstellen dieser zu aktivieren.

Beachten Sie, dass auf bestimmten Plattformen das Python-Paketverzeichnis (site-packages auf den meisten Distributionen und dist-packages auf Debian-basierten Distributionen) unter dem Installationspräfix liegen muss. Wenn Sie ein nicht standardmäßiges Präfix verwenden, können Sie die Option --pypkgdir verwenden, um das für die Installation verwendete Python-Paketverzeichnis zu ändern. Zum Beispiel:

root@kitploit:~
python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages

Wenn Sie in ein nicht standardmäßiges Präfix installieren müssen, ist ein besserer Ansatz, eine Python virtuelle Umgebung zu verwenden und Z3 dort zu installieren. Python-Pakete funktionieren auch für Python3. Denken Sie unter Windows daran, innerhalb der nativen Visual C++-Befehlsumgebung zu erstellen. Beachten Sie, dass das Verzeichnis build/python/z3 von dem Ort aus zugänglich sein sollte, an dem Python mit Z3 verwendet wird, und dass libz3.dll im Pfad vorhanden sein muss.

root@kitploit:~
virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# You will find Z3 and the Python bindings installed in the virtual environment
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...

Siehe examples/python für Beispiele.

Julia

Das Julia-Paket Z3.jl kapselt die C-API von Z3. Eine frühere Version kapselte die C++-API: Informationen zum Aktualisieren und Erstellen der Julia-Bindungen finden Sie in src/api/julia.

WebAssembly / TypeScript / JavaScript

Ein WebAssembly-Build mit zugehörigen TypeScript-Typisierungen wird auf npm als z3-solver veröffentlicht. Informationen zum Erstellen dieser Bindungen finden Sie in src/api/js.

Smalltalk (Pharo / Smalltalk/X)

Das Projekt MachineArithmetic bietet eine Smalltalk-Schnittstelle zur C-API von Z3. Weitere Informationen finden Sie unter MachineArithmetic/README.md.

AIX

Build-Einstellungen für AIX sind hier beschrieben.

Systemübersicht

System Diagram

Schnittstellen

  • Standard-Eingabeformat ist SMTLIB2

  • Andere native fremde Funktionsschnittstellen:

  • C++-API

  • .NET-API

  • Java-API

  • Python-API (auch im pydoc-Format verfügbar)

  • Rust

  • C

  • OCaml

  • Julia

  • Smalltalk (unterstützt Pharo und Smalltalk/X)

Power-Tools

  • Der Axiom Profiler, der derzeit von der ETH Zurich entwickelt wird
Tool herunterladen