Conversation
![cubic-dev-ai[bot]](https://avatars.github.com/in/1082092?s=60&v=4){kind=small}
There was a problem hiding this comment.
6 issues found across 14 files
Prompt for AI agents (unresolved issues)
Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.
<file name="scripts/check-acsl-coverage.py">
<violation number="1" location="scripts/check-acsl-coverage.py:48">
P2: Functions with a leading GCC/Clang attribute are rejected as unattributable even though they are valid C definitions; this repository already uses `__attribute__` in its C sources. Accept leading attributes (or use a C-aware parser) before matching the function header so adding such an attribute cannot break ACSL coverage.</violation>
<violation number="2" location="scripts/check-acsl-coverage.py:72">
P2: Disabled preprocessor branches are treated as live contracts, so configuration-specific or `#if 0` code can fail the verification gate even though Frama-C never analyzes it. Scanning the preprocessed source, or applying the same preprocessor conditions before coverage matching, would keep this check aligned with the proof input.</violation>
</file>
<file name="src/core/elf.c">
<violation number="1" location="src/core/elf.c:489">
P2: Path-based bootstrap loads can still consume bytes from a different file than the one parsed: `elf_load(path)` closes its descriptor, then `elf_map_segments(path)` reopens the path while this loop trusts the old metadata. Keeping the parse descriptor open through mapping, or validating the opened descriptor against the parsed image, would preserve the intended single-image guarantee.</violation>
</file>
<file name="scripts/check-wp-result.py">
<violation number="1" location="scripts/check-wp-result.py:115">
P3: When a proof leaves obligations open, the SUFFIX_KEY banner always says 'Each open obligation named above...', but the actual 'open:' lines are only emitted for lines that match the very specific OPEN_GOAL regex (exact [wp] [Timeout|Stepout|Unknown|Failed] prefix, a fixed list of model prefixes, and a short unanchored name token). If Frama-C's goal line format drifts or a goal name doesn't match, the printed output shows the banner with nothing above it, which makes the failure output misleading when the gate is tripped. Consider counting how many open-goal lines were actually printed and only printing the SUFFIX_KEY guidance when that count is non-zero (or fall back to printing a raw excerpt of the unproved lines), so the failure output stays self-consistent regardless of Frama-C output format.</violation>
</file>
<file name="src/core/guest.c">
<violation number="1" location="src/core/guest.c:1484">
P3: The new `if (region_end <= cur.gpa) break;` in `gva_contiguous_avail` only prevents calling `gva_chunk_clamp` with a violated `gpa < region_end` precondition; the comment claims this makes the guest-copy spin 'structural rather than argued', but the break doesn't deliver that guarantee for the extra-mapping/overflow branch. There, `gva_resolve_perm` returns a non-NULL pointer straight from `gva_contiguous_avail` (no primary-buffer clamp), so if the guard ever fired with `total == 0`, `*avail` would be 0 and `guest_copy` would advance by 0 and loop forever (it has no `if (avail == 0) return -1;` check). Since the preconditions are asserted (not enforced) unreachable, this is a robustness/comment-accuracy note rather than a reachable bug. Consider either wording the comment to only claim the clamp-underflow avoidance, or adding an `avail == 0` guard in `guest_copy` so the invariant is actually structural.</violation>
</file>
<file name="tests/test-fuse-basic.c">
<violation number="1" location="tests/test-fuse-basic.c:725">
P3: This regression test only detects an overrun (count > 16 and guards intact), but never asserts that the read returned the full 16 requested bytes or that the delivered body is the 0xA5 flood fill. A change that truncates the read to fewer than `count` bytes, or fails to deliver the daemon's payload, would pass silently even though read(2) semantics would be wrong. Also, the lead canary cannot detect a forward spill (guest_write only writes forward from `body`), so the 'catch a spill in either direction' comment overstates its role. Consider asserting `over_rc == (ssize_t) sizeof(guarded.body)` and checking `guarded.body` is filled with `OVER_REPLY_FILL` to make the test validate the delivered content, not just the absence of overrun.</violation>
</file>
Reply with feedback, questions, or to request a fix.
Re-trigger cubic
| "%d of %d proof obligations discharged, %d left open" | ||
| % (proved, total, total - proved) | ||
| ) | ||
| print(SUFFIX_KEY) |
There was a problem hiding this comment.
P3: When a proof leaves obligations open, the SUFFIX_KEY banner always says 'Each open obligation named above...', but the actual 'open:' lines are only emitted for lines that match the very specific OPEN_GOAL regex (exact [wp] [Timeout|Stepout|Unknown|Failed] prefix, a fixed list of model prefixes, and a short unanchored name token). If Frama-C's goal line format drifts or a goal name doesn't match, the printed output shows the banner with nothing above it, which makes the failure output misleading when the gate is tripped. Consider counting how many open-goal lines were actually printed and only printing the SUFFIX_KEY guidance when that count is non-zero (or fall back to printing a raw excerpt of the unproved lines), so the failure output stays self-consistent regardless of Frama-C output format.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At scripts/check-wp-result.py, line 115:
<comment>When a proof leaves obligations open, the SUFFIX_KEY banner always says 'Each open obligation named above...', but the actual 'open:' lines are only emitted for lines that match the very specific OPEN_GOAL regex (exact [wp] [Timeout|Stepout|Unknown|Failed] prefix, a fixed list of model prefixes, and a short unanchored name token). If Frama-C's goal line format drifts or a goal name doesn't match, the printed output shows the banner with nothing above it, which makes the failure output misleading when the gate is tripped. Consider counting how many open-goal lines were actually printed and only printing the SUFFIX_KEY guidance when that count is non-zero (or fall back to printing a raw excerpt of the unproved lines), so the failure output stays self-consistent regardless of Frama-C output format.</comment>
<file context>
@@ -0,0 +1,156 @@
+ "%d of %d proof obligations discharged, %d left open"
+ % (proved, total, total - proved)
+ )
+ print(SUFFIX_KEY)
+ print(" Full prover output: %s" % log_path)
+ return rc
</file context>
| * guest-supplied address. Every path that reaches here satisfies it | ||
| * today; this makes that structural rather than argued. | ||
| */ | ||
| if (region_end <= cur.gpa) |
There was a problem hiding this comment.
P3: The new if (region_end <= cur.gpa) break; in gva_contiguous_avail only prevents calling gva_chunk_clamp with a violated gpa < region_end precondition; the comment claims this makes the guest-copy spin 'structural rather than argued', but the break doesn't deliver that guarantee for the extra-mapping/overflow branch. There, gva_resolve_perm returns a non-NULL pointer straight from gva_contiguous_avail (no primary-buffer clamp), so if the guard ever fired with total == 0, *avail would be 0 and guest_copy would advance by 0 and loop forever (it has no if (avail == 0) return -1; check). Since the preconditions are asserted (not enforced) unreachable, this is a robustness/comment-accuracy note rather than a reachable bug. Consider either wording the comment to only claim the clamp-underflow avoidance, or adding an avail == 0 guard in guest_copy so the invariant is actually structural.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At src/core/guest.c, line 1484:
<comment>The new `if (region_end <= cur.gpa) break;` in `gva_contiguous_avail` only prevents calling `gva_chunk_clamp` with a violated `gpa < region_end` precondition; the comment claims this makes the guest-copy spin 'structural rather than argued', but the break doesn't deliver that guarantee for the extra-mapping/overflow branch. There, `gva_resolve_perm` returns a non-NULL pointer straight from `gva_contiguous_avail` (no primary-buffer clamp), so if the guard ever fired with `total == 0`, `*avail` would be 0 and `guest_copy` would advance by 0 and loop forever (it has no `if (avail == 0) return -1;` check). Since the preconditions are asserted (not enforced) unreachable, this is a robustness/comment-accuracy note rather than a reachable bug. Consider either wording the comment to only claim the clamp-underflow avoidance, or adding an `avail == 0` guard in `guest_copy` so the invariant is actually structural.</comment>
<file context>
@@ -1445,10 +1473,18 @@ static uint64_t gva_contiguous_avail(const guest_t *g,
+ * guest-supplied address. Every path that reaches here satisfies it
+ * today; this makes that structural rather than argued.
+ */
+ if (region_end <= cur.gpa)
+ break;
+
</file context>
| ctx.over_reply_read = 0; | ||
| if (over_rc < 0) | ||
| die("read(over-replying fuse file)"); | ||
| if ((size_t) over_rc > sizeof(guarded.body)) { |
There was a problem hiding this comment.
P3: This regression test only detects an overrun (count > 16 and guards intact), but never asserts that the read returned the full 16 requested bytes or that the delivered body is the 0xA5 flood fill. A change that truncates the read to fewer than count bytes, or fails to deliver the daemon's payload, would pass silently even though read(2) semantics would be wrong. Also, the lead canary cannot detect a forward spill (guest_write only writes forward from body), so the 'catch a spill in either direction' comment overstates its role. Consider asserting over_rc == (ssize_t) sizeof(guarded.body) and checking guarded.body is filled with OVER_REPLY_FILL to make the test validate the delivered content, not just the absence of overrun.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At tests/test-fuse-basic.c, line 725:
<comment>This regression test only detects an overrun (count > 16 and guards intact), but never asserts that the read returned the full 16 requested bytes or that the delivered body is the 0xA5 flood fill. A change that truncates the read to fewer than `count` bytes, or fails to deliver the daemon's payload, would pass silently even though read(2) semantics would be wrong. Also, the lead canary cannot detect a forward spill (guest_write only writes forward from `body`), so the 'catch a spill in either direction' comment overstates its role. Consider asserting `over_rc == (ssize_t) sizeof(guarded.body)` and checking `guarded.body` is filled with `OVER_REPLY_FILL` to make the test validate the delivered content, not just the absence of overrun.</comment>
<file context>
@@ -681,6 +704,42 @@ int main(void)
+ ctx.over_reply_read = 0;
+ if (over_rc < 0)
+ die("read(over-replying fuse file)");
+ if ((size_t) over_rc > sizeof(guarded.body)) {
+ fprintf(stderr, "read returned %zd for a %zu-byte request\n", over_rc,
+ sizeof(guarded.body));
</file context>
There was a problem hiding this comment.
1 issue found across 12 files (changes from recent commits).
Prompt for AI agents (unresolved issues)
Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.
<file name=".inferconfig">
<violation number="1" location=".inferconfig:2">
P2: This .inferconfig disables the PULSE_UNINITIALIZED_VALUE checker for the entire project, not just the one false-positive path. The workflow comment documents that 135 findings were audited and all callers check the return value, but that audit only holds for the current snapshot; any genuinely uninitialized read introduced anywhere in the codebase after this merge will no longer be caught by the gating Infer step. Consider a more surgical scope instead of a global disable — for example a file/pattern-scoped suppression in .inferconfig or per-function suppression near the chunked-copy path — so the rest of the codebase keeps this memory-safety check. If a global disable is intentional, tracking it in an issue with a follow-up trigger (e.g. when Infer models chunked copies, per the workflow comment) would make the residual risk explicit.</violation>
</file>
Tip: Review your code locally with the cubic CLI to iterate faster.
Re-trigger cubic
| @@ -0,0 +1,3 @@ | |||
| { | |||
| "disable-issue-type": ["PULSE_UNINITIALIZED_VALUE"] | |||
There was a problem hiding this comment.
P2: This .inferconfig disables the PULSE_UNINITIALIZED_VALUE checker for the entire project, not just the one false-positive path. The workflow comment documents that 135 findings were audited and all callers check the return value, but that audit only holds for the current snapshot; any genuinely uninitialized read introduced anywhere in the codebase after this merge will no longer be caught by the gating Infer step. Consider a more surgical scope instead of a global disable — for example a file/pattern-scoped suppression in .inferconfig or per-function suppression near the chunked-copy path — so the rest of the codebase keeps this memory-safety check. If a global disable is intentional, tracking it in an issue with a follow-up trigger (e.g. when Infer models chunked copies, per the workflow comment) would make the residual risk explicit.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At .inferconfig, line 2:
<comment>This .inferconfig disables the PULSE_UNINITIALIZED_VALUE checker for the entire project, not just the one false-positive path. The workflow comment documents that 135 findings were audited and all callers check the return value, but that audit only holds for the current snapshot; any genuinely uninitialized read introduced anywhere in the codebase after this merge will no longer be caught by the gating Infer step. Consider a more surgical scope instead of a global disable — for example a file/pattern-scoped suppression in .inferconfig or per-function suppression near the chunked-copy path — so the rest of the codebase keeps this memory-safety check. If a global disable is intentional, tracking it in an issue with a follow-up trigger (e.g. when Infer models chunked copies, per the workflow comment) would make the residual risk explicit.</comment>
<file context>
@@ -0,0 +1,3 @@
+{
+ "disable-issue-type": ["PULSE_UNINITIALIZED_VALUE"]
+}
</file context>
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
fuse_read_common asked the daemon for min(count, max_write) bytes and then wrote reply_len bytes into the guest buffer with no clamp back to count. reply_len is bounded only by FUSE_FRAME_CAP (8 MiB) in fuse_dev_write, so a guest process serving a FUSE mount could answer a 16-byte read with a multi-megabyte payload and overrun the reader's buffer. Linux sizes the copy from the request rather than the reply, so this was a divergence as well: read(2) returned more than count, and file->offset advanced past what had been delivered. Not a host escape. guest_write routes through gva_resolve_perm, so the write stayed inside the guest slab and honored page permissions. What it was is a cross-process memory-corruption primitive inside the guest that the kernel does not offer: mounting a FUSE filesystem let the daemon smash the memory of any process reading it. The sibling paths already got this right, which is why one site was easy to miss. getdents64 checks dst + lreclen > count per entry, fuse_dev_read rejects count < frame_len, fuse_dev_write bounds the header against both count and sizeof(hdr), and the three reply consumers that cast to a struct all check reply_len before the cast. tests/test-fuse-basic.c gains an over_reply_read mode that answers a small FUSE_READ with a 4080-byte flood while the reader issues a 16-byte read into a canary-guarded buffer. Verified to fail without the clamp, reporting "read returned 4080 for a 16-byte request", and to pass with it.
Everything the RSP stub parses comes from whoever connects to --gdb. Five client-reachable defects, all reads. handle_vcont advanced with "char action = *p++", so a payload ending in ';' consumed the NUL and the following "*p == ':'" read one byte past it. gdb_rsp_recv accepts payloads up to bufsz - 1 and writes the terminator at the last byte, so that read leaves the 128 KiB allocation. Reproduced under ASAN with a 131071-byte payload: heap-buffer-overflow READ of size 1, 0 bytes after a 131072-byte region. A malformed trailing ';' now returns an RSP error rather than falling out of the loop, which resumed every stopped thread and let invalid debugger input change execution state. handle_set_thread took op = pkt[0] and started p at pkt + 1 without checking for the terminator, so a bare "$H#XX" parsed whatever followed the packet as a thread id. gdb_hex_decode read both nibbles in one declaration, evaluating the second before testing the first, so a NUL on an even index caused a read one byte past it. The digits are read in order with a return between them now. Handing both to a helper does not work: C evaluates both arguments before the call, which is the same overread. handle_write_mem passed the M packet's length field straight to gdb_hex_decode, which needs 2*len readable digits, with nothing checking that many follow the ':'. A short payload walked the decoder past the packet buffer. The checksum compare was undefined behavior on any non-hex input: it decoded the trailing byte as (hex_nibble(hi) << 4) | hex_nibble(lo), and hex_nibble returns -1 for a non-digit, so "$x#zz" left-shifted a negative int. Both nibbles are validated before either is shifted, in unsigned arithmetic, and a malformed checksum is treated as a mismatch. gdb_rsp_recv requires bufsz >= 2 so the bare 0x03 (Ctrl+C) reply can be NUL-terminated like every other packet it returns; its one caller passes GDB_PKT_BUF_SIZE. tests/test-gdbstub.sh stays 17/17.
elf_map_segments_fd re-reads and re-parses the program header table, and its guard was weaker than the one in elf_load_fd: it checked only the product e_phnum * e_phentsize against 64KiB, never e_phentsize itself. The walk then advanced by e_phentsize while reading sizeof(elf64_phdr_t) bytes, so e_phentsize=1 with e_phnum=64 read 56 bytes from offset 63 of a 64-byte allocation, 55 bytes past the end. The two parses are of a file that can change between them, so the second cannot inherit the first one's validation: elfuse has no ETXTBSY, and elf_map_segments re-opens by path. Both sites now share elf_phdr_table_bytes, which rejects an empty table, a stride too small to hold a program header, and a total past the kernel's cap, and elf_phdr_fetch, which refuses an entry that does not lie wholly inside the buffer. The fetch copies rather than aliasing a struct pointer into the buffer: e_phentsize is attacker controlled and need not be a multiple of the program header alignment, so the old cast was unaligned access on a hostile input.
A PT_LOAD whose p_vaddr + p_memsz overflows 64 bits was saturated to UINT64_MAX and recorded. The clamp does not contain the problem, it relocates it: every consumer of load_max adds a load base before comparing against guest_size, so exec.c computes load_max + elf_load_base, which wraps to a small value and passes "ELF extends beyond guest address space" -- the exact check the saturation was meant to feed. Such a segment is unloadable under any base, so the parse now rejects it. elf_add_no_wrap is the checked add the rest of the parser will use for the other address it derives from unconstrained ELF fields.
The mapper already skips a PT_LOAD with p_memsz == 0, matching Linux, but the parse recorded it, and the record is what feeds load_min/load_max, the boot region tables and /proc/self/maps. A zero-memsz segment placed at p_vaddr == guest_size passes the mapper's extent bound (gpa > guest_size - memsz is false when memsz is 0), so load_max reaches the end of the slab and brk_base follows it there. Drop the segment at the parse instead, where every consumer sees the same decision.
phdr_gpa was load_min + e_phoff, an address that need not lie in any segment, and elf_map_segments_fd then memcpy'd the header table there to make AT_PHDR point at something real. For build/test-hello that copy landed 0x1a bytes past the end of .text. Linux 5.19+ (commit 0da1d5002745) derives AT_PHDR from the PT_LOAD whose file data contains e_phoff, which is the only reason the headers are visible to the guest at all. Doing the same makes the separate copy unnecessary: the covering segment's own file read delivers the table, so there is no second destination to bound-check and no way for the copy to land outside a mapping. Verified equivalent to the old formula on 1203 ELF64 binaries from the test fixtures and the Alpine sysroots: zero divergences. Requiring the whole table inside one segment is stricter than Linux, which only requires e_phoff itself to be covered. Linux can afford the weaker condition because it keeps the headers reachable through the file mapping; with no separate copy, a table spanning two PT_LOADs stays readable only if those segments happen to be adjacent in guest VA, which nothing checks. When no segment covers the table, phdr_gpa is 0 and AT_PHDR reports 0, as on Linux; such a program cannot use AT_PHDR there either, so this is not a load failure. phdr_valid carries that distinction because an ET_DYN image whose covering segment sits at p_vaddr 0 has a legitimate phdr_gpa of 0 and must still be relocated by the load base.
sys_execve bounds the executable with "elf_info.load_max + elf_load_base > g->guest_size", computed in wrapping arithmetic. A PT_LOAD ending exactly at UINT64_MAX does not wrap during the parse and is recorded, so adding PIE_LOAD_BASE truncates to a small value that passes. The interpreter got no extent check at all. Either way the load fails inside elf_map_segments_fd, which runs after the point of no return, where the only remaining option is exit(128). A guest able to write its own sysroot could kill elfuse on demand by patching a PT_LOAD in ld-musl. Both extents are now checked for the carry before the addition, while execve can still return ENOEXEC and leave the caller running.
elf_map_segments_fd re-read the ELF header and re-parsed the whole program header table to recover file offsets it already had. That is not merely wasteful. elf_map_segments re-opens by path and elfuse has no ETXTBSY, so a guest thread can rewrite the image another thread is execve'ing; the second parse then validated bytes nothing downstream consumes, because bootstrap.c and exec.c build the page-table permissions from info->segments[]. A changed PT_LOAD count or order left a segment mapped but never loaded, and the guest read pre-execve bytes at an address /proc/self/maps calls file-backed. The mapper now walks info->segments[] and reads only segment contents. Relocation is expressed as a window instead of a pre-wrapped base. A segment at p_vaddr lands at target_base + (p_vaddr - va_base), with the subtract and the add both checked. The Rosetta translator links at 0x800000000000 and is mapped low, which rosetta.c arranged by passing load_base = guest_base - va_base and relying on the truncated sum; the window computes the same address with no wraparound, so what was an implied invariant is now stated, and a guest ELF (va_base 0) can no longer reach an address by overflowing into it. elf_window_t is a struct rather than two adjacent uint64_t parameters deliberately: during this change three of six call sites were left passing the old shape. Same arity, all integers, compiled clean, SIGILL on every exec path. Named fields make that a compile error. The per-segment extent arithmetic (relocation, filesz <= memsz, the guest_size bound, and the page-tail zero extent) now lives in one place instead of being spread across the loop body.
The loop body held PT_INTERP reading and PT_LOAD recording inline, nested three deep, with four copies of "free(ph_buf); return -1;". Move each to its own function and give the parse a single fail: label. No behavior change; the checks and their order are unchanged.
gva_resolve_perm returns host_base + gpa for a GPA inside the primary buffer and reports how many contiguous bytes follow, but it clamped that count only on the two branches that resolve outside the buffer. gva_contiguous_avail stops at guest_size only when the bound shortens a chunk, so a leaf whose extent ends flush with guest_size lets the walk continue into whatever the next descriptor resolves to. The caller then memcpy's past the end of the host allocation. Clamp the primary-buffer branch the same way the other two already do. The count is computed once and written once per branch. The old shape wrote *avail, then conditionally overwrote it, which also left the static analyzers unable to relate the final value to the returned pointer.
v5 is deprecated; the cache steps are otherwise unchanged.
ELF headers come from untrusted binaries, so the offsets and extents computed from them are the part of the loader most worth machine-checking. The five scalar helpers extracted earlier carry ACSL contracts discharged by Frama-C WP with -wp-rte: 64 of 64 obligations, including the implicit runtime-error goals (signed and unsigned overflow, out-of-bounds access, invalid dereference) that contracts alone would not cover. What this covers: every offset and extent feeding a pread, memcpy or memset in elf.c. The unproved code around them computes no guest-slab offset of its own. What it does not cover is stated in the source: info->segments[] is copied verbatim from the file and the callers that turn it into page-table permissions are ordinary reviewed code. Two floors keep the result from decaying into a tautology: check-wp-result.py fails on a nonzero exit, on "User Error", on a missing summary line, on N != M, and on a generated-obligation count below a per-proof floor. The last one matters most: "N of N discharged" is not evidence, because an emptied body or a deleted contract proves 0 of 0. check-acsl-coverage.py fails when a contracted function in the scanned sources is absent from -wp-fct. Frama-C ASSUMES the contract of anything outside the proof set, so a helper left off the list turns its postcondition into an unchecked axiom, and the run still prints PROVED. It scans the headers the source includes, not just the .c, since a contract added to utils.h would be assumed the same way. Contracts state what the caller relies on, not what the body happens to do. The one place where the distinction bites is documented at elf_phdr_fetch: an attempt to state the memcpy's byte-level result proved vacuously, because WP's model does not relate byte access through a cast to a struct's contents. Verified by mutation -- with that postcondition in place, replacing the memcpy with memset still proved everything. The CI job gates rather than advises: an unproved obligation fails the build, unlike tidy-macos and scan-macos. Frama-C, Alt-Ergo and Z3 are version-pinned and the opam root is cached on those versions. Frama-C 31 has no aarch64 machdep; gcc_x86_64 is a data model (type widths, endianness, alignment), not a code generation target, and the choice is justified property by property in mk/analysis.mk.
Every guest pointer a syscall touches is turned into a host pointer by gva_translate_perm and gva_resolve_perm: a page-table walk, a leaf offset, and a byte count clamped against whatever region the result lands in. The arithmetic is small, entirely scalar, and reachable with any address a guest cares to pass, which makes it worth proving rather than reviewing. The four operations move to src/core/gva-math.h as static inline functions with ACSL contracts: table-descriptor offset, leaf target plus remaining chunk, chunk clamp, and span-does-not-wrap. 40 of 40 obligations discharged with -wp-rte (make verify-gva). guest.c cannot be given to Frama-C -- it includes Hypervisor.framework -- so the proved arithmetic is in a header the callers include, and pointing the prover at the header is what makes it checkable at all. Two call-site guards follow from what the contracts require rather than from a proof: pt_at now aborts when a page-table offset does not leave room for the whole 4KiB table. The walker screens descriptors through gva_pt_table_offset, but roughly twenty other call sites -- find_l2_entry, guest_map_va_range, guest_extend_page_tables, guest_update_perms and the ttbr0 roots among them -- derive the offset with a bare subtraction and no bound, and unlike the walker they write descriptors. One check at the choke point cannot be forgotten by the next site added. It is not a guest-reachable condition: every descriptor comes from pt_alloc_page and the pool is absent from the boot region set, so reaching it means the allocator is broken, which is not recoverable. gva_contiguous_avail breaks out of the walk when the region ends at or before the current GPA. gva_chunk_clamp requires gpa < region_end and nothing checks call sites, so violating it would clamp the chunk to zero, return zero for a non-NULL translation, and spin guest_copy forever on a guest-supplied address. Every path satisfies it today; the break makes that structural. That gap is the honest limit of this proof and is documented in mk/analysis.mk: check-acsl-coverage.py catches a contract left out of the proof set, but nothing checks that unproved C honors a proved function's preconditions.
Everything the stub parses comes from whoever connects to --gdb, and the bounds fixed earlier in this series were found by reading. The four parsing helpers now carry ACSL contracts discharged by Frama-C WP with -wp-rte: 98 of 98 obligations covering hex-pair decoding, buffer-bounded decode, the parse loop's termination, and the checksum fold. The checksum contract is the one worth stating: rsp_checksum's postcondition is a recursive logic function folding the byte sum mod 256 at each step, so the proof is that the loop computes that fold, not merely that it stays in range. hex_nibble is proved here rather than assumed. It lives in utils.h, and the whole RSP proof rests on its "-1 for a non-digit" behavior: without the contract, WP takes the postcondition on faith, and a body mutated to "return 15;" still printed PROVED. VERIFY_UTILS_FCTS appends it to every proof whose source includes the header, which raises the ELF proof's floor from 64 to 78 for the same reason. The RSP proof uses the typed memory model, not the caveat model elf.c needs: gdb_hex_decode assigns a pointer range (dst[0 .. len-1]), which caveat's flat single-region memory cannot express. Nothing here reinterprets bytes at an attacker-chosen stride, which is what forced caveat on elf.c in the first place. Plain-char signedness is the one place the gcc_x86_64 data model diverges from arm64 macOS, and these helpers do take plain char. The result is signedness-independent because every char value passes through an explicit (unsigned char) or (uint8_t) cast before it is compared or accumulated. That is now written down in mk/analysis.mk as an invariant to preserve.
The Infer job reports 132 PULSE_UNINITIALIZED_VALUE findings on this branch and 0 on main, across thirteen files this series never touches. They are false positives: Pulse cannot prove that guest_copy's chunked "while (copied < len)" loop fills its destination, so every caller of guest_read_small looks like it reads uninitialized memory. Each flagged caller checks the return value, and the representative traces skip the check entirely. The clamp added earlier made the slow path reachable in Pulse's exploration, which is why the count moved. Three of the findings were mine and are fixed rather than suppressed: the phdr scratch in elf_load_fd's loop is now zero-initialized, one 56-byte clear per program header. Alternatives were measured, not assumed. Restructuring guest_copy does not help: memset(dst, 0, len) up front makes it 139 and costs a memset on every guest read; reverting the commit the count bisected to still leaves 135. Scoping the suppression narrower is worse, since the findings span syscall.c and proc.c, so a path block list covers most of the syscall surface while being harder to read, and censor-report does not take effect through `infer run` in v1.3.0. The cost is repo-wide and stated in the CI comment: a genuinely uninitialized read added later will not be caught here. Everything else Infer reports still gates -- null dereference, use-after-free, leaks, dead stores, stack-address escape -- and turning the checker back on immediately surfaced a real dead store in rosetta.c. `make infer-uninit` re-runs the analysis with the checker enabled and prints the count, so whether an Infer upgrade has made the suppression unnecessary is one command away.
This was referenced Aug 6, 2026
Closed
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
1 participant
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.
Summary by cubic
Adds Frama-C WP proofs gated in CI for ELF parsing, GDB RSP hex/checksum, and guest address math, and switches ELF relocation to a checked
elf_window_twindow. Tightens safety checks across exec, GDB, guest memory, and FUSE, and hardens the Infer workflow.New Features
verifyruns Frama-C on ELF, RSP, and GVA math; proofs gate merges with a pinned toolchain;scripts/check-wp-result.pyandscripts/check-acsl-coverage.pyenforce success and coverage; proof timeout set to 120s.src/core/gva-math.hand proved it; relocation useself_window_t(va_base/target_base); tightened ELF helpers and addedELF_PHDR_TABLE_MAX; AT_PHDR derived from the coveringPT_LOADand guarded byphdr_valid.PULSE_UNINITIALIZED_VALUEin.inferconfig; addmake infer-uninitto re-run with the check enabled and report the count.Bug Fixes
H; requirebufsz >= 2; return an error on malformedvCont.make infer-uninitto create the build dir, honor Infer exit status (treat exit 2 as expected), and fail on an empty/missing report.Written for commit a83af2f. Summary will update on new commits.