Skip to content

AFFIRMATION.adoc

Latest commit

 

History

History
120 lines (97 loc) · 5.69 KB

AFFIRMATION.adoc

File metadata and controls

120 lines (97 loc) · 5.69 KB
Raw

AFFIRMATION — 0patch-lsa-sentinel, as of 2026-07-02

the No-Bullshit file: what we affirm was true and checkable at this moment.

Table of Contents

What this is, and how it works

A short, dated, signed snapshot of what Jonathan D.A. Jewell can honestly and verifiably claim about 0patch-lsa-sentinel at one exact commit. Nothing here is marketing and nothing is a promise about the future — those live in README.md and DESIGN.md. This file is the receipt.

It stays trustworthy through three moving parts:

  1. Ground truth, not memory. Every claim below is produced by running the project’s own checks (gnatprove, idris2 --build, cargo test, zig build test) — not by trusting a status doc.

  2. A frozen anchor. The file names the commit, branch, UTC date, and toolchain (see Verifiable anchor); "true" means "true at this point".

  3. A real signature. It is landed by a signed git commit.

We are fallible. This is our best honest belief, not a proof of its own correctness. Treat it as a falsifiable claim, not gospel.

The epistemic contract

This document records the maintainer’s best belief at the timestamp below. It is not a guarantee of correctness. The only guarantee is no intentional overclaim: where something is proven we say "proven"; where it is untested or speculative, we say so. You are invited to refute any claim here with a counter-example, a failing run, or a contradicting source.

What we affirm

Claim Status Evidence (command / file:line)

The SPARK classifier (Sentinel.Classifier.Classify) is proved pure, total, and free of runtime errors

proven

just prove → gnatprove -P sentinel_core.gpr --level=2 --report=all discharges all VCs

The classifier verdict is cross-checked across four languages (SPARK kernel, Idris2 ABI, Rust host, Zig FFI seam) against one shared contract

affirmed

core-spark/, abi-idris2/src/Sentinel/ABI.idr, host-rust/src/classify.rs, ffi-zig/src/sentinel_ffi.zig; just all

The Idris2 ABI proofs type-check and totality-check

affirmed

just abi-check → idris2 --build sentinel-abi.ipkg

The single Rust unsafe block (the FFI call) is isolated, documented, and fail-safe decoded (out-of-range → Indeterminate, never a false "covered")

affirmed

host-rust/src/ffi.rs; reviewed in audits/audit-residuals.adoc §1

The design + public alert (why "just turn off LSA Protection" is not good enough) is complete and on the record

affirmed

DESIGN.md, README.md

The registry collector was validated on a real Windows host (2026-07-02): live reg.exe output for RunAsPPL=0x1 parsed correctly as On

affirmed

docs/FIELD-VALIDATION.md §1; host-rust/src/collectors/registry.rs, parse.rs::parse_runas_ppl

The 0patch install paths and the patch-status source (the UTF-16LE agent log C:\ProgramData\0patch\Logs\0patch.log, Patch NNNN applied in application X lines) are field-confirmed on a real install; the speculative list-patches CLI was removed

affirmed

docs/FIELD-VALIDATION.md §2–3; host-rust/src/collectors/opatch.rs

What we do NOT claim

  • Field validation is partial, not total. On 2026-07-02 the collectors were exercised against a real Windows host (LSA Protection ON, live 0patch agent installed) via WSL interop — see docs/FIELD-VALIDATION.md. What that session established and what it did not:

    • Validated: the registry collector — live reg.exe output for RunAsPPL=0x1 parsed correctly as On.

    • Confirmed: the 0patch install paths (C:\Program Files (x86)\0patch\Agent\, casing corrected) and the real patch-status source — the UTF-16LE agent log C:\ProgramData\0patch\Logs\0patch.log. The former 0patchConsole.exe list-patches collector was a guess and has been removed; opatch.rs was rewritten against the field-confirmed log format.

    • NOT yet observed live: the Present path of the patch-status collector — no lsass-targeted patch was outstanding on the validation host, so “Patch NNNN applied in application lsass.exe” has never been seen in a real log; the "no lsass line in the recent log ⇒ Absent" inference remains a heuristic.

    • NOT yet observed live: the CodeIntegrity 3033/3063 block-event path — the wevtutil query ran, but no 0patch block event existed on the host (no user-mode lsass injection attempt was occurring), so the positive-match branch of the event-log collector is unverified in the field.

  • No end-to-end run exists. The full "collect → classify → report" path has never executed on the target platform. The 🟢/🔴/⚪ verdict pipeline is proved at the classifier core but not demonstrated end to end.

  • This is a DESIGN-stage repository. The container (Layer A policy / Layer B sentinel) described in DESIGN.md is specified, not deployed.

  • No affiliation with ACROS Security / 0patch. This is independent, good-faith analysis.

Verifiable anchor

Project

0patch-lsa-sentinel

Repository

https://github.com/hyperpolymath/0patch-lsa-sentinel

Commit (SHA)

a44dedc10e576407b059bcaea4e0f724b366b25d (re-anchor on the signing commit)

Branch

main

Date (UTC)

2026-07-02

Toolchain

gnatprove (SPARK), idris2, cargo/rustc, zig — versions as recorded in .tool-versions / CI at signing time

Affirmed by

Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>

Landed by a signed git commit. Verify with git log --show-signature that the anchor SHA above matches the commit that introduced (or last updated) this affirmation.