AI REVIEW: THE AUTOMATED CHECKS

Written by AI. Held to an unusually strict test bar.

secure-terminal is AI-assisted software. Precisely because a machine wrote it, the security claims are not asked to rest on trust: they rest on a large, automated, adversarial test suite and separate analysis passes that run on every change. This page lists exactly what is checked, so you can read the tests, not just the marketing. Every claim below is something you can verify in the code.

1. The adversarial corpus: real, disclosed attacks

The core of the audit is the terminal-poc-corpus: 32 proofs-of-concept drawn from actual, publicly-disclosed terminal vulnerabilities - answerback injection, DECRQSS and device-status reflection, bracketed-paste bypass, charset-shift deception, cursor-addressing spoofs, homoglyph and Trojan-Source text, iTerm2 title-report injection, and more. Each carries a machine assertion that secure-terminal neutralises it. That corpus is what proves the guarantees; the conformance suites only confirm ordinary programs still render.

Because the corpus stores real attack payloads, it is handled carefully - see the corpus SAFETY notes for the full handling. Two properties matter most:

Hex-encoded. Each payload is stored as hexadecimal in a payload.hex file, not as raw bytes, so browsing or grepping the repository can never accidentally feed a live escape sequence to your own terminal or a code viewer. It is decoded only at run time.

Canary-forked. Each attack is paired with a variant that, on a vulnerable terminal, would write a known "canary" marker file. The harness runs it and checks for the marker, so it can tell "the terminal actively neutralised this" apart from "the test silently did nothing" - the test proves the attack would have fired.

2. A security invariant over the whole spec surface

Beyond the curated attacks, the conformance harness feeds the entire reflection-class spec surface - 387 escape sequences - to secure-terminal in CLI mode and checks three invariants on every one. These are the query and report sequences a terminal historically answers, and answering them is the "output becomes input" bug class; each is documented in the XTerm Control Sequences reference:

the primary, secondary and tertiary device-attribute queries (DA1/DA2/DA3);
DECRQSS (request a setting the program just set), and the XTVERSION and XTGETTCAP name/version and terminfo queries;
the cursor-position and device-status reports (DSR/CPR), and ENQ answerback;
the window-size/position and palette/colour queries.

The class, and why answering any of them is dangerous, is laid out in David Leadbeater's 2023 terminal-security review. On each sequence the harness checks:

i. Nothing is written back to the pty. A vulnerable terminal answers a query by writing its reply onto the same channel - which is the program's keyboard. secure-terminal must write zero bytes back, for every query. This is the whole "output becomes input" attack class, closed and asserted.

ii. Nothing non-ASCII is smuggled to the screen. The rendered text may contain only printable ASCII plus tab, newline, and the documented line-local cursor controls (backspace and carriage return, plus the effect of CSI C/D/G/K, all clamped to the line being written). Any other control byte, or any codepoint above 0x7e (the invisible / bidi / homoglyph classes), is a violation.

iii. Nothing crashes. Every sequence must render in bounded time without an exception, including deliberately malformed and over-long ones.

The harness checks itself, too. A positive control feeds a deliberately-vulnerable result and asserts the check FLAGS it; a negative control runs the same predicate over a known-bad terminal to prove the check can actually detect a failure. And a dedicated check asserts that CLI mode never even instantiates the pyte screen engine - so there is no VT state machine to attack in the default mode. A test that cannot fail proves nothing; these can.

3. A machine-checked proof, over every possible input

Everything above samples the input space: the corpus runs crafted attacks, the invariant harness runs 387 spec sequences, the property and fuzz tests run random and generated input. A separate artifact (verify_formal.py) goes further and proves the sanitizer's core safety properties - input and output - hold for every possible input, with no sampling. It runs in CI on every change (local-formal-verification.yml) using the Z3 SMT solver together with exhaustive enumeration. It is deliberately scoped to the pure, Qt-free sanitizer - the code the tests above exercise - not the whole application.

