3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-01 12:07:51 +00:00

Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988)

* Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it.

* Fix configuration error for non-MSVC compilers.

* Reviewed and updated configuration for Python build and added comment for CFG.
This commit is contained in:
hwisungi 2025-10-22 05:18:25 -07:00 committed by Nikolaj Bjorner
parent 06d142119f
commit ba03d35957
5 changed files with 155 additions and 27 deletions

View file

@ -49,7 +49,12 @@ cd build
nmake
```
Z3 uses C++20. The recommended version of Visual Studio is therefore VS2019 or later.
Z3 uses C++20. The recommended version of Visual Studio is therefore VS2019 or later.
**Security Features (MSVC)**: When building with Visual Studio/MSVC, a couple of security features are enabled by default for Z3:
- Control Flow Guard (`/guard:cf`) - enabled by default to detect attempts to compromise your code by preventing calls to locations other than function entry points, making it more difficult for attackers to execute arbitrary code through control flow redirection
- Address Space Layout Randomization (`/DYNAMICBASE`) - enabled by default for memory layout randomization, required by the `/GUARD:CF` linker option
- These can be disabled using `python scripts/mk_make.py --no-guardcf` (Python build) or `cmake -DZ3_ENABLE_CFG=OFF` (CMake build) if needed
## Building Z3 using make and GCC/Clang