Repository navigation
Land Set B audit fixes with strict archive termination #7
Description
Two sets of open PRs fix the findings of the bar audit (Proven-Commons/mission#1). Both change TarPilot/Path.lean, TarPilot/Archive.lean, TarPilot/Header.lean, Main.lean, README.md and tests/run_tests.py, and both add SPEC.md. So only one set can merge, and the other should then be closed.
- Set A: Correct the status line: built, not yet verified #1 → Prove joined-path containment and share extraction with the CLI #2 → Reject unsupported tar metadata and check the pilot in CI #3. Correct the status line: built, not yet verified #1 corrects the status line and comes from a Claude session. Prove joined-path containment and share extraction with the CLI #2 and Reject unsupported tar metadata and check the pilot in CI #3 come from Codex.
- Set B: Prove containment for every line the tool prints (audit F1, F5) #4 → Reject what the pilot cannot read, extract contiguous files (audit F2-F4) #5 → Adopt verified bar v2 for tar (in progress: spec approval pending) #6, from a Claude session. Prove containment for every line the tool prints (audit F1, F5) #4 makes the same status-line change as Correct the status line: built, not yet verified #1.
How they differ
| Set A | Set B | |
|---|---|---|
| Audit findings | F1 to F5, and F6's axiom gap | F1 to F6, and three more found in review (listed in #5) |
| The path gate rejects | absolute names, and .., / or NUL in a component |
the same, and control characters (C0, DEL, C1) and the line and paragraph separators U+2028 and U+2029 |
| Names in the output | printed as they are | escaped, and a proof pins every line manifest prints |
| GNU-format archives | all rejected, including what GNU tar writes by default for short names | read when the header carries nothing ustar does not; long names and other GNU extensions rejected |
| End of the archive | two zero blocks, and only zeros after them | the first zero block, as GNU tar and Python's tarfile read it |
| Proof check | lake check --paranoid in CI |
verified bar v2: a Spec.lean of reviewed statements, lake comparator --paranoid, and bar.toml |
| Differential tests | 2,641 checks: 512 random and 512 mutated archives | 23,243 checks: 10,000 random archives, half of them mutated |
| CI check | Proofs and differential tests |
bar / bar, the verified-bar workflow from mission#2 |
Forged output lines
On main, and on Set A, an archive can make manifest print a line naming a path outside the destination. Take an entry whose name is a, a newline, OK, a tab, /etc/passwd, a tab, 5, a tab, 500, a newline, and b. Then tar-pilot manifest <file> out prints (␉ marks a tab):
OK␉out/a
OK␉/etc/passwd␉5␉500
b␉5␉532
A program that reads the manifest line by line sees a file extracted to /etc/passwd. Set A's gate accepts newlines and tabs, and its Main.lean prints names unchanged. Set B rejects that name and prints it escaped. Its theorems manifest_lines_eq and manifest_lines cover every line it prints.
Cross-test
Set A's 2,600 parser checks (tests/parser_cases.py) were run against Set B's build. All 517 archives Set A reads give the same list and manifest output on Set B. The 31 cases that differ come from two rows of the table: GNU-format headers and the end of the archive.
Decisions needed
- Which set to merge. The other set then closes. If Set B is chosen, Correct the status line: built, not yet verified #1 closes too, because Prove containment for every line the tool prints (audit F1, F5) #4 carries its change.
- If Set B: adopt Set A's end-of-archive rule? Under Set B's current rule, a reader run with
--ignore-zeroswould extract entries hidden after a single zero block, and the pilot never lists them. Set A's rule rejects such archives. It can be ported into Reject what the pilot cannot read, extract contiguous files (audit F2-F4) #5 and Adopt verified bar v2 for tar (in progress: spec approval pending) #6.
The recommendation is Set B, with Set A's end-of-archive rule ported into it. It comes from the session that wrote Set B, so weigh it with that in mind. Every row above can be checked against the PRs.
Requiring a check on main waits on this choice, because the two sets add different checks (tracked in mission).
Current landing plan
Use Set B (#4, #5, #6), with the strict end-of-archive rule: at least two zero blocks, only zero padding afterward, and an input length divisible by 512. The current-head code reviews request these fixes and the correction of README proof scope. The shared status correction in #1 can land independently; it does not select the unsafe output path in #2 or #3. Those competing implementation branches remain unmerged until a replacement lands.
Current work
Set B is selected. The current review requests strict archive termination; #4 and #6 also have proof-scope and specification corrections pending.
Awaiting the changes requested in code review: #5.
Activity
zero-aska commentedon Oct 27, 2026
This is an independent check of the comparison above, for the decision. One agent checked each row against the PR heads: #3 at
511465ais the top of Set A, and #6 ata04d5a4is the top of Set B. A second agent then tried to refute each finding. Neither agent ran the projects' binaries. The evidence comes from:tarfile, on archives built for the purpose;What holds
--format=gnushort-name header is rejected by A and read by B;mainand on Set A. Set B rejects the name and prints it escaped./, NUL or.., absolute names are rejected, and symlink and hardlink entries are never extracted.Corrections the table needs
The "Audit findings" row undersells Set A. By rejecting archives, A already closes two of the three extra findings listed in Reject what the pilot cannot read, extract contiguous files (audit F2-F4) #5:
Header.lean:69), so a file cannot hide in a symlink's or directory's payload;Header.lean:62-63), which covers the incremental time fields.Only the third item stays open in A: typeflag
0or7with a name ending in/. A also closes F6 as the audit's own fix text defines it. It has an axiom allowlist intests/run_tests.py:276-284and runslake check --paranoidincheck.yml.Set B's test count is stale. The record at
a04d5a4says 23,269 checks from 10,059 inputs, and CI reports 10,059. The 23,243 figure belongs to the earlier headf0e17be.The "CI check" row gives Set A's workflow name. The check run GitHub reports, which is what branch protection would match, is
check.Proofs and differential testsis the workflow name. Requiring that name would wait on a check that never reports.The forged-line section leaves out that Set A documents this limit. See its
SPEC.md:71-72("names containing tabs or line breaks are printed literally") andREADME.md:44. Set B removing the limit is still the stronger position.Two points the issue does not raise
Statements that pin the rules. Every Set A theorem is soundness-only: each is guarded by
gate … = some,extractEntry … = someor… ∈ extractAll. So implementations that differ from the page still satisfy all 14 statements. A check in Lean confirmed this for each of these mutants:cleanComponentsthat also drops a componentx;extractEntrythat always returnsnone.None of these escapes the destination. But A's README lists the gate rules under "What is proved", which is the kind of gap audit F1 was about. Set B pins the same rules exactly with
gate_eq,manifest_eqandmanifest_lines_eq. A row for this would be: "Statements pin the rules exactly: A no, B yes."The
--ignore-zerosgap is wider than one zero block. GNU tar-iandtarfilewithignore_zeros=Truealso read entries after a correct two-zero-block end, as in a plaincat a.tar b.tar. Set B stops at its first zero block (Archive.lean:37), so its manifest omits those entries too. Set A rejects both cases. So decision 2 needs A's whole end rule:A narrower "reject a lone zero block" rule would leave the concatenated case open.
One overclaim in Set B: its
README.md:3says every line the tool prints for a parsed archive is proved.listlines are covered by no statement, and B's ownREADME.md:45andSPEC.md:78say so. "Every linemanifestprints" would be accurate.For the decision
The evidence supports the recommendation: Set B, with Set A's full end-of-archive rule ported into #5 and #6. The table should first be corrected as above. The case for B is also stronger than the table shows, because B's statements pin the rules and A's do not.
Generated by Claude Code
[-]Decide which set of audit-fix PRs to merge: #1–#3 or #4–#6[/-][+]Land Set B audit fixes with strict archive termination[/+]orda-aska commentedon Oct 29, 2026
Status on 2026-10-29: tracked by the Set B stack #4 → #5 → #6. All three heads are unchanged since the change requests, and each request still applies:
85ef13a): Prove containment for every line the tool prints (audit F1, F5) #4 (review). Narrow the README.md:3 claim tomanifestlines. The branch also now conflicts with main inREADME.mdandlakefile.toml, after Correct the status line: built, not yet verified #1 and Add the Apache License 2.0 #8 merged, so it needs a rebase.5efda8c): Reject what the pilot cannot read, extract contiguous files (audit F2-F4) #5 (review). Adopt the strict end-of-archive rule (two zero blocks, only zero padding after them, length a multiple of 512), with rejection tests that include concatenated archives.TarPilot/Archive.lean:37still returns at the first zero block.a04d5a4): Adopt verified bar v2 for tar (in progress: spec approval pending) #6 (review). Carry the same end rule intoSPEC.md, the model and the tests, and narrow the README.md:3 claim. The spec approval is still not recorded inbar.toml.Set A (#2, #3) still has changes requested for the unescaped names in
Main.lean. It stays open until Set B lands, and then closes as superseded.Generated by Claude Code