From 511465a4370952514722ebe113bcce5be49c90f1 Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Sun, 25 Oct 2026 00:22:55 -0500 Subject: [PATCH] Reject unsupported tar metadata and run the pilot checks in CI --- .github/scripts/setup-lean.sh | 22 +++++ .github/workflows/check.yml | 41 +++++++++ .gitignore | 1 + README.md | 14 ++- SPEC.md | 99 +++++++++++++++++++++ TarPilot/Archive.lean | 14 ++- TarPilot/Header.lean | 43 ++++++--- tests/HeaderSafety.lean | 18 ++++ tests/TEST-RESULTS.md | 6 +- tests/parser_cases.py | 162 ++++++++++++++++++++++++++++++++++ tests/run_tests.py | 24 +++-- 11 files changed, 417 insertions(+), 27 deletions(-) create mode 100644 .github/scripts/setup-lean.sh create mode 100644 .github/workflows/check.yml create mode 100644 SPEC.md create mode 100644 tests/HeaderSafety.lean create mode 100644 tests/parser_cases.py diff --git a/.github/scripts/setup-lean.sh b/.github/scripts/setup-lean.sh new file mode 100644 index 0000000..b3d587d --- /dev/null +++ b/.github/scripts/setup-lean.sh @@ -0,0 +1,22 @@ +#!/bin/sh +# Install the pinned toolchain manager and require a working kernel-check sandbox. +# Adapted from Proven-Commons/mission's proposed verified bar v2 setup script. +set -eu + +ELAN_VERSION=v4.2.4 +ELAN_SHA256=42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63 +task_tmp=$(mktemp -d) +trap 'rm -rf "$task_tmp"' EXIT +curl -sSfL -o "$task_tmp/elan.tar.gz" \ + "https://github.com/leanprover/elan/releases/download/$ELAN_VERSION/elan-x86_64-unknown-linux-gnu.tar.gz" +printf '%s %s\n' "$ELAN_SHA256" "$task_tmp/elan.tar.gz" | sha256sum -c - +tar -xzf "$task_tmp/elan.tar.gz" -C "$task_tmp" +"$task_tmp/elan-init" -y --no-modify-path --default-toolchain none +printf '%s\n' "$HOME/.elan/bin" >> "$GITHUB_PATH" + +sudo apt-get update -q +sudo apt-get install -yq bubblewrap +if [ -f /proc/sys/kernel/apparmor_restrict_unprivileged_userns ]; then + sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0 +fi +bwrap --ro-bind / / --dev /dev --proc /proc --unshare-all true diff --git a/.github/workflows/check.yml b/.github/workflows/check.yml new file mode 100644 index 0000000..9882e2e --- /dev/null +++ b/.github/workflows/check.yml @@ -0,0 +1,41 @@ +name: Proofs and differential tests + +on: + push: + branches: [main] + pull_request: + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + check: + runs-on: ubuntu-24.04 + timeout-minutes: 45 + steps: + - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5 + with: + persist-credentials: false + - uses: actions/setup-python@ece7cb06caefa5fff74198d8649806c4678c61a1 # v6 + with: + python-version: "3.12" + - name: Install Lean and bubblewrap + run: sh .github/scripts/setup-lean.sh + - name: Build, regressions, differential tests and axiom allowlist + run: | + rm -f tests/TEST-RESULTS.md + python3 tests/run_tests.py + - name: Replay proofs under all six kernels in the sandbox + run: lake check --paranoid + - name: Save the differential test report + if: always() + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 + with: + name: tar-test-results + path: tests/TEST-RESULTS.md + if-no-files-found: error diff --git a/.gitignore b/.gitignore index 01f8cdb..ae73679 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ .lake/ +__pycache__/ diff --git a/README.md b/README.md index 1644d22..9c817a4 100644 --- a/README.md +++ b/README.md @@ -4,6 +4,8 @@ This repo reads a tar archive (ustar format) and extracts regular files into an It is the first Proven Commons project. The org's home repo, [mission](https://github.com/Proven-Commons/mission), publishes the verified bar it is measured against. Status: built, not yet verified. The [bar audit of 2026-10-24](https://github.com/Proven-Commons/mission/blob/main/reviews/tar/2026-10-24-bar-audit.md) found that the bar is not yet met, and lists the fixes. +The [draft specification](SPEC.md) defines the supported ustar subset and extraction contract. It awaits independent review. GNU magic, extension metadata, invalid UTF-8 path fields, incomplete end blocks, and nonzero trailing data reject the whole archive before `list` or `manifest` prints entries. + ## Run it Needs Lean 4.35.0 (install with elan, toolchain pinned in `lean-toolchain`). @@ -29,7 +31,7 @@ The path gate and the extraction rule, in `TarPilot/Path.lean` and `TarPilot/Arc The CLI's `OK` lines call `extractEntry` and `joinPath`, the same functions used by these statements. `extractAll` filters the results of `extractEntry`. The CLI adds only `REJECT` and `SKIP` diagnostics for entries with no extracted result, preserving archive order. Parsing, diagnostics, and formatting sizes and byte sums remain outside the proof. -The gate rules: absolute names are rejected. Any `..` component is rejected, as is a component containing `/` or NUL. Empty and `.` components are dropped. A name with nothing left is rejected. Only regular files (typeflag `0` or NUL) are extracted. Directory, link, and other entries are skipped, so a link entry cannot place a later entry outside the destination. +The gate rules: absolute names are rejected. Any `..` component is rejected, as is a component containing `/` or NUL. Empty and `.` components are dropped. A name with nothing left is rejected. Data files (typeflag `0`, NUL, or `7`) are extracted. Directory, link, and other supported non-data entries are skipped, so a link entry cannot place a later entry outside the destination. Axiom check: each proof depends only on the standard Lean axioms (`propext`, `Classical.choice`, `Quot.sound`, or a subset). Full output is recorded in `tests/TEST-RESULTS.md`. @@ -37,9 +39,9 @@ Axiom check: each proof depends only on the standard Lean axioms (`propext`, `Cl Read this before trusting the pilot with real archives: -- Header parsing, octal fields, checksums, and archive writing are tested, not proved. The tests compare the Lean code against Python's `tarfile` module and against an independent copy of the extraction spec. Results are in `tests/TEST-RESULTS.md`: the original 14 archive entries and create/readback checks, plus 524 path cases (512 random, seed `20261024`) under eight destinations. Manifest comparisons preserve duplicate names and entry order; `posixpath` independently checks containment of emitted paths. Lean regressions cover embedded separators, NUL, the old theorem's traversal counterexample, and lexical resolution. Broken inputs cover truncated archives, garbage, and bad checksums. +- Header parsing, octal fields, checksums, and archive writing are tested, not proved. The tests compare the Lean code against Python's `tarfile` module and against an independent copy of the extraction spec. The [test report](tests/TEST-RESULTS.md) records the original archive and create/readback checks, 524 path cases across eight destinations, and the parser campaign (seed `20261025`: 512 random valid archives and 512 mutated invalid archives, plus fixed regressions). Every parser case checks both `list` and `manifest`; rejected cases must print no stdout. All 256 typeflag bytes are covered. `posixpath` independently checks emitted paths. Lean regressions cover separators, NUL, UTF-8 decoding, header writing, and the old theorem's traversal counterexample. - Extraction works on an in-memory model. Nothing here writes files to disk, so the step from a proved in-memory path to a safe write on a real filesystem (races, symlinked destination folders) is outside this project for now. -- Invalid UTF-8 becomes an empty header field. With a split ustar name, a valid prefix or name can survive while the invalid field is lost. GNU longname and pax path overrides are ignored rather than reliably rejected, so extension-bearing archives can produce incorrect names. Base-256 sizes and sparse files are not supported. Typeflag `7` (contiguous file) is skipped even though Python treats it as regular. These parser and compatibility findings from the audit remain open; use the pilot only for its supported ustar subset. +- The reader intentionally rejects formats outside its [supported subset](SPEC.md): GNU magic, pax/GNU extension headers, sparse extension types, base-256 sizes, non-data entries with payloads, and ambiguous NUL-type directory names. It requires block alignment, two zero end blocks, and only zero record padding after them. Some other tar readers accept inputs this pilot rejects. UTF-8 is required for both path fields; other encodings are not converted. The CLI prints tabs and line breaks in names literally; its text output is not an escaped wire format. - The Lean compiler, runtime, kernel, and hardware are trusted. The tests also rely on Python's `tarfile` and `posixpath` as oracles. Bugs in these are outside the proof. ## Re-check it @@ -48,10 +50,13 @@ Read this before trusting the pilot with real archives: lake build lake env lean TarPilot/Verify.lean python3 tests/run_tests.py +lake check --paranoid ``` The build checks the proofs, but accepts `sorry` with a warning. The second command prints the axiom list. The test script always rebuilds, runs the Lean regressions and every comparison, and rewrites `tests/TEST-RESULTS.md`. It requires each named theorem's axiom list to contain only `propext`, `Classical.choice`, and `Quot.sound`, so `sorryAx` and custom axioms fail the tests. +`lake check --paranoid` needs a working `bubblewrap` sandbox on Linux. It replays proofs through all six bundled kernels and rejects nonstandard axioms. The `Proofs and differential tests` workflow runs the test script and the sandboxed proof check on pull requests and pushes to `main`, and saves the test report as an artifact. Branch protection must separately require this workflow; independent specification approval is still outstanding. + ## Layout - `TarPilot/Path.lean`: the path gate and its proofs. @@ -62,3 +67,6 @@ The build checks the proofs, but accepts `sorry` with a warning. The second comm - `Main.lean`: the command line front end. - `tests/run_tests.py`: differential tests against Python's `tarfile`. - `tests/PathSafety.lean`: path safety regressions, including the old statement's counterexample. +- `tests/HeaderSafety.lean`: UTF-8 decoding and header-builder regressions. +- `tests/parser_cases.py`: format regressions and seeded parser comparisons. +- `SPEC.md`: the draft contract for review. diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..d8d24b3 --- /dev/null +++ b/SPEC.md @@ -0,0 +1,99 @@ +# Tar pilot specification + +Status: **draft, awaiting independent specification review**. This document +records the intended contract of this implementation. It is not an approval +record and does not establish the org's verified bar. + +## Supported archive input + +The reader accepts a strict subset of POSIX ustar. It returns the complete +entry list or an error; it never returns a successfully parsed prefix of an +invalid archive. + +- Input length is a multiple of 512 bytes. Every entry has a complete + 512-byte header and enough bytes for its declared payload and block padding. +- Header magic is exactly `ustar` followed by NUL, and version is exactly + `00`. GNU's different magic/version is rejected. +- The checksum is the unsigned sum of all 512 header bytes, treating bytes + 148 through 155 as ASCII spaces. Both checksum and size are octal fields: + leading spaces and trailing spaces/NUL are removed, remaining bytes must + be `0` through `7`, and an empty field means zero. Base-256 sizes fail. +- Types NUL, `0`, and `7` are data files. Types `1` through `6` are accepted + only with size zero and are skipped by extraction. Every other type + rejects the whole archive, including GNU longname/longlink, pax per-file + and global headers, and sparse extension types. +- The name and prefix fields are each decoded as UTF-8 up to their first + NUL. Invalid UTF-8 in either field rejects the whole archive. Bytes after + a terminating NUL are outside the field value. A nonempty prefix is + joined to the name with `/`. No invalid field is replaced with empty text. +- A NUL-type entry whose full name ends with `/` is rejected: legacy readers + can interpret it as a directory rather than a regular file. +- The archive ends with at least two consecutive all-zero blocks. All bytes + after the first end block must also be zero. Missing end blocks, partial + blocks, concatenated nonempty archives, and nonzero trailing data are rejected. + +Extension-free output from a tool using its pax option can still satisfy +this subset; format labels alone do not determine acceptance. Header mode, +owner, timestamps, device fields, and link targets are ignored. They do not +affect the emitted in-memory file paths or contents. Payload padding need +not be zero. This reader does not decompress archives or write extracted +files to disk. + +## Extraction + +The parser returns names, original typeflags, and payload bytes in archive +order. `extractEntry` emits a result only for NUL, `0`, or `7` entries whose +names pass the path gate. `extractAll` preserves the order and duplicates of +those results. Non-data entries are skipped; a rejected data-file name does +not reject the archive. + +The gate rejects names beginning with `/`, any `..` component, and any +component containing `/` or NUL. It drops empty and `.` components and +requires a nonempty result. It joins those relative components after the +caller-supplied destination components. + +`PlainName`, `gate_plain`, `extractAll_contained`, `extractAll_joined`, and +`extractAll_resolves_inside` state the formal guarantees. With slash-free +destination components, the rendered string splits into exactly the +destination followed by nonempty plain names. Resolving it with the relative +POSIX lexical resolver gives the resolved destination followed by those +names. This does not model absolute-root handling, Windows paths, existing +filesystem symlinks, or filesystem races. + +## Commands and archive writing + +`list` and `manifest` parse the whole archive before printing any entries. +Malformed or unsupported archives exit 1, print an error to stderr, and +produce no stdout. Accepted archives exit 0. `manifest` calls `extractEntry` +and `joinPath` for `OK` results, printing `REJECT` for a data-file name that +fails the gate and `SKIP` for a non-data entry. + +The CLI output is a textual view, not an escaped wire format: names containing +tabs or line breaks are printed literally. Formatting, I/O handling, byte sums, +and exit behavior are outside the proof. Tests cover formatting, byte sums, +and archive-rejection exits; they do not cover every I/O failure. + +`create` emits regular ustar entries followed by two zero blocks. It fails +when a name cannot fit the ustar name/prefix fields or a size cannot fit an +octal size field. The header builder rejects embedded NUL, unsupported +types, non-data entries with payloads, and ambiguous NUL-type directories. +Mode is fixed at 0644; owner IDs and timestamps are zero. Archive writing is +tested rather than proved. + +## Evidence and limits + +`python3 tests/run_tests.py` builds the current sources, runs the Lean +regressions, compares accepted archives with Python `tarfile`, checks +rejected cases for exit 1 and no stdout, and checks every printed theorem's +axioms against the standard three. The committed report records seeds, +case counts, versions, and failures. `tests/parser_cases.py` includes the +format and UTF-8 failures from the +[2026-10-24 audit](https://github.com/Proven-Commons/mission/pull/1), all 256 +typeflag bytes, valid random archives, and mutated invalid archives. + +`lake check --paranoid` replays the built proof declarations through all six +bundled kernels in a sandbox. CI runs both commands. Passing them does not +prove the byte parser or writer, validate this specification's adequacy, or +supply independent approval. The compiler, runtime, kernels, hardware, and +test oracles remain trusted. Requiring the CI check through branch protection +is a separate repository setting. diff --git a/TarPilot/Archive.lean b/TarPilot/Archive.lean index d1806e1..cb75e57 100644 --- a/TarPilot/Archive.lean +++ b/TarPilot/Archive.lean @@ -34,7 +34,12 @@ def parseBlocks (data : ByteArray) (off : Nat) : Nat → Option (List RawEntry) if off + 512 > data.size then none else let block := data.extract off (off + 512) - if block.toList.all (· = 0) then some [] + if block.toList.all (· = 0) then + -- Require two end blocks, then only zero record padding. Reject + -- hidden trailing entries instead of returning a clean prefix. + if off + 1024 > data.size then none + else if (data.extract off data.size).toList.all (· = 0) then some [] + else none else match parseBlock block with | none => none | some h => @@ -49,13 +54,14 @@ def parseBlocks (data : ByteArray) (off : Nat) : Nat → Option (List RawEntry) /-- Parse a whole archive. -/ def parseArchive (data : ByteArray) : Option (List RawEntry) := - parseBlocks data 0 (data.size / 512 + 1) + if data.size % 512 != 0 then none + else parseBlocks data 0 (data.size / 512 + 1) -/-- Regular files only: typeflag `0` or NUL. Directories, links, and +/-- Data files only: typeflag `0`, NUL, or `7`. Directories, links, and everything else are never extracted, so a link entry cannot be used to place a later entry outside the destination. -/ def isRegular (e : RawEntry) : Bool := - e.typeflag == '0' || e.typeflag == Char.ofNat 0 + isRegularType e.typeflag /-- The extraction decision shared by the CLI and the in-memory model. -/ def extractEntry (dest : List String) (e : RawEntry) : Option (List String × ByteArray) := diff --git a/TarPilot/Header.lean b/TarPilot/Header.lean index 68885a7..0ca8418 100644 --- a/TarPilot/Header.lean +++ b/TarPilot/Header.lean @@ -31,11 +31,21 @@ def byteAt (b : ByteArray) (i : Nat) : UInt8 := def sliceList (b : ByteArray) (off len : Nat) : List UInt8 := (b.extract off (off + len)).toList -/-- A name field: bytes up to the first NUL, read as UTF-8. - Invalid UTF-8 reads as the empty string. -/ -def bytesToName (bs : List UInt8) : String := +/-- A name field: bytes up to the first NUL, decoded without replacement. + Invalid UTF-8 rejects the header instead of losing half a split name. -/ +def bytesToName (bs : List UInt8) : Option String := let raw := bs.takeWhile (fun b => b ≠ 0) - (String.fromUTF8? (ByteArray.mk raw.toArray)).getD "" + String.fromUTF8? (ByteArray.mk raw.toArray) + +/-- Ustar data files, including the POSIX contiguous-file type. -/ +def isRegularType (typeflag : Char) : Bool := + typeflag == '0' || typeflag == Char.ofNat 0 || typeflag == '7' + +/-- Types this reader understands. Extension metadata must reject the + archive: skipping it could silently substitute a different pathname. -/ +def isSupportedType (typeflag : Char) : Bool := + isRegularType typeflag || typeflag == '1' || typeflag == '2' || + typeflag == '3' || typeflag == '4' || typeflag == '5' || typeflag == '6' /-- The header checksum: sum of all 512 bytes, with the checksum field itself (bytes 148 to 155) counted as spaces. -/ @@ -43,20 +53,27 @@ def blockChecksum (bs : List UInt8) : Nat := (bs.zipIdx).foldl (fun acc p => acc + (if 148 ≤ p.2 ∧ p.2 < 156 then 32 else p.1.toNat)) 0 -/-- Parse one 512-byte header block. Fails on a short block, a bad - magic, a checksum mismatch, or a bad size field. -/ +/-- Parse the supported POSIX ustar subset: exact magic and version, + supported types, octal size and checksum, and UTF-8 pathname fields. + Non-data entries must have zero size. -/ def parseBlock (block : ByteArray) : Option Header := if block.size < 512 then none else do - if sliceList block 257 5 ≠ [117, 115, 116, 97, 114] then none else + if sliceList block 257 6 ≠ [117, 115, 116, 97, 114, 0] then none else + if sliceList block 263 2 ≠ [48, 48] then none else let stored ← parseOctal (sliceList block 148 8) if stored ≠ blockChecksum (sliceList block 0 512) then none else + let typeflag := Char.ofNat (byteAt block 156).toNat + if !isSupportedType typeflag then none else let size ← parseOctal (sliceList block 124 12) - let name := bytesToName (sliceList block 0 100) - let pfx := bytesToName (sliceList block 345 155) + if !isRegularType typeflag && size != 0 then none else + let name ← bytesToName (sliceList block 0 100) + let pfx ← bytesToName (sliceList block 345 155) let fullName := if pfx = "" then name else pfx ++ "/" ++ name - some { name := fullName, size := size, - typeflag := Char.ofNat (byteAt block 156).toNat } + -- Old tar readers interpret a NUL-type trailing slash as a directory. + -- Reject that ambiguous form rather than disagree about its payload. + if typeflag == Char.ofNat 0 && fullName.endsWith "/" then none else + some { name := fullName, size := size, typeflag := typeflag } /-- Content padded on the right with NUL bytes to width `w`, or cut to `w` when longer. -/ @@ -79,6 +96,10 @@ def splitUstarName (name : String) : Option (String × String) := Mode is fixed at 0644, uid, gid, and mtime at 0. Fails when the size or the name does not fit. -/ def buildBlock (name : String) (size : Nat) (typeflag : Char) : Option ByteArray := do + if Char.ofNat 0 ∈ name.toList then none else + if !isSupportedType typeflag then none else + if !isRegularType typeflag && size != 0 then none else + if typeflag == Char.ofNat 0 && name.endsWith "/" then none else let (pfx, short) ← splitUstarName name let sizeF ← formatOctal size 12 let modeF ← formatOctal 0o644 8 diff --git a/tests/HeaderSafety.lean b/tests/HeaderSafety.lean new file mode 100644 index 0000000..7bdd192 --- /dev/null +++ b/tests/HeaderSafety.lean @@ -0,0 +1,18 @@ +import TarPilot + +open TarPilot + +-- UTF-8 decoding distinguishes an empty field from an invalid field. +#guard bytesToName [] == some "" +#guard bytesToName [195, 169, 0] == some "é" +#guard bytesToName [255] == none +#guard bytesToName [195] == none +#guard bytesToName [0, 255] == some "" + +-- The writer must not create a header the supported-subset reader rejects. +#guard (buildBlock "safe.txt" 7 '7').isSome +#guard (buildBlock "link" 0 '2').isSome +#guard (buildBlock "link" 7 '2').isNone +#guard (buildBlock "extension" 0 'x').isNone +#guard (buildBlock ("safe" ++ String.singleton (Char.ofNat 0) ++ "hidden") 0 '0').isNone +#guard (buildBlock "legacy/" 0 (Char.ofNat 0)).isNone diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index e0751f7..f385fb2 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -3,13 +3,15 @@ Run by `tests/run_tests.py` against Python's `tarfile` module. Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release). Python: 3.12.14. -- Checks run: 40 +- Checks run: 2641 - Failures: 0 - Archive A entries compared (list and manifest): 14 - Manifest outcome on archive A: 9 extracted, 3 rejected by the path gate, 2 skipped as non-regular - Files written by the Lean `create` command and read back by Python: 3 - Path regression entries: 524 (512 random, seed 20261024), compared with the spec under 8 destinations and checked with `posixpath` -- `tests/PathSafety.lean`: cleaner, gate, joined-path and relative-resolution regressions +- Lean regressions: `tests/PathSafety.lean` (paths and resolution) and `tests/HeaderSafety.lean` (UTF-8 decoding and header writing) +- Parser archives: 517 compared with Python tarfile (1887 entries), 783 rejected with no output +- Parser seed: 20261025; 512 random valid archives and 512 mutated archives; every case checks list and manifest - Broken inputs rejected with exit code 1: truncated archive, random garbage, corrupted checksum Axiom check (`TarPilot/Verify.lean`): diff --git a/tests/parser_cases.py b/tests/parser_cases.py new file mode 100644 index 0000000..67c43c5 --- /dev/null +++ b/tests/parser_cases.py @@ -0,0 +1,162 @@ +"""Parser contract regressions and seeded comparisons with Python tarfile. + +Parsing remains outside the Lean proof. Valid inputs are compared with +tarfile; inputs outside the documented subset must fail without output. +""" + +import io +import random +import tarfile + +PARSER_SEED = 20261025 +RANDOM_ARCHIVES = 512 +MUTATED_ARCHIVES = 512 +REGULAR = (tarfile.REGTYPE, tarfile.AREGTYPE, tarfile.CONTTYPE) +SUPPORTED = REGULAR + (tarfile.LNKTYPE, tarfile.SYMTYPE, tarfile.CHRTYPE, + tarfile.BLKTYPE, tarfile.DIRTYPE, tarfile.FIFOTYPE) + + +def archive(entries, fmt=tarfile.USTAR_FORMAT): + out = io.BytesIO() + with tarfile.open(fileobj=out, mode="w", format=fmt, encoding="utf-8") as tf: + for name, data, typ in entries: + ti = tarfile.TarInfo(name) + ti.type = typ + ti.mtime = 0 + ti.size = len(data) if typ in REGULAR else 0 + if typ in (tarfile.LNKTYPE, tarfile.SYMTYPE): + ti.linkname = "target" + tf.addfile(ti, io.BytesIO(data) if ti.size else None) + return out.getvalue() + + +def patch(raw, offset, value, repair_checksum=True, header_offset=0): + out = bytearray(raw) + out[header_offset + offset:header_offset + offset + len(value)] = value + if repair_checksum: + out[header_offset + 148:header_offset + 156] = b" " * 8 + checksum = sum(out[header_offset:header_offset + 512]) + out[header_offset + 148:header_offset + 156] = f"{checksum:06o}\0 ".encode() + return bytes(out) + + +def reference(raw): + with tarfile.open(fileobj=io.BytesIO(raw), encoding="utf-8", errors="strict") as tf: + return [(m.name.rstrip("/") if m.isdir() else m.name, + tf.extractfile(m).read() if m.type in REGULAR else b"", m.type[0]) + for m in tf.getmembers()] + + +def run_parser_cases(work, run_lean, check, expected_manifest): + counts = {"accepted": 0, "rejected": 0, "entries": 0, + "seed": PARSER_SEED, "random_archives": RANDOM_ARCHIVES, + "mutated_archives": MUTATED_ARCHIVES} + path = work / "parser-case.tar" + + def accepted(label, raw): + counts["accepted"] += 1 + entries = reference(raw) + counts["entries"] += len(entries) + path.write_bytes(raw) + listed = run_lean("list", str(path)) + actual = [] + for line in listed.stdout.splitlines(): + parts = line.split("\t") + if len(parts) == 3: + name, size, flag = parts + actual.append((name.rstrip("/") if flag == "53" else name, int(size), int(flag))) + expected = [(name, len(data), flag) for name, data, flag in entries] + check(f"parser-list-{label}", listed.returncode == 0 and actual == expected, + f"rc={listed.returncode}, got={actual[:3]}, want={expected[:3]}, {listed.stderr}") + manifest = run_lean("manifest", str(path), "out") + lines = [] + for line in manifest.stdout.splitlines(): + parts = line.split("\t") + if parts[0] == "SKIP": + parts[1] = parts[1].rstrip("/") + lines.append("\t".join(parts)) + want = expected_manifest(entries) + check(f"parser-manifest-{label}", manifest.returncode == 0 and lines == want, + f"rc={manifest.returncode}, got={lines[:3]}, want={want[:3]}, {manifest.stderr}") + + def rejected(label, raw): + counts["rejected"] += 1 + path.write_bytes(raw) + for command in ("list", "manifest"): + args = (command, str(path), "out") if command == "manifest" else (command, str(path)) + result = run_lean(*args) + check(f"parser-reject-{label}-{command}", result.returncode == 1 and result.stdout == "", + f"rc={result.returncode}, stdout={result.stdout[:160]}, stderr={result.stderr[:160]}") + + one = archive([("safe.txt", b"payload", tarfile.REGTYPE)]) + split = archive([("p" * 30 + "/" + "q" * 90 + "/file.txt", b"x", tarfile.REGTYPE)]) + accepted("empty", bytes(1024)) + accepted("all-types", archive([(f"type-{typ[0]}", b"data", typ) for typ in SUPPORTED])) + accepted("utf8", archive([("café/notes.txt", b"hello", tarfile.REGTYPE), + ("é" * 40 + "/" + "q" * 80 + "/file.txt", b"split", tarfile.REGTYPE)])) + accepted("contiguous-hostile", archive([("../evil", b"x", tarfile.CONTTYPE), + ("./safe//data", b"data", tarfile.CONTTYPE)])) + accepted("two-zero-blocks", one[:2048]) + + # Formats with extension metadata must not silently change the pathname. + rejected("gnu-short", archive([("short.txt", b"x", tarfile.REGTYPE)], tarfile.GNU_FORMAT)) + rejected("gnu-long", archive([("d/" + "n" * 120, b"x", tarfile.REGTYPE)], tarfile.GNU_FORMAT)) + rejected("pax-long", archive([("d/" + "n" * 120, b"x", tarfile.REGTYPE)], tarfile.PAX_FORMAT)) + rejected("pax-utf8", archive([("café/notes.txt", b"x", tarfile.REGTYPE)], tarfile.PAX_FORMAT)) + pax = io.BytesIO() + with tarfile.open(fileobj=pax, mode="w", format=tarfile.PAX_FORMAT, + pax_headers={"path": "../../etc/cron.d/x"}) as tf: + info = tarfile.TarInfo("safe.txt") + info.size = 1 + tf.addfile(info, io.BytesIO(b"x")) + rejected("pax-override", pax.getvalue()) + for flag in range(256): + if bytes([flag]) not in SUPPORTED: + rejected(f"type-{flag}", patch(one, 156, bytes([flag]))) + for label, raw in ( + ("bad-prefix-utf8", patch(split, 345, b"\xff")), + ("bad-name-utf8", patch(split, 0, b"\xff")), + ("bad-both-utf8", patch(patch(split, 0, b"\xff"), 345, b"\xff")), + ("bad-short-utf8", patch(one, 0, b"\xff")), + ("bad-magic", patch(one, 257, b"vstar\0")), + ("bad-version", patch(one, 263, b"01")), + ("base256-size", patch(one, 124, b"\x80" + bytes(10) + b"\x07")), + ("non-octal-size", patch(one, 124, b"8")), + ("bad-checksum", patch(one, 0, b"X", repair_checksum=False)), + ("one-zero-block", one[:1536]), + ("no-zero-blocks", one[:1024]), + ("short-empty", bytes(512)), + ("partial-block", one[:-1]), + ("trailing-garbage", one + b"X" + bytes(511)), + ("second-zero-nonzero", patch(one, 0, b"X", repair_checksum=False, header_offset=1536)), + ("nonregular-data", patch(one, 156, tarfile.SYMTYPE)), + ("legacy-directory", patch(patch(one, 0, b"dir/\0"), 156, tarfile.AREGTYPE)), + ): + rejected(label, raw) + # Invalid later entries reject the whole archive, with no clean prefix output. + two = archive([("first", b"x", tarfile.REGTYPE), ("second", b"y", tarfile.REGTYPE)]) + rejected("late-unsupported", patch(two, 156, b"x", header_offset=1024)) + rejected("late-invalid-utf8", patch(two, 0, b"\xff", header_offset=1024)) + + rng = random.Random(PARSER_SEED) + names = ("file", "dir/nested", "../evil", "/absolute", "./dot//path", "same", "café/data") + for i in range(RANDOM_ARCHIVES): + entries = [(rng.choice(names), rng.randbytes(rng.randrange(0, 1025)), rng.choice(SUPPORTED)) + for _ in range(rng.randrange(1, 7))] + accepted(f"seeded-{i}", archive(entries)) + # Random positions and values in known-invalid classes, with checksums repaired + # except in the checksum case. This exercises the actual parser, not just gates. + for i in range(MUTATED_ARCHIVES): + kind = i % 5 + if kind == 0: + bad = patch(one, rng.randrange(0, 8), bytes([rng.randrange(0xF5, 256)])) + elif kind == 1: + bad = patch(one, 156, bytes([rng.choice([f for f in range(256) if bytes([f]) not in SUPPORTED])])) + elif kind == 2: + bad = patch(one, 263, bytes([rng.randrange(49, 256), 48])) + elif kind == 3: + bad = patch(one, rng.randrange(0, 8), b"Z", repair_checksum=False) + else: + bad = one[:rng.randrange(0, 2048)] + rejected(f"mutated-{i}", bad) + return counts diff --git a/tests/run_tests.py b/tests/run_tests.py index 5bafdd8..2f934a2 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -23,6 +23,8 @@ import tempfile from pathlib import Path +from parser_cases import run_parser_cases + PILOT_DIR = Path(__file__).resolve().parent.parent EXE = PILOT_DIR / ".lake" / "build" / "bin" / "tar-pilot" RESULTS = PILOT_DIR / "tests" / "TEST-RESULTS.md" @@ -43,7 +45,7 @@ def check(name, ok, detail=""): def run_lean(*args, cwd=None): - return subprocess.run([str(EXE), *args], capture_output=True, text=True, cwd=cwd) + return subprocess.run([str(EXE), *args], capture_output=True, text=True, cwd=cwd, timeout=15) def spec_gate(name): @@ -112,7 +114,7 @@ def expected_manifest(entries_data, dest="out"): entries_data: list of (name, data, typeflag_byte).""" lines = [] for name, data, tcode in entries_data: - if tcode not in (ord("0"), 0): + if tcode not in (ord("0"), 0, ord("7")): lines.append(f"SKIP\t{name}\t{tcode}") continue rel = spec_gate(name) @@ -127,10 +129,11 @@ def expected_manifest(entries_data, dest="out"): def main(): # Rebuild even if the binary exists: source edits must reach the tests. subprocess.run(["lake", "build"], cwd=PILOT_DIR, check=True) - regression = subprocess.run(["lake", "env", "lean", "tests/PathSafety.lean"], - cwd=PILOT_DIR, capture_output=True, text=True) - check("path-regressions", regression.returncode == 0, - regression.stdout + regression.stderr) + for name in ("PathSafety", "HeaderSafety"): + regression = subprocess.run(["lake", "env", "lean", f"tests/{name}.lean"], + cwd=PILOT_DIR, capture_output=True, text=True) + check(f"{name}-regressions", regression.returncode == 0, + regression.stdout + regression.stderr) with tempfile.TemporaryDirectory() as td: td = Path(td) @@ -263,6 +266,8 @@ def main(): posixpath.commonpath([root, path]) == root and path != root for path in resolved), f"root={root}, paths={resolved[:5]}") + parser_counts = run_parser_cases(td, run_lean, check, expected_manifest) + # 7. Axiom check: every named theorem must print only standard axioms. ax = subprocess.run(["lake", "env", "lean", "TarPilot/Verify.lean"], cwd=PILOT_DIR, capture_output=True, text=True) @@ -295,7 +300,12 @@ def main(): f"- Files written by the Lean `create` command and read back by Python: {len(files)}", f"- Path regression entries: {len(path_entries)} ({PATH_RANDOM_CASES} random, seed {PATH_SEED}), " f"compared with the spec under {len(DESTINATIONS)} destinations and checked with `posixpath`", - "- `tests/PathSafety.lean`: cleaner, gate, joined-path and relative-resolution regressions", + "- Lean regressions: `tests/PathSafety.lean` (paths and resolution) and " + "`tests/HeaderSafety.lean` (UTF-8 decoding and header writing)", + f"- Parser archives: {parser_counts['accepted']} compared with Python tarfile " + f"({parser_counts['entries']} entries), {parser_counts['rejected']} rejected with no output", + f"- Parser seed: {parser_counts['seed']}; {parser_counts['random_archives']} random valid archives " + f"and {parser_counts['mutated_archives']} mutated archives; every case checks list and manifest", "- Broken inputs rejected with exit code 1: truncated archive, " "random garbage, corrupted checksum", "",