Skip to content
KitploitKITPLOIT
도구블로그
제출
도구블로그
제출

해킹, 침투 테스트 및 사이버 보안 도구를 당신의 보안 무기고에!

Kitploit은 해킹, 사이버 보안 및 침투 테스트 도구 디렉토리입니다. 최신 프로젝트 업데이트를 발견하여 취약점을 찾고, 시스템을 분석하고, 테스트를 자동화하고, 보안을 강화하세요.

··피드·문의·개인정보·© 2026 Kitploit

도구 디렉토리

카테고리

모든 카테고리 보기
Loading categories
z3 — 자동 정리 증명, 제약 조건 해결 및 프로그램 검증을 위한 고성능 SMT 해결사. 형식적 분석을 위한 여러 이론 및 언어 바인딩을 지원합니다. | Kitploit
도구/GitHubGitHub/z3prover/z3
Static AnalysisCryptographyBinary AnalysisPapers & ResearchLearning & Education
GitHubz3prover/z3

z3

자동 정리 증명, 제약 조건 해결 및 프로그램 검증을 위한 고성능 SMT 해결사. 형식적 분석을 위한 여러 이론 및 언어 바인딩을 지원합니다.

저장소 보기
12.5k1.7k17시간 16분 전Kitploit 검토 완료

인기

모두 보기 →

커뮤니티에서 가장 많이 사용되는 도구를 찾아보세요.

모든 도구 탐색

도구 컬렉션을 둘러보세요

모든 도구 보기 →
공유

Z3

Z3는 Microsoft Research의 정리 증명기입니다. MIT 라이선스에 따라 사용이 허가됩니다. Windows 바이너리 배포판에는 C++ 런타임 재배포 가능 패키지가 포함되어 있습니다.

Z3에 익숙하지 않다면 여기에서 시작할 수 있습니다.

안정 및 야간 릴리스의 미리 빌드된 바이너리는 여기에서 사용할 수 있습니다.

Z3는 Visual Studio, Makefile, CMake, vcpkg 또는 Bazel을 사용하여 빌드할 수 있습니다. 여러 프로그래밍 언어에 대한 바인딩을 제공합니다.

Z3의 다양한 안정 릴리스에 대한 참고 사항은 릴리스 노트를 참조하세요.

온라인 Z3 가이드 사용해보기

빌드 상태

Pull Request 및 Push 워크플로우

WASM 빌드Windows 빌드CIOCaml 바인딩

예약된 워크플로우

수동 및 릴리스 워크플로우

문서릴리스 빌드WASM 릴리스NuGet 빌드

특수 워크플로우

야간 검증Copilot 설정Agentics 유지 관리
Nightly Build ValidationCopilot Setup Steps

에이전트 워크플로우

TPTP 벤치마크
TPTP Front-End Benchmark

Windows에서 Visual Studio 명령 프롬프트를 사용하여 Z3 빌드

32비트 빌드의 경우 다음으로 시작합니다.

root@kitploit:~
python scripts/mk_make.py

또는 64비트 빌드의 경우:

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

그런 다음 실행:

root@kitploit:~
cd build
nmake

Z3는 C++20을 사용합니다. 따라서 권장 Visual Studio 버전은 VS2019 이상입니다.

보안 기능 (MSVC): Visual Studio/MSVC로 빌드할 때 Z3에 대해 기본적으로 몇 가지 보안 기능이 활성화됩니다.

  • 제어 흐름 보호 (/guard:cf) - 기본적으로 활성화되어 함수 진입점 이외의 위치 호출을 차단하여 코드 손상 시도를 감지하므로, 공격자가 제어 흐름 리디렉션을 통해 임의 코드를 실행하기 어렵게 만듭니다.
  • 주소 공간 레이아웃 무작위화 (/DYNAMICBASE) - 메모리 레이아웃 무작위화를 위해 기본적으로 활성화되며, /GUARD:CF 링커 옵션에 필요합니다.
  • 필요한 경우 python scripts/mk_make.py --no-guardcf (Python 빌드) 또는 cmake -DZ3_ENABLE_CFG=OFF (CMake 빌드)를 사용하여 비활성화할 수 있습니다.

