diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 6276c986..953ae2d4 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -4,6 +4,8 @@ # lint : format/newline/security/cppcheck/dispatch on Linux # build-macos : compile + entitlement check on macOS Apple Silicon # tidy-macos : clang-tidy via `make lint` +# verify : Frama-C WP proofs of the attacker-facing arithmetic via +# `make verify`; gating, not advisory # scan-macos : LLVM scan-build via `make analyze` # infer-macos : Facebook Infer capture + analyze over the full build # runtime-macos : HVF runtime tests on self-hosted Apple Silicon, @@ -56,7 +58,7 @@ jobs: uses: actions/checkout@v7 - name: Cache apt packages - uses: actions/cache@v5 + uses: actions/cache@v6 with: path: ~/apt-cache key: apt-${{ runner.os }}-${{ env.LINT_PKGS }} @@ -130,7 +132,7 @@ jobs: - name: Cache Homebrew downloads # No restore-keys: a partial match would mask upstream regressions. - uses: actions/cache@v5 + uses: actions/cache@v6 with: path: ~/Library/Caches/Homebrew/downloads key: brew-${{ runner.os }}-${{ runner.arch }}-${{ env.BREW_PKGS }} @@ -189,7 +191,7 @@ jobs: uses: actions/checkout@v7 - name: Cache Homebrew downloads - uses: actions/cache@v5 + uses: actions/cache@v6 with: path: ~/Library/Caches/Homebrew/downloads key: brew-${{ runner.os }}-${{ runner.arch }}-${{ env.BREW_PKGS }} @@ -209,6 +211,107 @@ jobs: - name: clang-tidy (make lint) run: make lint + # Frama-C WP proofs of the attacker-facing arithmetic via `make verify`. + # + # GATING, unlike tidy-macos and scan-macos: the inputs these proofs cover come + # from untrusted binaries and from the guest itself, so an unproved + # obligation fails the job instead of being logged for review. Without this + # job the proofs are only enforced when a human runs them, and they rot the + # first time someone edits elf.c or gdbstub-rsp.c. + verify: + name: Frama-C WP proofs (make verify) + runs-on: macos-15 + timeout-minutes: 60 + env: + HOMEBREW_NO_INSTALL_CLEANUP: 1 + HOMEBREW_NO_AUTO_UPDATE: 1 + # graphviz/llvm/zlib are frama-c's system dependencies; conf-graphviz + # fails without dot(1). The exact Python formula opam wants moves between + # releases, so it is not listed here: OPAMCONFIRMLEVEL below lets opam + # install whatever depexts it still needs rather than having this list + # guess. Guessing python@3.11 when opam wanted python@3.9 is what made the + # previous attempt abort. + BREW_PKGS: opam gmp pkg-config graphviz llvm@17 zlib + # Without this, opam's "some required external dependencies are missing" + # prompt has no TTY to answer it, silently takes option 4 (abort), and the + # step exits 10. + OPAMCONFIRMLEVEL: unsafe-yes + # The gate fails on any single [Timeout], and a shared runner is slower + # than a dev machine (the three proofs take 3-9s each locally). The job + # already has a 60-minute budget, so headroom here costs nothing and + # removes a flake class that would read as a proof regression. + FRAMAC_TIMEOUT: 120 + # Pinned so the gating proofs run against a known toolchain. The opam + # cache key below is built from these three, so bumping a version here is + # all that is needed to install afresh rather than reuse a stale switch. + FRAMAC_VERSION: "31.0" + ALT_ERGO_VERSION: 2.6.3 + Z3_VERSION: 4.16.0 + OPAMROOT: ${{ github.workspace }}/.opam + OPAM_SWITCH: frama-c-elfuse + steps: + - name: Checkout + uses: actions/checkout@v7 + + - name: Cache Homebrew downloads + uses: actions/cache@v6 + with: + path: ~/Library/Caches/Homebrew/downloads + key: brew-${{ runner.os }}-${{ runner.arch }}-${{ env.BREW_PKGS }} + + - name: Install Homebrew packages + # shellcheck disable=SC2086 -- BREW_PKGS is a space-separated list. + run: | + set -euo pipefail + brew install --quiet $BREW_PKGS + + # Building Frama-C and the provers from source takes tens of minutes, so + # the whole opam root is cached. Bump the key suffix to force a rebuild. + - name: Cache opam switch + id: opam-cache + uses: actions/cache@v6 + with: + path: ${{ env.OPAMROOT }} + # Keyed on the pinned versions, so changing any of them installs + # afresh instead of silently reusing a stale toolchain. + key: opam-${{ runner.os }}-${{ runner.arch }}-frama-c${{ env.FRAMAC_VERSION }}-ae${{ env.ALT_ERGO_VERSION }}-z3${{ env.Z3_VERSION }} + + - name: Install Frama-C, Alt-Ergo, Z3 + if: steps.opam-cache.outputs.cache-hit != 'true' + run: | + set -euo pipefail + opam init -y --bare --disable-sandboxing + opam switch create "$OPAM_SWITCH" 4.14.1 + eval "$(opam env --switch="$OPAM_SWITCH")" + # No --assume-depexts: the system packages are installed above, and + # asserting they exist when they do not is what made conf-graphviz + # fail with "dot: command not found". + opam install -y \ + frama-c.$FRAMAC_VERSION \ + alt-ergo.$ALT_ERGO_VERSION \ + z3.$Z3_VERSION + + - name: Prove the parsers and translation (make verify) + # why3 config detect runs here rather than in the install step: it + # writes ~/.why3.conf, which lives outside OPAMROOT and so is absent on + # a cache hit. Skipping it makes WP abort with "Prover not found in + # why3.conf" instead of reporting unproved obligations, which the gate + # would then report as "Frama-C emitted no result". + run: | + set -euo pipefail + eval "$(opam env --switch="$OPAM_SWITCH")" + why3 config detect + frama-c -version + make verify + + - name: Upload prover log + if: always() + uses: actions/upload-artifact@v7 + with: + name: verify-logs + path: build/verify-*.log + if-no-files-found: warn + # LLVM scan-build via `make analyze`. Runs in parallel with build/tidy. # Advisory: scan-build's Make target does not pass --status-bugs, so # findings appear in logs and in the uploaded HTML report but do not @@ -228,7 +331,7 @@ jobs: uses: actions/checkout@v7 - name: Cache Homebrew downloads - uses: actions/cache@v5 + uses: actions/cache@v6 with: path: ~/Library/Caches/Homebrew/downloads key: brew-${{ runner.os }}-${{ runner.arch }}-${{ env.BREW_PKGS }} @@ -283,7 +386,7 @@ jobs: uses: actions/checkout@v7 - name: Cache Homebrew downloads - uses: actions/cache@v5 + uses: actions/cache@v6 with: path: ~/Library/Caches/Homebrew/downloads key: brew-${{ runner.os }}-${{ runner.arch }}-${{ env.BREW_PKGS }} @@ -302,6 +405,21 @@ jobs: with: infer_version: v1.3.0 + # .inferconfig disables PULSE_UNINITIALIZED_VALUE repo-wide. Pulse cannot + # prove guest_copy's chunked "while (copied < len)" loop fills its + # destination, so every guest_read_small caller looks uninitialized; the + # findings were audited and every caller checks the return value. The rest + # of the Infer gate is untouched: null dereference, use-after-free, leaks, + # dead stores and stack-address escape all still fail the job. + # + # The cost is real and repo-wide: a genuinely uninitialized read added + # after this point is not caught here. Scoping it narrower was tried and + # is worse -- the findings span thirteen files including syscall.c and + # proc.c, so a path block list suppresses the same class over most of the + # syscall surface while being harder to read, and censor-report does not + # take effect through `infer run` in v1.3.0. `make infer-uninit` re-runs + # the analysis with the checker back on and prints the count, so whether + # an Infer upgrade has made this unnecessary is one command away. - name: Infer capture + analyze (make -B elfuse) # -B forces a clean rebuild so Infer captures every translation unit. # Non-C build steps (shim.S assembly, objcopy) pass through untouched. @@ -501,7 +619,7 @@ jobs: test "$(uname -m)" = "arm64" - name: Cache Homebrew downloads - uses: actions/cache@v5 + uses: actions/cache@v6 with: path: ~/Library/Caches/Homebrew/downloads key: brew-runtime-${{ runner.os }}-${{ runner.arch }}-${{ env.BREW_PKGS }} diff --git a/.inferconfig b/.inferconfig new file mode 100644 index 00000000..21d21fec --- /dev/null +++ b/.inferconfig @@ -0,0 +1,3 @@ +{ + "disable-issue-type": ["PULSE_UNINITIALIZED_VALUE"] +} diff --git a/mk/analysis.mk b/mk/analysis.mk index 1ad9e77a..fbc4b916 100644 --- a/mk/analysis.mk +++ b/mk/analysis.mk @@ -1,8 +1,10 @@ # Static analysis and formatting -.PHONY: lint analyze check-format indent +.PHONY: lint analyze check-format indent verify verify-elf verify-rsp \ + verify-gva infer-uninit CLANG_TIDY ?= clang-tidy +INFER ?= infer # Tracked source-like files only. Avoid editor/agent worktrees and other # untracked mirrors under dot-directories. @@ -11,14 +13,233 @@ C_FORMAT_FILES := $(shell git ls-files --cached --others --exclude-standard \ 'tests/*.c' 'tests/*.h') SHELL_SCRIPTS := $(shell git ls-files --cached --others --exclude-standard \ -- '*.sh') -PYTHON_FORMAT_FILES := $(shell git ls-files --cached --others --exclude-standard \ - -- '*.py') +PYTHON_FORMAT_FILES := $(shell git ls-files --cached --others \ + --exclude-standard -- '*.py') ## Run clang-tidy on all source files lint: $(BUILD_DIR)/shim_blob.h $(BUILD_DIR)/version.h @echo " TIDY src/" $(Q)$(CLANG_TIDY) $(SRCS) -- $(CFLAGS) -Isrc -I$(BUILD_DIR) +# Frama-C proof of the ELF parsing core. ELF headers come from untrusted +# binaries, so every offset and extent computed from them is discharged as a +# machine-checked proof rather than reviewed by eye. -wp-rte adds the implicit +# runtime-error goals (overflow, out-of-bounds, invalid dereference) that the +# ACSL contracts alone would not cover. +# +# Model: caveat. The default typed model cannot follow the byte-addressed +# program header buffer, whose entry stride (e_phentsize) is attacker chosen +# and need not match the struct alignment. caveat assumes formal pointer +# parameters do not alias, which the contracts state explicitly via \separated. +# The callers are not in -wp-fct, so nothing checks that they honor it: today +# they pass a malloc'd ph_buf plus distinct stack locals, but a future +# elf_segment_extent(..., &x, &x) would invalidate the proof with no diagnostic. +# +# That caveat is general, and it bites hardest for gva-math.h: guest.c cannot be +# given to Frama-C at all, so NOTHING checks that its call sites honor the eight +# `requires` clauses there. check-acsl-coverage.py closes the other direction +# (a contract assumed because its function was left out of -wp-fct); it says +# nothing about preconditions at call sites. Those are reviewed by hand, and +# gva_contiguous_avail additionally guards itself at runtime. +# +# Install: opam install frama-c, then why3 config detect (without the latter WP +# aborts with "Prover not found" instead of reporting unproved goals). +# +# Data model: Frama-C's -machdep names a C DATA MODEL (type widths, alignment, +# endianness, char signedness), not a code generation target. Nothing here is +# proved "for x86_64" and no x86_64 code is involved; the flag only tells the +# prover how wide a size_t is. +# +# Frama-C 31 ships avr_16, avr_8, gcc_x86_16, gcc_x86_32, gcc_x86_64, +# msvc_x86_64, ppc_32, x86_16, x86_32, x86_64 -- no aarch64 entry at all. Of +# those, gcc_x86_64 is the only one that matches arm64 macOS on the properties +# these proofs rest on: +# +# property arm64 macOS gcc_x86_64 used by the proof? +# pointer / long / size_t 64-bit 64-bit yes +# byte order little little yes +# uint64_t alignment 8 8 yes +# plain char signedness unsigned signed see below +# +# Plain-char signedness is the one mismatch, and the RSP proof DOES cover +# functions taking plain char (gdb_hex_pair, gdb_hex_decode, rsp_checksum). +# What keeps the result signedness-independent is not their parameter types but +# that every use of a char value goes through an explicit (unsigned char) or +# (uint8_t) cast before it is compared or accumulated. That is the invariant to +# preserve: no proved function may read a plain char without such a cast. Prove +# one that does, and supply a custom machdep rather than extending this list. +FRAMAC ?= frama-c +FRAMAC_DATA_MODEL ?= gcc_x86_64 +FRAMAC_TIMEOUT ?= 30 + +# The analyzer parses against Frama-C's own modeled libc headers, never the +# host's. -print-share-path runs at recipe time rather than through $(shell) so +# a make invocation with no frama-c installed does not pay for it. +FRAMAC_CPP_ARGS = -nostdinc \ + -isystem $$($(FRAMAC) -print-share-path)/libc -Isrc -I$(BUILD_DIR) + +# One proof per attacker-facing parser. Each is declared by a single +# verify_target call below; the recipe itself lives in one place. +# +# MIN_GOALS is a floor on obligations GENERATED. "N of N discharged" is not +# evidence on its own: an emptied function body or a dropped contract proves +# 0 of 0. Raise it when adding proved functions; it is a tripwire, not a target. + +# Contracts in the shared src/utils.h. Every proof whose source includes that +# header must prove them too, not merely assume them, so this list is appended +# to each such proof's -wp-fct. Proving hex_nibble twice costs a second or two; +# assuming it once is how the RSP proof came to rest on an unchecked axiom. +VERIFY_UTILS_FCTS := hex_nibble + +VERIFY_ELF_SRC := src/core/elf.c +VERIFY_ELF_FCTS := elf_add_no_wrap elf_phdr_gpa_in_segment \ + elf_phdr_table_bytes elf_phdr_fetch elf_segment_extent \ + $(VERIFY_UTILS_FCTS) +VERIFY_ELF_MIN_GOALS ?= 78 +VERIFY_ELF_MODEL := caveat + +# Includes utils.h and elf.h: elf.c includes both, and utils.h already carries +# contracts, so scanning only the .c would let one added there become an +# unchecked axiom for this proof. +VERIFY_ELF_SCAN := src/core/elf.c src/core/elf.h src/utils.h +VERIFY_ELF_CLAIM := for ANY byte sequence an untrusted ELF can supply +VERIFY_ELF_UNPROVED := the pread/malloc I/O around them stays test-covered + +VERIFY_GVA_SRC := src/core/gva-math.h +VERIFY_GVA_FCTS := gva_pt_table_offset gva_leaf_target gva_chunk_clamp \ + gva_span_ok +VERIFY_GVA_MIN_GOALS ?= 40 +VERIFY_GVA_MODEL := typed +VERIFY_GVA_SCAN := src/core/gva-math.h +VERIFY_GVA_CLAIM := for ANY guest address, length, and page-table content +VERIFY_GVA_UNPROVED := the walk and copy loops around them stay test-covered + +VERIFY_RSP_SRC := src/debug/gdbstub-rsp.c +VERIFY_RSP_FCTS := $(VERIFY_UTILS_FCTS) gdb_hex_pair gdb_hex_decode \ + gdb_parse_hex rsp_checksum +VERIFY_RSP_MIN_GOALS ?= 98 + +# typed, not caveat: gdb_hex_decode assigns a pointer RANGE (dst[0 .. len-1]), +# which caveat's flat single-region memory cannot express ("Undefined +# array-size"). elf.c can use caveat because its proved functions assign only +# single locations. Nothing here reinterprets bytes at an attacker-chosen +# stride, which is the reason elf.c needed caveat in the first place. +VERIFY_RSP_MODEL := typed + +# Includes utils.h: hex_nibble lives there and the whole RSP proof rests on it. +VERIFY_RSP_SCAN := src/debug/gdbstub-rsp.c src/utils.h +VERIFY_RSP_CLAIM := for ANY packet bytes a GDB remote can send +VERIFY_RSP_UNPROVED := the socket I/O and framing loop stay test-covered + +# -wp-fct wants one comma-separated argument; the lists stay space-separated so +# the recipe can iterate them for the banner. +verify_empty := +verify_space := $(verify_empty) $(verify_empty) +verify_comma := , +commafy = $(subst $(verify_space),$(verify_comma),$(strip $(1))) + +# Per-proof values, consumed by the single recipe below through target-specific +# variables. Adding a proof means adding a VERIFY__* block, one line of +# assignments here, and the target name to the shared rule; the recipe itself is +# written once. + +## Prove the ELF parser cannot be driven out of bounds by a crafted binary +verify-elf: NAME := elf +verify-elf: SRC := $(VERIFY_ELF_SRC) +verify-elf: FCTS := $(VERIFY_ELF_FCTS) +verify-elf: FCT_ARG := $(call commafy,$(VERIFY_ELF_FCTS)) +verify-elf: MIN_GOALS := $(VERIFY_ELF_MIN_GOALS) +verify-elf: MODEL := $(VERIFY_ELF_MODEL) +verify-elf: SCAN := $(VERIFY_ELF_SCAN) +verify-elf: CLAIM := $(VERIFY_ELF_CLAIM) +verify-elf: UNPROVED := $(VERIFY_ELF_UNPROVED) + +## Prove guest address translation cannot compute an out-of-bounds window +verify-gva: NAME := gva +verify-gva: SRC := $(VERIFY_GVA_SRC) +verify-gva: FCTS := $(VERIFY_GVA_FCTS) +verify-gva: FCT_ARG := $(call commafy,$(VERIFY_GVA_FCTS)) +verify-gva: MIN_GOALS := $(VERIFY_GVA_MIN_GOALS) +verify-gva: MODEL := $(VERIFY_GVA_MODEL) +verify-gva: SCAN := $(VERIFY_GVA_SCAN) +verify-gva: CLAIM := $(VERIFY_GVA_CLAIM) +verify-gva: UNPROVED := $(VERIFY_GVA_UNPROVED) + +## Prove the GDB RSP parser cannot be driven out of bounds by a remote +verify-rsp: NAME := rsp +verify-rsp: SRC := $(VERIFY_RSP_SRC) +verify-rsp: FCTS := $(VERIFY_RSP_FCTS) +verify-rsp: FCT_ARG := $(call commafy,$(VERIFY_RSP_FCTS)) +verify-rsp: MIN_GOALS := $(VERIFY_RSP_MIN_GOALS) +verify-rsp: MODEL := $(VERIFY_RSP_MODEL) +verify-rsp: SCAN := $(VERIFY_RSP_SCAN) +verify-rsp: CLAIM := $(VERIFY_RSP_CLAIM) +verify-rsp: UNPROVED := $(VERIFY_RSP_UNPROVED) + +# One recipe, shared by every verify-* target above. Listing several targets on +# one rule gives each of them this recipe; the target-specific variables select +# what gets proved. +# +# The recipe only runs the prover. Deciding whether the run counts as a proof +# lives in scripts/check-wp-result.py: as a shell recipe it needed every $ +# doubled and every line continued, which put the gate that matters out of +# reach of any test. +verify-elf verify-rsp verify-gva: | $(BUILD_DIR) + @command -v $(FRAMAC) >/dev/null 2>&1 || { \ + printf "$(RED)frama-c not found$(RESET) "; \ + printf "(set FRAMAC=, or eval \$$(opam env --switch=))\n"; \ + exit 1; \ + } + @python3 scripts/check-acsl-coverage.py --target verify-$(NAME) \ + --fcts "$(FCTS)" $(SCAN) + @echo " PROVE $(SRC) (Frama-C WP: weakest-precondition prover)" + @echo " claim: $(CLAIM)," + @echo " these compute no out-of-bounds access and no overflow" + @for f in $(FCTS); do echo " - $$f"; done + @echo " memory model: $(MODEL); data model: $(FRAMAC_DATA_MODEL)" + @echo " (data model is type widths only; Frama-C 31" + @echo " has no aarch64 machdep, so this is the LP64 stand-in)" + @$(FRAMAC) -machdep $(FRAMAC_DATA_MODEL) \ + -cpp-extra-args="$(FRAMAC_CPP_ARGS)" \ + $(SRC) -wp -wp-rte -wp-model $(MODEL) \ + -wp-fct $(FCT_ARG) \ + -wp-prover alt-ergo,z3 -wp-timeout $(FRAMAC_TIMEOUT) \ + > $(BUILD_DIR)/verify-$(NAME).log 2>&1; \ + python3 scripts/check-wp-result.py --status $$? \ + --log $(BUILD_DIR)/verify-$(NAME).log --min-goals $(MIN_GOALS) \ + --src $(SRC) --unproved "$(UNPROVED)" + +## Run every Frama-C proof +verify: verify-elf verify-gva verify-rsp + +## Re-run Infer with the uninitialized-value checker that .inferconfig disables +infer-uninit: | $(BUILD_DIR) + @command -v $(INFER) >/dev/null 2>&1 || { \ + printf " $(RED)infer not found$(RESET) (set INFER=)\n"; exit 1; \ + } + @echo " INFER uninitialized-value checker (disabled in .inferconfig)" + @echo " A count of 0 means the suppression is no longer needed and" + @echo " .inferconfig should be deleted. Anything else is the known" + @echo " false-positive class: Pulse cannot prove guest_copy's" + @echo " chunked loop fills its destination." + @status=0; \ + $(INFER) run --keep-going --enable-issue-type PULSE_UNINITIALIZED_VALUE \ + --results-dir $(BUILD_DIR)/infer-uninit \ + -- $(MAKE) -B elfuse > $(BUILD_DIR)/infer-uninit.log 2>&1 || status=$$?; \ + if [ "$$status" -ne 0 ] && [ "$$status" -ne 2 ]; then \ + printf " $(RED)FAILED$(RESET) infer exited %s; this is an analysis\n" "$$status"; \ + printf " failure, not an audit result. See $(BUILD_DIR)/infer-uninit.log\n"; \ + exit 1; \ + fi; \ + if [ ! -s $(BUILD_DIR)/infer-uninit/report.json ]; then \ + printf " $(RED)FAILED$(RESET) infer produced no report\n"; exit 1; \ + fi; \ + python3 -c "import json,sys; \ + d=json.load(open('$(BUILD_DIR)/infer-uninit/report.json')); \ + u=[x for x in d if x['bug_type']=='PULSE_UNINITIALIZED_VALUE']; \ + print(' %d PULSE_UNINITIALIZED_VALUE finding(s) across %d file(s)' \ + % (len(u), len({x['file'] for x in u})))" + ## Run clang static analyzer (scan-build) analyze: @echo " SCAN elfuse" diff --git a/scripts/check-acsl-coverage.py b/scripts/check-acsl-coverage.py new file mode 100644 index 00000000..55045dbf --- /dev/null +++ b/scripts/check-acsl-coverage.py @@ -0,0 +1,171 @@ +#!/usr/bin/env python3 +"""Fail when a function carrying an ACSL contract is missing from the proof set. + +Frama-C ASSUMES the contract of any function it is not asked to prove. A +contracted helper left out of -wp-fct therefore becomes an unchecked axiom that +every goal above it rests on, and the gate still reports success. That is not +hypothetical: hex_nibble sat outside the RSP proof set, and replacing its body +with "return 15;" -- which contradicts its own ensures -- still produced +"PROVED 74 of 74", because gdb_parse_hex's termination and gdb_hex_decode's +stop-at-NUL both follow from that contract and from nothing else. + +Usage: + check-acsl-coverage.py --fcts "a b c" FILE [FILE ...] + +Exits non-zero, naming the offenders, when a scanned file carries an ACSL +contract that is not in the proof set -- or one this script cannot attribute to +a function at all, since a contract it cannot read is one it cannot confirm. +""" + +import argparse +import re +import sys + +# ACSL annotations. Both forms count: Frama-C assumes a contract written with +# one-line //@ exactly as readily as a /*@ ... */ block, so scanning only the +# block form would let two characters re-open the very hole this script exists +# to close. +ACSL_BLOCK = re.compile( + r"/\*@.*?\*/" # /*@ ... */ + r"|^[ \t]*//@[^\n]*(?:\n[ \t]*//[^\n]*)*", # //@ ..., plus its continuations + re.DOTALL | re.MULTILINE, +) + +# Annotations that are not function contracts, so have no function to attribute +# to: logic declarations (no C definition at all) and statement annotations +# (attached to a loop or a statement inside a body already covered by its own +# function's contract). +NOT_A_CONTRACT = re.compile( + r"^\s*(predicate|logic|axiomatic|lemma|type|ghost" + r"|loop|assert|check|admit|assume|breaks|continues|returns)\b" +) + +# A C function definition header, up to the opening brace. Deliberately loose: +# the codebase writes one parameter per line, so match across newlines and take +# the identifier that precedes the parameter list. +DEFINITION = re.compile( + r"""^[ \t]* # start of a line + (?:static\s+|inline\s+)* # storage/inline qualifiers + [A-Za-z_][A-Za-z_0-9\s*]*? # return type, possibly with pointers + \b(?P[A-Za-z_][A-Za-z_0-9]*)\s* # the function name + \([^;{]*?\)\s* # parameter list + \{ # a body, not a declaration + """, + re.VERBOSE | re.DOTALL, +) + + +def contracted_definitions(path): + """Contracted function names in @path, plus contracts not attributable to one. + + Returns (names, unattributed). Anything this cannot identify goes into + `unattributed` and fails the run rather than being skipped: silently + ignoring a contract is precisely the failure this script exists to prevent, + so an unrecognized construct must be loud, not absent. A preprocessor + directive or an ordinary comment between the annotation and the function is + enough to defeat a regex, so those are stepped over explicitly. + """ + with open(path, encoding="utf-8") as handle: + text = handle.read() + + names, unattributed = [], [] + for block in ACSL_BLOCK.finditer(text): + raw = block.group(0) + if raw.startswith("/*"): + body = raw[3:-2] + else: + # //@ form: drop the marker from the first line and the leading // + # from any continuation lines. + body = "\n".join( + re.sub(r"^[ \t]*//@?", "", line) for line in raw.splitlines() + ) + if NOT_A_CONTRACT.match(body.lstrip("\n")): + continue + + # Step over what can legitimately sit between an annotation and the + # function it applies to: further annotation blocks (a predicate + # declared just above its user), ordinary comments, and preprocessor + # directives. + rest = text[block.end() :] + while True: + stripped = rest.lstrip() + if stripped.startswith("/*"): + rest = stripped[stripped.index("*/") + 2 :] + elif stripped.startswith("//") or stripped.startswith("#"): + newline = stripped.find("\n") + if newline < 0: + rest = "" + break + rest = stripped[newline + 1 :] + else: + rest = stripped + break + + match = DEFINITION.match(rest) + if match: + names.append(match.group("name")) + else: + unattributed.append(first_line(rest)) + return names, unattributed + + +def first_line(text): + """First non-empty line of @text, for an error message.""" + for line in text.splitlines(): + if line.strip(): + return line.strip()[:72] + return "" + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--fcts", required=True, help="space-separated names passed to -wp-fct" + ) + parser.add_argument( + "--target", default="the proof", help="proof name, for the error message" + ) + parser.add_argument("files", nargs="+") + args = parser.parse_args() + + proved = set(args.fcts.split()) + missing, unattributed = [], [] + for path in args.files: + names, strays = contracted_definitions(path) + missing += [(path, n) for n in names if n not in proved] + unattributed += [(path, s) for s in strays] + + if unattributed: + sys.stderr.write( + " ACSL coverage: %d contract(s) not attributable to a function\n" + % len(unattributed) + ) + for path, excerpt in unattributed: + sys.stderr.write(" %s: before %r\n" % (path, excerpt)) + sys.stderr.write( + " Refusing to guess: a contract this script cannot read\n" + " is one it cannot confirm is proved, which is the blind\n" + " spot it exists to close.\n" + ) + return 1 + + if missing: + sys.stderr.write( + " ACSL coverage: %d contracted function(s) are assumed, not proved\n" + % len(missing) + ) + for path, name in missing: + sys.stderr.write(" %s: %s\n" % (path, name)) + sys.stderr.write( + " Frama-C assumes the contract of any function outside\n" + " -wp-fct, so each of these is an unchecked axiom the\n" + " rest of %s rests on. Add them to the proof set, or\n" + " drop their contracts if they are not load-bearing.\n" + % args.target + ) + return 1 + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/check-wp-result.py b/scripts/check-wp-result.py new file mode 100644 index 00000000..9781452f --- /dev/null +++ b/scripts/check-wp-result.py @@ -0,0 +1,156 @@ +#!/usr/bin/env python3 +"""Turn a Frama-C WP log into a pass/fail verdict for `make verify-*`. + +Frama-C's own "Proved goals: N / M" line is not sufficient evidence on its +own, so this applies four independent gates before reporting success: + + 1. The process exited 0. A crashed run can still have printed a summary. + 2. No "User Error" appeared, which means the input was rejected outright. + 3. At least --min-goals obligations were GENERATED. An emptied function body + or a dropped contract proves 0 of 0, and that is not a proof. + 4. Every generated obligation was discharged. + +Lives outside the makefile because the same logic written as a shell recipe +needs every `$` doubled and every line continued, which is how it grew past +80 columns and out of reach of any test. + +Usage: + check-wp-result.py --log FILE --status N --min-goals N --src FILE \ + --unproved TEXT +""" + +import argparse +import re +import sys + +RED = "\033[0;31m" +GREEN = "\033[0;32m" +RESET = "\033[0m" + +# An obligation WP could not discharge. The goal name carries a memory-model +# prefix that varies per proof and says nothing about which function is open, +# so strip it and report the bare name. +OPEN_GOAL = re.compile( + r"^\[wp\] \[(?:Timeout|Stepout|Unknown|Failed)\] " + r"(?:typed_caveat_|typed_|bytes_)?([A-Za-z0-9_]+)" +) + +PROVED_GOALS = re.compile(r"^\[wp\] Proved goals: *([0-9]+) / ([0-9]+)$") + +# Everything up to and including a "User Error:" marker, so the message can be +# reprinted without its channel prefix. The gate itself is the looser substring +# "User Error": a report this cannot reformat must still fail the run. +USER_ERROR = re.compile(r"^.*User Error: *") + +# A function WP took on faith: it generated a spec instead of analyzing a body. +ASSUMED = re.compile( + r"Neither code nor explicit .* for function ([A-Za-z_][A-Za-z_0-9]*)," +) + +# Printed verbatim under their respective banners. Kept as literal blocks +# rather than a run of print() calls so the alignment that makes them readable +# survives any reformatting. +MIN_GOALS_HINT = """\ + a gutted function body or a dropped contract proves trivially; + raise VERIFY_*_MIN_GOALS when adding proved functions\ +""" + +SUFFIX_KEY = """\ + Each open obligation named above is either a real defect or an + ACSL contract too weak to justify the code. Read the suffix: + _ensures[_N] postcondition N does not hold + _assigns_* the function writes outside its frame + _assert_rte_* a runtime error is reachable (overflow, + out-of-bounds, invalid dereference) + _call__requires_* a precondition of callee is not met\ +""" + + +def unproven(reason): + """Print @reason under an UNPROVEN banner and return the failure status.""" + print(" %sUNPROVEN%s %s" % (RED, RESET, reason)) + return 1 + + +def report(log_path, lines, status, min_goals, src, unproved): + """Verdict for one proof. Returns the process exit status.""" + for line in lines: + match = OPEN_GOAL.match(line) + if match: + print(" open: %s" % match.group(1)) + + if status != 0: + rc = unproven("frama-c exited %s; its own summary is not trusted" % status) + print(" full output: %s" % log_path) + return rc + + if any("User Error" in line for line in lines): + unproven("frama-c rejected the input:") + for error in sorted( + {USER_ERROR.sub("", line) for line in lines if USER_ERROR.match(line)} + ): + print(" %s" % error) + return 1 + + counts = next((m for m in map(PROVED_GOALS.match, lines) if m), None) + if not counts: + rc = unproven("Frama-C emitted no result; it likely failed to run") + print(" full output: %s" % log_path) + return rc + + proved, total = int(counts.group(1)), int(counts.group(2)) + + if total < min_goals: + rc = unproven( + "only %d obligations generated, expected at least %d" % (total, min_goals) + ) + print(MIN_GOALS_HINT) + return rc + + if proved != total: + rc = unproven( + "%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 + + print( + " %sPROVED%s %d of %d proof obligations discharged by alt-ergo/z3" + % (GREEN, RESET, proved, total) + ) + assumed = sorted({m.group(1) for m in map(ASSUMED.search, lines) if m}) + if assumed: + print( + " assumed (spec generated, body not analyzed): %s" + % "".join(name + " " for name in assumed) + ) + print(" (holds for the ACSL contracts in %s;" % src) + print(" %s, not proved)" % unproved) + return 0 + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--log", required=True, help="Frama-C output file") + parser.add_argument( + "--status", type=int, required=True, help="exit status of the frama-c run" + ) + parser.add_argument( + "--min-goals", type=int, required=True, help="floor on obligations generated" + ) + parser.add_argument("--src", required=True, help="proved source file") + parser.add_argument( + "--unproved", required=True, help="what this proof does NOT cover" + ) + args = parser.parse_args() + + with open(args.log, encoding="utf-8", errors="replace") as handle: + lines = handle.read().splitlines() + + return report(args.log, lines, args.status, args.min_goals, args.src, args.unproved) + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/src/core/bootstrap.c b/src/core/bootstrap.c index 828cdb15..81fb061c 100644 --- a/src/core/bootstrap.c +++ b/src/core/bootstrap.c @@ -270,8 +270,9 @@ static bool load_interpreter(guest_t *g, uint64_t infra_lo = g->interp_base - INFRA_RESERVE; uint64_t infra_hi = g->interp_base; if (elf_map_segments(&boot->interp_info, boot->interp_resolved, - g->host_base, g->guest_size, boot->interp_base, - infra_lo, infra_hi) < 0) { + g->host_base, g->guest_size, + (elf_window_t) {0, boot->interp_base}, infra_lo, + infra_hi) < 0) { log_error("failed to map interpreter segments"); if (interp_host_temp) unlink(boot->interp_resolved); @@ -444,7 +445,8 @@ int guest_bootstrap_prepare(guest_t *g, uint64_t infra_lo = g->interp_base - INFRA_RESERVE; uint64_t infra_hi = g->interp_base; if (elf_map_segments(&boot->elf_info, elf_host_path, g->host_base, - g->guest_size, boot->elf_load_base, infra_lo, + g->guest_size, + (elf_window_t) {0, boot->elf_load_base}, infra_lo, infra_hi) < 0) { log_error("failed to map ELF segments"); return -1; diff --git a/src/core/elf.c b/src/core/elf.c index 0426b98f..26d07e8e 100644 --- a/src/core/elf.c +++ b/src/core/elf.c @@ -14,13 +14,319 @@ #include #include #include -#include #include #include "core/elf.h" #include "debug/log.h" #include "utils.h" +/* Verified parsing core. + * + * The five functions below take scalars and a bounded byte buffer, touch no + * I/O, and carry ACSL contracts discharged by Frama-C WP with -wp-rte (make + * verify-elf). They are ordered primitive-first. + * + * Covered: the offsets and extents feeding the host-side reads and writes in + * THIS file. The unproved code around them computes no guest-slab offset or + * extent of its own, so no pread, memcpy, or memset here can leave the slab. + * + * NOT covered, and do not assume otherwise: + * - info->segments[] holds p_vaddr and p_memsz verbatim, never bounds-checked + * here. Callers add a load base to them and build the mem_region_t ranges + * that decide RX vs RW page-table permissions (bootstrap.c + * append_elf_segment_regions, register_elf_segment_regions, and the exec.c + * region tables). That arithmetic is unproved. + * - The pread return-length checks and the interp_path handling are ordinary + * reviewed code. + */ + +/* a + b, or 0 when the sum does not fit in 64 bits. + * + * ELF address fields are unconstrained uint64_t, so the addresses derived from + * them (segment end, program header GPA) can only be formed with the carry + * checked. Saturating to UINT64_MAX instead is worse than rejecting: every + * consumer adds a load base to the result, so the clamp only relocates the wrap + * into the consumer, where the bound check it defeats reads "elf_end > + * guest_size" and silently passes. + */ +/*@ + requires \valid(sum); + assigns *sum; + ensures \result != 0 ==> *sum == a + b; + */ +static int elf_add_no_wrap(uint64_t a, uint64_t b, uint64_t *sum) +{ + if (a > UINT64_MAX - b) + return 0; + + *sum = a + b; + return 1; +} + +/* Size of the program header table in bytes, or 0 when the header geometry is + * unusable. Rejects an empty table, an entry stride too small to hold a program + * header, and a total past the kernel's 64KiB cap. + */ +/*@ + requires \valid(total); + assigns *total; + ensures \result != 0 ==> *total == (size_t) phnum * phentsize; + ensures \result != 0 ==> phentsize >= sizeof(elf64_phdr_t); + ensures \result != 0 ==> 0 < *total <= ELF_PHDR_TABLE_MAX; + */ +static int elf_phdr_table_bytes(uint16_t phnum, + uint16_t phentsize, + size_t *total) +{ + if (phnum == 0 || phentsize < sizeof(elf64_phdr_t)) + return 0; + + size_t bytes = (size_t) phnum * phentsize; + if (bytes > ELF_PHDR_TABLE_MAX) + return 0; + + *total = bytes; + return 1; +} + +/* Copy program header idx out of a buffer of buflen bytes. + * + * Returns 0 when the entry does not lie wholly inside the buffer. + * + * The contract below constrains the copy's SAFETY (the source range lies in the + * buffer), not its correctness (that *out holds those bytes). Stating the + * latter was tried and does not work: an ensures over ((char *) out)[k] is + * discharged vacuously, because WP's memory model does not relate byte-level + * access through a cast to the struct's typed contents. Verified by mutation: + * with the byte-equality postcondition in place, replacing this memcpy with + * memset(out, 0, sizeof(*out)) still proved every obligation. Do not restate it + * without re-running that mutation. + */ +/*@ + requires \valid_read(buf + (0 .. buflen - 1)); + requires \valid(out); + requires \separated(out, buf + (0 .. buflen - 1)); + requires phentsize >= sizeof(elf64_phdr_t); + assigns *out; + ensures \result != 0 ==> + (size_t) idx * phentsize + sizeof(elf64_phdr_t) <= buflen; + */ +static int elf_phdr_fetch(const uint8_t *buf, + size_t buflen, + uint16_t idx, + uint16_t phentsize, + elf64_phdr_t *out) +{ + size_t off = (size_t) idx * phentsize; + if (off > buflen || buflen - off < sizeof(*out)) + return 0; + + /* memcpy rather than an aliased struct pointer: e_phentsize is attacker + * controlled and need not be a multiple of the program header alignment, so + * buf + off is not guaranteed to be suitably aligned. + */ + memcpy(out, buf + off, sizeof(*out)); + return 1; +} + +/* Guest VA of the program header table, given one PT_LOAD's file range. + * + * Linux derives AT_PHDR from the PT_LOAD whose file data contains e_phoff + * (fs/binfmt_elf.c), not from the lowest mapped address. The two agree for the + * usual layout where the first PT_LOAD maps from file offset 0, and diverge + * otherwise. + * + * Returns 0 unless the whole table lies inside this segment's file data, which + * Returns 0 unless the whole table lies inside this segment's file data. Linux + * only requires e_phoff itself to be inside a PT_LOAD, but Linux keeps the + * headers reachable through the file mapping; elfuse dropped the separate phdr + * copy, so a table spanning two PT_LOADs would only stay readable if those + * segments happened to be adjacent in guest VA, which nothing checks. Requiring + * one segment to hold it all is what makes the no-copy scheme sound. + */ +/*@ + requires \valid(gpa_out); + assigns *gpa_out; + ensures \result != 0 ==> p_offset <= phoff; + ensures \result != 0 ==> phoff + total <= p_offset + p_filesz; + ensures \result != 0 ==> *gpa_out == p_vaddr + (phoff - p_offset); + */ +static int elf_phdr_gpa_in_segment(uint64_t phoff, + size_t total, + uint64_t p_offset, + uint64_t p_filesz, + uint64_t p_vaddr, + uint64_t *gpa_out) +{ + if (phoff < p_offset) + return 0; + + uint64_t rel = phoff - p_offset; + if (rel > p_filesz || p_filesz - rel < total) + return 0; + + return elf_add_no_wrap(p_vaddr, rel, gpa_out); +} + +/* Place one PT_LOAD segment in the guest slab. On success gpa_out is the + * relocated load address and zero_len_out is the extent the loader may touch, + * rounded up to the page boundary after the segment ends. Both outputs are + * bounded by guest_size, and zero_len_out is never smaller than filesz. + */ +/*@ + requires \valid(gpa_out); + requires \valid(zero_len_out); + requires \separated(gpa_out, zero_len_out); + assigns *gpa_out, *zero_len_out; + ensures \result != 0 ==> vaddr >= va_base; + ensures \result != 0 ==> *gpa_out == target_base + (vaddr - va_base); + ensures \result != 0 ==> *gpa_out + *zero_len_out <= guest_size; + ensures \result != 0 ==> memsz <= *zero_len_out; + ensures \result != 0 ==> filesz <= *zero_len_out; + */ +static int elf_segment_extent(uint64_t vaddr, + uint64_t va_base, + uint64_t target_base, + uint64_t filesz, + uint64_t memsz, + uint64_t guest_size, + uint64_t *gpa_out, + uint64_t *zero_len_out) +{ + /* Relocation is expressed as a window, not a pre-wrapped base: the segment + * at vaddr sits at target_base + (vaddr - va_base). + * + * The Rosetta translator links at 0x800000000000 and is mapped low, which + * rosetta.c used to arrange by passing load_base = guest_base - va_base and + * relying on the truncated sum. That is the same value this computes + * without any wrapping, so the pair states the intent the wrap only + * implied, and a guest ELF (va_base 0) can no longer reach an address by + * overflowing into it. + */ + if (vaddr < va_base) + return 0; + + uint64_t gpa; + if (!elf_add_no_wrap(target_base, vaddr - va_base, &gpa)) + return 0; + + /* A segment cannot contain more initialized file data than its in-memory + * extent. + */ + if (filesz > memsz) + return 0; + + /* Keep the mapped segment inside the configured IPA-sized guest slab. */ + if (memsz > guest_size || gpa > guest_size - memsz) + return 0; + + /* The loader zeros up to the next page boundary AFTER the segment ends, so + * the extent is PAGE_ALIGN_UP(gpa + memsz) rather than gpa + + * PAGE_ALIGN_UP(memsz): gpa is not always page-aligned (e.g. ld.so's RW + * segment at vaddr 0x2f650), and with the older bytes-from-gpa formula the + * page covering the last memsz byte kept its mid-page tail untouched. + * execve into a dynamic-linked target then read stale state from the prior + * incarnation of the same interpreter at offsets ld.so allocates beyond + * memsz (e.g. the first link_map in _dl_new_object). + */ + uint64_t end = gpa + memsz; + uint64_t aligned = PAGE_ALIGN_UP(end); + /* aligned < end catches the align-up carrying past UINT64_MAX. */ + if (aligned < end || aligned > guest_size) + aligned = guest_size; + + *gpa_out = gpa; + *zero_len_out = aligned - gpa; + return 1; +} + +/* Read a PT_INTERP segment's dynamic linker path into info->interp_path. + * + * Returns 0 on success, -1 when the path does not fit. The path lives in the + * file rather than in a loadable segment, so it is read while the ELF is still + * open. + */ +static int elf_read_interp(int fd, + const elf64_phdr_t *ph, + const char *display_path, + elf_info_t *info) +{ + size_t len = ph->p_filesz; + if (len >= sizeof(info->interp_path)) { + log_error("%s: PT_INTERP path too long (%zu >= %zu)", display_path, len, + sizeof(info->interp_path)); + return -1; + } + if (len == 0) + return 0; + + /* len counts the NUL stored in the file. A short read leaves the path + * unusable, so clear it rather than act on a truncated interpreter name; a + * full read is force-terminated as insurance. + */ + if (pread(fd, info->interp_path, len, ph->p_offset) < (ssize_t) len) + info->interp_path[0] = '\0'; + else + info->interp_path[len - 1] = '\0'; + return 0; +} + +/* Record one PT_LOAD segment and fold its extent into the load bounds. + * + * Returns 0 on success, -1 when the segment table is full or the extent wraps. + * seg_count is the caller's running total, kept out of info until the whole + * table parses so a rejected ELF leaves no partial segment list behind. + */ +static int elf_record_load(const elf64_phdr_t *ph, + const char *display_path, + uint16_t idx, + int *seg_count, + elf_info_t *info) +{ + /* Linux ignores a PT_LOAD that maps no bytes, and so does the mapper. + * Recording it anyway would still feed load_min/load_max, the boot region + * tables and /proc/self/maps: a zero-memsz segment at p_vaddr == + * guest_size satisfies the 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. + */ + if (ph->p_memsz == 0) + return 0; + + if (*seg_count >= ELF_MAX_SEGMENTS) { + log_error("%s: too many PT_LOAD segments", display_path); + return -1; + } + + /* A PT_LOAD whose extent wraps past the end of the address space is + * unloadable in any case, and it must be rejected here rather than + * saturated: consumers of load_max add a load base before comparing against + * guest_size (exec.c "ELF extends beyond guest address space"), so a + * UINT64_MAX sentinel wraps there and passes the very check it should trip. + */ + uint64_t seg_end; + if (!elf_add_no_wrap(ph->p_vaddr, ph->p_memsz, &seg_end)) { + log_error("%s: PT_LOAD %u extent 0x%llx+0x%llx wraps the address space", + display_path, idx, (unsigned long long) ph->p_vaddr, + (unsigned long long) ph->p_memsz); + return -1; + } + + int slot = *seg_count; + info->segments[slot].gpa = ph->p_vaddr; + info->segments[slot].offset = ph->p_offset; + info->segments[slot].filesz = ph->p_filesz; + info->segments[slot].memsz = ph->p_memsz; + info->segments[slot].flags = (int) ph->p_flags; + *seg_count = slot + 1; + + if (ph->p_vaddr < info->load_min) + info->load_min = ph->p_vaddr; + if (seg_end > info->load_max) + info->load_max = seg_end; + return 0; +} + int elf_load_fd(int fd, const char *display_path, elf_info_t *info) { memset(info, 0, sizeof(*info)); @@ -76,26 +382,19 @@ int elf_load_fd(int fd, const char *display_path, elf_info_t *info) info->load_min = UINT64_MAX; info->load_max = 0; - /* Program headers drive both memory mappings and auxv AT_PHDR. */ - if (ehdr.e_phnum == 0) { - log_error("%s: no program headers", display_path); - return -1; - } - if (ehdr.e_phentsize < sizeof(elf64_phdr_t)) { - log_error("%s: e_phentsize too small (%u < %zu)", display_path, - ehdr.e_phentsize, sizeof(elf64_phdr_t)); - return -1; - } - /* Linux kernel caps program headers at 64KiB. Reject pathological inputs - * before allocating to avoid attacker-controlled large allocations. + /* Program headers drive both memory mappings and auxv AT_PHDR. The table + * geometry is rejected before anything is allocated, so a pathological + * e_phnum/e_phentsize pair cannot drive a large attacker-chosen malloc. */ - if ((size_t) ehdr.e_phnum * ehdr.e_phentsize > 65536) { - log_error("%s: program header table too large (%u * %u)", display_path, - ehdr.e_phnum, ehdr.e_phentsize); + size_t ph_total; + if (!elf_phdr_table_bytes(ehdr.e_phnum, ehdr.e_phentsize, &ph_total)) { + log_error( + "%s: unusable program header table (e_phnum=%u, " + "e_phentsize=%u)", + display_path, ehdr.e_phnum, ehdr.e_phentsize); return -1; } - size_t ph_total = (size_t) ehdr.e_phnum * ehdr.e_phentsize; uint8_t *ph_buf = malloc(ph_total); if (!ph_buf) { perror("malloc"); @@ -104,82 +403,81 @@ int elf_load_fd(int fd, const char *display_path, elf_info_t *info) if (pread(fd, ph_buf, ph_total, ehdr.e_phoff) != (ssize_t) ph_total) { log_error("%s: failed to read program headers", display_path); - free(ph_buf); - return -1; + goto fail; } /* Collect only the program headers that affect process startup. */ int seg_count = 0; for (uint16_t i = 0; i < ehdr.e_phnum; i++) { - const elf64_phdr_t *ph = - (const elf64_phdr_t *) (ph_buf + (size_t) i * ehdr.e_phentsize); - - /* PT_INTERP stores the dynamic linker path in the file, not in a - * loadable segment, so read it before closing the ELF. + /* Zero-initialized so the phdr scratch is never read uninitialized + * on a path Pulse cannot follow; three of the suppressed Infer + * findings were here. One 56-byte clear per program header. */ - if (ph->p_type == PT_INTERP) { - size_t interp_len = ph->p_filesz; - if (interp_len >= sizeof(info->interp_path)) { - log_error("%s: PT_INTERP path too long (%zu >= %zu)", - display_path, interp_len, sizeof(info->interp_path)); - free(ph_buf); - return -1; - } - if (interp_len > 0) { - ssize_t n = - pread(fd, info->interp_path, interp_len, ph->p_offset); - /* interp_len includes the NUL from the ELF file. On short - * read, clear the path (unusable). On full read, - * force-terminate as insurance. - */ - if (n < (ssize_t) interp_len) - info->interp_path[0] = '\0'; - else - info->interp_path[interp_len - 1] = '\0'; - } + elf64_phdr_t ph = {0}; + if (!elf_phdr_fetch(ph_buf, ph_total, i, ehdr.e_phentsize, &ph)) { + log_error("%s: program header %u outside the header table", + display_path, i); + goto fail; } - if (ph->p_type == PT_LOAD) { - if (seg_count >= ELF_MAX_SEGMENTS) { - log_error("%s: too many PT_LOAD segments", display_path); - free(ph_buf); - return -1; - } + if (ph.p_type == PT_INTERP && + elf_read_interp(fd, &ph, display_path, info) < 0) + goto fail; - info->segments[seg_count].gpa = ph->p_vaddr; - info->segments[seg_count].offset = ph->p_offset; - info->segments[seg_count].filesz = ph->p_filesz; - info->segments[seg_count].memsz = ph->p_memsz; - info->segments[seg_count].flags = (int) ph->p_flags; - seg_count++; - - /* Track load bounds */ - if (ph->p_vaddr < info->load_min) - info->load_min = ph->p_vaddr; - uint64_t seg_end = ph->p_vaddr + ph->p_memsz; - if (seg_end < ph->p_vaddr) - seg_end = UINT64_MAX; /* overflow */ - if (seg_end > info->load_max) - info->load_max = seg_end; - } + if (ph.p_type == PT_LOAD && + elf_record_load(&ph, display_path, i, &seg_count, info) < 0) + goto fail; } info->num_segments = seg_count; if (seg_count == 0) { log_error("%s: no PT_LOAD segments", display_path); - free(ph_buf); - return -1; + goto fail; } - /* Store program header file offset for later phdr_gpa calculation. The - * loader places program headers at the same GPA as they would be in the - * first PT_LOAD segment (they are typically within it). + /* AT_PHDR, following Linux 5.19+ (commit 0da1d5002745, which replaced the + * older load_addr + e_phoff): the program headers are visible to the guest + * only because some PT_LOAD maps the file range they occupy, so their + * address comes from that segment. The two formulas agree for the usual + * layout where the first PT_LOAD starts at file offset 0. + * + * phdr_gpa stays 0 when no PT_LOAD covers the table, which is what Linux + * reports and what a hand-linked static binary with its phdrs outside the + * loaded range gets. Such a program cannot use AT_PHDR on Linux either, so + * there is nothing to deliver and the load is not an error. The old code + * instead memcpy'd the table to load_min + e_phoff, an address inside no + * segment: for build/test-hello that landed 0x1a bytes past the end of + * .text. + * + * Requiring the whole table inside one segment's file data is what lets + * elf_map_segments_fd deliver it with no separate copy and no second + * destination to bound-check. */ - info->phdr_gpa = info->load_min + ehdr.e_phoff; + /* A segment that covers e_phoff but whose p_vaddr + rel is + * unrepresentable is skipped rather than distinguished, so in principle + * the table could be attributed to a later segment. Unreachable: such a + * p_vaddr sits within a few bytes of UINT64_MAX, and elf_segment_extent + * rejects it at map time because every accepted segment satisfies + * gpa <= guest_size - memsz with guest_size at most 1 TiB, so phdr_gpa + * never reaches build_linux_stack. + */ + for (int i = 0; i < seg_count; i++) { + if (elf_phdr_gpa_in_segment(ehdr.e_phoff, ph_total, + info->segments[i].offset, + info->segments[i].filesz, + info->segments[i].gpa, &info->phdr_gpa)) { + info->phdr_valid = true; + break; + } + } free(ph_buf); return 0; + +fail: + free(ph_buf); + return -1; } int elf_load(const char *path, elf_info_t *info) @@ -199,7 +497,7 @@ int elf_map_segments_fd(const elf_info_t *info, const char *display_path, void *guest_base, uint64_t guest_size, - uint64_t load_base, + elf_window_t window, uint64_t infra_lo, uint64_t infra_hi) { @@ -210,127 +508,60 @@ int elf_map_segments_fd(const elf_info_t *info, */ bool infra_active = infra_lo < infra_hi; - /* Re-read ELF header to get phoff */ - elf64_ehdr_t ehdr; - if (pread(fd, &ehdr, sizeof(ehdr), 0) != sizeof(ehdr)) { - return -1; - } - - /* Read and parse program headers again to get file offsets. The size was - * already bound-checked during elf_load(); recheck defensively in case the - * header sizes changed since (e.g. corrupt file races). - */ - size_t ph_total = (size_t) ehdr.e_phnum * ehdr.e_phentsize; - if (ph_total == 0 || ph_total > 65536) { - return -1; - } - uint8_t *ph_buf = malloc(ph_total); - if (!ph_buf) { - return -1; - } - - if (pread(fd, ph_buf, ph_total, ehdr.e_phoff) != (ssize_t) ph_total) { - free(ph_buf); - return -1; - } - - /* Copy program headers into guest memory at phdr_gpa + load_base (needed - * for AT_PHDR auxv entry). Fail hard if they do not fit. A missing copy - * would leave AT_PHDR pointing at uninitialized memory, crashing the - * dynamic linker. + /* The layout comes entirely from the single parse in elf_load_fd. Do not + * re-read or re-parse the header here. * - * phdr_gpa + load_base may wrap via 2's complement for high-VA binaries. - * The bounds check below catches invalid results. - */ - uint64_t phdr_dest = info->phdr_gpa + load_base; - if (phdr_dest + ph_total < phdr_dest || phdr_dest + ph_total > guest_size) { - log_error( - "%s: program headers at 0x%llx exceed guest memory " - "(size 0x%llx)", - display_path, (unsigned long long) (phdr_dest + ph_total), - (unsigned long long) guest_size); - free(ph_buf); - return -1; - } - if (infra_active && phdr_dest < infra_hi && - phdr_dest + ph_total > infra_lo) { - log_error( - "%s: program headers at 0x%llx overlap infra reserve " - "[0x%llx, 0x%llx)", - display_path, (unsigned long long) phdr_dest, - (unsigned long long) infra_lo, (unsigned long long) infra_hi); - free(ph_buf); - return -1; - } - memcpy((uint8_t *) guest_base + phdr_dest, ph_buf, ph_total); - - /* Copy PT_LOAD contents after AT_PHDR is in place; ET_DYN segments are - * relocated by load_base before writing into guest memory. + * This function used to, and that was unsound rather than 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. A second parse + * then validates bytes that nothing downstream consumes: 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 program headers need no separate copy either. elf_load_fd sets + * phdr_gpa only to an address inside a PT_LOAD whose file data holds the + * whole table, so the segment read below delivers them at phdr_gpa + + * load_base as a side effect; when no segment covers the table phdr_gpa is + * 0 and AT_PHDR reports 0, as on Linux. Dropping that copy removed the last + * hand-written extent check in this file along with the second destination + * it guarded. */ - int seg_idx = 0; - for (uint16_t i = 0; i < ehdr.e_phnum && seg_idx < info->num_segments; - i++) { - const elf64_phdr_t *ph = - (const elf64_phdr_t *) (ph_buf + (size_t) i * ehdr.e_phentsize); - - if (ph->p_type != PT_LOAD) - continue; - - /* p_vaddr + load_base may wrap via 2's complement for high-VA binaries - * (see comment above). Bounds check below catches invalid results. - */ - uint64_t gpa = ph->p_vaddr + load_base, filesz = ph->p_filesz; - uint64_t memsz = ph->p_memsz; - - /* A segment cannot contain more initialized file data than its - * in-memory extent. - */ - if (filesz > memsz) { + for (int i = 0; i < info->num_segments; i++) { + uint64_t filesz = info->segments[i].filesz; + uint64_t memsz = info->segments[i].memsz; + uint64_t gpa, zero_len; + + if (!elf_segment_extent(info->segments[i].gpa, window.va_base, + window.target_base, filesz, memsz, guest_size, + &gpa, &zero_len)) { log_error( - "%s: segment at 0x%llx has filesz > memsz " - "(0x%llx > 0x%llx)", - display_path, (unsigned long long) gpa, - (unsigned long long) filesz, (unsigned long long) memsz); - free(ph_buf); - return -1; - } - - /* Keep the mapped segment inside the configured IPA-sized guest slab. - */ - if (memsz > guest_size || gpa > guest_size - memsz) { - log_error("%s: segment at 0x%llx+0x%llx exceeds guest memory", - display_path, (unsigned long long) gpa, - (unsigned long long) memsz); - free(ph_buf); + "%s: segment vaddr 0x%llx (memsz 0x%llx, filesz 0x%llx) is " + "not loadable: %s [window va_base 0x%llx target 0x%llx, guest " + "size 0x%llx]", + display_path, (unsigned long long) info->segments[i].gpa, + (unsigned long long) memsz, (unsigned long long) filesz, + info->segments[i].gpa < window.va_base + ? "below the relocation window" + : (filesz > memsz ? "filesz exceeds memsz" + : "does not fit guest memory"), + (unsigned long long) window.va_base, + (unsigned long long) window.target_base, + (unsigned long long) guest_size); return -1; } /* PT_LOAD with memsz == 0 maps no bytes, but the page-tail zero extent - * below still rounds up to the next page boundary. For an unaligned gpa - * that means a crafted ELF could splat zeros across the tail of a - * previously loaded segment in the same page, or trip the infra-overlap - * check with no live mapping behind it. Linux ignores zero-memsz - * PT_LOADs; mirror that here. + * still rounds up to the next page boundary. For an unaligned gpa that + * means a crafted ELF could splat zeros across the tail of a previously + * loaded segment in the same page, or trip the infra-overlap check with + * no live mapping behind it. Linux ignores zero-memsz PT_LOADs; mirror + * that here. */ - if (memsz == 0) { - seg_idx++; + if (memsz == 0) continue; - } - /* The host memset zeros up to the next page boundary AFTER the segment - * ends, so the infra-overlap check has to use the same rounded extent. - * The end is PAGE_ALIGN_UP(gpa + memsz) rather than gpa + - * PAGE_ALIGN_UP(memsz) because gpa is not always page-aligned (e.g. - * ld.so's RW segment at vaddr 0x2f650): with the older bytes-from-gpa - * formula the page covering the last memsz byte kept its mid-page tail - * untouched, and execve into a dynamic-linked target then read stale - * state from the prior incarnation of the same interpreter at offsets - * ld.so allocates from beyond memsz (e.g. the first link_map in - * _dl_new_object). - */ - uint64_t zero_len = PAGE_ALIGN_UP(gpa + memsz) - gpa; - if (gpa + zero_len > guest_size) - zero_len = guest_size - gpa; if (infra_active && gpa < infra_hi && gpa + zero_len > infra_lo) { log_error( "%s: segment at 0x%llx+0x%llx (zero-extent 0x%llx) overlaps " @@ -338,14 +569,13 @@ int elf_map_segments_fd(const elf_info_t *info, display_path, (unsigned long long) gpa, (unsigned long long) memsz, (unsigned long long) zero_len, (unsigned long long) infra_lo, (unsigned long long) infra_hi); - free(ph_buf); return -1; } /* Zero only the tail beyond filesz: the BSS portion [filesz, memsz) * plus the page-padding [memsz, zero_len) that Linux guarantees clean * for dynamic linkers allocating from the last mapped page's tail. - * Skipping the file-data range avoids writing zeros that the fread + * Skipping the file-data range avoids writing zeros that the pread * below would immediately overwrite; for typical shared libraries that * is a hundreds-of-KiB win per segment. */ @@ -353,22 +583,18 @@ int elf_map_segments_fd(const elf_info_t *info, memset((uint8_t *) guest_base + gpa + filesz, 0, zero_len - filesz); if (filesz > 0) { - if (pread(fd, (uint8_t *) guest_base + gpa, filesz, ph->p_offset) != - (ssize_t) filesz) { + if (pread(fd, (uint8_t *) guest_base + gpa, filesz, + info->segments[i].offset) != (ssize_t) filesz) { log_error( "%s: short read for segment at 0x%llx " "(expected %llu)", display_path, (unsigned long long) gpa, (unsigned long long) filesz); - free(ph_buf); return -1; } } - - seg_idx++; } - free(ph_buf); return 0; } @@ -376,7 +602,7 @@ int elf_map_segments(const elf_info_t *info, const char *path, void *guest_base, uint64_t guest_size, - uint64_t load_base, + elf_window_t window, uint64_t infra_lo, uint64_t infra_hi) { @@ -385,8 +611,8 @@ int elf_map_segments(const elf_info_t *info, perror(path); return -1; } - int rc = elf_map_segments_fd(info, fd, path, guest_base, guest_size, - load_base, infra_lo, infra_hi); + int rc = elf_map_segments_fd(info, fd, path, guest_base, guest_size, window, + infra_lo, infra_hi); close(fd); return rc; } diff --git a/src/core/elf.h b/src/core/elf.h index 0361785f..47ea3861 100644 --- a/src/core/elf.h +++ b/src/core/elf.h @@ -11,6 +11,7 @@ #pragma once +#include #include #include @@ -67,6 +68,12 @@ typedef struct { uint64_t p_offset, p_vaddr, p_paddr, p_filesz, p_memsz, p_align; } elf64_phdr_t; +/* Upper bound on the program header table, matching the Linux kernel's 64KiB + * cap (fs/binfmt_elf.c). e_phnum and e_phentsize come straight from an + * untrusted file, so the product is rejected before anything is allocated. + */ +#define ELF_PHDR_TABLE_MAX 65536 + /* Loaded ELF info */ #define ELF_MAX_SEGMENTS 16 @@ -83,8 +90,14 @@ typedef struct { uint64_t load_min; /* Lowest loaded GPA (page-aligned) */ uint64_t load_max; /* Highest loaded GPA + memsz (page-aligned up) */ - /* Program headers location in guest memory (for AT_PHDR auxv) */ - uint64_t phdr_gpa; /* GPA of program headers in guest memory */ + /* GPA of the program headers, derived from the PT_LOAD whose file data + * contains them. Only meaningful when phdr_valid is set: an ET_DYN image + * whose covering segment has p_vaddr == 0 and p_offset == e_phoff yields a + * legitimate phdr_gpa of 0, which a zero sentinel could not tell apart from + * "no segment covers the table". + */ + uint64_t phdr_gpa; + bool phdr_valid; /* PT_INTERP: dynamic linker path (empty if statically linked) */ char interp_path[256]; @@ -100,6 +113,19 @@ typedef struct { } segments[ELF_MAX_SEGMENTS]; } elf_info_t; +/* Where a loaded image lands: a segment at p_vaddr goes to + * target_base + (p_vaddr - va_base). + * + * A struct rather than two uint64_t parameters on purpose. They were adjacent + * same-typed arguments once, and a signature change left three call sites + * passing the old shape: identical arity, all integers, so it compiled clean + * and broke every exec path. Naming the fields makes that a compile error. + */ +typedef struct { + uint64_t va_base; /* lowest p_vaddr the image is described against */ + uint64_t target_base; /* GPA that va_base maps to */ +} elf_window_t; + /* API */ /* Load and parse an ELF64 file. Validates header, extracts PT_LOAD info. @@ -109,21 +135,27 @@ int elf_load(const char *path, elf_info_t *info); int elf_load_fd(int fd, const char *display_path, elf_info_t *info); /* Copy ELF segments into guest memory. Call after elf_load() and guest_init(). - * Also copies program headers into guest memory for AT_PHDR. load_base is added - * to all virtual addresses (0 for ET_EXEC at link addr, non-zero for ET_DYN - * loaded at a chosen base). infra_lo and infra_hi delimit the runtime infra - * reserve (page-table pool, shim text, shim_data, vDSO). Any PT_LOAD or PT_PHDR - * copy whose destination intersects [infra_lo, infra_hi) is rejected: those - * writes go through host_base directly and would otherwise bypass the EL1-only - * page-table protection on shim_data. Pass 0,0 only when the guest_t is not yet - * built. - * Returns 0 on success, -1 on failure. + * + * Reads nothing from the file but the segment contents: the layout comes + * entirely from info, filled by the single parse in elf_load(). The program + * headers need no separate copy because elf_load() only sets phdr_gpa to an + * address inside a PT_LOAD, so the segment read here delivers them. + * + * Guest images pass a window of {0, load_base} (load_base 0 for ET_EXEC at its + * link address, non-zero for ET_DYN). Rosetta passes its own va_base so its + * 0x800000000000 link address maps low without relying on unsigned + * wraparound. infra_lo and infra_hi + * delimit the runtime infra reserve (page-table pool, shim text, shim_data, + * vDSO). Any PT_LOAD copy whose destination intersects [infra_lo, infra_hi) is + * rejected: those writes go through host_base directly and would otherwise + * bypass the EL1-only page-table protection on shim_data. Pass 0,0 only when + * the guest_t is not yet built. Returns 0 on success, -1 on failure. */ int elf_map_segments(const elf_info_t *info, const char *path, void *guest_base, uint64_t guest_size, - uint64_t load_base, + elf_window_t window, uint64_t infra_lo, uint64_t infra_hi); int elf_map_segments_fd(const elf_info_t *info, @@ -131,7 +163,7 @@ int elf_map_segments_fd(const elf_info_t *info, const char *display_path, void *guest_base, uint64_t guest_size, - uint64_t load_base, + elf_window_t window, uint64_t infra_lo, uint64_t infra_hi); diff --git a/src/core/guest.c b/src/core/guest.c index 2bf395e0..eb73d4e7 100644 --- a/src/core/guest.c +++ b/src/core/guest.c @@ -40,6 +40,7 @@ #include #include "core/guest.h" +#include "core/gva-math.h" #include "core/startup-trace.h" #include "debug/log.h" #include "utils.h" @@ -207,9 +208,36 @@ static uint64_t pt_alloc_page(guest_t *g) return gpa; } -/* Get host pointer to a page table entry array at a given GPA */ +/* Get host pointer to a page table entry array at a given GPA. + * + * Every caller indexes a full 4 KiB table (512 descriptors) from the result, so + * the whole table must fit inside the primary buffer, not merely its first + * byte. The walker screens descriptors through gva_pt_table_offset before + * getting here, but the ~20 other call sites -- find_l2_entry, + * guest_map_va_range, guest_extend_page_tables, guest_invalidate_ptes, + * guest_update_perms, guest_install_va_pages, and the ttbr0 roots -- derive the + * offset with a bare "ipa - base" and no bound at all, and unlike the walker + * they WRITE descriptors. + * + * Bounding here rather than at each of those sites keeps one check instead of + * twenty and cannot be forgotten by the next one added. A violation is not a + * guest-reachable condition (every descriptor value originates from + * pt_alloc_page, and the PT pool is absent from the boot region set so EL0 + * cannot map it) -- it means the pool allocator itself is broken, which is + * unrecoverable and must not be allowed to scribble outside the slab. + */ static uint64_t *pt_at(const guest_t *g, uint64_t gpa) { + /* Underflow guard first, matching gva_pt_table_offset. Written the other + * way round the subtraction wraps for a sub-page slab and the comparison + * silently passes, leaving the second clause to catch it by luck. + */ + if (g->guest_size < GVA_PT_TABLE_BYTES || + gpa > g->guest_size - GVA_PT_TABLE_BYTES) { + log_fatal("pt_at: page table offset 0x%llx outside the %llu-byte slab", + (unsigned long long) gpa, (unsigned long long) g->guest_size); + abort(); + } return (uint64_t *) ((uint8_t *) g->host_base + gpa); } @@ -1308,19 +1336,19 @@ static int gva_translate_perm(const guest_t *g, if (!(l0e & PT_VALID)) return -1; - uint64_t l1_ipa = l0e & 0xFFFFFFFFF000ULL; - if (l1_ipa < base || l1_ipa - base >= g->guest_size) + uint64_t l1_off; + if (!gva_pt_table_offset(l0e, base, g->guest_size, &l1_off)) return -1; - const uint64_t *l1 = pt_at(g, l1_ipa - base); + const uint64_t *l1 = pt_at(g, l1_off); unsigned l1_idx = (unsigned) ((gva / BLOCK_1GIB) % 512); uint64_t l1e = pte_load_acquire(&l1[l1_idx]); if (!(l1e & PT_VALID)) return -1; - uint64_t l2_ipa = l1e & 0xFFFFFFFFF000ULL; - if (l2_ipa < base || l2_ipa - base >= g->guest_size) + uint64_t l2_off; + if (!gva_pt_table_offset(l1e, base, g->guest_size, &l2_off)) return -1; - const uint64_t *l2 = pt_at(g, l2_ipa - base); + const uint64_t *l2 = pt_at(g, l2_off); unsigned l2_idx = (unsigned) ((gva / BLOCK_2MIB) % 512); uint64_t l2e = pte_load_acquire(&l2[l2_idx]); if (!(l2e & PT_VALID)) @@ -1328,10 +1356,10 @@ static int gva_translate_perm(const guest_t *g, if (l2e & PT_TABLE) { /* L3 page descriptor: 4KiB granularity. */ - uint64_t l3_ipa = l2e & 0xFFFFFFFFF000ULL; - if (l3_ipa < base || l3_ipa - base >= g->guest_size) + uint64_t l3_off; + if (!gva_pt_table_offset(l2e, base, g->guest_size, &l3_off)) return -1; - const uint64_t *l3 = pt_at(g, l3_ipa - base); + const uint64_t *l3 = pt_at(g, l3_off); unsigned l3_idx = (unsigned) ((gva / PAGE_SIZE) % 512); uint64_t l3e = pte_load_acquire(&l3[l3_idx]); if (!(l3e & PT_VALID)) @@ -1351,10 +1379,10 @@ static int gva_translate_perm(const guest_t *g, if ((perms & required_perms) != required_perms) return -1; - uint64_t page_ipa = l3e & 0xFFFFFFFFF000ULL; - if (page_ipa < base) + uint64_t page_ipa = l3e & GVA_PT_ADDR_MASK; + uint64_t gpa, leaf_chunk; + if (!gva_leaf_target(page_ipa, base, gva, PAGE_SIZE, &gpa, &leaf_chunk)) return -1; - uint64_t gpa = (page_ipa - base) + (gva & (PAGE_SIZE - 1)); /* Accept GPAs inside the primary buffer or covered by an extra IPA * mapping (rosetta segments, kbuf, etc.). Anything else is a dangling @@ -1365,7 +1393,7 @@ static int gva_translate_perm(const guest_t *g, return -1; out->gpa = gpa; - out->chunk = PAGE_SIZE - (gva & (PAGE_SIZE - 1)); + out->chunk = leaf_chunk; /* Populate TLB cache for this 4KiB page */ gva_tlb.owner = g; @@ -1390,15 +1418,15 @@ static int gva_translate_perm(const guest_t *g, return -1; uint64_t block_ipa = l2e & L2_BLOCK_ADDR_MASK; - if (block_ipa < base) + uint64_t gpa, leaf_chunk; + if (!gva_leaf_target(block_ipa, base, gva, BLOCK_2MIB, &gpa, &leaf_chunk)) return -1; - uint64_t gpa = (block_ipa - base) + (gva & (BLOCK_2MIB - 1)); if (gpa >= g->guest_size && !guest_find_mapping(g, gpa) && !guest_find_overflow(g, gpa)) return -1; out->gpa = gpa; - out->chunk = BLOCK_2MIB - (gva & (BLOCK_2MIB - 1)); + out->chunk = leaf_chunk; /* Populate TLB cache for this 2MiB block */ gva_tlb.owner = g; @@ -1445,10 +1473,18 @@ static uint64_t gva_contiguous_avail(const guest_t *g, region_end = o->ipa_start + o->size; } } - if (chunk > region_end - cur.gpa) - chunk = region_end - cur.gpa; - if (chunk > limit - total) - chunk = limit - total; + + /* gva_chunk_clamp requires gpa < region_end, and nothing checks that: + * guest.c cannot be handed to Frama-C, so its call sites are outside + * the proof. Violating it would clamp chunk to 0, make this function + * return 0 for a non-NULL translation, and spin guest_copy forever on a + * guest-supplied address. Every path that reaches here satisfies it + * today; this makes that structural rather than argued. + */ + if (region_end <= cur.gpa) + break; + + chunk = gva_chunk_clamp(chunk, cur.gpa, region_end, limit, total); total += chunk; if (total == limit) @@ -1495,12 +1531,29 @@ static void *gva_resolve_perm(const guest_t *g, if (gva_translate_perm(g, gva, required_perms, &first) < 0) return NULL; - if (avail) { - *avail = - gva_contiguous_avail(g, gva, required_perms, &first, avail_limit); - } - if (first.gpa < g->guest_size) + /* Computed once and clamped once per branch below. Writing *avail twice + * (here, then again in the branch) left the analyzers unable to relate the + * final value to the returned pointer. + */ + uint64_t bytes = avail ? gva_contiguous_avail(g, gva, required_perms, + &first, avail_limit) + : 0; + + if (first.gpa < g->guest_size) { + /* Clamp to the end of the primary buffer, the same way the mapping and + * overflow branches below clamp to the end of the region their pointer + * points into. gva_contiguous_avail only stops at guest_size when the + * clamp shortens a chunk, so a leaf whose extent ends flush with + * guest_size lets the walk continue into whatever the next descriptor + * resolves to, and the caller's memcpy would run off the end of the + * host buffer. + */ + if (avail) { + uint64_t cap = g->guest_size - first.gpa; + *avail = bytes < cap ? bytes : cap; + } return (uint8_t *) g->host_base + first.gpa; + } /* GPA outside the primary buffer: consult the extra IPA mappings (rosetta * segments, kbuf) first, then the overflow segments (lazy 1 GiB bump @@ -1512,8 +1565,7 @@ static void *gva_resolve_perm(const guest_t *g, if (m) { if (avail) { uint64_t cap = (m->gpa + m->size) - first.gpa; - if (*avail > cap) - *avail = cap; + *avail = bytes < cap ? bytes : cap; } return (uint8_t *) m->host_va + (first.gpa - m->gpa); } @@ -1521,8 +1573,7 @@ static void *gva_resolve_perm(const guest_t *g, if (o) { if (avail) { uint64_t cap = (o->ipa_start + o->size) - first.gpa; - if (*avail > cap) - *avail = cap; + *avail = bytes < cap ? bytes : cap; } return (uint8_t *) o->host_base + (first.gpa - o->ipa_start); } @@ -1568,7 +1619,7 @@ static inline int guest_copy(const guest_t *g, if ((required_perms == MEM_PERM_R && !dst) || (required_perms == MEM_PERM_W && !src)) return -1; - if (gva > UINT64_MAX - len) + if (!gva_span_ok(gva, len)) return -1; size_t copied = 0; diff --git a/src/core/gva-math.h b/src/core/gva-math.h new file mode 100644 index 00000000..96e91096 --- /dev/null +++ b/src/core/gva-math.h @@ -0,0 +1,169 @@ +/* + * Guest address arithmetic: the parts a proof can reach + * + * Copyright 2026 elfuse contributors + * SPDX-License-Identifier: Apache-2.0 + * + * Every offset and window computed from a guest address before the host + * dereferences it. A guest controls the address, the length, and (through + * mmap/mprotect) much of the page-table content these read, so an arithmetic + * slip here is a host out-of-bounds access rather than a guest fault. + * + * Split out of guest.c because guest.c cannot be given to Frama-C at all: it + * includes sys/sysctl.h and Hypervisor.framework, which the analyzer's libc + * does not model. These functions need nothing but stdint.h, so `make + * verify-gva` proves this header directly. + * + * static inline rather than a separate translation unit on purpose: + * gva_translate_perm runs on every guest pointer access, and + * tests/bench-hot-guard.c holds that path to a ceiling. + * + * Offsets within a granule use "% granule" rather than "& (granule - 1)". For + * the power-of-two granules in play the compiler emits the same instruction, + * and the prover reasons about the arithmetic form without first having to + * establish the mask is one less than a power of two. + */ + +#pragma once + +#include + +/* Output-address field of a page-table descriptor (bits [47:12]). */ +#define GVA_PT_ADDR_MASK 0xFFFFFFFFF000ULL + +/* Offset within the primary buffer of the table a descriptor points at, or 0 + * when the descriptor points outside it. + * + * A table descriptor must land inside the primary buffer: the walker reads the + * next level straight out of it. Leaf descriptors are different and go through + * gva_leaf_target instead, because a leaf may name a GPA in an extra IPA + * mapping (Rosetta segments, kbuf) that the caller looks up rather than one + * this function can bound. That lookup is currently a dormant path: + * guest_add_mapping and guest_overflow_alloc have no callers in the tree, so + * n_mappings and noverflow stay 0 and every accepted leaf resolves inside the + * primary buffer. The split is kept because wiring either back up must not + * require revisiting this bound. A page table is a full 4 KiB of descriptors + * and the walker indexes all 512 of them, so the whole table must fit, not + * merely its first byte. "*off < guest_size" would be satisfied by off == + * guest_size - 8, which puts l1[511] past the end of the slab. + */ +#define GVA_PT_TABLE_BYTES 4096ULL + +/*@ + requires \valid(off); + assigns *off; + ensures \result == 0 || \result == 1; + ensures \result != 0 ==> *off + GVA_PT_TABLE_BYTES <= guest_size; + ensures \result != 0 ==> *off == (desc & GVA_PT_ADDR_MASK) - base; + ensures \result != 0 <==> + ((desc & GVA_PT_ADDR_MASK) >= base && + (desc & GVA_PT_ADDR_MASK) - base + GVA_PT_TABLE_BYTES + <= guest_size); + */ +static inline int gva_pt_table_offset(uint64_t desc, + uint64_t base, + uint64_t guest_size, + uint64_t *off) +{ + uint64_t ipa = desc & GVA_PT_ADDR_MASK; + if (ipa < base) + return 0; + + uint64_t candidate = ipa - base; + if (guest_size < GVA_PT_TABLE_BYTES || + candidate > guest_size - GVA_PT_TABLE_BYTES) + return 0; + + *off = candidate; + return 1; +} + +/* Guest physical address and remaining-bytes-in-granule for a leaf descriptor. + * + * chunk is what stops the copy loops from spinning: it is at least 1 for any + * accepted descriptor, so every iteration makes progress. Takes the + * descriptor's output address already masked, rather than the descriptor and a + * mask: the two leaf kinds use different masks (page vs 2MiB block), and + * keeping the bitwise step outside means the contract never has to reason about + * "desc & addr_mask" with both operands symbolic, which Z3 does not discharge. + */ +/*@ + requires 0 < granule <= GVA_PT_ADDR_MASK; + requires ipa <= GVA_PT_ADDR_MASK; + requires \valid(gpa); + requires \valid(chunk); + requires \separated(gpa, chunk); + assigns *gpa, *chunk; + ensures \result == 0 || \result == 1; + ensures \result != 0 <==> ipa >= base; + ensures \result != 0 ==> 1 <= *chunk <= granule; + ensures \result != 0 ==> *chunk == granule - gva % granule; + ensures \result != 0 ==> *gpa == ipa - base + gva % granule; + */ +static inline int gva_leaf_target(uint64_t ipa, + uint64_t base, + uint64_t gva, + uint64_t granule, + uint64_t *gpa, + uint64_t *chunk) +{ + if (ipa < base) + return 0; + + uint64_t offset = gva % granule; + *gpa = (ipa - base) + offset; + *chunk = granule - offset; + return 1; +} + +/* Bytes copyable in one step: the smallest of what the descriptor grants, what + * remains in the backing region, and what the caller still wants. + * + * The preconditions are what the caller must already know, and the + * postcondition that the result is at least 1 is what makes the surrounding + * loop terminate. + * + * The last clause (below every bound AND equal to one of them) pins the result + * to the minimum. Without it an implementation that always returns 1 satisfies + * every other clause: still safe, but it would copy a byte at a time forever. + */ +/*@ + requires chunk >= 1; + requires gpa < region_end; + requires total < limit; + assigns \nothing; + ensures 1 <= \result <= chunk; + ensures \result <= region_end - gpa; + ensures \result <= limit - total; + ensures \result == chunk || \result == region_end - gpa || + \result == limit - total; + */ +static inline uint64_t gva_chunk_clamp(uint64_t chunk, + uint64_t gpa, + uint64_t region_end, + uint64_t limit, + uint64_t total) +{ + if (chunk > region_end - gpa) + chunk = region_end - gpa; + if (chunk > limit - total) + chunk = limit - total; + return chunk; +} + +/* Whether [gva, gva + len) is a non-empty span that does not wrap. + * + * Checked before any copy loop starts, so that gva + copied cannot wrap partway + * through and resolve to an unrelated address. + */ +/*@ + assigns \nothing; + ensures \result == 0 || \result == 1; + ensures \result != 0 <==> (len != 0 && gva + len <= 0xFFFFFFFFFFFFFFFF); + */ +static inline int gva_span_ok(uint64_t gva, uint64_t len) +{ + if (len == 0) + return 0; + return gva <= UINT64_MAX - len; +} diff --git a/src/core/rosetta.c b/src/core/rosetta.c index 2a93eaaa..c8a3871d 100644 --- a/src/core/rosetta.c +++ b/src/core/rosetta.c @@ -257,16 +257,15 @@ int rosetta_prepare(guest_t *g, return -1; } - /* Load rosetta into the primary buffer. load_base = guest_base - - * va_base places p_vaddr+load_base inside host_base+guest_base. The - * wrap math is the same trick elf.c documents for high-VA binaries: - * uint64_t arithmetic, two's-complement intentional. + /* Load rosetta into the primary buffer: the [va_base, ...) window of + * the image lands at guest_base. Passing the pair rather than a + * pre-subtracted base keeps the arithmetic free of wraparound. */ - uint64_t load_base = guest_base - va_base; uint64_t infra_lo = g->interp_base - INFRA_RESERVE; uint64_t infra_hi = g->interp_base; if (elf_map_segments(ri, ROSETTA_PATH, g->host_base, g->guest_size, - load_base, infra_lo, infra_hi) < 0) { + (elf_window_t) {va_base, guest_base}, infra_lo, + infra_hi) < 0) { log_error("rosetta: elf_map_segments failed"); return -1; } @@ -312,11 +311,11 @@ int rosetta_prepare(guest_t *g, * be rebuilt. Segments get reloaded in place. */ guest_base = g->rosetta_guest_base; - uint64_t load_base = guest_base - va_base; uint64_t infra_lo = g->interp_base - INFRA_RESERVE; uint64_t infra_hi = g->interp_base; if (elf_map_segments(ri, ROSETTA_PATH, g->host_base, g->guest_size, - load_base, infra_lo, infra_hi) < 0) { + (elf_window_t) {va_base, guest_base}, infra_lo, + infra_hi) < 0) { log_error("rosetta: re-entry elf_map_segments failed"); return -1; } diff --git a/src/core/stack.c b/src/core/stack.c index 06fa87e7..ff3c7502 100644 --- a/src/core/stack.c +++ b/src/core/stack.c @@ -267,6 +267,7 @@ uint64_t build_linux_stack(guest_t *g, do { \ stack_err |= push_u64(g, &sp, (val)); \ } while (0) + /* Serialize auxv once, then push it in reverse so guest memory and * /proc/self/auxv expose the same bytes. */ @@ -282,7 +283,14 @@ uint64_t build_linux_stack(guest_t *g, if (vdso_base != 0) AUX(AT_SYSINFO_EHDR, vdso_base); AUX(AT_PAGESZ, 4096); - AUX(AT_PHDR, elf_info->phdr_gpa + elf_load_base); + + /* phdr_valid is false when no PT_LOAD covers the program header table, so + * there is no guest address to report and Linux passes AT_PHDR 0. Testing + * phdr_gpa itself would be wrong: 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 elf_load_base. + */ + AUX(AT_PHDR, elf_info->phdr_valid ? elf_info->phdr_gpa + elf_load_base : 0); AUX(AT_PHENT, elf_info->phentsize); AUX(AT_PHNUM, elf_info->phnum); AUX(AT_ENTRY, elf_info->entry + elf_load_base); @@ -290,6 +298,7 @@ uint64_t build_linux_stack(guest_t *g, AUX(AT_EUID, proc_get_euid()); AUX(AT_GID, proc_get_gid()); AUX(AT_EGID, proc_get_egid()); + /* Bionic's __libc_init_AT_SECURE aborts when AT_SECURE is absent. elfuse * never elevates privileges, so AT_SECURE is always 0. */ diff --git a/src/debug/gdbstub-rsp.c b/src/debug/gdbstub-rsp.c index b0db730d..50bdd8f3 100644 --- a/src/debug/gdbstub-rsp.c +++ b/src/debug/gdbstub-rsp.c @@ -23,36 +23,191 @@ int gdb_hex_encode(char *dst, const uint8_t *src, size_t len) return (int) bytes_to_hex(dst, src, len); } +/* Combine two hex digits into a byte. + * + * Returns 0 when either is not a hex digit, leaving *out untouched. + * + * Both nibbles are validated before either is shifted. hex_nibble returns -1 + * for a non-digit, and shifting a negative int left is undefined behavior, so + * the obvious "(hex_nibble(hi) << 4) | hex_nibble(lo)" is UB on any input the + * remote sends that is not hex. The remote controls these bytes completely. + */ +/*@ predicate is_hex_digit(integer c) = + ('0' <= c <= '9') || ('a' <= c <= 'f') || ('A' <= c <= 'F'); + */ +/*@ + requires \valid(out); + assigns *out; + ensures \result == 0 || \result == 1; + ensures \result != 0 <==> (is_hex_digit((unsigned char) hi) && + is_hex_digit((unsigned char) lo)); + ensures \result != 0 ==> *out == 16 * hex_val((unsigned char) hi) + + hex_val((unsigned char) lo); + */ +static int gdb_hex_pair(char hi, char lo, uint8_t *out) +{ + int h = hex_nibble((unsigned char) hi); + if (h < 0) + return 0; + + int l = hex_nibble((unsigned char) lo); + if (l < 0) + return 0; + + /* Unsigned arithmetic, and "* 16 +" rather than "<< 4 |": a signed left + * shift that overflows is undefined, and the prover reasons about the + * arithmetic form directly whereas the bitwise OR needs it to first + * establish that the two operands do not share bits. + */ + *out = (uint8_t) ((unsigned int) h * 16u + (unsigned int) l); + return 1; +} + +/* Decode len bytes from 2*len hex digits. + * + * Returns len, or -1 on the first non-hex digit. + * + * The caller must supply 2*len readable digits; nothing here can check that, + * which is why the contract states it. Decoding stops at the first bad digit + * without reading its partner: the pair used to be read together before either + * was validated, so a NUL landing on an even index caused a one-byte read past + * it, and gdb_rsp_recv can place that NUL at the last byte of the packet + * buffer. + */ +/*@ + requires len <= INT_MAX; + requires \valid(dst + (0 .. len - 1)); + requires \valid_read(src + (0 .. 2 * len - 1)); + requires \separated(dst + (0 .. len - 1), src + (0 .. 2 * len - 1)); + assigns dst[0 .. len - 1]; + ensures \result == -1 || \result == (int) len; + ensures \result != -1 <==> + (\forall integer k; 0 <= k < 2 * len ==> + is_hex_digit((unsigned char) src[k])); + ensures \result != -1 ==> + (\forall integer k; 0 <= k < len ==> + dst[k] == 16 * hex_val((unsigned char) src[2 * k]) + + hex_val((unsigned char) src[2 * k + 1])); + */ int gdb_hex_decode(uint8_t *dst, const char *src, size_t len) { + /*@ + loop invariant 0 <= i <= len; + loop invariant \forall integer k; 0 <= k < 2 * i ==> + is_hex_digit((unsigned char) src[k]); + loop invariant \forall integer k; 0 <= k < i ==> + dst[k] == 16 * hex_val((unsigned char) src[2 * k]) + + hex_val((unsigned char) src[2 * k + 1]); + loop assigns i, dst[0 .. len - 1]; + loop variant len - i; + */ for (size_t i = 0; i < len; i++) { - int hi = hex_nibble((unsigned char) src[i * 2]), - lo = hex_nibble((unsigned char) src[i * 2 + 1]); - if (hi < 0 || lo < 0) + /* Read the digits in order and bail between them. Handing both to + * gdb_hex_pair would not do: C evaluates both arguments before the + * call, so the low digit gets read before the high one is rejected, + * which is the overread this loop is supposed to avoid. + */ + int hi = hex_nibble((unsigned char) src[i * 2]); + if (hi < 0) return -1; - dst[i] = (uint8_t) ((hi << 4) | lo); + + int lo = hex_nibble((unsigned char) src[i * 2 + 1]); + if (lo < 0) + return -1; + + dst[i] = (uint8_t) ((unsigned int) hi * 16u + (unsigned int) lo); } return (int) len; } +/* Consume a run of hex digits and return its value, advancing *pp past them. + * + * The scan is bounded only by the terminating NUL, so the caller must pass a + * NUL-terminated string; gdb_rsp_recv guarantees that for every packet it + * returns. The contract states it rather than leaving it to the reader. + * + * NOT proved: the returned value. Specifying it needs a recursive logic + * function over the digit run, and the resulting loop invariant (which must + * relate the accumulator to a pointer-offset expression through a modulo-2^64 + * fold) times out in Z3 even at 120s. What is proved here is memory safety, + * termination, and that *pp only advances within the same object. The value is + * covered end to end by tests/test-gdbstub.sh, whose memory and register cases + * cannot pass if addresses parse wrongly. + * + * More than 16 digits wraps, which is deliberate and matches gdbserver: the + * value feeds addresses and lengths that every caller bound-checks against + * guest memory anyway, so a wrapped value is rejected downstream rather than + * here, where refusing it would change the parse position. + */ +/*@ + requires \valid(pp); + requires valid_read_string(*pp); + assigns *pp; + ensures valid_read_string(*pp); + ensures \base_addr(*pp) == \base_addr(\old(*pp)); + ensures \offset(*pp) >= \offset(\old(*pp)); + */ uint64_t gdb_parse_hex(const char **pp) { const char *p = *pp; uint64_t val = 0; + + /*@ + loop invariant valid_read_string(p); + loop invariant \base_addr(p) == \base_addr(\at(*pp, Pre)); + loop invariant \offset(p) >= \offset(\at(*pp, Pre)); + loop assigns p, val; + loop variant strlen(p); + */ while (1) { int d = hex_nibble((unsigned char) *p); if (d < 0) break; - val = (val << 4) | (uint64_t) d; + + /* val * 16 + d, not (val << 4) | d: same value for d <= 15 (the shift + * clears the low nibble), and the prover reasons about the arithmetic + * form without first proving the operands are disjoint. + */ + val = val * 16u + (uint64_t) d; p++; } *pp = p; return val; } +/* RSP checksum: the low byte of the sum of the payload. Wrapping is the + * protocol, not an accident, so uint8_t arithmetic is deliberate. + * + * byte_sum below defines that value recursively, folding modulo 256 at every + * step exactly as the uint8_t accumulator does. Defining it as a plain sum and + * taking "% 256" only in the postcondition also specifies the right value, but + * then every loop step asks the prover to show (x % 256 + b) % 256 == (x + b) % + * 256, which Z3 times out on. + */ +/*@ axiomatic RspByteSum { + logic integer byte_sum{L}(char *d, integer n) reads d[0 .. n - 1]; + axiom byte_sum_empty{L}: + \forall char *d; byte_sum(d, 0) == 0; + axiom byte_sum_step{L}: + \forall char *d, integer n; n > 0 ==> + byte_sum(d, n) == + (byte_sum(d, n - 1) + (unsigned char) d[n - 1]) % 256; + } + */ +/*@ + requires \valid_read(data + (0 .. len - 1)); + assigns \nothing; + ensures \result == byte_sum(data, len); + */ static uint8_t rsp_checksum(const char *data, size_t len) { uint8_t sum = 0; + /*@ + loop invariant 0 <= i <= len; + loop invariant sum == byte_sum(data, i); + loop assigns i, sum; + loop variant len - i; + */ for (size_t i = 0; i < len; i++) sum += (uint8_t) data[i]; return sum; @@ -118,16 +273,22 @@ void gdb_rsp_set_noack(gdb_rsp_ctx_t *ctx, bool enabled) } /* Read one RSP packet from the client into @buf. Strips $...# framing and - * verifies the checksum, sending + acknowledgment on success. Returns packet - * length, 0 on EOF, -1 on error. Also handles bare 0x03 (Ctrl+C) by returning - * "\x03" as a 1-byte packet. + * verifies the checksum, sending + acknowledgment on success. + * + * Returns packet length, 0 on EOF, -1 on error. Also handles bare 0x03 (Ctrl+C) + * by returning "\x03" as a 1-byte packet. * * Uses a static read buffer to batch socket reads instead of reading one byte * at a time. Packets exceeding @bufsz are rejected with E00. */ int gdb_rsp_recv(gdb_rsp_ctx_t *ctx, int fd, char *buf, size_t bufsz) { - if (bufsz == 0) { + /* Two bytes minimum: every returned packet is NUL-terminated, and the bare + * 0x03 (Ctrl+C) reply needs one byte for the payload and one for the + * terminator. Accepting bufsz 1 would hand back an unterminated packet and + * break the guarantee gdb_parse_hex's contract relies on. + */ + if (bufsz < 2) { errno = EINVAL; return -1; } @@ -157,6 +318,12 @@ int gdb_rsp_recv(gdb_rsp_ctx_t *ctx, int fd, char *buf, size_t bufsz) if (c == 0x03) { buf[0] = 0x03; + + /* Terminate like every other returned packet: gdb_parse_hex's + * contract requires a NUL-terminated string and cites this + * function as the guarantee. bufsz >= 2 is enforced above. + */ + buf[1] = '\0'; return 1; } @@ -198,9 +365,19 @@ int gdb_rsp_recv(gdb_rsp_ctx_t *ctx, int fd, char *buf, size_t bufsz) buf[pos] = '\0'; - uint8_t expected = - (uint8_t) ((hex_nibble((unsigned char) ck_hi) << 4) | - hex_nibble((unsigned char) ck_lo)); + /* A non-hex checksum is a corrupt packet, handled like a + * mismatch. Decoding it as a number first would shift a + * negative nibble. + */ + uint8_t expected; + if (!gdb_hex_pair(ck_hi, ck_lo, &expected)) { + if (!ctx->no_ack_mode) + (void) rsp_send_byte(fd, '-'); + state = 0; + pos = 0; + break; + } + uint8_t actual = rsp_checksum(buf, pos); if (expected == actual) { if (!ctx->no_ack_mode) diff --git a/src/debug/gdbstub.c b/src/debug/gdbstub.c index 0b2b5032..b73a5310 100644 --- a/src/debug/gdbstub.c +++ b/src/debug/gdbstub.c @@ -575,6 +575,17 @@ static void handle_write_mem(const char *pkt) return; } + /* len comes from the packet's length field, which need not agree with how + * many hex digits actually follow the ':'. gdb_hex_decode requires 2*len + * readable digits, so bound it by what is there rather than trusting the + * field; otherwise a short payload walks the decoder off the end of the + * packet buffer. + */ + if (len > strlen(p) / 2) { + rsp_reply_error(1); + return; + } + uint8_t *tmp = malloc(len); if (!tmp) { rsp_reply_error(12); @@ -602,14 +613,23 @@ static void handle_write_mem(const char *pkt) static void handle_set_thread(const char *pkt) { char op = pkt[0]; + + /* A bare "H" leaves op as the terminator, and p would then start one byte + * past it, parsing whatever follows the packet as a thread id. + */ + if (op == '\0') { + rsp_reply_error(1); + return; + } + const char *p = pkt + 1; - int64_t tid; bool negative = false; if (*p == '-') { negative = true; p++; } - tid = (int64_t) gdb_parse_hex(&p); + + int64_t tid = (int64_t) gdb_parse_hex(&p); if (negative) tid = -tid; @@ -695,6 +715,7 @@ static void handle_breakpoint(const char *pkt, int insert) static void handle_q_supported(const char *pkt) { (void) pkt; + /* Advertise features: * - PacketSize: max packet the stub accepts * - hwbreak+: the GDB stub supports hardware breakpoints @@ -787,7 +808,21 @@ static void handle_vcont(const char *pkt) while (*p == ';') { p++; - char action = *p++; + + /* A payload ending in ';' leaves the terminator here. Advancing past it + * unconditionally would step off the end of the packet buffer, and + * gdb_rsp_recv can place that terminator at its very last byte. + */ + char action = *p; + if (action == '\0') { + /* A trailing ';' with no action is malformed. Falling out of the + * loop here would resume every stopped thread, letting invalid + * debugger input change execution state. + */ + rsp_reply_error(1); + return; + } + p++; int64_t tid = -1; if (*p == ':') { diff --git a/src/syscall/exec.c b/src/syscall/exec.c index 598a2306..357ab4e9 100644 --- a/src/syscall/exec.c +++ b/src/syscall/exec.c @@ -902,7 +902,22 @@ int64_t sys_execve(hv_vcpu_t vcpu, */ uint64_t elf_load_base = (elf_info.e_type == ET_DYN) ? PIE_LOAD_BASE : 0; - /* Validate that the ELF fits within the guest address space */ + /* Validate that the ELF fits within the guest address space. + * + * load_max can be exactly UINT64_MAX: elf_load_fd rejects a PT_LOAD whose + * p_vaddr + p_memsz wraps, but a segment ending precisely at UINT64_MAX + * does not wrap and is recorded. Adding the load base to that truncates to + * a small value which passes the bound below, and the load then fails + * inside elf_map_segments_fd, which is past the point of no return where + * the only option left is exit(128). Reject it here, where execve can still + * return an error. + */ + if (elf_info.load_max > UINT64_MAX - elf_load_base) { + log_error("execve: ELF load extent overflows the address space for %s", + path); + err = -LINUX_ENOEXEC; + goto fail; + } uint64_t elf_end = elf_info.load_max + elf_load_base; if (elf_end > g->guest_size) { log_error( @@ -980,6 +995,22 @@ int64_t sys_execve(hv_vcpu_t vcpu, err = -LINUX_ENOEXEC; goto fail; } + + /* Bound the interpreter's extent here, the same way the executable's is + * bounded above. Without this the only thing that rejects an + * over-large interpreter is elf_map_segments_fd, which runs after the + * point of no return where the sole 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; Linux returns ENOEXEC and the caller + * survives. + */ + if (interp_info.load_max > UINT64_MAX - g->interp_base || + interp_info.load_max + g->interp_base > g->guest_size) { + log_error("execve: interpreter extends beyond guest memory: %s", + interp_resolved); + err = -LINUX_ENOEXEC; + goto fail; + } } /* Past pre-PNR validation. Fall through to point of no return. The fail @@ -1264,8 +1295,8 @@ int64_t sys_execve(hv_vcpu_t vcpu, uint64_t infra_lo = g->interp_base - INFRA_RESERVE; uint64_t infra_hi = g->interp_base; if (elf_map_segments_fd(&elf_info, exec_fd, path_host, g->host_base, - g->guest_size, elf_load_base, infra_lo, - infra_hi) < 0) { + g->guest_size, (elf_window_t) {0, elf_load_base}, + infra_lo, infra_hi) < 0) { log_fatal( "execve failed after point of no return: " "failed to map ELF segments for %s", @@ -1286,8 +1317,9 @@ int64_t sys_execve(hv_vcpu_t vcpu, if (elf_info.interp_path[0] != '\0') { interp_base = g->interp_base; if (elf_map_segments_fd(&interp_info, interp_fd, interp_resolved, - g->host_base, g->guest_size, interp_base, - infra_lo, infra_hi) < 0) { + g->host_base, g->guest_size, + (elf_window_t) {0, interp_base}, infra_lo, + infra_hi) < 0) { log_fatal( "execve failed after point of no return: " "failed to map interpreter segments"); diff --git a/src/syscall/fuse.c b/src/syscall/fuse.c index 1e2d230b..af71545b 100644 --- a/src/syscall/fuse.c +++ b/src/syscall/fuse.c @@ -197,6 +197,7 @@ typedef struct { #define FUSE_MAX_MOUNTS 8 #define FUSE_MAX_OPEN_FILES 128 #define FUSE_MAX_PENDING 128 + /* Per-session capacity for held lookup references. Sized for recursive * directory walks (ls -R style) without pushing the per-session struct into * multi-page territory; node_refs at this cap is ~96 KiB, kept off the stack. @@ -265,6 +266,7 @@ typedef struct { char source[256]; char fstype[16]; int mount_id; + /* session is the live transport for this mount; NULL once the owning * /dev/fuse fd is closed (the slot is tombstoned, keeping path/source/ * fstype/mount_id intact so consumers stuck on this mount path can be @@ -277,6 +279,7 @@ typedef struct { typedef struct { bool used; + /* refcount keeps the slot alive while any thread holds a snapshot or does * an in-flight FUSE request against this fd. 1 = held by the underlying * open fd; +1 per in-flight op acquired via fuse_file_get_locked. The slot @@ -291,6 +294,7 @@ typedef struct { uint64_t offset; int linux_flags; bool path_only; + /* session is pinned by the file's own session ref taken at open time. The * mount slot the file came from may be reassigned independently; mount_id * is the stable identifier used to detect that case without dereferencing a @@ -300,6 +304,7 @@ typedef struct { int mount_id; char path[LINUX_PATH_MAX]; fuse_attr_t attr; + /* Serialize stream read() / readdir() against the offset field. lseek also * waits on io_in_progress to avoid clobbering an in-flight read's * post-update. @@ -361,6 +366,7 @@ static int fuse_join_virtual_path(const char *base, } size_t depth = 0; + /* marks[i] stores the output index at which the i-th surviving component * begins. Each value is bounded by outsz (capped at LINUX_PATH_MAX = 4096), * so uint16_t is sufficient and shrinks the host-stack footprint from 16 @@ -474,8 +480,8 @@ static fuse_session_t *fuse_unbind_dev_fd_locked(int guest_fd) return NULL; } -/* First guest fd still bound to session, or -1 when none remain. Doubles as - * the alias-count > 0 test and names the surviving alias so the close path can +/* First guest fd still bound to session, or -1 when none remain. Doubles as the + * alias-count > 0 test and names the surviving alias so the close path can * repoint session->guest_fd (the synchronous SIGIO target) at a live slot. */ static int fuse_dev_alias_fd_locked(fuse_session_t *session) @@ -532,6 +538,7 @@ static void fuse_notify_readable_locked(fuse_session_t *session) return; uint8_t byte = 1; write(session->notify_wr, &byte, 1); + /* Fire SIGIO synchronously: a parked daemon can dequeue the request and * drain the notify byte before the asyncio watcher's kevent() revalidates * the readiness edge, silently losing the signal (FUSE_INIT is one-shot). @@ -984,6 +991,7 @@ static int fuse_walk_path_locked(fuse_session_t *session, return -LINUX_ENOENT; memcpy(name, p, len); name[len] = '\0'; + /* The path is canonicalized before reaching the walk, so "." and ".." * should never appear as a real component. Defend against accidental * forwarding to the daemon (which has no notion of the mount root's @@ -1169,6 +1177,7 @@ static int fuse_release_common_locked(fuse_session_t *session, { if (!session || session->daemon_dead || session->closed) return 0; + /* O_PATH opens skip FUSE_OPEN, so there is no fh to release. The path walk * still incremented the daemon's nlookup, so emit FORGET to balance it. * Without this, every successful O_PATH close leaks one reference. @@ -1387,6 +1396,7 @@ int fuse_proc_open(int linux_flags) return -1; } pthread_mutex_unlock(&fuse_lock); + /* Publish under fd_lock so the write is on the same lock domain as * sys_fcntl(F_SETFL/F_SETFD), not stranded behind fuse_lock. */ @@ -1414,6 +1424,7 @@ static int parse_mount_fd(const char *data) char *endp; errno = 0; long fd = strtol(fdp, &endp, 10); + /* Reject empty digit run, overflow, negative, and out-of-range fd values so * a malformed options string cannot smuggle in an integer that bypasses * later RANGE_CHECK gates. @@ -1491,6 +1502,7 @@ int64_t sys_mount(guest_t *g, return -LINUX_EBUSY; } } + /* Prefer reclaiming a tombstoned slot at the same path so the mount_id * sequence stays stable for consumers that cached it. */ @@ -1539,6 +1551,7 @@ bool fuse_path_matches_mount(const char *path) if (fuse_canonical_abs(path, canon, sizeof(canon)) < 0) return false; pthread_mutex_lock(&fuse_lock); + /* Matches both live and tombstoned mounts so post-daemon-death operations * get routed to a deterministic -LINUX_ENOTCONN instead of silently falling * through to host-filesystem resolution. @@ -1859,6 +1872,7 @@ int64_t fuse_open_path(guest_t *g, const char *path, int linux_flags, int mode) pthread_mutex_unlock(&fuse_lock); return -LINUX_ENOTDIR; } + /* Linux open(2): when O_PATH is set, access-mode bits (O_RDONLY / O_WRONLY * / O_RDWR) are ignored. The descriptor is opaque to read/write but usable * for fstat, fchdir, *at() dirfd, etc. Reject non-RDONLY only for ordinary @@ -1922,6 +1936,7 @@ int64_t fuse_open_path(guest_t *g, const char *path, int linux_flags, int mode) file->fh = out.fh; file->linux_flags = linux_flags; file->path_only = path_only; + /* Donate the session ref taken above to the file's own ref slot. The mount * pointer itself is not cached; mount_id is enough to detect stale * mount-slot reassignment without dereferencing a recycled fuse_mount_t. @@ -1945,6 +1960,7 @@ int64_t fuse_open_path(guest_t *g, const char *path, int linux_flags, int mode) return -LINUX_EMFILE; } pthread_mutex_unlock(&fuse_lock); + /* Publish under fd_lock so the open's flags land on the same lock domain * that sys_fcntl(F_SETFL/F_SETFD) uses. */ @@ -2094,6 +2110,19 @@ static int64_t fuse_read_common(guest_t *g, pthread_mutex_unlock(&snap->session->lock); if (rc < 0) return rc; + + /* Never deliver more than was asked for. Linux sizes the copy from the + * request rather than the reply, so a daemon answering with more data than + * it was asked for cannot overrun the reader's buffer. Without this clamp a + * guest process serving a FUSE mount could reply to a 16-byte read with a + * FUSE_FRAME_CAP-sized payload and smash the memory of any other guest + * process reading the mount -- a cross-process corruption primitive the + * kernel does not offer. It would also make read(2) return more than count + * and advance the stream offset past what was delivered. + */ + if (reply_len > size) + reply_len = size; + if (guest_write(g, buf_gva, reply, reply_len) < 0) { free(reply); return -LINUX_EFAULT; @@ -2172,6 +2201,7 @@ int64_t fuse_getdents64(guest_t *g, int fd, uint64_t buf_gva, uint64_t count) size_t dst = 0; while (src + FUSE_NAME_OFFSET <= (size_t) raw) { fuse_dirent_t *fde = (fuse_dirent_t *) (tmp + src); + /* The daemon supplies fde->namelen; bound it to Linux NAME_MAX before * any further arithmetic so a malicious daemon cannot make lreclen * overflow the fixed entry[] buffer below or exceed the remaining frame @@ -2189,6 +2219,7 @@ int64_t fuse_getdents64(guest_t *g, int fd, uint64_t buf_gva, uint64_t count) break; size_t lreclen = (19 + fde->namelen + 1 + 7) & ~7ULL; + /* d_ino(8) + d_off(8) + d_reclen(2) + d_type(1) + name(<=255) + NUL(1) * + padding(<=7) <= 280. Defense in depth against an arithmetic error * -- never trust the daemon's record length. @@ -2265,6 +2296,7 @@ int64_t fuse_dev_read(int guest_fd, host_fd_ref_close(¬ify_ref); return -LINUX_EAGAIN; } + /* An untimed cond_wait has no re-check point: a FUSE daemon thread * parked here with no requests queued is invisible to * thread_join_workers' poll cap and touches guest memory (the reply @@ -2339,6 +2371,7 @@ int64_t fuse_dev_write(guest_t *g, { if (count < sizeof(fuse_out_header_t)) return -LINUX_EINVAL; + /* Reject any daemon write that exceeds the implementation hard ceiling. The * same ceiling is applied at FUSE_INIT negotiation, so a daemon cannot * advertise max_write larger than this and then have its reply payload @@ -2391,6 +2424,7 @@ int64_t fuse_dev_write(guest_t *g, } req->answered = true; + /* The daemon's error field is in Linux errno space (negative). Pass it * through unchanged; the consumer side already treats req->error as a * negative Linux errno. @@ -2506,6 +2540,7 @@ int64_t fuse_lseek_fd(int fd, int64_t offset, int whence) fd_entry_t snap; if (!fd_snapshot(fd, &snap)) return -LINUX_EBADF; + /* /dev/fuse: stream-like, no absolute position. Linux returns ESPIPE on * lseek of a pipe-equivalent fd. */ @@ -2536,6 +2571,7 @@ int64_t fuse_lseek_fd(int fd, int64_t offset, int whence) return -LINUX_EINVAL; pthread_mutex_lock(&fuse_lock); + /* Block while a stream read is in flight on this fd so the seek does not * race the post-read offset update. The wait holds a file ref so io_cond * cannot be destroyed under it. diff --git a/src/utils.h b/src/utils.h index ec533af3..79a72699 100644 --- a/src/utils.h +++ b/src/utils.h @@ -114,7 +114,9 @@ static inline void close_keep_errno(int fd) /* Encode @len bytes of @src as lowercase hex into @dst, writing len*2 hex * characters followed by a terminating NUL. @dst must hold at least len*2+1 - * bytes. Returns the number of hex characters written (len*2). + * bytes. + * + * Returns the number of hex characters written (len*2). */ static inline size_t bytes_to_hex(char *dst, const uint8_t *src, size_t len) { @@ -128,7 +130,22 @@ static inline size_t bytes_to_hex(char *dst, const uint8_t *src, size_t len) } /* Decode a single hex digit to its 0-15 value, or -1 if @c is not a hex digit. - * The inverse building block of bytes_to_hex; accepts either case. + * The inverse building block of bytes_to_hex; accepts either case. The bounds + * matter to callers that shift the result: "hex_nibble(c) << 4" is undefined + * behavior when c is not a hex digit, so the range and the digit-or-not + * equivalence are both stated for Frama-C (make verify-rsp). + */ +/*@ logic integer hex_val(integer c) = + ('0' <= c <= '9') ? c - '0' : + ('a' <= c <= 'f') ? c - 'a' + 10 : + ('A' <= c <= 'F') ? c - 'A' + 10 : -1; + */ +/*@ + assigns \nothing; + ensures -1 <= \result <= 15; + ensures \result >= 0 <==> (('0' <= c <= '9') || ('a' <= c <= 'f') || + ('A' <= c <= 'F')); + ensures \result == hex_val(c); */ static inline int hex_nibble(unsigned char c) { @@ -142,9 +159,11 @@ static inline int hex_nibble(unsigned char c) } /* Write exactly @len bytes to a blocking @fd, resuming across short writes and - * EINTR. Returns 0 once every byte is written, or -1 with errno set on error. - * An unexpected zero-byte return is treated as EIO rather than spun on, since - * the offset would otherwise never advance. A zero-length request returns 0. + * EINTR. + * + * Returns 0 once every byte is written, or -1 with errno set on error. An + * unexpected zero-byte return is treated as EIO rather than spun on, since the + * offset would otherwise never advance. A zero-length request returns 0. */ static inline int write_all(int fd, const void *buf, size_t len) { @@ -328,9 +347,9 @@ static inline int bit_popcount64(uint64_t word) return __builtin_popcountll(word); } -/* 64-bit FNV-1a over @len bytes. Not cryptographic: collision resistance is - * the birthday bound on 64 bits, which suits stable identifiers derived from - * names (synthetic inode numbers, derived filenames), not adversarial input. +/* 64-bit FNV-1a over @len bytes. Not cryptographic: collision resistance is the + * birthday bound on 64 bits, which suits stable identifiers derived from names + * (synthetic inode numbers, derived filenames), not adversarial input. * Constants from the FNV reference (offset basis, prime). */ static inline uint64_t fnv1a64(const void *data, size_t len) diff --git a/tests/test-fuse-basic.c b/tests/test-fuse-basic.c index daed3b44..0aa0679e 100644 --- a/tests/test-fuse-basic.c +++ b/tests/test-fuse-basic.c @@ -135,6 +135,11 @@ struct linux_dirent64 { char d_name[]; }; +/* Byte the over-reply daemon floods with, distinct from anything in hello_data + * so a canary check can tell a spill apart from stale memory. + */ +#define OVER_REPLY_FILL 0xA5 + static const char hello_name[] = "hello"; static const char hello_data[] = "hello from guest fuse\n"; static const char source_name[] = "elfuse-test"; @@ -150,6 +155,12 @@ typedef struct { uint64_t pending_read_unique; int stall_read_once; int stalled_read_active; + + /* When set, FUSE_READ answers with more bytes than fuse_read_in.size asked + * for. A daemon is a guest process like any other, so nothing stops it; the + * transport must not pass the surplus through to the reader's buffer. + */ + int over_reply_read; } daemon_ctx_t; static volatile sig_atomic_t got_usr1; @@ -349,6 +360,17 @@ static void *daemon_main(void *arg) ctx->pending_read_unique = in->unique; break; } + if (ctx->over_reply_read) { + /* Deliberately antisocial: answer a small request with a large + * payload. reply_frame's buffer caps this at 4096 - 16. + */ + static uint8_t flood[4096 - 16]; + memset(flood, OVER_REPLY_FILL, sizeof(flood)); + if (reply_frame(ctx->fusefd, in->unique, 0, flood, + sizeof(flood)) < 0) + exit(1); + break; + } size_t len = sizeof(hello_data) - 1; if (rin->offset >= len) { if (reply_frame(ctx->fusefd, in->unique, 0, NULL, 0) < 0) @@ -564,9 +586,9 @@ int main(void) return 1; } - /* Close the original device fd: the session must repoint synchronous - * SIGIO delivery at the surviving dup, so the next request still raises - * the signal. + /* Close the original device fd: the session must repoint synchronous SIGIO + * delivery at the surviving dup, so the next request still raises the + * signal. */ if (close(sigio_origfd) < 0) die("close(original /dev/fuse fd)"); @@ -579,9 +601,10 @@ int main(void) fprintf(stderr, "no SIGIO after closing the original /dev/fuse fd\n"); return 1; } - /* Disarm O_ASYNC: every later FUSE request would otherwise raise SIGIO, - * and a non-SA_RESTART handler firing mid-syscall surfaces spurious EINTR - * in the unrelated tests below. + + /* Disarm O_ASYNC: every later FUSE request would otherwise raise SIGIO, and + * a non-SA_RESTART handler firing mid-syscall surfaces spurious EINTR in + * the unrelated tests below. */ fuse_fl = fcntl(fusefd, F_GETFL); if (fuse_fl < 0 || fcntl(fusefd, F_SETFL, fuse_fl & ~O_ASYNC) < 0) @@ -681,6 +704,42 @@ int main(void) } expect_hello_fd(fd); + /* A daemon that answers with more than it was asked for must not reach past + * the reader's buffer. Linux sizes the copy from the request, so read(2) + * can never return more than count; elfuse must match. Canaries around a + * deliberately small buffer catch a spill in either direction. + */ + if (lseek(fd, 0, SEEK_SET) < 0) + die("lseek(fuse-file)"); + ctx.over_reply_read = 1; + struct { + uint8_t lead[64]; + uint8_t body[16]; + uint8_t trail[64]; + } guarded; + memset(&guarded, 0x5C, sizeof(guarded)); + ssize_t over_rc = read(fd, guarded.body, sizeof(guarded.body)); + 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)); + return 1; + } + for (size_t i = 0; i < sizeof(guarded.lead); i++) { + if (guarded.lead[i] != 0x5C || guarded.trail[i] != 0x5C) { + fprintf(stderr, + "FUSE over-reply overran the read buffer at guard byte %zu " + "(lead=0x%02x trail=0x%02x)\n", + i, guarded.lead[i], guarded.trail[i]); + return 1; + } + } + if (lseek(fd, 0, SEEK_SET) < 0) + die("lseek(fuse-file)"); + expect_hello_fd(fd); + void *map = mmap(NULL, 4096, PROT_READ, MAP_PRIVATE, fd, 0); if (map != MAP_FAILED || errno != ENODEV) { fprintf(stderr,