Theorem 1 - output inertness. The CLI wrapper writes the sanitizer's output straight to your real terminal, so that output is the attack surface. The proof establishes that for any program output whatsoever, in the strict display modes, every byte the sanitizer emits is inert: printable ASCII plus tab, newline, and the two honored cursor controls (backspace and carriage return) - and nothing else. No escape, control, bidi, invisible or homoglyph byte can ever reach the outer terminal. This is checked on the real sanitizer for all 1,114,112 Unicode code points, and the codepoint-badge arithmetic is proved symbolically in Z3 for the entire codepoint range at once. This is the "output becomes input" guarantee of the invariant harness above (item ii), lifted from a 387-sequence check to a proof over all inputs. The richer "show" display mode, which by design lets a printable non-ASCII glyph through, is separately proved to still never emit an invisible, bidi, or control byte.

Theorem 2 - line containment. The line editor is proved, by induction in Z3 over its state machine, to keep the cursor within the line currently being written for every possible input - so program output can never move up into an earlier line or the scrollback, and a completed line, once shown, is never rewritten. The abstract model Z3 reasons over is validated against the real line editor on an exhaustive grid of states, so the proof binds to the actual code rather than a hand model.

Theorem 3 - input and clipboard safety. The same technique proves the input side over every input: a pasted string can never carry an escape, control, bidi or invisible character to the shell and can never auto-execute - no trailing carriage return survives, so a single-line paste waits for your Enter; nothing placed on the system clipboard carries a control, bidi or invisible byte, and the ASCII clipboard drops every non-ASCII byte so a homoglyph cannot ride out; a program-supplied window title is reduced to printable ASCII; and every full-screen (TUI) grid cell is a single safe display unit, never an invisible or bidi character. The paste warning is also proved to name a character the SAME class the on-screen colour does, so the two can never disagree.

Theorem 4 - split escapes cannot leak. Output arrives one read at a time, and an escape can be cut across a read boundary. The wrapper holds the fragment so its tail cannot render as text - proved by bounded exhaustion: every short stream over the escape alphabet, under every possible chunking, renders identically to the whole-stream case, together with a bound that a never-terminated sequence stays constant in memory. Stated honestly, this one is bounded (short streams) rather than the unbounded induction of Theorem 2; the pathological over-length path stays fuzz-tested.

What it does and does not cover, plainly. This verifies the whole pure sanitizer - the neutralization, line-editing, paste, clipboard and cell core, input and output. It does not prove the Qt widget itself, the pyte full-screen emulator, the pseudo-terminal plumbing, or the "nothing is written back to the pty" half of the closure (Theorems 1-4 cover what the sanitizer produces; the no-write-back side and the emulator stay covered by the invariant harness in section 2 and the fuzz / differential tests, which drive the live widget and emulator). One data assumption - that Unicode character names are ASCII - is not assumed but discharged, by exercising the real code on every named code point. And, like the harness above, each proof is self-checked: twenty deliberately broken models must each make a proof fail, so a passing run means the checks have teeth.

4. Reference-parser self-tests

TUI mode renders through a confined pyte screen model. The audit runs pyte's own test suite at the reviewed pin, and cross-checks against libvterm, so the engine secure-terminal relies on is held to its own correctness bar. The public conformance suites (esctest2, pyte, libvterm, vttest) are tracked not to pass them - CLI mode "fails" them by design - but as a corpus of every sequence a real program might emit. Full detail on the compatibility page.

5. Unit, GUI, property and fuzz tests

The application itself carries a large suite that runs in CI on every change, shipped as packages in dist-ai.

Suite	What it checks
Core sanitizer (`test_secure_terminal`)	~336 assertions over the Qt-free sanitizer: escape stripping, the four unicode display modes, paste sanitisation, bell detection, the render invariants.
Widget / GUI (`test_widget`)	~626 assertions driving the real Qt widget headless: line editing, scrollback, the paste warning, caret handling - and the character-inspect copy guard that asserts the popup copies the `\uXXXX` escape and never the raw glyph.
Corpus runner (`test_corpus`)	Runs the dangerous corpus, an every-codepoint sweep over all of Unicode, the Trojan-Source techniques and the git-diffs-lie fixtures against the shipped code, so these attacks gate the package, not just a standalone harness.
Property + fuzz (`test_fuzz`, `fuzz_secure_terminal`)	Hypothesis property tests (idempotency, ASCII-only output, box-to-underscore export) plus a randomized fuzzer that throws adversarial input at the parse/render path and asserts no crash and every invariant, printing the seed on failure.
Coverage-guided fuzzing (ClusterFuzzLite + Atheris)	Seven in-tree fuzz harnesses (the line-mode editor, the strip renderer, the paste sanitiser and classifier, the safe-colour SGR parser, the single-instance IPC frame reassembler, and the settings/session parsers) run under the OSS-Fuzz engine on every PR that touches the parse path, via local-python-fuzz.yml.
AppArmor (`secure-terminal-tests-apparmor`)	Confirms the shipped AppArmor profile loads and confines the application (defence in depth around the memory-safe core).

