Hardening - #2
Merged
Merged
Conversation
Move all non-trivial uGC logic into plain C (ugc_core.c, ugc_zalloc.c) with ACSL contracts so Frama-C can verify it with WP and Eva; the C++ classes uGCHeap, uGCHandleStore and uGCHandleManager become thin wrappers over these functions. The zeroing allocator lives in its own translation unit so the core is verified against its contract only. Update build.sh and release.yml to pick up object files from the new subdirectory. Signed-off-by: Maxim Menshikov <maksim.menshikov@nethermind.io>
Add a dependency-free test harness and CTest-driven suites covering the bump allocator (refill, exact fit, overflow, bypass) and the handle store (creation variants, dependent slots, exhaustion, slot CAS). The top-level CMakeLists gains a UGC_BUILD_TESTS option and skips the ugc-zero library when UGC_RUNTIME_INCLUDE_DIR is not set, enabling host-only test builds. Signed-off-by: Maxim Menshikov <maksim.menshikov@nethermind.io>
Add verify.sh, which proves the ACSL contracts of ugc/core with WP (failing unless every goal is discharged) and runs Eva value analysis to check for absence of runtime errors. Add eva_main.c, a Frama-C-only driver that exercises allocation, handle store, and slot operations with unconstrained inputs. Signed-off-by: Maxim Menshikov <maksim.menshikov@nethermind.io>
Run unit tests on ubuntu with no sanitizer, ASan, and UBSan, and run the Frama-C WP + Eva gate in a docker container alongside the riscv64 cross-build. Harden the object-file check to fail when no .obj files are produced, and ignore the build-tests and .frama-c directories. Signed-off-by: Maxim Menshikov <maksim.menshikov@nethermind.io>
Describe the ACSL-specified C core, host-side unit tests, and the Frama-C verification gate (WP + Eva) added in recent commits, including local run instructions via Docker. Signed-off-by: Maxim Menshikov <maksim.menshikov@nethermind.io>
Ship a prebuilt uGC archive for the riscv64 architecture so the library can be deployed on RISC-V targets without building from source. Signed-off-by: Maxim Menshikov <maksim.menshikov@nethermind.io>
Handle slots were never reclaimed, so runtime GCHandle churn would exhaust the fixed-capacity store. Add ugc_handle_destroy_at, which scrubs the slot, guards against double destroy, and pushes the index on a free stack popped before the array grows; wire it into the manager's destroy paths, give dependent handles a HandleType, and extend the ACSL contracts, unit tests, and Eva harness. Signed-off-by: Maxim Menshikov <maksim.menshikov@nethermind.io>
Count bytes served by the slow-path Alloc (including per-context SOH/UOH counters) and report them from GetTotalAllocatedBytes, GetTotalBytesInUse, GetCurrentObjSize and GetMemoryInfo. Correct stub returns the BCL depends on: MaxGeneration is 2, RegisterForFinalization and IsPromoted succeed, WaitForFullGC* report not-applicable, and GetLOHThreshold reports the standard large-object threshold. Signed-off-by: Maxim Menshikov <maksim.menshikov@nethermind.io>
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
Comment on lines
+17
to
+42
| name: Unit tests (${{ matrix.sanitizer }}) | ||
| runs-on: ubuntu-latest | ||
| strategy: | ||
| fail-fast: false | ||
| matrix: | ||
| sanitizer: [none, address, undefined] | ||
|
|
||
| steps: | ||
| - name: Checkout code | ||
| uses: actions/checkout@v4 | ||
|
|
||
| - name: Configure | ||
| run: | | ||
| if [ "${{ matrix.sanitizer }}" != "none" ]; then | ||
| export CFLAGS="-fsanitize=${{ matrix.sanitizer }} -fno-sanitize-recover=all -g" | ||
| export LDFLAGS="-fsanitize=${{ matrix.sanitizer }}" | ||
| fi | ||
| cmake -S . -B build-tests -DUGC_BUILD_TESTS=ON -DCMAKE_BUILD_TYPE=Debug | ||
|
|
||
| - name: Build | ||
| run: cmake --build build-tests | ||
|
|
||
| - name: Run tests | ||
| run: ctest --test-dir build-tests --output-on-failure | ||
|
|
||
| formal-verification: |
Comment on lines
60
to
99
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.