Hardening

.github/workflows/ci.yml

@@ -13,42 +13,87 @@
       - develop
 
 jobs:
+  unit-tests:
+    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:
+    name: Formal verification (Frama-C)
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+
+      - name: Pull Frama-C image
+        run: docker pull framac/frama-c:30.0
+
+      - name: Run WP + Eva
+        run: |
+          chmod +x formal/verify.sh
+          docker run --rm -v "$PWD":/work -w /work framac/frama-c:30.0 \
+            ./formal/verify.sh
+
   build:
+    name: Cross-build (riscv64)
     runs-on: ubuntu-latest
 
     steps:
       - name: Checkout code
         uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
         uses: docker/setup-buildx-action@v3
 
       - name: Build with Docker
         run: |
           chmod +x build.sh
           ./build.sh docker
 
       - name: Verify build artifacts
         run: |
           if [ -f "build/usr/lib/libugc-zero.a" ]; then
             echo "✅ Build successful: libugc-zero.a created"
             ls -lh build/usr/lib/libugc-zero.a
             file build/usr/lib/libugc-zero.a
           else
             echo "❌ Build failed: libugc-zero.a not found"
             exit 1
           fi
 
       - name: Check object files
         run: |
           echo "Checking object files..."
-          ls -lh build/usr/lib/objects/ugc-zero/
+          find build/usr/lib/objects/ugc-zero -name '*.obj' | tee objects.txt
+          test -s objects.txt
 
       - name: Upload artifacts
         uses: actions/upload-artifact@v4
         with:
           name: ugc-riscv64-build
           path: |
             build/usr/lib/libugc-zero.a
-            build/usr/lib/objects/ugc-zero/*
-          retention-days: 7
+            build/usr/lib/objects/ugc-zero/**
+          retention-days: 7

.github/workflows/release.yml

@@ -62,7 +62,7 @@ jobs:
           prerelease: false
           files: |
             build/usr/lib/libugc-zero.a
-            build/usr/lib/objects/ugc-zero/*.obj
+            build/usr/lib/objects/ugc-zero/**/*.obj
             ugc-riscv64.tar.gz
           body: |
             ## uGC Release ${{ steps.version.outputs.version }}
@@ -71,7 +71,7 @@ jobs:
 
             ### Files
             - `libugc-zero.a` - Static library
-            - `*.obj` - Individual object files (uGC.cpp.obj, uGCHandleManager.cpp.obj, uGCHandleStore.cpp.obj, uGCHeap.cpp.obj)
+            - `*.obj` - Individual object files (C++ wrappers and the formally verified C core)
             - `ugc-riscv64.tar.gz` - Complete archive with library and object files
 
             ### Usage

.gitignore

@@ -41,4 +41,6 @@
 *.dwo
 
 /build
+/build-tests
 .DS_Store
+/.frama-c

CMakeLists.txt

@@ -2,4 +2,17 @@ cmake_minimum_required(VERSION 3.20)
 
 project(ugc)
 
-add_subdirectory(ugc)
+option(UGC_BUILD_TESTS "Build uGC core unit tests" OFF)
+
+# The ugc-zero library needs the .NET runtime headers; skip it when they are
+# not provided (e.g. host-only unit-test builds).
+if(DEFINED UGC_RUNTIME_INCLUDE_DIR)
+    add_subdirectory(ugc)
+else()
+    message(STATUS "UGC_RUNTIME_INCLUDE_DIR not set - skipping ugc-zero library")
+endif()
+
+if(UGC_BUILD_TESTS)
+    enable_testing()
+    add_subdirectory(tests)
+endif()

README.md

