Created shell - #2
Open
sidd-gadgil wants to merge 18 commits into
Open
Conversation
…ckSafe decider
Build the bash-pipeline verifier from scaffold to an executable safety gate.
- Basic: core types (Path, Content, WriteMode, ExitCode) + DecidableEq
- Syntax: closed-world Cmd and Pipeline
- Semantics: total/deterministic evalCmd/evalPipeline execution model, content
helpers, and the stdout out-of-scope threat-model note (v1)
- Policy: classify/ownerOf as a subtree-matching, deny-by-default policy table
- Safety: IsPublic (incl. of_uniq), and SafeCmd/SafePipeline indexed by stdin
content so write_public_ok binds the actual content written
- Decide: checkSafe — an executable prove-or-reject decision procedure
(sorry-free, validated against 20 cases)
- Gate: Verdict + gate entry point
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Replace `abbrev Path := List String` with `System.FilePath`. classify/ownerOf now match on a `segments` helper (`components` with empty segments filtered), so absolute-path components' leading "" is normalized and the Prompt 05 subtree patterns are preserved verbatim. Behavior unchanged: all 26 validation verdicts and the composed-policy report are identical, and every proof ports without modification (they reason on classify/ownerOf results, not Path structure). checkSafe_sound / checkFull_sound axioms remain clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Cosmetic/hygiene only: no behavior, type, proof, or signature changes. Added Lean docstrings to every type, constructor, and top-level declaration (with careful security prose on IsPublic/SafeCmd/SafePipeline and the soundness lemmas). Fixed stale comments (resolved TODO(5b), Phase 5c past-tense, dropped placeholder line). No dead code found; /private no-op and checkCmd's _s documented as deliberate. 2 sorries unchanged; #print axioms clean; all 26 battery verdicts identical. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Task 1: gate = if checkSafe then .permit else .reject; only shellwall_ noninterference remains sorry. Task 2: Test/Battery.lean — 26 #guard assertions (Test/Fixtures.lean), elaborated by lake build via a Test lean_lib in defaultTargets; a moved verdict fails the build (verified by flipping one). Tasks 3-6: ShellWall/Fidelity.lean + fidelity exe (not a default target; lake build stays pure). Shell detection prefers Git Bash over the WSL launcher. Tier 1 stream corpus: 8 shouldMatch all PASS, grep/wc/sort divergences recorded (wc matches under file-redirect, diverges under pipe; sort C-locale here). Tier 2 filesystem PoC: 4 cases PASS. No fidelity bugs found. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…it-code flow) Test/ImplicitFlow.lean: noninterference_false_via_implicit_flow, proved (no sorry). An andThen whose guard's exit depends on private content gates a public write, so private data sets public state without copying bytes — 1 bit per conditional, andThen/orElse only (seq control confirms no leak). SafePipeline for the leak comes from the proven checkSafe_sound, so it's accepted honestly; checkSafe/gate permit it in both states. Axioms: the standard three plus native_decide (ofReduceBool), forced by FilePath's kernel-irreducible classify; checkSafe_sound/checkFull_sound stay axiom-clean. shellwall_noninterference unchanged (still the only sorry). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
touchesOnlyPublic (Semantics): a pipeline touches only public paths. SafePipeline andThen/orElse now carry hguard : touchesOnlyPublic p₁ = true, and checkFull's andThen/orElse safety conjunct gains && touchesOnlyPublic p₁. A public-only guard's exit code is public-determined, closing the exit-code implicit channel (Prompt 13). checkSafe_sound/checkFull_sound re-proved, still axiom-clean (three standard). Only battery movement: C4 flips permit→reject (private-reading guard); leak added as a permanent rejected entry; ImplicitFlow.lean converted to a rejection witness. shellwall_noninterference unchanged (still the only sorry). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…e IsPublic) Test/ExplicitFlow.lean: noninterference_still_false (no sorry). A plain pipe `cat /private/secret > /public/out` is SafePipeline-accepted whenever secret's bytes coincide with some public path's bytes in each state, yet copies private data to a public path — public projection differs across agreeing states. Independent of the Prompt-06 witness bug, the Prompt-13 implicit flow, and the Prompt-14 guards. Root cause: IsPublic s c is PER-STATE (value is public in s) not provenance-based (built from public reads). The decider checkSafe REJECTS it (provenance flags the private read), so the leak is in SafePipeline \ checkSafe. isPublic_agrees proved as a reusable building block. shellwall_noninterference marked KNOWN-FALSE; still the only sorry; checkSafe_sound/checkFull_sound axiom-clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… IsPublic leak) Finding: the Prompt-15 leak cannot be fixed by a local IsPublic/of_public_read tweak — no per-state, value-based obligation can force the written content to be equal across agreeing states (the two runs' stdins genuinely differ, each individually public). The fix must thread forward PROVENANCE, matching the already-correct decider. Spec change (only IsPublic/SafeCmd/SafePipeline; decider unchanged): - Semantics: move cmdOutIsPublic here, add provOut (pipeline-level forward provenance = checkFull's .2 component). - SafeCmd/SafePipeline gain a `pub : Bool` provenance flag, threaded via provOut exactly as checkFull threads it. write_public_ok now requires `pub = true` instead of `IsPublic s stdin`. IsPublic retained for isPublic_agrees, no longer the obligation. - checkFull_sound re-proved and SIMPLER (write obligation is the checkable flag; second component is now the provOut alignment, no IsPublic reconstruction). checkSafe_sound: SafePipeline ... .empty false. Both stay axiom-clean (three standard axioms — fully symbolic). Result: the leak `cat /private/secret > public` is now rejected by SafePipeline itself (write_public_ok's pub=true is unsatisfiable; provenance of a private read is false), not just by checkSafe. ExplicitFlow.lean converted to a rejection witness (safe1/safe2 no longer typecheck, by design); isPublic_agrees kept. All battery verdicts unchanged (decider untouched). shellwall_noninterference marker updated (no longer known-false; believed provable, Prompt 17). Still 1 sorry. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
ShellWall/Parser.lean: parsePipeline (String → Except String Pipeline), unverified tooling entirely upstream of the verified core (not imported by any spec/decider/ proof). Deny-by-default: out-of-fragment input is rejected, never coerced. Drop three files from the tracked/pushed tree, keeping them as local working files (no history rewrite, not deleted from disk): - Test/ImplicitFlow.lean, Test/ExplicitFlow.lean (Prompt 13-16 investigation witnesses; ExplicitFlow also held isPublic_agrees, referenced only in Safety.lean prose comments, not code) - Test/ParseRoundtrip.lean (this session's parser round-trip test; stays local) Test.lean now imports only Battery so the pushed tree builds standalone. Verified: lake build green (24 jobs), 1 sorry (shellwall_noninterference), checkSafe_sound/checkFull_sound axiom-clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Step 0 finding (sufficiency): the fix IS sufficient, incl. compound guards. A conditional's guard exit is public-determined iff the guard reads only public paths (touchesOnlyPublic, Prompt 14) AND its incoming stdin is public-provenance. `.empty` must count as public-provenance (constant, agrees across runs) or legitimate top-level `a && b` is wrongly rejected. Compound/nested guards are handled by the inductive exit-agreement fact (proved by induction over guard structure) plus the per-conditional hstdin premise; no fifth channel found. Fix (spec + decider; nothing weakened): - SafePipeline.andThen/orElse gain `hstdin : pub = true ∨ stdin = .empty` alongside the existing hguard. (Chose the `∨ stdin=.empty` disjunct over re-threading pub=true for .empty: same acceptance, minimal change, no theorem-statement change, and only private-fed conditionals move.) - checkFull andThen/orElse safety conjunct gains `&& (pub || decide (stdin = .empty))`. Exit-aware output-flag logic (Prompt 09) unchanged. - checkFull_sound re-proved: the four conditional sub-cases discharge hstdin from the new decider conjunct (Bool.or_eq_true + of_decide_eq_true). checkSafe_sound/ checkFull_sound stay axiom-clean (three standard axioms). Fourth leak `cat /private/secret | (grep yes && (cat /shared/ref > pub))` now rejected by SafePipeline itself (hstdin unsatisfiable: private-provenance stdin) and by checkSafe, both states. Three prior counterexamples stay closed; the two legitimate controls (.empty-stdin and public-fed conditionals) still permit. No existing battery verdict moved; added the fourth counterexample + both controls as permanent entries. Marker updated (four holes closed; believed provable). 1 sorry. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The relational (two-execution) noninterference theorem is now PROVED against the current spec, after four prior refutations (each against a spec with an open hole, all four now closed). No sorry anywhere; #print axioms shows exactly [propext, Classical.choice, Quot.sound] (no sorryAx, no native_decide/ofReduceBool). Proof infrastructure added to Safety.lean, bottom-up: - agreement algebra: updateState_agrees, updateState_private_agrees, updateState_private_self, agree_symm/agree_trans, publicProjection_eq_of_agree; - evalCmd_agrees: command-level relational agreement (the single base case) — consumes the Prompt-16 pub-provenance write obligation so equal content lands in public paths; private writes touch only private paths; - touchesOnlyPublic_agrees: the public-program-counter lemma (Prompt-14 hguard payoff) — a public-touching guard has agreeing state, EQUAL stdout, EQUAL exit across agreeing states with equal stdin; induction covers nested/compound guards; - eval_agrees: the main induction carrying (1) public-state agreement, (2) stdout equality when provOut = true, (3) provOut-flag agreement. The andThen/orElse cases derive stdin1 = stdin2 from BOTH runs' hstdin premises (Prompt 21), fire touchesOnlyPublic_agrees to get guard-exit agreement, so the SAME branch runs in both — then recurse. shellwall_noninterference specialises eval_agrees to top-level .empty stdin (pub = false makes the stdin obligation vacuous) and lifts state agreement to equal public projections. checkSafe_sound/checkFull_sound remain axiom-clean; the 30-case battery still passes (four counterexamples rejected, controls permit). v1's verified core is complete: zero sorry, machine-checked end-to-end noninterference for a gate that survived four soundness attacks. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The noninterference proof (c56497b) confirmed the verified core runs entirely on forward provenance (provOut / the pub flag) and never touches IsPublic or isPublic_agrees. Remove the dead value-based predicate so the upcoming trusted-kernel refactor builds on a clean tree. Step-1 inventory (tracked *.lean): IsPublic and its constructors (of_public_read/of_concat/of_filter/of_sort/of_uniq) were referenced in tracked CODE only by their own definition in Safety.lean; every other tracked hit was prose. isPublic_agrees is prose-only in the tracked tree (defined solely in the untracked Test/ExplicitFlow.lean). No tracked code — provOut, cmdOutIsPublic, checkFull, checkSafe_sound, shellwall_noninterference — depends on it. Prose-only ⇒ safe delete. Changes: - Safety.lean: delete the `inductive IsPublic` + its 5 constructors and docstring; the load-bearing "never certify aggregation as public" note survives in cmdOutIsPublic (`| .wc => false`). Replace with a short provenance design note. - Reword the stale prose that named IsPublic / isPublic_agrees / its constructors as if live (Safety SafeCmd + SPEC-HISTORY docstrings, Decide checkCmd/checkFull_sound comments, Policy path-class rationale, Semantics threat-model + provOut docstrings, Battery case 9c) to describe the current provenance-based design; each notes the Prompt-22 deletion where it aids the historical narrative. - isPublicPath (Bool classifier) and cmdOutIsPublic are unrelated and untouched. Test/ExplicitFlow.lean (untracked, holds isPublic_agrees) left on disk untouched; it is a local artifact, not in the build graph. Verified: lake build green (24 jobs, 30-case battery passes), 0 sorry in tracked source, #print axioms for shellwall_noninterference / checkSafe_sound / checkFull_sound all [propext, Classical.choice, Quot.sound], autoImplicit still off. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…idge Restructure the trust story per the manager's design: a small, auditable inductive characterization of public-provenance, the fast Bool functions proven sound against it, and an explicit trusted/untrusted boundary. Option (A): SafePipeline and shellwall_noninterference are UNTOUCHED (zero risk to the capstone); the kernel + bridge sit alongside as the trusted characterization and its soundness link. New (ShellWall/Provenance.lean): - PublicProv : Cmd → FileState → Bool → Prop — the atomic public-provenance kernel. Genuinely PROVENANCE not value: indexed by the command/execution, so a private read has NO constructor even when its bytes coincide with a public file (the deleted value-based IsPublic could not express this — the third soundness hole). No aggregation constructor (wc/count/hash), mirroring cmdOutIsPublic's `| .wc => false`. - cmdOutIsPublic_sound : cmdOutIsPublic c s pub = true → PublicProv c s pub. - PipeProv : Pipeline → FileState → Content → Bool → Prop — the pipeline lift, threading through operators exactly as evalPipelineFull runs; references the execution MODEL but NOT the decision functions. The `pipe` case guards its inner flag (b = true requires a PipeProv proof of stage 1), so `cat priv | grep x` is correctly not PipeProv. - provOut_sound : provOut p s stdin pub = true → PipeProv p s stdin pub, by induction mirroring provOut's recursion. Both bridges: no sorry, axioms [propext, Classical.choice, Quot.sound]. Boundary made explicit (docstrings, no code moved): - ShellWall.lean: ARCHITECTURE note — trusted base (classify/ownerOf tables, CanWrite/SafeCmd/SafePipeline, PublicProv/PipeProv) vs untrusted-proven-sound (cmdOutIsPublic/provOut/checkFull/checkSafe) vs untrusted-fidelity-tested model (evalCmd/evalPipelineFull, parser, executor); the bridge theorems connect them. - Safety.lean: "TRUSTED KERNEL — the safety spec" section marker over CanWrite/SafeCmd/SafePipeline; provenance note cross-refs PublicProv. - Decide.lean: "UNTRUSTED DECISION LAYER (proven sound)" header. Framing (what's new vs. present): checkSafe_sound/checkFull_sound already bridged the Bool decider to the inductive SafePipeline — not rebuilt. New here is (1) the atomic inductive public-provenance kernel (provOut/cmdOutIsPublic were only Bool functions before), (2) its soundness bridge, (3) the explicit module boundary + ARCHITECTURE note. Verified: lake build green (26 jobs, 30-case battery passes), 0 sorry, autoImplicit off; #print axioms clean on shellwall_noninterference, checkSafe_sound, checkFull_sound, cmdOutIsPublic_sound, provOut_sound. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Two cleanup tasks on the verified core. No behavior, spec, proof, or signature
changes — comment/docstring edits only; build green, 0 sorry, all five key theorems
still axiom-clean.
Task 1 (dead-code / duplication sweep): inventoried every declaration and reference.
No dead code found — every helper (updateState_agrees, agree_symm/trans,
updateState_private_self, publicProjection_eq_of_agree, evalCmd_fst_read/grep,
evalCmd_agrees, touchesOnlyPublic_agrees, eval_agrees, byteArray_eq_of_data_eq) is
referenced by a live proof; the deleted IsPublic orphaned nothing (isPublicPath_sound/
grep_out were retired earlier). evalPipeline (wrapper) and evalPipelineFull (threading
helper) are both used. The provOut/cmdOutIsPublic (Bool) <-> PublicProv/PipeProv
(inductive) pair is the intended function/kernel coexistence linked by the bridge —
left intact, not collapsed. Linter clean (no unused imports/binders). No deletions.
Task 2 (strip process scaffolding from comments/docstrings): removed every "Prompt NN"
citation, process/tooling reference, and build-history narration across ShellWall/ and
Test/, preserving the design rationale (the why) and dropping only the scaffolding.
Reworded IsPublic tombstones to state the value-vs-provenance rationale without the
deletion history. Design-doc section citations (no design doc ships — only README.md)
rewritten inline: §4 -> "this project's central assumption", §7.3 dropped, Phase 5 /
gap C2 removed. The ARCHITECTURE note and kernel docstrings kept their substance
(trusted/untrusted/bridge) with process framing scrubbed ("the manager's ..." ->
plain statement). grep for Prompt/Claude/CC/Phase/§/manager across tracked
ShellWall/ and Test/ now returns empty.
Untracked witness files (Test/ImplicitFlow.lean, ExplicitFlow.lean, ParseRoundtrip.lean)
left untouched.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Just the skeleton