Skip to content

Conversation

@manastasova
Copy link
Contributor

Change types uint32_t t0, t1; to int32_t t0, t1; due to potential overflow in if (t0 < 9){a[ctr++] = 4 - t0;} causing cbmc proofs to fail.

Issues:

From pq-code-package/mldsa-native#86.

Description of changes:

The output array is of type int32_t* a, thus, uint32_t aux values t0, t1 cause cbmc proofs to fail due to potential overflow.

Testing:

./crypto/crypto_test

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license and the ISC license.

@manastasova manastasova requested a review from a team as a code owner April 2, 2025 00:21
@hanno-becker
Copy link
Contributor

hanno-becker commented Apr 2, 2025

@manastasova Why not include an explicit cast here prior to 2 - t_i and 4 - t_i? The computation of t0,t1 is unsigned, I think, and you would want CBMC to check that it does not underflow.

This PR should wait until the corresponding PR pq-code-package/mldsa-native#86 is merged.

@codecov-commenter
Copy link

codecov-commenter commented Apr 8, 2025

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 78.82%. Comparing base (1ba9056) to head (ecfb6be).

Additional details and impacted files
@@            Coverage Diff             @@
##             main    #2308      +/-   ##
==========================================
- Coverage   78.83%   78.82%   -0.01%     
==========================================
  Files         667      667              
  Lines      114088   114088              
  Branches    16063    16063              
==========================================
- Hits        89940    89935       -5     
- Misses      23374    23380       +6     
+ Partials      774      773       -1     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

@justsmth justsmth requested a review from hanno-becker October 2, 2025 12:17
The resulting array is of type 'int32_t* a', thus, uint32_t aux values t0, t1 cause cbmc proofs to fail due to potentional overflow.
@justsmth justsmth enabled auto-merge (squash) October 2, 2025 12:50
@justsmth justsmth merged commit 154edc9 into aws:main Oct 2, 2025
365 of 369 checks passed
@justsmth justsmth mentioned this pull request Oct 13, 2025
justsmth added a commit that referenced this pull request Oct 13, 2025
### Description of changes: 
Prepare v1.62.0 release

#### What's Changed
* nginx now supports AWS-LC by @samuel40791765 in
#2714
* Fix tests that assume X25519 will be negotiated by @alexw91 in
#2682
* Fixing a bug in ML-DSA poly_uniform function by @dkostic in
#2721
* Migrate integration omnibus by @skmcgrail in
#2715
* Delete util/bot directory by @justsmth in
#2723
* Don't ignore CMAKE_C_FLAGS w/ MSVC by @justsmth in
#2722
* Bump urllib3 from 2.2.3 to 2.5.0 in /tests/ci by @dependabot[bot] in
#2551
* Type fix in mldsa by @manastasova in
#2308
* Centralize password handling tool-openssl by @kingstjo in
#2555
* crypto/pem: replace strncmp with CRYPTO_memcmp to fix -Wstring-compare
error by @R3hankhan123 in #2724
* Implement dgst CLI command by @nhatnghiho in
#2638
* Add ASN.1 decoding for ML-KEM private keys as seeds by @jakemas in
#2707
* Implement genrsa command by @kingstjo in
#2535
* Move udiv and sencond tweak calculations to when needed by @nebeid in
#2726
* Add null check on RSA key checks by @samuel40791765 in
#2727
* Implement workaround for FORTIFY_SOURCE warning with jitterentropy by
@skmcgrail in #2728
* Implement coverity suggestions by @skmcgrail in
#2730
* Add minimal EC CLI tool implementation by @kingstjo in
#2640
* Adding pkeyutl tool to the CLI by @smittals2 in
#2575
* Add CI dimensions for legacy AVX512 flags by @smittals2 in
#2732
* Fix Libwebsockets CI by @smittals2 in
#2737
* Add option ENABLE_SOURCE_MODIFICATION by @justsmth in
#2739
* Simple script to build/run tests by @justsmth in
#2736
* Add build-time option to opt-out of CPU Jitter Entropy by
@torben-hansen in #2733


By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 license and the ISC license.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants