Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use the RelWithDebInfo build type #145

Closed
wants to merge 1 commit into from
Closed

Use the RelWithDebInfo build type #145

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions NSym/scripts/entrypoint_check.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ rm -rf build/
rm -rf build_src/

# Build crypto_test binary for Graviton2
./scripts/build_aarch64.sh "Release" "neoverse-n1"
./scripts/build_aarch64.sh "RelWithDebInfo" "neoverse-n1"
./scripts/post_build.sh

cp -r ./build ./proof/
Expand All @@ -40,7 +40,7 @@ rm -rf build/
rm -rf build_src/

# Build crypto_test binary for Graviton3
./scripts/build_aarch64.sh "Release" "neoverse-512tvb"
./scripts/build_aarch64.sh "RelWithDebInfo" "neoverse-512tvb"
./scripts/post_build.sh

cp -r ./build ./proof/
Expand Down
2 changes: 1 addition & 1 deletion SAW/proof/RSA/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ The caveats associated with the RSA-PSS verification results are defined in the
| --------------| ------------|
| RSA_Blinding | Functions rsa_blinding_get, and rsa_blinding_release are are not verified, and are assumed to get and release a valid blinding factor.
| CRYPTO_MUTEX_Correct | Functions CRYPTO_MUTEX_lock_read, CRYPTO_MUTEX_unlock_read, CRYPTO_MUTEX_lock_write, and CRYPTO_MUTEX_unlock_write are not verified, and are assumed to behave correctly. |
| DebugSettings | The implementation is verified correct using code that is compiled using CMake's `-DCMAKE_BUILD_TYPE=Debug` settings, which does not apply certain optimizations that are used in `-DCMAKE_BUILD_TYPE=Release` settings. |
| DebugSettings | The implementation is verified correct using code that is compiled using CMake's `-DCMAKE_BUILD_TYPE=Debug` settings, which does not apply certain optimizations that are used in `-DCMAKE_BUILD_TYPE=RelWithDebInfo` settings. |

The EVP_DigestSign*/EVP_DigestVerify* functions are verified to have the following properties related to RSA-PSS with SHA-384. For more detailed specifications, see [evp-function-specs.saw](evp-function-specs.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. KEY_SIZE is the RSA key size, in bytes. For RSA-PSS-1024 with SHA-384, BLOCK_LENGTH is 64 and KEY_SIZE is 128.

Expand Down
2 changes: 1 addition & 1 deletion SAW/scripts/aarch64/entrypoint_check.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,6 @@ go env -w GOPROXY=direct

# The following warning seems like a bug in wllvm and are benign
# WARNING:Did not recognize the compiler flag "--target=aarch64-unknown-linux-gnu"
./scripts/aarch64/build_llvm.sh "Release"
./scripts/aarch64/build_llvm.sh "RelWithDebInfo"
./scripts/aarch64/post_build.sh
./scripts/aarch64/run_checks.sh
6 changes: 3 additions & 3 deletions SAW/scripts/x86_64/entrypoint_check.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ apply_patch "p384_validate"

# Build in release mode

./scripts/x86_64/build_llvm.sh "Release"
./scripts/x86_64/build_llvm.sh "RelWithDebInfo"
mkdir -p build/llvm_x86/crypto build/x86/crypto
cp build_src/llvm_x86/crypto/crypto_test build/llvm_x86/crypto/crypto_test
extract-bc build/llvm_x86/crypto/crypto_test
Expand Down Expand Up @@ -70,8 +70,8 @@ apply_patch "noinline_ec_GFp_simple_is_at_infinity"

# Check the proofs using CMake's Release settings...

./scripts/x86_64/build_x86.sh "Release"
./scripts/x86_64/build_llvm.sh "Release"
./scripts/x86_64/build_x86.sh "RelWithDebInfo"
./scripts/x86_64/build_llvm.sh "RelWithDebInfo"
./scripts/x86_64/post_build.sh
./scripts/x86_64/run_checks_release.sh

Expand Down
Loading