make 및 GCC/Clang을 사용하여 Z3 빌드

실행:

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

기본적으로 g++을 사용할 수 있으면 C++ 컴파일러로 사용됩니다. Clang을 선호하는 경우 mk_make.py 호출을 다음과 같이 변경하세요.

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

Clang < 3.7은 OpenMP를 지원하지 않습니다.

Cygwin 및 Mingw-w64 크로스 컴파일러를 사용하여 Windows용 Z3를 빌드할 수도 있습니다. 이 경우 Cygwin 자체 Python을 사용하고 Windows에 설치된 Python을 사용하지 않도록 하십시오.

64비트 빌드(Cygwin64에서)의 경우 다음으로 Z3 소스를 구성합니다.

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

32비트 빌드도 비슷하게 작동해야 하지만(테스트되지 않음) Cygwin32 내에서 32/64비트 빌드에도 동일하게 적용됩니다.

기본적으로 Z3 실행 파일은 PREFIX/bin에, 라이브러리는 PREFIX/lib에, include 파일은 PREFIX/include에 설치됩니다. 여기서 PREFIX 설치 접두사는 mk_make.py 스크립트에 의해 유추됩니다. 대부분의 Linux 배포판에서는 일반적으로 /usr이고, FreeBSD 및 macOS에서는 /usr/local입니다. 설치 접두사를 변경하려면 --prefix= 명령줄 옵션을 사용하세요. 예:

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

Z3를 제거하려면 다음을 사용하세요.

root@kitploit:~
sudo make uninstall

Z3를 정리하려면 빌드 디렉터리를 삭제하고 mk_make.py 스크립트를 다시 실행하면 됩니다.

CMake를 사용하여 Z3 빌드

Z3에는 CMake를 사용하는 빌드 시스템이 있습니다. 자세한 내용은 README-CMake.md 파일을 읽으세요. OCaml 바인딩 빌드를 제외한 대부분의 빌드 작업에 권장됩니다.

vcpkg를 사용하여 Z3 빌드

vcpkg는 완전한 플랫폼 패키지 관리자입니다. vcpkg로 Z3를 설치하려면 다음을 실행하세요.

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

Bazel을 사용하여 Z3 빌드

Z3는 Bazel을 사용하여 빌드할 수 있습니다. 이는 Ubuntu에서 Clang과 함께 작동하는 것으로 알려져 있습니다(다른 컴파일러를 사용하는 다른 환경에서도 작동할 수 있음).

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

종속성

Z3 자체는 종속성이 거의 없습니다. C++ 런타임 라이브러리를 사용하며 멀티스레딩을 위해 pthreads를 포함합니다. 선택적으로 다중 정밀도 정수에 GMP를 사용할 수 있지만 Z3에는 자체 포함된 다중 정밀도 기능이 포함되어 있습니다. Z3를 빌드하려면 Python이 필요합니다. Java, .NET, OCaml 및 Julia API를 빌드하려면 관련 툴체인을 설치해야 합니다.

Z3 바인딩

Z3는 다양한 프로그래밍 언어에 대한 바인딩을 제공합니다.

.NET

최신 릴리스 Z3용 NuGet 패키지를 nuget.org에서 설치할 수 있습니다.

mk_make.py와 함께 --dotnet 명령줄 플래그를 사용하여 빌드를 활성화합니다.

예제는 examples/dotnet를 참조하세요.

C

항상 활성화됩니다.

예제는 examples/c를 참조하세요.

C++

항상 활성화됩니다.

예제는 examples/c++를 참조하세요.

Java

mk_make.py와 함께 --java 명령줄 플래그를 사용하여 빌드를 활성화합니다.

IDE 설정 지침(Eclipse, IntelliJ IDEA, Visual Studio Code) 및 문제 해결은 Java IDE 설정 가이드를 참조하세요.

예제는 examples/java를 참조하세요.

Go

mk_make.py와 함께 --go 명령줄 플래그를 사용하여 빌드를 활성화합니다. Go 바인딩은 CGO를 사용하며 빌드하려면 Go 툴체인(Go 1.20 이상)이 필요합니다.

CMake에서는 -DZ3_BUILD_GO_BINDINGS=ON 옵션을 사용하세요.