Coverage. A continuous-integration ratchet gate enforces 100% line coverage on every module of the package - the sanitizer, CLI wrapper, IPC framing, session persistence, settings, and the dialog/terminal/main GUI - so a line the tests stop reaching fails the build. Every module is gated, with no un-gated glue left, so whole-package line coverage is 100% (re-verified 2026-08-12).

6. Static analysis and continuous scanners

Alongside the tests, several static analysers run on the repository. Each is a committed GitHub Actions workflow.

Scanner	What it looks for	Runs
Bandit	Common Python security anti-patterns (unsafe subprocess, eval, temp-file races, weak crypto).	On every change (consumer-bandit.yml).
CodeQL (Python)	Dataflow / taint analysis over the Python code - untrusted input reaching a sensitive sink.	On every change (consumer-codeql-python.yml).
CodeQL (Actions)	The same analysis applied to the GitHub Actions workflows themselves (injection, unpinned actions).	On every change (consumer-codeql-actions.yml).
Coverity	Deeper interprocedural static analysis.	Active - weekly scheduled scan (consumer-coverity.yml); findings land on the Coverity dashboard.

7. AI review by other models

Because the code is AI-authored, it is also AI-reviewed - by different models than wrote it, with fresh context, as a second opinion. This is not an independent third-party audit; it is a different tool looking for defects the authoring model missed. Unlike the checks above, this is run on demand (before a change lands), not on a schedule:

Codex and CodeRabbit review the diff for logic, design and security defects; a fresh-context Claude reviewer does a final local sweep. Each finding is then reconciled individually - verified against the code, applied if real, dropped with a stated reason if not - rather than applied blindly, so the reviewers are advisors, not an autopilot. Real defects caught this way are fixed before the change lands.

8. A live differential regression test

An opt-in test (terminal-resilience-tests) feeds the crafted hostile log to secure-terminal and asserts the neutralisation directly: the output carries no escape byte and no title marker, on every run. That is the part that protects you - a continuous guard that the safe behaviour has not regressed.

The same test also feeds the payload to a real traditional emulator and checks its window title is hijacked. That is not a claim that benefits you; it is a positive control - if a known-vulnerable terminal is somehow not hijacked, the harness itself is broken and the secure-terminal half would be meaningless. It is the automated version of the comparison, and you can reproduce it yourself.

Read the corpus See the comparison Compatibility detail

Run the evidence yourself

None of this is take-our-word-for-it. The adversarial corpus - the check that proves the neutralization claims - is clone-and-run in a sandbox VM.

The adversarial corpus sandbox VM only

real disclosed attacks, hex at rest - asserts secure-terminal neutralizes each

# clone the corpus (read SAFETY.md first):

git clone https://github.com/secure-terminal/terminal-poc-corpus && cd terminal-poc-corpus

# drive secure-terminal with every PoC and assert each is neutralized:

POC_CORPUS_IN_SANDBOX=1 harness/adversarial.py

# the reflection-class spec surface (the "output becomes input" invariant):

POC_CORPUS_IN_SANDBOX=1 harness/conformance.py

Every PoC doubles as a test fixture: index.json records each one's class, CVE and expected-safe behaviour; payloads are hex-encoded and canary-forked (the few real decoder/DoS triggers are risk-tiered and sandbox-gated). The rest of the suite - the unit, GUI and Z3 formal-proof runner (secure-terminal-tests, run against a secure-terminal checkout via SECURE_TERMINAL_REPO), the resilience suite (terminal-resilience-tests) and the fuzzers - lives in dist-ai.