@@ -15,6 +15,8 @@ This is a custom GC implementation designed to be used with [Nethermind's **bfla
 - Zero-dependency static library
 - Minimal overhead and memory footprint
 - No actual free() implementation
+- Core logic (allocation, handle store) implemented in plain C with ACSL
+  contracts, formally verified with Frama-C (WP + Eva)
 
 ## Building
 
@@ -45,6 +47,41 @@ Then run:
 ./build.sh
 ```
 
+## Architecture
+
+All non-trivial logic lives in `ugc/core/` as dependency-free C11 code with
+ACSL specifications (`ugc_core.h`). The C++ classes implementing the CLR GC
+interface (`uGCHeap`, `uGCHandleStore`, `uGCHandleManager`) are thin wrappers
+over that core.
+
+## Testing
+
+Unit tests cover the core allocator and handle store and run on the host
+(no .NET runtime headers required):
+
+```bash
+cmake -S . -B build-tests -DUGC_BUILD_TESTS=ON -DCMAKE_BUILD_TYPE=Debug
+cmake --build build-tests
+ctest --test-dir build-tests --output-on-failure
+```
+
+## Formal Verification
+
+The ACSL contracts of the core are verified with [Frama-C](https://frama-c.com):
+
+- **WP** proves every contract (with runtime-error guards) deductively;
+- **Eva** checks the absence of undefined behavior on a driver that
+  exercises the core with unconstrained inputs.
+
+Run the whole gate locally (requires Docker):
+
+```bash
+docker run --rm -v "$PWD":/work -w /work framac/frama-c:30.0 ./formal/verify.sh
+```
+
+CI fails if a single proof obligation is not discharged or Eva reports any
+alarm.
+
 ## License
 
 This project is licensed under the terms of MIT license.

build.sh

@@ -37,7 +37,7 @@ pushd "${TOP_DIR}"
         file="usr/lib/libugc-zero.a"
         printf '\x00' | dd of="$file" bs=1 seek=$((0x30)) count=1 conv=notrunc
         pushd usr/lib/objects/ugc-zero
-            for file in  uGC.cpp.obj uGCHandleManager.cpp.obj uGCHandleStore.cpp.obj uGCHeap.cpp.obj ; do
+            for file in $(find . -name '*.obj') ; do
                 printf '\x00' | dd of="$file" bs=1 seek=$((0x30)) count=1 conv=notrunc
             done
         popd

formal/eva_main.c

@@ -0,0 +1,89 @@
+/**
+ * @file
+ * @brief uGC - Frama-C/Eva driver: exercises the core with unconstrained
+ *        inputs to verify absence of runtime errors (undefined behavior)
+ *
+ * This file is only compiled by Frama-C (formal/verify.sh); it is not part
+ * of the production library or the unit tests.
+ *
+ * Copyright (C) 2026 Demerzel Solutions Limited (Nethermind)
+ *
+ * @author Maxim Menshikov <maksim.menshikov@nethermind.io>
+ */
+#include "ugc_core.h"
+#include "__fc_builtin.h"
+
+static int object_a, object_b;
+
+int
+main(void)
+{
+    /* --- Allocation: no context, arbitrary size (overflow + direct) --- */
+    size_t size = Frama_C_size_t_interval(0, SIZE_MAX);
+    (void)ugc_core_alloc((uint8_t **)0, (uint8_t **)0, size, false, 8);
+
+    /* --- Allocation: context paths (refill, then bump / direct) --- */
+    uint8_t *alloc_ptr = (uint8_t *)0;
+    uint8_t *alloc_limit = (uint8_t *)0;
+    size_t s1 = Frama_C_size_t_interval(0, 2 * UGC_ALLOC_QUANTUM);
+    size_t s2 = Frama_C_size_t_interval(0, 2 * UGC_ALLOC_QUANTUM);
+    bool bypass = Frama_C_interval(0, 1);
+
+    (void)ugc_core_alloc(&alloc_ptr, &alloc_limit, s1, false, 8);
+
+    /* Re-establish the context invariant for the non-relational domain:
+     * at runtime alloc_ptr/alloc_limit are either both null or both point
+     * into the same quantum (the context_window precondition). */
+    if (alloc_ptr == (uint8_t *)0 || alloc_limit == (uint8_t *)0)
+    {
+        alloc_ptr = (uint8_t *)0;
+        alloc_limit = (uint8_t *)0;
+    }
+    (void)ugc_core_alloc(&alloc_ptr, &alloc_limit, s2, bypass, 8);
+
+    /* --- Handle store: creation up to exhaustion --- */
+    ugc_handle_store_reset();
+
+    void **h1 = ugc_handle_create(&object_a, Frama_C_interval(0, 12));
+    void **h2 = ugc_handle_create_with_extra(&object_a,
+        Frama_C_interval(0, 12), &object_b);
+    void **h3 = ugc_handle_create_dependent(&object_a, &object_b,
+        Frama_C_interval(0, 12));
+
+    if (h1 != (void **)0)
+    {
+        (void)ugc_handle_store_contains(h1);
+        (void)ugc_handle_index(h1);
+
+        /* --- Destroy + recycle: double destroy must be harmless --- */
+        ugc_handle_destroy_at(ugc_handle_index(h1));
+        ugc_handle_destroy_at(ugc_handle_index(h1));
+        h1 = ugc_handle_create(&object_b, Frama_C_interval(0, 12));
+    }
+    (void)ugc_handle_store_contains(&object_a);
+    (void)ugc_handle_store_contains((const void *)0);
+
+    /* --- Handle accessors over the whole index range --- */
+    size_t idx = Frama_C_size_t_interval(0, UGC_HANDLE_COUNT - 1);
+    ugc_handle_set_type_at(idx, Frama_C_interval(0, 12));
+    (void)ugc_handle_get_type_at(idx);
+    ugc_handle_set_extra_at(idx, &object_b);
+    (void)ugc_handle_get_extra_at(idx);
+    ugc_handle_set_dependent_at(idx, &object_b);
+    (void)ugc_handle_dependent_slot_at(idx);
+
+    /* --- Handle slot operations --- */
+    if (h2 != (void **)0)
+    {
+        ugc_handle_slot_store(h2, &object_b);
+        (void)ugc_handle_slot_store_if_null(h2, &object_a);
+        (void)ugc_handle_slot_cas(h2, &object_a, &object_b);
+    }
+    if (h3 != (void **)0)
+    {
+        (void)ugc_handle_slot_store_if_null(h3, &object_a);
+    }
+
+    ugc_handle_store_reset();
+    return 0;
+}

formal/verify.sh

@@ -0,0 +1,68 @@
+#!/usr/bin/env bash
+# uGC formal verification gate (Frama-C).
+#
+# Runs two analyses over the formally specified core (ugc/core):
+#   1. WP  - deductive proof of the ACSL contracts (with RTE guards);
+#      fails unless every goal is discharged.
+#   2. Eva - value analysis of formal/eva_main.c driver; fails if any
+#      alarm (potential undefined behavior) is reported.
+#
+# Usage: ./formal/verify.sh
+#   FRAMAC=<frama-c binary>  (default: frama-c)
+#   WP_TIMEOUT=<seconds per goal>  (default: 60)
+#
+# Copyright (C) 2026 Demerzel Solutions Limited (Nethermind)
+# Author: Maxim Menshikov <maksim.menshikov@nethermind.io>
+
+set -uo pipefail
+
+cd "$(dirname "$0")/.."
+
+FRAMAC="${FRAMAC:-frama-c}"
+WP_TIMEOUT="${WP_TIMEOUT:-60}"
+NPROC="$(nproc 2>/dev/null || echo 4)"
+
+fail=0
+
+echo "=== WP: deductive verification of ACSL contracts ==="
+wp_out=$("$FRAMAC" -wp -wp-rte \
+    -wp-timeout "$WP_TIMEOUT" -wp-par "$NPROC" \
+    ugc/core/ugc_core.c 2>&1)
+wp_status=$?
+echo "$wp_out" | grep -E "Proved goals|Qed:|Alt-Ergo|Timeout|Failed|Unknown" \
+    | head -20
+
+proved=$(echo "$wp_out" \
+    | sed -n 's/.*Proved goals:[[:space:]]*\([0-9][0-9]*\)[[:space:]]*\/[[:space:]]*\([0-9][0-9]*\).*/\1 \2/p')
+ok=$(echo "$proved" | awk '{print $1}')
+total=$(echo "$proved" | awk '{print $2}')
+
+if [ "$wp_status" -ne 0 ] || [ -z "$ok" ] || [ -z "$total" ] || \
+   [ "$ok" != "$total" ] || [ "$total" = "0" ]; then
+    echo "WP: FAILED (proved ${ok:-?}/${total:-?} goals)" >&2
+    fail=1
+else
+    echo "WP: OK - all $total goals proved"
+fi
+
+echo ""
+echo "=== Eva: absence of runtime errors ==="
+eva_out=$("$FRAMAC" -eva -eva-precision 2 \
+    formal/eva_main.c ugc/core/ugc_core.c ugc/core/ugc_zalloc.c \
+    -cpp-extra-args=-Iugc/core 2>&1)
+eva_status=$?
+echo "$eva_out" | grep -E "alarm|invalid|coverage|Assertions|Preconditions" \
+    | head -20
+
+if [ "$eva_status" -ne 0 ] || \
+   ! echo "$eva_out" | grep -q "0 alarms generated by the analysis"; then
+    echo "Eva: FAILED (alarms or analysis error)" >&2
+    fail=1
+elif echo "$eva_out" | grep -qE "[1-9][0-9]* invalid"; then
+    echo "Eva: FAILED (invalid logical properties)" >&2
+    fail=1
+else
+    echo "Eva: OK - no alarms"
+fi
+
+exit $fail

tests/CMakeLists.txt

@@ -0,0 +1,18 @@
+# uGC unit tests
+#
+# Copyright (C) 2026 Demerzel Solutions Limited (Nethermind)
+# Author: Maxim Menshikov <maksim.menshikov@nethermind.io>
+
+add_library(ugc-core-host
+            STATIC
+            ${CMAKE_CURRENT_SOURCE_DIR}/../ugc/core/ugc_core.c
+            ${CMAKE_CURRENT_SOURCE_DIR}/../ugc/core/ugc_zalloc.c)
+target_include_directories(ugc-core-host
+                           PUBLIC
+                           ${CMAKE_CURRENT_SOURCE_DIR}/../ugc/core)
+
+foreach(test test_core_alloc test_core_handles)
+    add_executable(${test} ${test}.c)
+    target_link_libraries(${test} PRIVATE ugc-core-host)
+    add_test(NAME ${test} COMMAND ${test})
+endforeach()