예제는 examples/go를 참조하고 전체 API 문서는 src/api/go/README.md를 참조하세요.

OCaml

mk_make.py와 함께 --ml 명령줄 플래그를 사용하여 빌드를 활성화합니다.

예제는 examples/ml를 참조하세요.

Python

최신 릴리스용 Z3 Python 래퍼는 pypi에서 다음 명령을 사용하여 설치할 수 있습니다.

root@kitploit:~
   pip install z3-solver

mk_make.py와 함께 --python 명령줄 플래그를 사용하여 빌드를 활성화합니다.

특정 플랫폼에서는 Python 패키지 디렉터리(대부분의 배포판에서는 site-packages, Debian 기반 배포판에서는 dist-packages)가 설치 접두사 아래에 있어야 합니다. 비표준 접두사를 사용하는 경우 --pypkgdir 옵션을 사용하여 설치에 사용할 Python 패키지 디렉터리를 변경할 수 있습니다. 예:

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

비표준 접두사에 설치해야 하는 경우 더 나은 방법은 Python 가상 환경을 사용하여 Z3를 설치하는 것입니다. Python 패키지는 Python3에서도 작동합니다. Windows에서는 Visual C++ 네이티브 명령 빌드 환경 내에서 빌드해야 합니다. build/python/z3 디렉터리는 Z3와 함께 Python을 사용하는 위치에서 액세스할 수 있어야 하며 libz3.dll이 경로에 있어야 합니다.

root@kitploit:~
virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# 가상 환경에 Z3 및 Python 바인딩이 설치된 것을 찾을 수 있습니다.
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...

예제는 examples/python를 참조하세요.

Julia

Julia 패키지 Z3.jl는 Z3의 C API를 래핑합니다. 이전 버전은 C++ API를 래핑했습니다. Julia 바인딩 업데이트 및 빌드에 대한 정보는 src/api/julia에서 찾을 수 있습니다.

WebAssembly / TypeScript / JavaScript

연결된 TypeScript 타이핑이 포함된 WebAssembly 빌드는 npm에 z3-solver로 게시됩니다. 이러한 바인딩 빌드에 대한 정보는 src/api/js에서 찾을 수 있습니다.

Smalltalk (Pharo / Smalltalk/X)

프로젝트 MachineArithmetic은 Z3의 C API에 대한 Smalltalk 인터페이스를 제공합니다. 자세한 내용은 MachineArithmetic/README.md를 참조하세요.

AIX

AIX용 빌드 설정은 여기에 설명되어 있습니다.

시스템 개요

시스템 다이어그램

인터페이스

  • 기본 입력 형식은 SMTLIB2입니다.

  • 기타 네이티브 외부 함수 인터페이스:

  • C++ API

  • .NET API

  • Java API

  • Python API (pydoc 형식으로도 제공)

  • Rust

  • C

  • OCaml

  • Julia

  • Smalltalk (Pharo 및 Smalltalk/X 지원)

파워 툴

  • 현재 ETH Zurich에서 개발 중인 Axiom Profiler
도구 다운로드
WASM Build
Windows
CI
OCaml Binding CI
오픈 버그Android 빌드Pyodide 휠 (PyPI)야간 빌드크로스 빌드
Open IssuesAndroid BuildPyodide Wheel (PyPI)Nightly BuildRISC V and PowerPC 64
MSVC 정적MSVC Clang-CLZ3 캐시 빌드메모리 안전성PR 준비 표시
MSVC Static BuildMSVC Clang-CL Static BuildBuild and Cache Z3Memory Safety AnalysisMark PRs Ready for Review
Documentation
Release Build
WebAssembly Publish
Build NuGet Package
Agentics Maintenance
API 일관성코드 단순화릴리스 노트워크플로우 제안학술 인용
API Coherence CheckerCode SimplifierRelease Notes UpdaterWorkflow Suggestion AgentAcademic Citation Tracker
이슈 백로그메모리 안전성 보고서QF-S 벤치마크Specbot 충돌 분석기SMTLIB 벤치마크 파인더
Issue Backlog ProcessorMemory Safety ReportZIPT String Solver BenchmarkSpecbot Crash AnalyzerSMTLIB Benchmark Finder