[ THE COMPLETE FIELD MANUAL ]
Know what is running.
Usage, configuration, evidence and recovery. Plain text with clickable links, shipped with the software.
[ download + install ] / [ stack YAML ] / [ launch AWS stack ]
Katarina manual
# Katarina manual
Katarina coordinates security reviews of Solidity, Java, Rust, C/C++ and other backend repositories. It scouts for potential issues, records independent reviews, and prepares tests and evidence for human assessment. This manual covers configuration, running and resuming reviews, and preparing reports for an audit. Use the reports to prioritize investigation and document design decisions; completed coverage does not establish that a repository is free of vulnerabilities.
## First review
1. [Download and install the prebuilt executable], or build with `make build` and put `bin/katarina` on your PATH. See [development] for build requirements.
2. Run `katarina init` in your working directory. This writes an example `katarina.yaml` without overwriting an existing file.
3. Provide `DEEPSEEK_API_KEY` for the example configuration, or configure different providers and agent models. The API key stays out of CLI arguments and reports.
4. Run `katarina doctor` to check configuration, linked pi support and installed optional tools.
5. Run `katarina index ./project > inventory.json` to inspect included files and explicit exclusions.
6. Run `katarina start --tui ./project`. Omit `--tui` for normal logs or CI. Flags must appear before the path.
7. Review `.katarina/sessions/SESSION/report.md` and the corresponding JSON. State defaults to `PROJECT/.katarina`; the CLI prints the exact resume command and report directory.
By default, model-generated test files are saved, but not executed. Configure permitted test commands even when execution is off if you want the assessor to request test generation. Then select `tests.runner: local` or `ec2` to enable execution.
Concurrency defaults to 16 model workers; use `--max-agents` to adjust it. Set `--token-budget deepseek=100M` to cap that family's token reservations at 100 million. YAML and CLI caps accept `K`, `M`, `B` and `T` suffixes, including amounts such as `1.5B`. Family labels are configured per agent; flags precede the repository path. The printed resume command retains these overrides. See [budgets and concurrency].
## Continue interrupted work
Use the session ID printed at startup:
```sh
katarina sessions --state ./project/.katarina
katarina resume --config katarina.yaml --state ./project/.katarina SESSION
katarina report --state ./project/.katarina SESSION
```
A completed job is reused, including context-request responses and assessor decisions. A call interrupted before its durable result may be retried and billed again. Billing reservations are retained. An interrupted test is marked indeterminate and is not silently repeated.
Resume requires the same repository root, included file contents, inventory and effective configuration. If code, models, budgets or policies change, begin a new session. Credential values can change without invalidating a session. A process lock prevents two controllers writing the same state directory simultaneously.
## Typical Solidity setup
```yaml
tests:
runner: local
allowed_paths: ["test/Katarina*.t.sol"]
commands:
foundry: [forge, test, --match-path, "test/Katarina*.t.sol", -vvv]
design_notes: [docs/invariants.md, docs/trust-model.md]
```
The example excludes `lib/**`; remove that exclusion if you want vendored Solidity dependencies included and copied to test workspaces. Explain economic invariants, roles, upgradeability, accepted oracle assumptions, token behavior and off-chain dependencies in design notes. The assessor must cite evidence before labeling an issue “by design.”
## Typical Java setup
```yaml
language_servers:
- name: java
command: [jdtls, -data, "{workspace}"]
extensions: [.java]
language_id: java
timeout_seconds: 120
tests:
runner: local
allowed_paths: ["src/test/java/**"]
commands:
maven: [mvn, -B, -Dtest=KatarinaSecurityTest, test]
```
Use a JDK compatible with the chosen JDT LS release and your project. Supply dependency resolution through an operator-controlled command or prepared toolchain. The clean test environment does not inherit credentials or your usual HOME. Read [navigation] and [testing] for the practical implications.
## Choose what to read next
| Task | Guide |
|---|---|
| Download, verify and install; macOS Gatekeeper | [Installation] |
| Current product scope, defaults, contracts and limitations | [Product specification] |
| Terminology, numbered requirements and failure cases | [Behavior and definitions] |
| Providers, models, credentials and spend limits | [Configuration] |
| Components, diagrams, data flow, FFI and recovery | [Architecture] |
| Claude-loop/MDASH principles and comparative evaluation | [Research design] |
| Shared security knowledge, specific questions, evidence and grouping | [Security analysis] |
| Shannon's code-analysis workflow and design influences | [Shannon design review] |
| Solidity economic mechanisms, incentives and game theory | [Economics] |
| Java/Solidity/Rust/C/C++ navigation and analyzer adapters | [Navigation] |
| Generated tests and execution boundaries | [Testing] |
| Create and use temporary EC2 infrastructure | [AWS] |
| Report schemas and recovering evidence | [Reports] |
| Build, test, package and evaluate Katarina | [Development] |
Download and install
# Download and install The current download is **0.1.0-preview.1**, an unsigned development preview. The executable includes pi through FFI and embedded SQLite. Running Katarina itself needs no Go, Rust, Python or database server. Project compilers, test frameworks and optional analyzers/language servers are installed separately. ## Choose a download | Download | Platform and contents | |---|---| | [Linux x86_64 binary archive] | Native pi-linked executable, manual, schemas, examples and dependency notices. Built on Linux x86_64 with glibc 2.35; use Ubuntu 22.04 or a compatible newer glibc distribution. | | [Source archive] | Source snapshot, locked dependency manifests, schemas and website sources. Compilers and dependency downloads are needed to build it. | | [SHA-256 checksums] | Checksums of the downloadable archives. | `amd64` means x86_64, including Intel and AMD processors. This Linux binary does not run on macOS or ARM Linux. On Windows, use an x86_64 Linux environment under WSL. Native macOS archives are not included in this upload; the macOS instructions below apply when a matching native archive is published or provided by the maintainer. See [building from source] for other platforms. These downloads are previews, not a claim that live model providers, AWS execution or security-detection quality have been validated. The source archive corresponds to the packaged source snapshot; its build manifest records the base Git revision, source digest and any working-tree changes. ## Verify and extract on Linux Download both files into a new directory: ```sh curl -fLO https://katarina.fyi/downloads/katarina-0.1.0-preview.1-linux-amd64.tar.gz curl -fLO https://katarina.fyi/downloads/SHA256SUMS sha256sum --check --ignore-missing SHA256SUMS tar -xzf katarina-0.1.0-preview.1-linux-amd64.tar.gz cd katarina-0.1.0-preview.1-linux-amd64 ./katarina version ``` Confirm the archive's checksum reports `OK` before extracting. A checksum detects a changed or incomplete download; an unsigned checksum from the same website does not independently authenticate the publisher. `version` should report `0.1.0-preview.1` and `pi FFI linked: true`. The archive preserves executable permissions; if they were lost during copying, use `chmod +x ./katarina`. Install without administrator privileges, keeping the rest of the extracted archive for its documentation and notices: ```sh mkdir -p "$HOME/.local/bin" cp ./katarina "$HOME/.local/bin/katarina" export PATH="$HOME/.local/bin:$PATH" katarina version ``` Add the PATH export to the startup file used by your shell, such as `~/.bashrc` or `~/.zshrc`, if it is not already present. An `Exec format error` usually means the archive targets the wrong OS or CPU. A `GLIBC_... not found` error requires a compatible Linux distribution or a build on your target system; do not replace the system C library to install Katarina. ## First review after installation From a directory where you want to keep the configuration: ```sh katarina init # Set DEEPSEEK_API_KEY in your environment, or configure credentials_file. katarina doctor katarina start --tui ./your-project ``` The default configuration selects DeepSeek models. Edit `katarina.yaml` to select other providers/models, configure family budgets, or enable test execution. Use a private credentials file or environment variables for keys. See [configuration] and [the first-review guide]. Test execution is off until an execution runner is selected; configured test commands are required even for generated-only test plans. ## macOS downloads and Gatekeeper A native macOS archive must match the Mac: `darwin-arm64` for Apple silicon, `darwin-amd64` for Intel. Check with `uname -m`. Verify the archive's SHA-256 with `shasum -a 256 ARCHIVE.tar.gz` and compare it with the matching entry in `SHA256SUMS`, then extract it and try `./katarina version`. No macOS signing or notarization is claimed for this preview. For a trusted, verified native download blocked as an unidentified developer, first attempt to open it, then use **System Settings → Privacy & Security → Open Anyway** and confirm. This grants an exception for that program. Apple describes the current process in [Safely open apps on your Mac]. For a command-line executable where the normal exception is unavailable, inspect the exact extracted file: ```sh xattr -l ./katarina ``` If it has `com.apple.quarantine`, and you have verified the source and download and deliberately accept running this unsigned executable, remove only that file's quarantine attribute: ```sh xattr -d com.apple.quarantine ./katarina ./katarina version ``` Do not disable Gatekeeper globally or recursively remove quarantine from the Downloads directory. An alert that the file contains malware, will damage the computer, or is damaged calls for investigation and a fresh verified download, not a quarantine workaround. On managed Macs, follow the organization's software policy. Install the verified executable in `~/.local/bin` using the commands above.
Katarina product specification
# Katarina product specification This document describes the implemented pre-release product as of 15 September 2026. It defines scope and observable behavior; it is not a claim of release readiness or measured security effectiveness. [Behavior and definitions] provides stable behavioral requirements, and [architecture] explains components, protocols and data flow. | Contract | Current value | |---|---| | Application version default | `0.1.0-dev`; release builds can override it | | Configuration version | `1` | | Report schema version | `1.3.0` | | SQLite storage version | `1`, with additive tables | | Review policy | `5-source-coverage-and-proof-history` | | Agent runtime | Statically linked `pi_agent_rust 0.3.0` through a Rust C ABI bridge | | Application implementation | Go controller, CLI, providers, workers, persistence, navigation, runners, TUI and reports | Version values are defined in [the CLI], [configuration], [models], [store] and the [bridge package]. ## Purpose and scope Katarina reviews a local software repository, investigates security hypotheses with multiple model roles, records arguments and evidence, and optionally generates and executes tests. Its intended outcomes are better software security and less repetitive preparation and clarification during a human audit. Detection quality, comparison with other harnesses, and audit-cost savings require separate measurement. The review covers included UTF-8 text rather than a fixed extension allowlist. Solidity, Java and other backend code, Rust, and C/C++ have the following support: | Area | Implemented support | |---|---| | General source analysis | Numbered source chunks, repository outlines, bounded reads and literal search, optional analyzer output and design notes | | Solidity | Access/state/accounting review plus economic incentives, game theory, capital, payoff, MEV, oracle, liquidation, governance and griefing guidance | | Java/backend | Entry-point, tenant, authorization, data-flow, state and integration reasoning; optional language-server navigation | | Rust | Ownership, aliasing, lifetime, unsafe code, FFI and build-feature guidance; optional rust-analyzer | | C/C++ | Memory/lifetime, allocation units, arithmetic, ABI, build and concurrency guidance; optional clangd | | Test integration | Operator-configured commands for the repository's existing test framework, including Foundry, Go, JVM, Rust and native tests | Go outlines use its parser. Other built-in outlines are heuristic. Optional language servers provide symbols, definitions and references; successful startup does not establish complete project indexing. Tools such as Slither, Semgrep, graph generators or search utilities can be configured as external commands. No particular optional analyzer or graph product is mandatory or automatically installed. Katarina does not implement live API/web pentesting, exploitation of deployed targets, autonomous production patches, formal whole-program verification, a game-theoretic equilibrium solver, live market feeds, or an auditor approval system. These are outside the current product contract. ## Distribution and execution modes The release build is one executable containing the Go application, embedded SQLite, the statically linked pi runtime, website/manual assets and CloudFormation template. It requires no database server, model-agent daemon, separate pi executable or Node/Python runtime for ordinary controller operation. Provider access, OS facilities and any selected project tools remain external dependencies. | Engine | Behavior | |---|---| | `pi` | Invokes pi through FFI inside each model worker; the Go provider adapter supplies the actual HTTP completion. Requires a pi-linked build. | | `direct` | Uses the same controller workflow and Go provider adapter without invoking pi. | | `demo` | Uses deterministic, explicitly synthetic fixture responses without paid model requests; it does not perform model security analysis. | Source builds need Go 1.24+, a C toolchain and the pinned Rust toolchain. Linux and macOS are intended host platforms; Windows controller locking is unsupported, so Windows usage requires a supported environment such as WSL. Platform builds and libc compatibility are separate release concerns. Optional compilers, test frameworks, analyzers and language servers are installed and configured by the operator. See [development]. ## Public interfaces Flags precede positional arguments. Successful commands return zero; reported command errors return nonzero. A review command does not use finding severity as a CI failure threshold: a completed review with high-severity findings can return zero. | Command | Observable purpose | |---|---| | `init` | Writes an annotated YAML configuration without overwriting an existing file; supports `--out`. | | `start PATH` | Loads configuration, inventories the repository, creates a session, runs the workflow and exports reports. | | `resume SESSION` | Reuses compatible committed work and retained budgets; refuses a different source inventory, effective configuration or review policy. | | `sessions` | Lists saved sessions in the selected state directory. | | `report SESSION` | Exports committed session data without performing new model analysis. | | `index PATH` | Emits the source inventory, including exclusions and chunk metadata. | | `search QUERY` | Searches included repository text using the built-in bounded literal search. | | `doctor` | Checks configuration, linked pi support, credential presence and optional executable availability; it is not a live-provider or project-indexing certification. | | `aws template` / `aws link` | Exports the stack YAML or creates a CloudFormation quick-create review URL; AWS requires a hosted S3 template endpoint. | | `aws cleanup SESSION` / `aws reap` | Performs explicit recovery cleanup or termination requests for expired tagged instances. | | `serve` | Serves the embedded static website and manual; defaults to `127.0.0.1:8787`. This is not a review-control API. | | `version` / `help` | Reports build/pi availability or command usage. | `worker` is an internal subprocess entry point, not a supported interactive workflow. `start` defaults state to `PATH/.katarina`; saved-session commands default to `.katarina` in the current directory. The printed resume command preserves the selected state, configuration and limit overrides. `--tui` enables terminal progress when stderr is a terminal; otherwise progress is ordinary text. The TUI displays active/completed jobs, failed attempts, decisions, elapsed time and recent events. ## Configuration, credentials and limits Configuration is strict YAML: unknown fields, duplicate keys, multiple documents and invalid values are rejected. The controller loads it once. CLI `--engine`, `--max-agents` and repeatable `--token-budget FAMILY=AMOUNT` override the corresponding settings and are included in the effective session configuration. Providers are selected by configured name. Built-in transport kinds are `openrouter`, `anthropic`, `openai`, `deepseek` and `compatible`. Claude uses Messages; the others use text Chat Completions. `base_url` is an API root, with the appropriate completion path appended. HTTPS is required unless `allow_http: true`; redirects are refused. Arbitrary OAuth schemes, proprietary response shapes and every provider-specific parameter are not part of compatibility. Model credentials come from environment variables, a separate YAML credential file, or an inline provider key, in that precedence order. Credential-file keys are configured provider names; credential files require private permissions. AWS uses the AWS SDK credential chain independently. Only the provider key needed by a worker is sent over its anonymous protobuf pipe. API-key values are excluded from saved effective configuration and the configuration digest; known provider keys are redacted from recorded model/tool text. Redaction and filename exclusions are not general secret detection. New `init` files and omitted-field defaults differ deliberately for optional analysis: | Setting | New `init` configuration | When omitted from existing YAML | Bound / meaning | |---|---:|---:|---| | `scan.workers` | 16 | 16 | 1–64 concurrent model workers | | `scan.passes` | 2 | 2 | 1–8 baseline passes per included chunk | | `scan.scout_mode` | `specialized` | `specialized` | `specialized` or `focused` | | `scan.deep_percent` | 10 | 0 | 0–100 deterministic hash sample; explicit `deep_paths` also select chunks | | `analysis.shared_knowledge` | true | false | Architecture extraction before scouting | | `analysis.max_investigations` | 8 | 0 | 0–64 generated questions, additional to configured questions | | `analysis.evidence_checks` | true | false | Structured review, capability and applicability validation | | `analysis.grouping` | true | false | Conservative grouping after individual decisions | | `analysis.max_group_size` | 6 | 6 | 2–12 members per group | | `scan.context_requests` | 3 | 3 | 0–12 extra navigation rounds for ordinary tasks | | `analysis.investigation_context_requests` | 8 | 8 | 0–64 extra rounds for additional questions | | `scan.max_calls` | 1,000 | 1,000 | Persisted session-wide model dispatch cap | | `scan.max_cost_usd` | 0 | 0 | Zero disables the USD reservation cap | | `scan.token_budgets` | empty | absent | Per-family caps; an absent family cap is unlimited under other limits | | `tests.runner` | `none` | `none` | `none`, `local` or `ec2` | | `tests.max_iterations` | 2 | 2 | 1–5 plans/executions per finding or shared group | | `tests.commands` | empty | empty | No test disposition until a command is configured | Initial defaults also include 16,000-byte chunks, an 8 MiB file-size limit, 64,000-byte source/context budgets, 4,096 output tokens, 180-second model and test timeouts, two completion attempts per unfinished job per invocation, and 65,536 bytes of captured test output. Context budgets bound individual context collections; they are not a cap on total process memory or the complete prompt with instructions and all evidence blocks. The full accepted ranges and path defaults are specified by [configuration], [the generated example] and [validation code]. Family names are explicit `agents.ROLE.family` labels; without one, the exact model ID is its family. No provider-to-family inference is performed. YAML and CLI accept positive integer counts or decimal K/M/B/T suffixes, case-insensitively, including `100M`, `1B` and `1.5B`. Expansion must yield a whole token count in 1 through 2^60. Equivalent spellings normalize to the same persisted count and digest. Before each dispatch, including navigation and retries, SQLite atomically reserves a call, family tokens and the configured USD estimate. Token reservation is `system bytes + prompt bytes + 1024 + max_output_tokens`. Reservations are never refunded. USD limits require configured positive model rates; AWS and external-tool costs are separate. These limits control dispatch, not exact tokenization or provider invoices. Exhaustion stops new dependent work and leaves the session incomplete; the controller does not silently switch models or skip the failed stage. ## Source inventory and navigation Inventory traverses the local filesystem independently of Git. It records included/excluded paths, sizes, source hashes, line counts, outlines and reasons for exclusions. It does not automatically apply `.gitignore`. Built-in credential filenames, dependency/state/metadata directories, nonregular files and symlinks, non-UTF-8/binary content, configured exclusions, oversized files and files containing a line beyond the chunk limit are excluded. An excluded directory has one entry rather than entries for all descendants. Included text is partitioned into numbered chunks, with five-line overlap where possible. Every baseline pass schedules every included chunk. Primary chunk space is reserved before supplementary shared knowledge and design/tool context. That is a source-supply property, not a guarantee that the model understood every line. Cross-file context and question starting windows remain bounded. No reviewable chunks is a visible error. Agents request included-file line reads, literal searches and optional LSP symbols/definitions/references through typed YAML context requests. Each request allows at most 16 combined operations; a read spans at most 1,001 lines and a search returns at most 30 matches. Requests cannot fetch a model-supplied URL, install a tool, invoke arbitrary shell commands or read outside the included inventory. Configured tools and language servers run against disposable copies and may themselves have host or network effects. ## Analysis and decision workflow The following order describes a successful configured workflow. Optional stages are omitted only when disabled or when no eligible work exists; a stage failure is not converted into an empty successful result. 1. **Preparation:** validate configuration and budgets, acquire the state-directory lock, build the inventory, create/recover the session, capture configured analyzer output and include configured design notes. 2. **Shared knowledge, when enabled:** one architect job per chunk extracts up to eight cited component, boundary, actor, asset, invariant or dependency claims. Claims are `observed`, `inferred` or `unknown`; the controller assigns IDs and binds the combined artifact to the source digest. 3. **Question planning:** an optional planner proposes up to the generated-question cap. Up to 32 configured questions are additional. Each question has 1–32 included target files; configured globs must resolve within that limit. Generated knowledge references must exist. Invalid or unmatched targets fail visibly. 4. **Discovery:** ordinary passes, selected independent deeper scouts and additional investigators use the bounded model-worker pool. Neither a cheap-scout result nor the question plan gates ordinary coverage or the deeper sample. Deep scouts receive no shared model claims or earlier scout findings. A question with empty knowledge references receives none; configured questions start this way. 5. **Question answers:** investigators persist an answer, citations, unresolved obligations and zero or more findings. No citations is permitted only with unresolved obligations and no findings. New candidates join ordinary candidates. Each discovery response is limited to twelve findings. 6. **Fingerprinting:** the controller assigns finding IDs from path, start line, CWE and normalized title and coalesces exact fingerprints. This is not exhaustive semantic deduplication or a record of every duplicate producer's wording. 7. **Debate:** challenger and defender independently review each candidate without seeing one another's initial answer. The defender then receives the challenge and its own earlier answer and produces a rebuttal. 8. **Assessment:** the judge receives the candidate, source context and debate and chooses `log`, `ignore` or `test`, with rationale, severity and confidence. `by_design` requires explicit design evidence. Decisions are retained, including ignores. 9. **Grouping, when enabled:** a grouper considers non-ignored findings in deterministic, bounded windows. It proposes common validation conditions and an assertion for every member. The controller rejects unknown/overlapping member IDs. Every original finding and decision remains. Only groups with all members individually selected for `test` share a plan; other eligible tests remain individual. 10. **Proof work:** generate a validated individual/shared test plan, optionally execute it, independently review recorded execution and request a bounded revision when justified. 11. **Export:** save completion status and export committed evidence. A handled error/cancellation leaves incomplete status and attempts an export; a hard kill can leave status and files stale until recovery/export. Models are independently configurable per role. Architect and investigator inherit the complete scout model/family/rate entry unless overridden; planner and grouper inherit judge. Deeper scouting requires its own configured role when enabled. An optional `proof_reviewer` overrides the judge model for execution interpretation. Separate role names do not promise different underlying models or statistically independent judgments. ### Structured evidence and economic analysis With evidence checks enabled, challenge, defense, rebuttal and assessment must address reachability, control, guards, invariant, impact and feasibility. Findings with structured `economics` additionally require incentives and capital. Unknown checks require `next_evidence`; other outcomes require source citations. Invariant, impact, incentives and capital cannot be waived as inapplicable. The host checks cited paths, line ranges and exact quotation matches. A citation spans at most 41 lines and 4,096 quote bytes. It does not prove that the quote entails the claim. A supporting review cannot contain unknown or refuted checks; a refuting review needs a refuted check. A supported assessor verdict requires resolved checks, meaningful additional capability and applicable/conditional deployment. An ignore requires a refuted verdict supported by a refuted obligation or inapplicability, even when behavior is intended. Capability analysis separates existing authority from additional access, control, profit or harm, the crossed boundary/invariant and economic effects. Applicability records deployment/build/integration conditions. Permission to act does not establish that resulting economic harm is accepted. Solidity guidance asks for feasible strategies, incentives, capital, net payoffs, griefing costs and sensitivity to assumptions; economic findings need not have a CWE. These are model reasoning requirements with structural guards, not a formal economic proof. ## Test generation and execution The writer selects an operator-configured command key and creates new files matching allowed paths. It cannot supply new executable arguments, overwrite inventoried implementation/tests, traverse paths, create hidden/credential paths or exceed twelve files and 256 KiB of generated content. Plans are saved under `tests/FINDING_ID/attempt-N/` or `tests/GROUP_ID/attempt-N/`. Execution copies only included files, verifies their hashes, and applies the new files in a disposable workspace. `none` saves one plan without execution or proof review. `local` runs the command with the operator's OS privileges, a private HOME, reduced environment, timeout, bounded output and process-group cleanup. This is not an OS sandbox. `ec2` uses an operator-prepared image, private S3 transfer and SSM to execute on a disposable host as an unprivileged test user in a separate network namespace. Selecting an execution runner authorizes configured tests without a per-test confirmation prompt. Execution status and security interpretation are separate. `passed` means exit zero; `failed` may be an assertion or setup failure. `error`, `timeout`, `indeterminate` and truncated evidence cannot yield a definitive supports/refutes interpretation. A reviewer can request revision only after completed passed/failed execution, with a concrete request. Revisions cannot repeat any earlier plan's command and file contents, including A → B → A cycles. An indeterminate attempt is never automatically rerun. Shared plans must map every member to an assertion excerpt in a generated file. Shared proof reviews must interpret every member separately; a group may support one and leave another inconclusive. Overall supports/refutes requires all member interpretations to agree. Assertion presence is checked by the host; meaningful execution and semantic adequacy still require review. Production repairs and repaired-version negative controls are not automatically generated/executed by this workflow. Proof scopes execute sequentially in the current controller, even when multiple test candidates exist. The model-worker limit is a maximum, not a promise that every stage or test runs that many tasks at once. ## AWS and infrastructure The included CloudFormation template creates network resources, an encrypted private artifact bucket, instance permissions/profile and an operator role. The website also distributes the unchanged YAML. Quick-create links preload a template from its S3 HTTPS endpoint; a custom website URL alone is not a supported CloudFormation template source. They do not issue access keys in one click, supply an AMI or eliminate AWS IAM approval. The controller uses the AWS SDK; the prepared remote image supplies AWS CLI/SSM and test tools. Each remote attempt records a resource intent and idempotent EC2 client token before launch, uses ownership/expiry tags and an in-instance shutdown timer, and requests instance termination and source-object deletion on completion/error/cancellation. Ambiguous SSM submission is not automatically repeated. Cleanup/reap commands and resume cleanup handle recoverable leftovers. Cleanup errors remain visible. TTL and termination requests are safeguards, not guaranteed deletion during AWS outages or failed boot. Live AWS deployment validation remains pending. See [AWS setup and boundaries]. ## Persistence, reports and completion semantics SQLite in a private state directory is authoritative for sessions, jobs, reservations, findings, immutable analysis artifacts, test intents/results and cloud intents. It uses WAL, FULL synchronous writes, foreign keys and one database connection; an OS lock excludes concurrent controllers for that directory. No server-based database or worker-to-worker message bus is used. Accepted completed jobs are reused on compatible resume; unfinished jobs may be retried and billed again. Job records preserve the latest result/error, attempt count and accumulated usage, not every discarded retry response. Navigation completions have distinct persisted job IDs. Shared test evidence is checkpointed atomically for all members, and replaying earlier stages preserves later committed proof progress. A persisted test intent without a result remains indeterminate. Resume does not refund reservations or reset budgets. Reports are JSON, Markdown and SARIF 2.1.0, with inventory, event JSONL and conditional knowledge/question/group exports. JSON contracts use Draft 2020-12 schemas. Reports retain source/configuration identity, separate coverage counts, findings and ignores, evidence and assumptions, economic/capability analysis, groups, generated plans, test outcomes, model interpretations, usage/reservations, events and outstanding resources. SARIF preserves member findings and encodes locations as relative URIs; ignores are suppressions under review, not auditor approval. See [artifact contracts]. Each export file is written atomically; the complete set is not a single filesystem transaction. SQLite-backed report regeneration repairs stale exports after interruption. The inventory/configuration files provide the saved inputs needed by report export; SQLite alone is not a full copy of the source repository. Retain the exact source revision and session directory for audit handoff. Session `completed` means the scheduled workflow returned successfully, not that all security questions were resolved or all tests passed. It may include logged concerns, ignored findings, inconclusive proof reviews, unsuccessful test commands or an iteration limit. `incomplete` means orchestration stopped with an error or handled cancellation. A hard-killed process may leave `running` status until recovered; that status alone is not proof a controller is alive. ## Release boundaries and maintenance The static site uses monospace/ASCII-style presentation and a red high heel drawn with Unicode Braille characters. The embedded manual preserves text and diagram source with clickable links; Mermaid-capable Markdown viewers can render the architecture diagrams. No diagram-rendering service is required at runtime. Native preview downloads, the source snapshot and unsigned SHA-256 checksums are generated under the Git-ignored `web/downloads/` directory. Archives include documentation, schemas, source/build identity and dependency notices. The current prepared binary targets Linux x86_64; native macOS binary/signing validation is separate release work. Download archives are hosted externally and are not embedded inside the binary. Automated checks cover orchestration, budgets, exact amount parsing, evidence shapes/provenance, source coverage, recovery, protobuf/FFI boundaries, provider response handling, local runners, SARIF locations and mocked AWS lifecycles. They do not establish parity with Claude Code, MDASH or Shannon, live-provider reliability, live AWS correctness, complete language-server indexing, detection recall or audit savings. Those remain evaluation/release work, with a procedure in [development] and [research design]. Changes to observable workflow must update this specification, the relevant behavior IDs, architecture, configuration/examples and report contracts together. Changes to review semantics must also review the policy digest boundary; changing documentation alone does not change the policy. Behavior IDs are stable references for issues, tests and release notes.
Katarina behavior and definitions
# Katarina behavior and definitions This is the behavioral contract for the current product described in [the specification]. It defines terms, desired behaviors (`b01`, `b02`, …), and undesirable behaviors (`ub01`, `ub02`, …). Use these IDs in issues, tests, evaluation cases and release notes. IDs are stable: append new entries and retire obsolete ones explicitly rather than renumbering or reusing them. Each `ubNN` below is the failure counterpart of `bNN`. ## Interpretation and enforcement Desired behavior applies when the relevant feature is enabled and its documented prerequisites are met. An optional feature being disabled is not itself a defect. An undesirable behavior is something the implementation, model reasoning or product claims should avoid; listing it does not assert that every instance is mechanically detectable. | Label | Meaning | |---|---| | **Host** | Enforced by controller logic, data validation, operating-system/process boundaries or persistence rules. Tests can check the stated observable property. | | **Model** | Required by role instructions and assessed by review/evaluation. The controller may enforce structure and consistency without establishing semantic truth. | | **Operator** | Requires supplied scope, credentials, commands, dependencies, deployment assumptions, human judgment or infrastructure operation. | Several behaviors combine these labels. For example, exact quotation matching is Host-enforced; whether that quote proves an authorization bypass is a Model/Operator judgment. A valid schema, passing command, high confidence value or majority of agreeing agents is not independent vulnerability confirmation. ## Definitions | Term | Definition | |---|---| | Operator | The person or automation choosing the repository, configuration, providers, budget and permitted execution environment. | | Controller | The Go process that owns scheduling, scope, validation, budget reservations, authoritative state, runners and exports. | | Worker | A short-lived child invocation of the same executable, serving one protobuf request and one completion response. It does not own a database or peer message bus. | | Role | A review responsibility and model configuration, such as scout, challenger or judge. Two roles may use the same model. | | Task | A logical unit of work, potentially involving an initial completion and additional navigation completions. | | Job | A persisted completion slot identified within a session. Retries reuse the job ID; navigation rounds have their own job IDs. | | Attempt | Either a completion dispatch for an unfinished job or a numbered proof plan/execution. The two counters are separate. | | Session | A review bound to its root, inventory digest, effective configuration and review-policy digest, with durable results and reservations. | | Inventory | Included/excluded file metadata and included-source chunks. It records scope; it is not a call graph or a security verdict. | | Source snapshot | The source bytes represented by the inventory hashes. Source is held in memory for review and verified when copied for tools/tests; the saved inventory is not a complete source archive. | | Chunk | A bounded numbered source range used as a discovery seed. Adjacent chunks overlap where possible. | | Coverage | Counts of completed baseline, deeper, knowledge and planned-question jobs against their corresponding expected work. It measures workflow/source exposure, not defect recall. | | Independent review | Separate initial answers without access to the peer's answer. It does not imply different models or statistically independent errors. | | Shared knowledge | Session-scoped, source-cited model claims about components, actors, assets, boundaries, invariants and dependencies. Claims remain challengeable. | | Investigation | An additional configured or generated question with included starting files, selected shared claims, and a saved answer/unresolved obligations. | | Candidate / finding | A proposed defect with a location, claim, evidence, impact and other details. The term alone does not mean a confirmed vulnerability. | | Finding ID / fingerprint | A controller-derived identity based on location, CWE and normalized title. Exact fingerprint deduplication can coalesce discoveries; it is not complete root-cause classification. | | Assessed finding | A candidate with challenge, defense, rebuttal, disposition and optional structured assessment, group and proof history. | | Disposition | The judge's next action: retain the concern, retain a dismissal rationale, or request a test. It is distinct from a proof result. | | Citation | An included-file location and an exact source quotation. | | Provenance | Evidence that a quotation occurs in the claimed reviewed source range. Provenance does not establish semantic entailment or deployment truth. | | Evidence obligation / check | A question that must be addressed to support or defeat a claim, such as reachability, effective guards or economic feasibility. | | Invariant | A required safety, accounting, ownership, access or economic property. Comments and supplied design notes can describe it but are not automatically authoritative. | | Actor | A participant whose inputs, permissions, resources, incentives or timing matter to a claim. Economic actors need not act maliciously. | | Additional capability | Access, control, profit or imposed harm enabled by a mechanism beyond the actor's relevant existing authority. It includes economic effects, not only privilege escalation. | | Applicability | Whether a claim's build, deployment, integration and operating conditions hold, are conditional, are disproven or remain unknown. | | Economic risk | A harmful strategy, incentive failure, cost asymmetry or system response under stated capital, payoff, timing and operating assumptions, even if code follows its intended rules. | | By design | A model claim that behavior is intended, requiring explicit design evidence. It is not a synonym for safe, harmless or accepted by an auditor. | | Finding group | A proposal to validate multiple retained findings through common conditions and member-specific assertions. Group membership does not merge their verdicts. | | Test plan | A configured command key plus new generated files and an expected observation; a shared plan also identifies each member's assertion. | | Execution result | Recorded runner status, exit code, output, truncation, duration and runner type. | | Proof interpretation | A model's assessment of what a generated test and recorded execution establish about the claim. | | Proof of a defect | A scenario/assertion that succeeds in observing the defect and stops doing so after repair. It must exercise the real implementation and relevant trigger. | | Safety regression assertion | An assertion of the desired property: it should fail on the vulnerable implementation and pass after repair. | | Negative control | A repaired or deliberately non-triggering comparison demonstrating that the observed result depends on the claimed mechanism. Katarina does not automatically repair production code to create one. | | Model family | An explicit budget grouping shared across selected roles/models/providers; absent an explicit label, the exact model ID is used. | | Token budget | A cap on conservative input-plus-output reservations for a family in one session. `100M` means 100,000,000 reserved tokens. | | Reservation | Persisted dispatch allowance consumed before a request. It is not refunded after errors, unused output allowance or lost responses. | | Observed usage | Input/output token counts reported by a provider, or marked estimates when counts are unavailable. It is separate from reservations and invoices. | | Durable intent | A committed record made before a potentially externally effective operation such as test execution or instance launch. | | Indeterminate execution | An execution was recorded as started but has no committed outcome. It may have happened; automatically repeating it is unsafe. | | Complete workflow | Scheduled orchestration returned successfully. Findings, test failures, unresolved assumptions or inconclusive proofs can remain. | | Audit-ready evidence | Traceable source identity, scope, claims, arguments, assumptions and test artifacts suitable for human review. The label does not imply auditor acceptance or certification. | ## Status vocabularies These values belong to different objects and must not be substituted for one another. | Object | Values | Interpretation boundary | |---|---|---| | Session | `running`, `incomplete`, `completed` | A hard kill can leave `running`; completed is orchestration completion, not security approval. | | Job | `pending`, `running`, `failed`, `done` | Done means an accepted response is committed; it does not validate the model's conclusion as fact. | | Knowledge claim | `observed`, `inferred`, `unknown` | All are model-authored claims with source citations. | | Review position | `supports`, `refutes`, `uncertain` | The peer's position on the candidate. | | Evidence check | `established`, `refuted`, `unknown`, `not_applicable` | Established supports an obligation; refuted defeats it; unknown names next evidence. Inapplicability needs justification and is prohibited for core invariant/impact and economic incentive/capital checks. | | Evidence assessment | `supported`, `refuted`, `unresolved` | The assessor's structured evidence verdict, subject to consistency rules. | | Capability | `meaningful`, `equivalent`, `unknown` | Whether the mechanism adds relevant capability or harm; equivalence alone is insufficient to dismiss economic harm. | | Applicability | `applicable`, `conditional`, `not_applicable`, `unknown` | Whether the required operating conditions hold. | | Disposition | `log`, `ignore`, `test` | Log keeps a concern; ignore keeps a dismissal rationale; test requests a permitted plan. | | Severity | `critical`, `high`, `medium`, `low`, `info` | Model-assessed impact, distinct from evidence strength and probability. | | Execution | `passed`, `failed`, `error`, `timeout`, `indeterminate` | Command/runtime outcomes, not security verdicts. | | Proof interpretation | `supports`, `refutes`, `inconclusive`, `revise` | Revise requests another permitted, changed plan; it is not an instruction to repeat an unknown execution. | | Shared member interpretation | `supports`, `refutes`, `inconclusive` | One interpretation for each group member; revision is requested at the shared-plan level. | Confidence is a number from 0 to 1 supplied by a model. It is uncalibrated and is not an independently measured probability. ## Desired behavior | ID | Required behavior | Enforcement and observable acceptance | |---|---|---| | `b01` | Record the review scope explicitly, including exclusions and why content was omitted. Do not depend on a Git checkout or silently apply `.gitignore`. | **Host.** Inventory accounts for included files and exclusion entries; excluded directories may have one entry. | | `b02` | Supply every scheduled primary source chunk in full before allocating supplementary model/design/tool context. | **Host.** Complete numbered chunk text remains in the initial seed context even at supported tight context settings; coverage counts remain separate from understanding. | | `b03` | Run every baseline pass and the independently selected deeper sample regardless of whether cheap scouts return findings. | **Host.** A stronger scout can recover a case missed by ordinary scouts; the plan cannot reduce baseline expected jobs. | | `b04` | Honor context independence: deeper scouts receive no shared model claims or earlier scout conclusions; empty question knowledge references mean none. | **Host.** Prompt inspection verifies absence of unselected claims, including configured questions. Shared source/design notes are still permitted. | | `b05` | Preserve shared claims with source provenance and observed/inferred/unknown status; keep them challengeable. | **Host + Model.** Paths/ranges/quotes validate and host-assigned IDs persist; investigators must seek counterevidence rather than treat summaries as proof. | | `b06` | Run explicit/generated questions in addition to normal work, validate their included targets, and retain answers even when no finding results. | **Host.** Unmatched targets fail visibly; unresolved or unfinished questions are represented in saved answers/reports. | | `b07` | Bound navigation to included source and configured LSP operations, with explicit round/output limits and budget charges. | **Host.** Unavailable paths are not read; context exhaustion stops the task visibly; each completion consumes a reservation. | | `b08` | Obtain blind initial challenge and defense, then a rebuttal and an assessor decision using their arguments. | **Host + Model.** Initial peers cannot see one another's responses; reasoning should address the strongest alternative explanation. | | `b09` | When evidence checks are enabled, require complete obligations, cited resolved outcomes and specific next evidence for unknowns. | **Host + Model.** Unknown/refuted checks cannot produce support; refutation and ignores need the appropriate cited basis. Citation truth is assessed separately. | | `b10` | Include Solidity incentives, rational deviations, capital, net payoffs, cost asymmetry and operating assumptions. Preserve structured economic evidence when supplied. | **Model + Host.** Domain guidance reaches review stages; economic objects require their fields and additional incentive/capital checks. Economic adequacy requires evaluation. | | `b11` | Separate existing authority, additional capability/harm and deployment applicability from severity, confidence and disposition. | **Host + Model.** Structured assessment contains these fields; unknown conditions remain explicit and intended behavior alone does not justify dismissal. | | `b12` | Retain every distinct assessed finding and its disposition, including ignored findings and members of groups. | **Host.** Grouping does not delete findings or overwrite their individual severity/decision; exact fingerprint coalescing remains a separate discovery step. | | `b13` | Group only when a common scenario and assertions can address all members; reject unknown or overlapping membership. | **Host + Model.** IDs/size/citations validate; common mechanism and conditions require review. Uncertain or out-of-window matches remain separate. | | `b14` | Shared plans and proof reviews account for every member separately. Share execution only when every member was individually selected for testing. | **Host + Model.** Each plan maps an assertion excerpt to a generated file; each review has a member result. Overall support/refutation requires agreement. | | `b15` | Keep the reviewed implementation unchanged. Generate only permitted new test files and select only configured command keys. | **Host + Operator.** Reject traversal, forbidden/existing paths and new argv; run overlays in hash-checked disposable copies. Operators choose trusted commands. | | `b16` | Execute tests or create test instances only through an explicitly selected execution runner and configured commands. | **Host + Operator.** `runner: none` writes one plan and performs no test execution/review; `local`/`ec2` permits configured execution without a separate per-test prompt. | | `b17` | Distinguish command outcome from security evidence; inspect discovery, actual implementation reachability, assertion meaning and negative controls. | **Host + Model + Operator.** Incomplete/truncated execution cannot support/refute; semantic adequacy and repaired controls require independent review. | | `b18` | Bound revisions and reject a command/file-content plan already present in the same proof history. | **Host.** Description changes, file reordering and A → B → A cycles cannot authorize another identical execution. | | `b19` | Commit execution intent before launch and preserve unknown outcomes without automatic repetition. | **Host.** After interruption, a missing result becomes indeterminate and does not cause another dispatch for that attempt. | | `b20` | Reserve call, family-token and optional USD allowance atomically before each dispatch, including retries and navigation. Retain reservations across resume. | **Host.** Concurrent workers cannot race beyond the configured reservation caps; exhausted sessions stop rather than reset or silently skip work. | | `b21` | Parse token shorthand exactly, normalize equivalent amounts and keep family selection explicit. | **Host.** `100M`, `0.1B` and `100000000` have the same cap/digest; reject zero, overflow and fractional-token amounts. | | `b22` | Default to at most 16 simultaneous model workers, honor `--max-agents`/`scan.workers` within 1–64, and state what the limit covers. | **Host.** Worker peaks respect the cap; dependent/sequential stages may use fewer workers, and external compiler/LSP threads are separate. | | `b23` | Use the selected provider/model and documented optional-role inheritance, validate responses, and fail visibly on transport/refusal/truncation/schema errors. | **Host.** No automatic provider/model substitution occurs; completed responses use the configured API shape and role budget. | | `b24` | Keep keys out of argv and effective configuration, limit worker credentials to the selected provider, and redact known keys from recorded model/tool text. | **Host + Operator.** Credential precedence and private files work; reduced child environments do not inherit model/AWS secrets. Scope and embedded secret review remain operator duties. | | `b25` | Use the versioned protobuf child-pipe contract, bounded frames and matching job identity; keep workflow authority in the controller. | **Host.** Oversized/mismatched frames fail; model output does not select worker programs, database servers or a peer communication protocol. | | `b26` | Make committed SQLite state authoritative, retain accepted work and use atomic writes for exported files and shared member proof checkpoints. | **Host.** Reopening/replay preserves committed evidence; a stopped earlier stage cannot erase a later committed proof. Export files can be regenerated from saved session inputs/state. | | `b27` | Resume only with matching inventory, effective configuration and review policy; reuse completed jobs and allow key rotation. | **Host + Operator.** Source/model/budget/policy changes are rejected; equivalent budget notation and credential changes preserve compatible session identity. | | `b28` | Report completion, omissions, failures, uncertainty, reservations and outstanding resources honestly, and attempt export on handled interruption. | **Host + Operator.** Incomplete orchestration is not labeled a successful scan; a completed workflow may still have unresolved findings or failed tests. Hard-kill staleness is documented. | | `b29` | Record cloud intent before launch, use client tokens/expiry tags, request termination and object cleanup, and expose recovery failures. | **Host + Operator.** Mock lifecycle/recovery tests pass; operators verify AWS permissions/AMI, monitor leftovers and validate live behavior. TTL is not a deletion guarantee. | | `b30` | Describe execution boundaries accurately and keep optional tools optional. | **Host + Operator.** Ordinary review needs no separate agent/database service; local execution is labeled as using host privileges, and external toolchains/AMI dependencies are explicit. | | `b31` | Maintain accurate standalone documentation, runnable state-path examples, versioned artifact contracts and optional terminal progress. | **Host + Operator.** Generated manual matches source, links/defaults agree with code, schemas accept representative complete/partial outputs, and non-TUI usage works. | | `b32` | Make claims about readiness, effectiveness and audit savings only with appropriate evidence; label demonstration output clearly. | **Host + Model + Operator.** Demo is identified as synthetic; orchestration tests are not advertised as discovery recall, auditor approval or live AWS validation. | ## Undesirable behavior | ID | Failure to avoid | Concrete example / consequence | |---|---|---| | `ub01` | Hide excluded content or present the filesystem review as exhaustive without scope accounting. | A skipped dependency or oversized Solidity file disappears from the audit handoff. | | `ub02` | Let shared summaries/tool output displace primary lines while reporting the chunk as reviewed. | Tight context settings omit a line between overlap windows. | | `ub03` | Gate ordinary/deeper discovery on a cheap model flag or a planner's chosen files. | A cheap-scout false negative prevents every later agent from examining the mechanism. | | `ub04` | Interpret empty knowledge references as all knowledge, or leak earlier conclusions into independent deeper scouting. | An intended fresh look inherits the same mistaken trust assumption. | | `ub05` | Treat generated architecture claims, comments or matching quotes as authoritative safety facts. | A cited comment stating “trusted caller” substitutes for checking actual callers. | | `ub06` | Replace baseline work with targeted questions, silently drop invalid questions or require a finding from every question. | An unmatched configured path appears as a completed investigation with no concerns. | | `ub07` | Follow source-embedded instructions to fetch URLs, expose excluded files, install tools or execute arbitrary commands. | A repository comment attempts to redirect an investigator outside the reviewed inventory. Host tool restrictions limit effects; prompt compliance still requires evaluation. | | `ub08` | Expose one initial peer answer to the other or treat agreement as a vote that establishes truth. | The defender parrots the challenger instead of independently checking counterevidence. | | `ub09` | Convert unknown evidence into refutation/support, omit required obligations or accept invented source quotations. | Missing deployment evidence becomes a definitive “not exploitable” dismissal. | | `ub10` | Dismiss economic or incentive risk because code follows its specification or participation is permissionless. | Unprofitable liquidation remains “by design” while bad debt accumulates. A semantic miss may pass structural validation and must be caught by evaluation. | | `ub11` | Equate permission to act with accepted permission to impose losses, or invent operating assumptions. | An authorized withdrawal or governance vote is assumed harmless without examining induced losses or capital/timing. | | `ub12` | Delete ignored/grouped findings or overwrite all members with one disposition. | Auditors cannot inspect the original location or challenge the dismissal rationale. | | `ub13` | Group findings solely by similar names/files, conflicting prerequisites or unrecognized IDs. | Distinct bugs receive one insufficient shared scenario. Semantic grouping errors require review in addition to ID validation. | | `ub14` | Treat one passing assertion as proof for every group member, omit members or silently weaken their claims during revision. | One discovered test passes while another member's test is skipped but both receive support. | | `ub15` | Overwrite production/existing tests, accept model-supplied argv or mutate the original repository through the overlay mechanism. | A generated plan changes the guard rather than testing the reviewed implementation. | | `ub16` | Run generated code or launch an instance with `runner: none`, or imply that selecting an execution runner still waits for per-test approval. | A normal analysis unexpectedly incurs cloud execution, or an operator misunderstands configured automatic execution. | | `ub17` | Call exit zero, a compilation error, missing dependencies or zero discovered tests a reproduced or refuted vulnerability. | Setup failure is mistaken for evidence that the proposed defect is impossible. | | `ub18` | Repeat unchanged proof content through description edits, file reordering or nonconsecutive revision cycles. | A → B → A spends again without a new scenario under the same source/configuration. | | `ub19` | Automatically retry a started attempt whose outcome was lost or an ambiguous SSM submission. | An external action happens twice after a controller crash. | | `ub20` | Dispatch before reserving, reset/refund uncertainty on resume, or bypass a cap by silently switching families/models. | Several agents independently consume the same remaining allowance. | | `ub21` | Use binary suffix multipliers, floating-point rounding or guessed family membership. | `1B` changes across input paths or a fractional token rounds into an accepted cap. | | `ub22` | Exceed the configured worker cap or claim it constrains all child-tool threads and test parallelism. | The TUI worker count is mistaken for a total CPU/process limit. | | `ub23` | Accept incomplete/refused provider text as a clean result, follow redirects with credentials, or silently reroute a request. | An endpoint error becomes an empty findings list or consumes a different family's allowance. | | `ub24` | Put keys in arguments/reports, give a worker unrelated provider/AWS credentials, or promise universal secret filtering. | Embedded credentials in arbitrary source are assumed protected by a filename blacklist. | | `ub25` | Replace typed child messages with an unvalidated peer bus, ambient worker database or model-controlled process launcher. | A worker accepts an unrelated response or interprets source content as a transport command. | | `ub26` | Treat stale JSON exports as authoritative state, lose later proof progress during replay, or claim all retry responses are archived. | A resumed early assessment erases previously committed shared test results. | | `ub27` | Reuse results after source/configuration/policy changes, or force a new session solely because an equivalent cap spelling or API key changed. | Earlier truncated-context jobs are presented as having used the corrected coverage policy. | | `ub28` | Conflate an empty report, a completed workflow, successful tests and secure software, or hide export/cleanup failures. | A budget-exhausted run is presented as “no vulnerabilities found.” | | `ub29` | Promise guaranteed EC2 deletion, retry ambiguous execution or describe the stack link as issuing credentials and a ready test AMI. | A failed shutdown or incomplete AWS setup becomes an unreported operational assumption. | | `ub30` | Describe local execution as an OS sandbox, make optional analyzers mandatory without disclosure, or conflate one binary with bundled project toolchains. | An operator runs untrusted build code expecting host isolation that is not implemented. | | `ub31` | Ship stale defaults, mismatched schema/manual content, incorrect state-directory commands or a mandatory TUI. | Instructions list sessions from the wrong directory after `start ./project`. | | `ub32` | Present synthetic fixtures or mock lifecycle tests as real vulnerability discovery, live deployment validation or measured audit savings. | Unmeasured parity with another harness appears as a release claim. | ## Evidence and test traceability These are the current implementation/test entry points for the behavior groups. They are not a claim that every model or operating environment has been validated. A release issue should cite the behavior ID, triggering configuration/source fixture, expected result and observed result. | Behaviors | Implementation and validation entry points | |---|---| | `b01`–`b07` | [Source inventory/tests], [primary-context regression], [additional analysis integration], [navigation], [LSP tests] | | `b08`–`b14` | [Pipeline tests], [structured analysis/group tests], [economic models], [domain profiles] | | `b15`–`b19` | [Plan/local runner tests], [native controls], [proof/recovery/cycle tests], [shared proof integration] | | `b20`–`b23` | [Concurrent budgets], [exact token parsing], [CLI limits], [independent scouting/concurrency], [provider tests] | | `b24`–`b27` | [Credentials/config tests], [wire tests], [FFI tests], [store recovery], [shared recovery] | | `b28`–`b31` | [Report schemas], [SARIF path tests], [cloud lifecycle mocks], [runner], [CLI], [manual generator] | | `b32` | [Development validation boundaries], [comparative evaluation protocol], human adjudication on held-out vulnerable/repaired/benign cases | For Host behaviors, a reproducible violation is an implementation defect. For Model behaviors, retain the source, prompts/model configuration, candidate, evidence and counterexample and evaluate the miss under a fixed benchmark. For Operator behaviors, record the missing prerequisite or failed infrastructure assumption explicitly; do not convert it into a clean security conclusion.
Configuration
# Configuration
`katarina init` writes the complete annotated example. YAML uses strict known-field decoding: misspelled fields, duplicate keys and multiple documents are errors. Omitted fields receive defaults; explicitly invalid values fail validation. Configuration is loaded once by the controller, not independently by agents.
The examples below are configuration fragments. Merge them into the file generated by `katarina init`, retaining the required agent roles and any other settings needed for the review.
## Providers and credentials
```yaml
version: 1
engine: pi
credentials_file: /home/you/.config/katarina/credentials.yaml
providers:
router:
kind: openrouter
api_key_env: OPENROUTER_API_KEY
claude:
kind: anthropic
api_key_env: ANTHROPIC_API_KEY
openai:
kind: openai
deepseek:
kind: deepseek
local:
kind: compatible
base_url: http://127.0.0.1:1234/v1
allow_http: true
api_key_env: LOCAL_MODEL_KEY
token_parameter: max_tokens
```
Credential file (mode `0600`):
```yaml
router: your-openrouter-key
claude: your-anthropic-key
openai: your-openai-key
deepseek: your-deepseek-key
```
The map uses configured provider names, not necessarily provider kinds. Environment variables override the file, which overrides an inline provider `api_key`. Prefer the file or environment. `credentials_file` paths resolve relative to the configuration file. Native providers need a key; a custom compatible endpoint may accept anonymous requests.
| Kind | Default API root | Default environment variable | Wire API |
|---|---|---|---|
| `openai` | `https://api.openai.com/v1` | `OPENAI_API_KEY` | Chat Completions |
| `anthropic` | `https://api.anthropic.com/v1` | `ANTHROPIC_API_KEY` | Messages |
| `openrouter` | `https://openrouter.ai/api/v1` | `OPENROUTER_API_KEY` | Chat Completions |
| `deepseek` | `https://api.deepseek.com` | `DEEPSEEK_API_KEY` | Chat Completions |
| `compatible` | Required | Operator chosen | Chat Completions |
`base_url` is an API root; Katarina appends `/chat/completions` or `/messages`. HTTPS is required unless `allow_http: true` is explicit. Redirects are refused. Compatibility means the documented text Chat Completions request and response shape; provider-specific OAuth, nonstandard response shapes and arbitrary proprietary parameters are not implemented. Model refusals, truncated responses, malformed structured output and empty replies are failures, not clean security results.
OpenAI uses `max_completion_tokens`; other Chat Completions providers default to `max_tokens`. `token_parameter` can explicitly select either. No sampling temperature is forced, allowing reasoning models that reject it. Anthropic uses its top-level system prompt, `max_tokens`, `x-api-key` and version header. Upstream requests/responses use their required JSON API; worker communication uses protobuf.
## Model routing
Each role has an independent provider and model. Use exact model IDs available to your account:
```yaml
agents:
scout: {provider: deepseek, model: deepseek-v4-flash}
challenger: {provider: deepseek, model: deepseek-v4-flash}
defender: {provider: deepseek, model: deepseek-v4-flash}
judge: {provider: deepseek, model: deepseek-v4-pro}
test_writer: {provider: deepseek, model: deepseek-v4-pro}
```
Select models available to the configured provider accounts and evaluate them on representative repositories. Independent prompts and separate requests reduce simple agreement effects, but agents using the same model may share biases. Compare model and provider combinations when evaluating false positives.
## Scan limits
`katarina start --max-agents 16` sets the maximum simultaneous model requests. It overrides `scan.workers` (default 16, valid range 1–64). Scouting and the independent challenge/defense stages run concurrently; dependency-bound stages wait for their inputs. The limit covers model workers, not compiler threads or external language-server processes.
| Field | Default | Meaning |
|---|---:|---|
| `workers` | 16 | Concurrent model jobs, 1–64 |
| `passes` | 2 | Independent security lenses per chunk, 1–8 |
| `scout_mode` | specialized | `focused` uses an open-ended, file-seeded investigation prompt |
| `deep_percent` | 0; init example 10 | Stable hash sample, 0–100, for independent `deep_scout` jobs |
| `deep_paths` | [] | Included-file globs that always get an independent deeper scout |
| `token_budgets` | {} | Per-family input+output token reservation caps; integers or amounts such as `100M` and `1B` |
| `context_requests` | 3 | Extra read/search/LSP rounds, 0–12; question investigations use `analysis.investigation_context_requests` instead |
| `chunk_bytes` | 16000 | Approximate numbered primary-chunk size, minimum 1024 |
| `max_file_bytes` | 8388608 | Maximum included text file, up to 128 MiB |
| `max_context_bytes` | 64000 | Initial source and additional context limits, up to 2 MiB |
| `max_output_tokens` | 4096 | Per-completion output cap, 256–65536 |
| `max_calls` | 1000 | Hard persisted reservation cap; includes attempts and context requests |
| `max_cost_usd` | 0 | Disabled at zero; otherwise requires positive rates for every role |
| `timeout_seconds` | 180 | Per-model request timeout, 1–3600 |
| `max_attempts` | 2 | Attempts per incomplete job in one invocation, 1–5 |
| `exclude` | See example | `**` globs relative to repository root |
To enable cost reservations:
```yaml
agents:
scout:
provider: deepseek
model: deepseek-v4-flash
input_per_million: 0.14
output_per_million: 0.28
# Set current rates on ALL active roles, including deep_scout and proof_reviewer when enabled.
scan:
max_cost_usd: 20
max_calls: 400
```
The rates above are illustrative; replace them with the provider's current rates. Before execution, a job reserves an amount based on input bytes plus overhead, the output token limit and the configured per-million rates. Reservations are conservative, never refunded, and survive a crash. They bound dispatch under the configured rates. Actual charges can differ because providers may account for caching, reasoning or other features separately. AWS and optional external tools are not covered by the model budget.
Evaluate a small repository before increasing passes or context limits. Model selection and provider routing remain fixed for the session.
## Per-model-family token budgets
Give agent configurations a `family` label to share a session-wide cap across roles, models and providers. The label is explicit: an OpenRouter model and the same model's direct API can both use `family: claude`. If omitted, the exact model ID becomes its own family; the provider name is never used to guess a model family.
```yaml
agents:
scout: {provider: deepseek, model: deepseek-v4-flash, family: deepseek}
deep_scout: {provider: deepseek, model: deepseek-v4-pro, family: deepseek}
# Keep challenger, defender, judge and test_writer entries from katarina init.
scan:
workers: 16
token_budgets:
deepseek: 100M
```
Equivalent CLI overrides, using families assigned to active roles:
```sh
katarina start --max-agents 16 --token-budget deepseek=100M ./project
# If a configured active agent uses family: claude:
katarina start --max-agents 16 --token-budget deepseek=100M --token-budget claude=10M ./project
```
YAML and CLI budgets accept decimal suffixes, case-insensitively: `K` = 1,000, `M` = 1,000,000, `B` = 1,000,000,000 and `T` = 1,000,000,000,000. For example, `100M`, `1B`, `1.5B` and `250k` are valid; YAML quotes are optional. Unsuffixed integer counts still work. Fractional suffix amounts must expand to a whole token: `0.001K` is one token, but `0.0001K` is rejected. Zero, negative amounts, unsupported suffixes and expanded counts above 2^60 are rejected. These suffixes apply to family budgets, not to fields such as `max_output_tokens`.
Amounts are normalized to integer counts before validation and persistence. Reports and printed resume commands use these integer counts, so switching between equivalent spellings such as `100M` and `100000000` preserves the configuration digest and budget.
Each cap includes input **and** output across scouting, debate, assessment, proof reviews, revisions, context requests and retries. Before dispatch, SQLite atomically reserves `system/prompt UTF-8 bytes + 1024 + max_output_tokens`. This deliberately pessimistic estimate prevents workers racing past the configured reservation cap. Reservations are never refunded, including after a crash or an upstream error whose billing is unknown. Exhaustion stops the session as incomplete; it does not silently skip a stage or switch families.
These are dispatch limits, not provider-enforced invoice limits. Exact tokenization, hidden reasoning and provider accounting may differ. The report shows reserved tokens separately from observed input/output usage, marking estimated usage when a provider omits counts. Caps are per session; they do not cover other Katarina state directories or applications using the same API account. A missing cap means unlimited for that family, still subject to the global call/cost limits. Provided caps must expand to positive whole token counts and name an active family.
CLI limits are saved in the effective configuration. The printed resume command includes them; changing them requires a new session under the existing resume policy. This prevents restarting from resetting an exhausted budget.
## Test commands, tools and language servers
See [testing] and [navigation]. These execute operator-configured programs; model output can select a configured test command key but cannot supply arbitrary argv. Design notes are repository-relative included files. AWS settings are described in [AWS].
Solidity economic/game-theory guidance is active for `.sol` scouting and subsequent triage, even with one pass. Rust and C/C++ files receive their own review guidance within the same model requests. Supply protocol assumptions through `design_notes`; see [economics]. Optional rust-analyzer and clangd examples are included in `katarina init`.
## Shared knowledge, questions and evidence
The `analysis` block controls shared security knowledge, generated and configured questions, evidence checks with additional-capability/deployment analysis, and finding groups for shared tests. Fresh `katarina init` files enable these stages; existing files that omit the block retain their earlier behavior. See [the full configuration and workflow], including role inheritance and added model costs.
The optional `architect` and `investigator` roles inherit the complete `scout` agent configuration; `planner` and `grouper` inherit `judge`. Explicit role entries override that inheritance. Their calls use the inherited or configured family caps and rates. Configured questions are additional to `analysis.max_investigations`, and neither kind replaces regular or deeper scouting.
## Environment exposure
Worker subprocesses inherit a small allowlist: PATH, JAVA_HOME, GOROOT, locale and platform paths, plus a private HOME. Only that worker's provider key travels over its private protobuf pipe. Local test/tool processes receive no model/AWS keys from the controller. This is environment hygiene, not host isolation: same-user local processes may access other user files. Use disposable EC2 for untrusted execution.
Katarina architecture
# Katarina architecture
Katarina is a Go controller with short-lived model workers, an embedded SQLite store and a statically linked Rust agent runtime. The controller owns the review workflow and all consequential decisions about scope, dispatch, validation, execution and persistence. Workers supply model completions; they do not coordinate directly or own session state.
This document explains the current implementation. The [product specification] defines supported behavior and limits; [behavior and definitions] supplies stable requirements and terminology. The diagrams describe software boundaries and data dependencies, not a network of permanently running agents. The ASCII diagrams also remain readable in the embedded plain-text manual.
## Component map
```text
OPERATOR INPUTS REVIEW INPUTS
CLI + YAML + credentials repository + design notes
| |
v v
+--------------------------------------------------------------------+
| GO CONTROLLER |
| configuration -> source inventory -> stage scheduling |
| | | |
| optional tool/LSP <------+ prompt/context assembly |
| adapters on source copies | |
| budget reservation |
| | |
| result validation <---------------------+--------------------+ |
| | | | |
| v v | |
| assessed findings model dispatch | |
| | | |
| +-> test plans -> none / local / EC2 -> proof review ----+ |
| | |
| +-> JSON / Markdown / SARIF / event and analysis exports |
| |
| SQLite store <---- jobs, budgets, evidence, execution/cloud intents |
| events ------> optional TUI / text progress |
+-----------------------------------------+--------------------------+
| private framed protobuf
v
+-----------------------------------+
| SAME-BINARY WORKERS (bounded pool) |
| one completion per child process |
| |
| pi: Rust agent via C ABI |
| -> Go provider callback |
| direct: Go provider adapter |
+-----------------+-----------------+
| HTTPS / provider JSON
v
MODEL API ENDPOINTS
Local runner -> disposable directory, operator OS privileges
EC2 runner -> AWS SDK -> S3 + EC2 + SSM -> disposable test host
Static site -> embedded assets; independent of session execution
```
```mermaid
flowchart TB
Operator[CLI, YAML and credentials] --> Controller[Go controller]
Repo[Repository and design notes] --> Inventory[Source inventory]
Inventory --> Controller
Inventory --> Tools[Optional tools and LSP on copies]
Tools --> Controller
Controller <-->|jobs, budgets, evidence and intents| DB[(Embedded SQLite)]
Controller <-->|framed protobuf over private pipes| Worker[Same-binary model workers]
Worker --> Pi[Rust pi runtime through C ABI]
Pi -->|provider callback| Provider[Go provider adapter]
Worker -->|direct engine| Provider
Provider <-->|HTTPS and provider JSON| API[Configured model APIs]
Controller --> Runner[Test plan and runner]
Runner --> Local[Local disposable workspace]
Runner --> AWS[AWS SDK: S3, EC2 and SSM]
Local --> Result[Recorded execution evidence]
AWS --> Result
Result --> Controller
Controller --> Reports[JSON, Markdown, SARIF and artifacts]
Controller --> Progress[Optional TUI or text progress]
```
The `demo` engine supplies synthetic responses in the controller without an external model call. `serve` is a separate static-site command and exposes no controller or database API.
## Software responsibilities
| Component | Responsibility |
|---|---|
| [`cmd/katarina`] | CLI dispatch, effective configuration/overrides, state selection, preflight, process locking, startup/resume/export and static serving |
| [`internal/config`] | Strict YAML, credential resolution, role inheritance, defaults, exact token amount parsing and configuration/policy identity |
| [`internal/source`] | File inclusion/exclusion, source hashes/chunks, outlines, bounded context/search and verified source copies |
| [`internal/lsp`] | Optional language-server lifecycle and constrained JSON-RPC navigation |
| [`internal/engine`] | Stage dependencies, worker pool, deterministic job identity, prompts, context loops, evidence validation, grouping and proof history |
| [`internal/model`] | Typed domain objects and validation for findings, economics, reviews, plans, interpretations and report data |
| [`internal/wire`], [`proto/worker.proto`] | Versioned protobuf request/response types and bounded frame encoding |
| [`internal/provider`] | HTTP API compatibility, endpoint rules, response/refusal/truncation checks, usage and the pi transport adapter |
| [`internal/piffi`], [`ffi/pi-bridge`] | cgo/C ABI ownership and typed provider callbacks into the statically linked Rust agent runtime |
| [`internal/store`] | SQLite state, atomic budget claims, job checkpoints, immutable artifacts, proof/resource intents and recovery |
| [`internal/runner`] | Permitted generated paths, command selection, disposable local overlays, bounded execution and captured outcomes |
| [`internal/cloud`] | Remote source transfer, idempotent resource launch, SSM execution, expiry and cleanup/recovery |
| [`internal/process`] | Child process environment, bounded buffers, deadlines and platform process-group handling |
| [`internal/report`] | Committed-state aggregation and atomic individual JSON, Markdown, SARIF and event exports |
| [`internal/tui`] | Event-driven terminal progress; it does not schedule or approve work |
| [`deploy`], [`web`], [`cmd/manual`] | Embedded stack template/static assets, build-time manual links and public template generation |
| [`cmd/bundle`] | Native pi release/source archives, source/build identity, dependency notices and download checksums |
The engine depends on typed provider/executor, store and runner interfaces or adapters. Model output passes through domain validation before it can become a controller action. HTTP JSON, model YAML, protobuf IPC and SQLite JSON blobs serve different boundaries; they are not interchangeable protocols.
## Execution flow
```text
Go controller / SQLite
|
+-- inventory: hashes, line chunks, symbols and exclusions
+-- configured analyzer output / optional LSP snapshot
+-- optional per-chunk security knowledge / question planning
|
+-- cheap scouts, one job per chunk and security lens
| +-- bounded reads, literal search and LSP navigation
+-- independent deeper scouts (configured sample / paths)
+-- additional configured / generated question investigations
|
+-- deterministic candidate fingerprint / deduplication
|
+-- independent challenger -----+
+-- independent defender ------+--> defender rebuttal
| |
+--------------------------------------v
assessor
|
log / ignore / test
|
retain every disposition
|
optional grouping of log/test findings
|
test dispositions only
|
generate individual/shared tests
|
none / local / EC2
|
review execution evidence
/ \
retain conclusion bounded test revision
|
JSON + Markdown + SARIF
```
Every included UTF-8 text file is chunked with five-line overlap where possible. Binary files, credential filenames, dependencies/metadata directories, configured exclusions, oversized files and lines exceeding the chunk limit are recorded. Directory exclusions are represented by one directory entry rather than every descendant. The filesystem scan does not depend on Git and does not silently apply `.gitignore`; configure intentional exclusions explicitly.
Scouts have different lenses: input-to-sensitive-operation paths; state/economic invariants; and integration/trust-boundary challenges. Every pass covers all included chunks. Candidate fingerprints use location, CWE and normalized title. This deterministically deduplicates repeated candidates, but is not semantic clustering: differently phrased duplicates can remain.
`scout_mode: focused` uses an open-ended investigation prompt instead of the rotating lens. In either mode, seed chunks are starting points for cross-file reasoning. Optional `deep_scout` jobs use a separately configured model on a stable hash sample and explicit paths, independent of cheap scouts' results. This prevents the cheap stage from being the only possible discovery path. See [research design] for comparison principles and the limits of benchmark claims.
The challenger and defender see the candidate and repository context, but not each other's initial review. The defender then answers the challenge. The assessor sees both reviews and the rebuttal. Dispositions are retained even when ignored. A “by design” disposition needs explicit design evidence; intent alone is not proof of safety. With structured evidence enabled, an ignore also requires a cited refutation or inapplicability. Additional capability, economic effects and deployment assumptions are recorded separately from severity and action.
Optional knowledge extraction precedes scouting. The shared artifact contains source-cited, challengeable claims. Independent deeper scouts do not inherit these claims. Specific generated and configured questions add work to the bounded scout pool; they cannot remove baseline coverage. Grouping follows individual assessment and preserves every finding. Shared plans and proof reviews must account for each member. See [shared knowledge, questions and evidence].
When tests execute, a separate proof-review request sees the generated test and recorded result. It can support/refute the hypothesis, retain uncertainty or request a concrete revision within `tests.max_iterations`. An optional `proof_reviewer` model can supply an independent counterpoint; otherwise the judge model handles this request. Interpretations remain separate from command status and the initial disposition. Attempts retain separate plans, execution intents and reports.
## Stage dependencies and data flow
Stages form a directed workflow with bounded local navigation and proof-revision loops. There is no free-form agent mailbox. The controller places an earlier stage's validated output into a later stage's prompt when that dependency is allowed.
| Stage | Inputs and transformation | Committed output / next consumer |
|---|---|---|
| Prepare | Strict configuration, included source, source/configuration identity, analyzer snapshots and design notes | Session, saved effective configuration/inventory; context for later work |
| Architect, optional | Per-chunk source and permitted context become cited, typed claims; controller assigns and deduplicates IDs | Immutable `security_knowledge`; planner and selected ordinary tasks |
| Planner, optional | Bounded source map and knowledge become additional questions; configured questions are resolved separately | Immutable `investigation_plan`; investigators |
| Discover | Full baseline coverage plus selected independent deep chunks and additional questions; bounded navigation as requested | Accepted job responses, individual investigation artifacts, deduplicated candidates |
| Debate | Candidate and source feed blind challenge/defense, followed by defender rebuttal | Completed review jobs; judge context |
| Judge | Candidate, reviews, rebuttal, source and optional structured evidence become an individual disposition | Assessed findings, including ignores |
| Group, optional | Bounded windows of non-ignored assessments become validated member/scenario proposals | Immutable `finding_groups`; report relationships and eligible shared proof scopes |
| Write and execute | Test-selected scopes become permitted new-file plans; runner intent precedes execution | Saved plans, durable execution intent/result and per-finding proof history |
| Interpret and revise | Generated files plus actual command result become member-aware proof interpretations; a concrete revision can create a new bounded attempt | Updated proof history; next attempt or retained conclusion |
| Export | Committed state plus saved session inputs become schema-defined reports | JSON, Markdown, SARIF, event JSONL and conditional analysis artifacts |
An architect, scout, investigator, peer reviewer or judge can consume additional navigation completions, each with a separate job ID and reservation. Architect/investigator roles inherit scout configuration if omitted; planner/grouper inherit judge. A configured deeper scout is required when deeper work is enabled. The proof reviewer defaults to judge unless separately configured.
Ordinary scouting may use shared knowledge. A deep scout receives source/design/tool context but neither shared model claims nor ordinary discoveries. Investigations receive only selected knowledge references; an empty list supplies none. Peers share the candidate but not their initial answers. These are information-access constraints; using the same model for several roles can still produce correlated errors.
Grouping is bounded, not exhaustive global clustering. Proposals are made within deterministic windows of at most 20 assessments and a context-size limit. Oversized assessments and matches across windows can remain individual. A report group containing both `log` and `test` dispositions does not authorize a shared execution; its test-selected members still follow individual proof work. Proof scopes currently execute sequentially.
## pi integration through FFI
Katarina statically links pi through a C ABI bridge to package the agent runtime and Go controller in one executable. `ffi/pi-bridge` compiles a Rust `staticlib`; Go links it through cgo under the `pi` build tag. Provider transports and the security workflow are implemented in Go.
The bridge uses pi's documented `sdk::Agent`, `Provider`, `ToolRegistry`, `AgentConfig` and message types. It installs a custom provider whose typed C callback calls the Go HTTP provider adapter. This keeps model routing, output limits, credentials, timeout ownership and cost reservations consistent across providers. Pi owns the in-process agent invocation; Katarina owns the higher-level security workflow.
Pi is invoked with an empty tool registry. Source navigation is controlled by Katarina's validated context-request loop. Shell tools, ambient project extensions, arbitrary edits and workspace configuration are not loaded into pi. Implicit tool defaults, magic-keyword shortcuts and automatic turn continuation are disabled. These restrictions limit the runtime actions available to an agent exposed to prompt injection in source code.
The C ABI is in `internal/piffi/bridge.h`: versioned request/result structs, explicit ownership, one synchronous provider callback and a matching Rust result-free function. No Go pointer is retained in Rust; `runtime/cgo.Handle` carries an opaque integer. Rust panics are caught before crossing C. Pi and provider errors propagate as failed jobs.
`pi_agent_rust` is pinned to `0.3.0`, with a checked-in Cargo.lock and pinned nightly toolchain. Its `sqlite-sessions` feature is enabled because the published 0.3.0 library has imports requiring it even in a headless build. Its default TUI and BPE-token features are disabled. The Go controller owns Katarina's authoritative SQLite store.
## Workers and communication
The controller launches the **same Katarina binary** with its internal `worker` command. A worker performs one model request and exits. Concurrency is a bounded controller pool. A timeout kills the worker process group, including a blocked FFI invocation; no separate daemon needs supervision.
`--max-agents` overrides `scan.workers`, limiting simultaneous model workers across each pipeline stage. Family-token reservations, the call count and the USD reservation are checked atomically in one SQLite transaction before dispatch. `family` is a configured model grouping independent of provider transport. Retries and navigation rounds consume new reservations; interrupted or unused reservations are not refunded.
Messages use `proto/worker.proto`, generated Go types, and a four-byte big-endian length prefix over stdin/stdout. Frames are capped at 8 MiB. Requests and responses carry protocol version and job ID, which the controller validates. Credentials are passed only through the anonymous request pipe, not argv. Only the controller writes the database.
Provider adapters use the external model APIs' JSON formats, and optional language servers use standard Content-Length JSON-RPC. Worker pipes carry Protocol Buffers messages. Agent conclusions are strict YAML documents, parsed into typed Go models before checkpointing.
## Context and navigation
Initial context contains the primary numbered lines, a bounded repository map, selected nearby/imported files, design notes and captured analyzer output. For jobs seeded by a source chunk, space for the numbered primary chunk is reserved before supplementary context, including shared model claims. Additional questions start from bounded per-file windows and can request further source evidence. Context budgets are explicit; truncation is marked. Agents can request more evidence using a typed YAML `request_context` document: line reads, literal searches, document symbols, definitions and references. Each completion and retry consumes a persisted budget reservation.
Built-in Go outlines use Go's parser. Other language outlines use structural heuristics; they are not a sound call graph or type analysis. Optional language servers provide semantic navigation and Slither supplies Solidity-specific analyzer evidence. File context never follows a model-supplied URL or reads beyond the included inventory.
## Persistence and failure semantics
SQLite uses WAL, `synchronous=FULL`, foreign keys, bounded busy waiting and a controller process lock. Durable entities include sessions, jobs/attempts, events, assessed findings, immutable analysis artifacts, test execution intents/results and cloud resource intents. Interrupted running jobs become pending on resume; completed results are reused. Shared proof evidence is committed atomically for all members, and replaying earlier assessments preserves committed test progress. Unknown provider charges remain reserved.
A provider can complete a request before the controller commits its result, so resuming an interrupted call may repeat the request and its charge. Test execution intents are written before launching a command; missing results stay indeterminate. EC2 launch uses an idempotent client token and persists intent before upload/launch. Cleanup runs on success, error and cancellation, with explicit recovery commands.
### One model completion
```mermaid
sequenceDiagram
participant C as Controller
participant S as SQLite store
participant W as Worker process
participant P as Rust pi runtime
participant G as Go provider adapter
participant A as Model API
C->>S: Ensure job and read checkpoint
alt Accepted result already committed
S-->>C: Saved response
C->>C: Reuse accepted job in current stage
else Unfinished job
C->>S: Atomically claim job and reserve call, tokens and USD
S-->>C: Claim committed or error
Note over C,S: A rejected claim stops dispatch
C->>W: Framed protobuf request
W->>P: C ABI agent invocation
P->>G: Typed synchronous provider callback
G->>A: HTTP completion request
A-->>G: Text and usage, or transport error
G-->>P: Typed completion result
P-->>W: Agent result or error
W-->>C: Framed protobuf response
C->>C: Check identity, parse YAML and validate stage contract
C->>S: Commit accepted result or failed attempt
C->>S: Append progress event
end
Note over C,W: Context requests and retries consume further reservations
```
This sequence shows the `pi` engine. `direct` bypasses Rust and invokes the same Go HTTP adapter. A validated `request_context` response completes its own job; the controller performs allowed navigation, assembles the next prompt and dispatches a new completion. Invalid output can consume another attempt on the unfinished job within the configured per-invocation limit. Neither path refunds the original reservation.
The pool limit defaults to 16 and bounds simultaneous model workers. Before dispatch, the claim transaction updates job state, session call/USD totals and family reservations together or rolls all of them back. Reported token usage is accumulated separately. Database updates use one connection, while HTTP completions run concurrently in children. Tool/compiler/LSP threads are outside the model-worker limit. Source bytes and stage prompts are held in memory; neither the worker cap nor per-context limits impose a total RAM bound.
### Durable data model
```text
sessions (id, root, source/config digests, status, call/USD reservations)
|
+-- jobs (session, job ID, role, status, attempts, latest result, usage)
| +-- job_families (session, job ID -> family label)
+-- family_budgets (session, family -> reserved tokens)
+-- events (global sequence, session, time, kind, job ID, message)
+-- analysis_artifacts (session, name -> immutable JSON object)
| security_knowledge / investigation_plan / investigation:ID
| finding_groups
+-- findings (session, finding ID -> assessed-finding JSON aggregate)
| candidate + reviews + decision + group reference + proof history
+-- tests (session, scope:attempt:N -> intent state and result JSON)
+-- resources (resource ID, session, client token, instance, object, state)
meta (storage version)
Session/job parent links are database foreign keys.
IDs inside JSON evidence/groups are checked by controller validation.
```
| Stored entity | Identity and checkpoint semantics |
|---|---|
| Session | Global session ID; stores root, source/configuration digests, lifecycle state and cumulative call/USD reservations |
| Job | `(session_id, id)`; accepted result, latest error/result, attempt count and accumulated usage. It does not archive every failed retry response. |
| Family budget | `(session_id, family)`; monotonic reserved tokens. `job_families` ties a job to one family for usage reporting. |
| Event | Global autoincrement sequence plus session ID; ordered operational history. It is not an event-sourced replacement for the entity tables. |
| Analysis artifact | `(session_id, name)`; immutable accepted knowledge, plan, question answer or group artifact |
| Assessed finding | `(session_id, id)`; JSON aggregate. Saving earlier assessment work merges committed proof progress instead of erasing it. |
| Test attempt | `(session_id, finding_id)`; despite the column name, its value is an individual/group scope plus `:attempt:N`. Storage state is `running`/`done`; execution status lives in the result object. |
| Cloud resource | Global resource ID; durable token/object/instance lifecycle including planned, launching, running and cleaned states |
Knowledge, question and group IDs link JSON domain objects, not separate normalized SQL tables. Member-aware proof updates use one transaction for all affected finding aggregates. A job completion and its progress event are separate writes; a crash may commit evidence without its final progress message. The database records operational checkpoints, not every prompt token, provider billing event or arbitrary external effect.
### State transitions and recovery
| Object / interruption | Recovery behavior |
|---|---|
| Job: `pending` or `failed` | A successful budget claim sets `running` and increments attempts; accepted output becomes `done`, otherwise `failed`. |
| Job left `running` or `failed` on resume | Reset to `pending`; completed jobs stay reusable and earlier reservations remain consumed. |
| Test intent without a committed result | Preserve an `indeterminate` execution. Do not automatically rerun the attempt or treat it as a clean failure. |
| Test with a committed result | Reuse the result; resume proof interpretation/checkpointing as needed. Revisions reject every prior execution digest in that scope. |
| Cloud intent or live resource left behind | Use saved ownership/client-token metadata for cleanup; expose failures and retain explicit cleanup/reap commands. |
| Session handled error/cancellation | Set `incomplete` and attempt report export. |
| Session successful workflow return | Set `completed`, even if a finding remains unresolved or a test command failed. |
| Hard process kill | Session may still say `running`; exports can lag behind committed SQLite state. Process locking determines whether another controller may start. |
Resume checks the current root/inventory and effective configuration, including the review-policy version. Credentials can rotate without changing that identity. A different source revision, model allocation, budget or policy starts a new session. Older sessions can still be exported when their saved artifacts are supported; resuming old review policies requires a compatible build.
The state directory contains the SQLite database and per-session files. Saved `config.json` and `inventory.json` supply the inputs used by report regeneration; the inventory stores metadata, not complete source bytes. JSON/Markdown/SARIF and conditional exports are individually atomic files, not one atomic export set. Retain the exact source revision and the session directory together for audit handoff. See [reports and recovery].
## Execution and trust boundaries
The model proposes conclusions, navigation and permitted test content. The controller checks structure and source provenance before scheduling consequences. Exact quotation matches establish that text occurs in the included source; they do not establish that a claimed exploit, invariant or economic payoff follows from it. Economic and capability review require model reasoning and human assessment as well as typed fields.
| Boundary | Data and authority |
|---|---|
| Operator to controller | Scope, model routes, credentials, budgets, commands, runner and deployment assumptions are operator inputs. Strict configuration validates supported shape and values. |
| Repository to model | Included source, selected design/tool context and permitted prior evidence can reach configured API endpoints. Exclusions and known-key redaction are not universal secret detection. |
| Controller to worker | Only the selected provider credential and explicit prompt/request settings cross the private protobuf pipe. Workers have private working directories and reduced environments; process separation is not an OS security sandbox. |
| Model to controller | Strict YAML proposes findings, citations, context operations, decisions or test plans. It cannot add executable commands, install tools, choose arbitrary URLs for navigation or write the database. |
| Controller to analyzer/LSP | Configured executables run against disposable source copies. They are trusted local programs with possible host/network effects; LSP response locations are constrained to included source for agent navigation. |
| Controller to local tests | New allowed files overlay a hash-verified included-source copy. The configured argv runs with operator OS privileges, a private HOME, reduced environment, timeout and output cap. Generated code can still have host effects. |
| Controller to AWS | The SDK uses operator AWS credentials for encrypted S3 transfer, EC2 and SSM. The prepared host runs test code unprivileged in a separate network namespace; the AMI and control plane remain prerequisites. |
| State/reports to reviewer | Source excerpts, vulnerability hypotheses and execution output persist in local state and reports. Private directory/file permissions protect access; report content is not encrypted by Katarina. |
The EC2 controller records intent before uploading/launching, uses an idempotent client token and expiry tags, and requests instance termination and source-object deletion on completion, errors or cancellation. An in-instance shutdown timer and recovery commands cover additional failure cases. A failed boot, unavailable AWS API or missing permission can defeat immediate cleanup; a termination request is not proof of deletion. The CloudFormation quick-create link provisions supporting infrastructure, not access keys or a prepared test image. See [AWS] for the complete remote path and [testing] for proof semantics.
## Packaging and extension points
The pi release build links the Rust static archive into the Go executable and embeds the website, generated manual and CloudFormation template. SQLite is embedded; no database service is needed. Optional project compilers, analyzers, language servers, provider endpoints and AWS infrastructure are external. The manual includes clickable links, ASCII diagrams and Mermaid source without a runtime diagram-rendering dependency. The bundle command produces native/source archives and checksums under the Git-ignored website downloads directory; these archives are hosted externally and are not recursively embedded in the executable.
Additional OpenAI-compatible endpoints are normally configuration changes. A different transport shape belongs in the Go provider adapter, preserving credential, output and usage rules. New analyzers and language servers use configured argv adapters. A new workflow stage belongs in the controller with typed outputs, context rules, budget reservations, deterministic job IDs and recovery semantics. Domain-object changes require corresponding schemas and report handling. Observable behavior and policy changes must update the [specification], behavioral IDs and session-compatibility boundary together.
Shared knowledge, questions and evidence
# Shared knowledge, questions and evidence
Katarina can build a shared security model, investigate specific questions alongside regular scouting, require structured evidence for review decisions, and group findings for shared tests. These stages use the existing Go controller, protobuf workers, SQLite checkpoints and model-family budgets. They require no additional services or packages.
## Enable the workflow
New `katarina init` configurations enable these features. Add this block to an existing configuration to enable them there:
```yaml
analysis:
shared_knowledge: true
max_investigations: 8
investigation_context_requests: 8
evidence_checks: true
grouping: true
max_group_size: 6
questions:
- question: Can liquidation become unprofitable within the documented operating range, leaving debt unpaid?
paths: ["contracts/**/*.sol"]
- question: Does every tenant-scoped database query preserve the authenticated tenant identity?
paths: ["src/main/java/**/Tenant*.java"]
```
Use questions and paths that apply to the repository. Each question must match 1–32 included files; an unmatched or oversized selection fails visibly. Split a broad question into narrower starting points when necessary. Target files seed the investigation; agents can navigate to any included file using the existing read, search and LSP tools.
| Setting | Behavior and limits |
|---|---|
| `shared_knowledge` | One architecture extraction job per included chunk, followed by a saved shared artifact. |
| `max_investigations` | Maximum generated questions, 0–64. Zero disables the planner. Configured questions are additional. |
| `investigation_context_requests` | Additional navigation rounds for each question, 0–64; defaults to 8 even when the feature is otherwise disabled. Other tasks use `scan.context_requests`. |
| `evidence_checks` | Requires structured checks from both initial reviewers, the rebuttal and the assessor; also requires capability and deployment analysis from the assessor. |
| `grouping` | Asks whether multiple non-ignored findings can share a bounded validation scenario. |
| `max_group_size` | Members per group, 2–12; defaults to 6. |
| `questions` | Up to 32 explicit questions. Each has a nonblank question of at most 4,000 bytes and 1–32 repository-relative path globs. |
Omitting `analysis` leaves knowledge, generated questions, evidence checks and grouping disabled for compatibility with existing configurations. The settings can be enabled independently. Explicit questions work with `max_investigations: 0` and without shared knowledge. Changing these settings changes the session configuration digest: start a new session to apply a different review policy.
## Shared security knowledge
The architect extracts components, boundaries, actors, assets, invariants and dependency assumptions. Each claim has a stable controller-assigned ID, exact source citations and an `observed`, `inferred` or `unknown` status. The artifact is bound to the reviewed source digest. Solidity guidance includes economic mechanisms and incentives; Rust/C/C++ guidance includes ownership, unsafe/FFI contracts and build assumptions.
Katarina verifies that cited files are included, line ranges exist, and quoted text occurs within the cited lines. Citations span at most 41 lines with at most 4,096 quote bytes. This verifies provenance. It does not establish that the inference follows from the quotation, that a comment describes actual behavior, or that the system is safe.
Regular scouting and subsequent review receive bounded shared context, prioritizing claims citing the current file. Complete claims that do not fit are omitted with a count. Independent `deep_scout` jobs receive source, design notes and tool output but **no shared model claims or earlier scout conclusions**. This gives discovery a path that does not inherit errors in the shared summary. It does not make calls using the same model statistically independent.
Knowledge extraction finishes before planning and scouting. Failed extraction or an exhausted budget leaves the session incomplete; the controller does not silently discard the failed stage. Completed chunk jobs remain available for recovery even if the combined artifact has not yet been assembled.
## Additional questions
The planner receives a bounded repository map and shared knowledge and proposes specific mechanisms to examine. It may return fewer than the configured maximum, including none. The controller validates every target path and knowledge reference and assigns stable IDs. Planner output does not remove any ordinary scouting pass or independent deeper sample.
Generated questions can select specific shared claim IDs. An empty selection means no inherited knowledge. Configured questions also start without shared model claims. Investigators can request source evidence, follow callers and state transitions, seek counterexamples, and return an answer with citations, unresolved obligations and zero or more candidate findings. An answer without citations must retain unresolved obligations and cannot introduce findings. All candidates enter the normal challenge, defense, rebuttal and assessment process.
Question answers are persisted separately, including answers that produce no findings. A missing final answer appears as incomplete in the report. Knowledge and question coverage are reported separately from baseline and deeper scouting. Investigation counts describe the committed plan; if planning itself failed, inspect the incomplete session and failed jobs before interpreting coverage.
Useful questions include ownership obligations across a Rust safe wrapper and unsafe implementation; allocation units across C/C++ callers and build modes; Java tenant identity propagation; and Solidity asset flows or profitable deviations across multiple transactions. A question should identify a property to check and a possible way to refute the concern, without assuming a defect exists.
## Structured evidence and additional capability
When evidence checks are enabled, each reviewer must address every obligation:
| Check | Required reasoning |
|---|---|
| `reachability` | Can the relevant entry point and claimed path execute? |
| `control` | What input, state, action or timing can the participant influence? |
| `guards` | Do existing checks, call-site rules or environmental controls defeat the claim? |
| `invariant` | Which intended safety or economic property is violated? |
| `impact` | What concrete consequence follows? |
| `feasibility` | Are the sequence, build/deployment assumptions and resource requirements possible? |
| `incentives` | For economic findings, what motivates the deviation or griefing and what is the net payoff or cost asymmetry? |
| `capital` | For economic findings, what funding, locked capital, liquidity, duration or ordering capability is required? |
Outcomes are `established`, `refuted`, `unknown` and `not_applicable`. All outcomes except `unknown` require source citations. Unknown checks must name the next evidence needed. Invariant, impact, incentives and capital cannot be waived as inapplicable. The last two checks are mandatory when a finding contains structured `economics`; economic review guidance is active for Solidity regardless of this setting.
A supporting review cannot contain unresolved or refuted obligations. A refuting review needs a cited refuted obligation. The assessor separately records a `supported`, `refuted` or `unresolved` evidence verdict, the action, severity and confidence. A supported verdict requires resolved checks, meaningful additional capability, and applicable or explicitly conditional deployment. An ignored finding requires a cited refutation or cited inapplicability. Uncertainty and intended behavior alone cannot justify ignoring it.
Capability analysis describes the actor, existing authority, additional access/control/profit/harm, the boundary or invariant crossed, and economic effects. Its status is `meaningful`, `equivalent` or `unknown`. Deployment applicability is `applicable`, `conditional`, `not_applicable` or `unknown`, with explicit conditions. Known statuses need citations. Unknown build flags, integration settings, subsidies or market assumptions remain visible.
Existing privileges alone do not establish that a Solidity participant's imposed losses are accepted. Permission to liquidate, withdraw or vote can coexist with harmful incentives. Economic effects therefore remain part of capability analysis even when no additional access privilege is gained. A severe but unresolved concern can be logged or selected for a test without pretending its feasibility is established.
These checks enforce structural completeness, source provenance and consistency of conclusions. They do not mechanically verify reachability, profitability, semantic entailment or the truth of model judgments. Human review and meaningful tests remain necessary.
## Grouping and shared tests
After individual assessment, the grouper proposes findings that one scenario with member-specific assertions can evaluate. Each group retains all original IDs, locations, prerequisites, reviews, decisions and severities. The proposal must state the common question, conditions, cited rationale and required assertion for every member. Unknown IDs and overlapping membership are rejected. Similar titles or a shared file are insufficient grounds to group.
Only groups whose members all have an individual `test` disposition receive a shared plan. Other groups remain report organization, and any member selected for testing proceeds individually. Findings outside groups also keep their individual test path. Ignored findings remain in reports and do not enter grouping.
A shared plan has a `covers` entry for each member, naming a generated test file and an exact excerpt of its assertion. The controller checks that the excerpt exists in that file. The proof reviewer must then assess actual discovery, execution, prerequisites and observations for each member. An excerpt can be present without executing, so this second check matters. One successful command cannot establish every claim.
Shared verification includes a separate `supports`, `refutes` or `inconclusive` interpretation for each finding. The overall result cannot be supports/refutes unless all members agree. Mixed outcomes remain visible; a group can support one observation and leave another unresolved. Revision uses the existing `tests.max_iterations` limit and must preserve every member's assertion. Indeterminate execution is never automatically repeated.
Grouping uses deterministic windows of at most 20 candidates whose assessed records fit `scan.max_context_bytes`. Oversized candidates and matches spanning windows may stay separate. This bounds model context but does not guarantee global semantic deduplication or minimum test count. Original findings are never deleted by grouping.
## Models, costs and recovery
New roles inherit existing model settings unless explicitly overridden:
| Role | Default model configuration |
|---|---|
| `architect` | `agents.scout` |
| `investigator` | `agents.scout` |
| `planner` | `agents.judge` |
| `grouper` | `agents.judge` |
An override is a complete agent entry, with the same provider/model/family/rate fields as other roles. Role inheritance includes family and pricing. For example, keeping `scout.family: cheap` and `judge.family: judges` charges architecture/questions to `cheap` and planning/grouping to `judges`. Configure family caps such as `cheap: 100M` and `judges: 10M` under `scan.token_budgets`; include the families used by any independently configured deeper scouts, writers or proof reviewers as needed. The same shorthand works in CLI overrides, including `--token-budget cheap=1B`.
All stages obey `scan.workers` / `--max-agents` and share the existing call, token and USD reservation limits. Enabling knowledge adds one model job per chunk; planning adds one; each question adds one plus permitted navigation; grouping adds one per eligible window. Retries also count. Evidence checks enlarge the existing debate/assessment calls instead of adding a separate stage. Shared tests may reduce duplicate execution, but that saving is not guaranteed to outweigh the added analysis. Measure quality and cost on representative repositories.
Accepted jobs, shared knowledge, the plan and answers, grouping proposals and proof outcomes are checkpointed in SQLite. Shared execution evidence is committed atomically for every member. Resume reuses completed work and retains reservations, while previously interrupted model calls can still incur another charge. See [reports and recovery] for artifact contracts and compatibility rules, and [comparative evaluation] for measuring detection quality and audit effort.
Design principles and comparative evaluation
# Design principles and comparative evaluation
Katarina combines broad source coverage, independent review and test execution to investigate security hypotheses within a configured budget. Its evaluation criteria are validated findings, missed issues, human review time and cost. This chapter explains the research influences, the implemented workflow and a methodology for comparing results.
## Research influences
An [InfoQ report on Claude Code and Linux vulnerability discovery] describes a file-focused investigation loop. Katarina's focused scouting mode draws on the general approach of starting from a source location and following relevant evidence. It is a separate implementation, with its own tools, prompts and review stages.
Anthropic's [published methodology], coauthored by Nicholas Carlini, describes code reasoning, ordinary analysis tools, comparisons with prior fixes, dynamic checks and human validation. These methods inform Katarina's open-ended investigation prompts and emphasis on evidence beyond a detector checklist.
Microsoft's [MDASH technical writeup] describes preparation, specialized scanning, debate, semantic deduplication and a separate proving stage, using different models and domain tools. Its [model-routing update] emphasizes allocating expensive models to difficult work. Katarina applies specialized review, debate and model routing in its own workflow. Its implementation differences and evaluation requirements are described below.
## Implemented principles
| Principle | Katarina behavior |
|---|---|
| Broad coverage without a detector gate | Every included text chunk gets scouting; a seed location does not restrict where the investigator may find or cite a bug. |
| An open-ended comparison mode | `scan.scout_mode: focused` starts from one location and asks for the most consequential supported defect. `specialized` adds rotating lenses; neither requires a bug to exist. |
| Follow mechanisms across files | Bounded reads, search and optional LSP navigation trace callers, ownership/state transitions, protocol sequences and correctly handled analogues. |
| Independent deeper discovery | `deep_scout` independently reviews a deterministic sample and explicitly selected paths, even when inexpensive scouts return no findings. |
| Independent disagreement | Challenger and defender cannot see each other's initial answers. The assessor sees the arguments and their evidence. Models/providers are selectable per role. |
| Execution changes the investigation | A test writer creates a plan; a runner executes it; a proof reviewer examines the test and result and can request a bounded revision. |
| Budgeted autonomy | Every model attempt, context request, stronger scout and proof review shares the concurrency, call, cost and family-token limits. |
| Evidence survives stopping | SQLite checkpoints accepted jobs, per-attempt test intent/results, interpretations and token reservations. Reports retain uncertainty and earlier attempts. |
| Domain knowledge is explicit | Project design notes, analyzer adapters, LSP tools and configured test commands supply build rules and protocol knowledge. Solidity reviews include economic assumptions and incentives. |
| Shared context remains challengeable | Source-cited observed/inferred/unknown claims support regular review; independent deeper scouts do not inherit shared claims. |
| Questions add discovery paths | Configured and generated questions produce saved answers and candidates alongside ordinary scouting. |
| Conclusions have evidence obligations | Structured checks, additional-capability analysis and deployment applicability distinguish support, refutation and missing evidence. |
| Shared validation preserves individual outcomes | Grouping retains every finding and requires member-specific test assertions and interpretations. |
Fresh `katarina init` configurations enable a 10% hash sample for deeper scouting. The percentage is an approximate sample fraction, not a guarantee of that fraction for a small repository; `deep_percent: 100` covers every chunk and `deep_paths` guarantees selected paths. When those fields are omitted, deeper scouting defaults off for configuration compatibility. A sample is not proof that unsampled code is clean.
```yaml
agents:
# Merge these entries into your complete configuration.
deep_scout: {provider: your_provider, model: YOUR_CAPABLE_MODEL, family: strong}
proof_reviewer: {provider: independent_provider, model: YOUR_REVIEW_MODEL, family: counterpoint}
scan:
scout_mode: specialized
deep_percent: 10
deep_paths: ["contracts/lending/**", "src/auth/**"]
context_requests: 6
workers: 8
token_budgets: {strong: 1M, counterpoint: 500K}
tests:
max_iterations: 2
```
Define the referenced providers and replace the placeholder model IDs with models available to the configured accounts. `deep_scout` names a role; select and evaluate a model for that role against the intended workload. Independent providers or models can bring different review behavior. If `proof_reviewer` is omitted, the judge's configured model handles execution review using a separate prompt and request.
## What the feedback loop guarantees
With an execution runner enabled, each attempt saves its complete plan and observed result. The reviewer returns `supports`, `refutes`, `inconclusive` or `revise`. These are **model interpretations**, not independent confirmation. The report keeps them separate from command exit status and the original assessor decision.
Revision requires a concrete request and a meaningful change to test contents or the configured command. Rewording the plan or reordering its files cannot authorize an identical rerun. A revision is compared with every earlier attempt in that finding or shared group; a cycle such as A → B → A is rejected. Each revision uses a fresh source snapshot and its own persisted execution intent. Error, timeout and indeterminate outcomes cannot authorize another attempt. Unknown execution outcomes stop the loop; successful/failed commands may be revised within the configured limit. Truncated evidence cannot support a definitive interpretation. Missing negative controls remain explicit.
`runner: none` saves one plan for inspection and performs no execution review. With execution enabled, the default is at most two generated plans/executions per finding; `max_iterations` accepts 1–5. Budgets can stop the workflow before that limit. Every model call and each EC2 attempt may incur its own charge.
## Comparative evaluation
Keep two tasks separate. **Discovery** starts from source without a vulnerability description. **Reproduction** starts from a supplied hypothesis. Microsoft's reported CyberGym setup supplied source and a high-level description; [CyberGym's own task levels] distinguish those inputs. A reproduction success rate cannot be used as discovery recall.
Use a versioned, access-controlled benchmark with separate tuning and held-out sets:
1. Include vulnerable and repaired snapshots, benign lookalikes, cross-file/protocol defects and economic failures. Keep labels, patches and repair descriptions outside the discovery inventory. Add private or newly constructed cases to reduce memorization risk.
2. Record source/configuration digests, toolchains, model IDs, dates, token/call limits and execution environment. Match these conditions where possible across systems. Run multiple repetitions; do not select only the best result.
3. Compare a capable focused scout with the specialized panel, then enable independent deep sampling and execution feedback separately. Measure raw candidate recall as well as post-triage outcomes. Focused mode retains Katarina's tools and triage; it is an internal comparison, not the original Claude Code harness.
4. Adjudicate findings independently of the model that generated them. A test must exercise the actual implementation and appropriate trigger. Check discovery and assertions, then run a repaired negative control. Compilation failure, an arbitrary crash, a vacuous test or an accepted economic exposure is not automatically a true positive.
5. Report unique confirmed issues recovered / known issues, precision among adjudicated findings, pending cases, duplicate rate, incorrectly ignored issues, coverage completion, reproduction success and setup failures. Track human review minutes, observed tokens, billed costs and cost per validated finding. Token reservations and cost reservations are not invoices.
6. Compare under both equal spend and equal time. Define acceptance thresholds with the auditors before running: for example, no regression in held-out high-severity recall while reducing false-positive review time. Publish failures and uncertainty alongside successes.
The automated test suite checks orchestration, concurrency, persistence, evidence transport and local execution. Detection quality requires a separate blind security benchmark. Comparative performance against the Claude Code loop or MDASH has not been measured.
## Remaining design limits
Katarina uses deterministic candidate fingerprints and optional bounded grouping for shared tests; differently phrased findings about the same root cause may remain separate. Its shared security model is a collection of cited model claims, not a complete or verified threat model. It does not automatically mine Git history or solve whole-program reachability. Supply relevant historical fixes and invariants as included notes or analyzer output. Test commands require configuration for the project's build and test format. Scouting tools are limited to validated context requests, and generated changes are limited to new test files. Record these limits when interpreting benchmark results and investigating missed issues.
## Related implementation reviews
The [Shannon code-analysis review] examines its architecture modeling, investigation planning and evidence checks. Katarina's independent implementation is described in [shared knowledge, questions and evidence]. Evaluate knowledge, questions, structured assessment and grouping separately under matched budgets; measure missed issues and wrongly grouped findings as well as test savings. Comparative performance remains unmeasured.
Shannon: code-analysis design review
# Shannon: code-analysis design review
Reviewed on 14 September 2026 at [Shannon commit `25b90b0611f15ab945e051dfee8ae78600d3a002`]. This review examines the public source and prompts, with emphasis on ideas applicable to Katarina's repository analysis. Shannon was not installed or executed, and this review provides no comparative detection score. Katarina now implements shared knowledge, additional questions, structured evidence/capability assessment and shared-test grouping independently; see [the current workflow] for configuration and limits.
The most useful lessons concern how to organize investigations: build security context, assign concrete questions, validate individual claims, and preserve the distinction between uncertainty and refutation. These additions complement Katarina's concurrent review, configurable models and budgets, independent deeper scouting, durable sessions and bounded test feedback.
Several Capella prompts identify their methodology as derived from Mantis, with modifications by Keygraph and Shannon. These are implementation references, not a claim that every technique originated in Shannon. [Architecture prompt attribution].
## The code-analysis workflow
Shannon has two relevant paths. Its pentesting preparation prompt delegates architecture, entry-point and security-pattern discovery, followed by specialist inspection of sensitive operations and data flows. That preparation is scoped primarily to network-reachable application behavior. These are prompt instructions; they do not by themselves establish coverage. [Pre-recon prompt].
The separate Capella static-analysis pipeline has ten stages:
```text
Architecture → threat model → investigation plan
→ research: rapid file triage → selected deep investigations
→ deduplication → independent review → production viability
→ static confirmation → risk calibration → export
```
The workflow code establishes this ordering and retains stage artifacts for recovery. The configuration parser enables Capella when `agentic_sast.enabled` is the string `"true"`; its configuration schema describes it as off by default. [Workflow], [configuration parser], [configuration schema].
Capella confirms findings by reading source. Its confirmation stage cannot run a reproducer. Shannon's later live exploitation belongs to the broader pentesting workflow. Capella's SARIF export checks validity and production viability; that gate does not itself require a successful dynamic reproduction. [Confirmation prompt], [export gate].
## Practices worth adapting
### Shared security context
The architecture stage produces a knowledge base containing component descriptions, trust boundaries, relevant bug classes and dependency information. The planner assigns target files, a specific question and references to relevant knowledge-base entries. This gives downstream investigators context chosen for their task. [Architecture prompt], [planning prompt].
Katarina's shared security model sits alongside its inventory and supplied design notes. Claims include source locations, exact quotations and observed/inferred/unknown status; the artifact records the snapshot digest. Summaries remain challengeable evidence: an incorrect shared assumption can misdirect later agents. Independent deeper scouts do not inherit these shared model claims.
For Solidity, this model should include participants, privileges, assets, accounting invariants, oracle assumptions, capital requirements and incentives. For backend and native code, it should describe entry points, tenant or privilege boundaries, ownership contracts and deployment conditions.
### Investigations centered on a mechanism
Capella's research prompt requires tracing callers of functions with explicit safety contracts. It asks investigators to verify the contract at each call site, including callers outside the initial target files. [Research prompt].
Katarina permits navigation beyond the starting chunk and persists each additional question, its target files, selected knowledge references, final answer, citations, unresolved obligations and candidates. Configured and generated questions run alongside baseline scouting. Examples include:
- Java: follow tenant identity from authentication through service calls to database filtering.
- Rust: verify ownership, aliasing and lifetime obligations across a safe wrapper and unsafe implementation.
- C/C++: follow allocation sizes, units and build-dependent assumptions through every relevant caller.
- Solidity: follow deposits, share issuance, oracle updates and liquidation as a sequence of state and asset changes, including profitable deviations from intended participation.
Long investigations need their own context and token allowance. Katarina's additional questions use `analysis.investigation_context_requests`, default 8 and configurable up to 64 navigation rounds; other tasks default to three. Capella's research code allows up to 100 turns for triage and 200 for a deep audit. These units are not directly equivalent. Increasing Katarina's depth should be evaluated against cost per validated finding and missed-issue rate, with explicit stopping conditions. [Research implementation].
### Explicit evidence checks
Capella records review criteria individually, with outcomes for satisfied, failed, unresolved and inapplicable checks. Its collector rejects a `VALID` decision with unresolved checks, so this is enforced beyond prompt wording. Other collectors separately record viability and static confirmation. These checks enforce consistency of model output; they cannot establish that the model's underlying claims are true. [Collector implementation].
Katarina's optional structured checks cover reachability, control, guards, invariant, impact and feasibility. Structured economic findings also require incentive and capital checks. Unknown obligations must identify the next evidence needed. The controller validates quotation provenance and consistency between checks and conclusions; it does not prove semantic entailment.
Keep separate fields for impact, evidence strength, deployment applicability and the next action. A potentially severe issue can have uncertain feasibility. Combining those into one confidence or priority score hides information auditors need.
### Capability and deployment analysis
Capella has a dedicated production-viability review and a risk-calibration policy centered on the additional capability an actor gains from the defect. The calibration collector records advisory scores without changing exported severity or eligibility. [Critic prompt], [calibration policy], [collector implementation].
For Katarina, this supports asking exactly which boundary or invariant is defeated under the documented deployment. Existing permission to call a Solidity function does not imply permission to impose its economic consequences on other participants. Capability analysis therefore needs asset flows, losses and incentives as well as access privileges. Unknown build flags, integrations or deployment settings should remain explicit conditions.
### Group work that one test can resolve
Shannon's reconciliation stage can group observations when one validation attempt and verdict would settle them together. The host accepts only supplied observation labels, rejects conflicting group membership, and keeps internal producer identities out of the grouping input. [Task formation], [group validation].
This grouping is separate from Capella's own deduplication prompt, which requires a shared exact file-and-line location and a similar title. That narrower rule should not be described as general root-cause clustering. [Deduplication prompt].
Katarina can reuse one test for several observations while retaining each location, prerequisite, review history and disposition. Every shared plan maps assertions to member IDs, and proof review records each member's outcome separately. Incorrect grouping can conceal distinct bugs, so prompts require uncertain matches to remain separate. Grouping uses bounded candidate windows and does not guarantee global duplicate removal.
## Design choices requiring caution
**Initial triage gates deep review.** Capella dispatches an investigation only if triage flags at least one of its files. Coverage accounting compares classifications against the planner's file set, not an independently enumerated repository inventory. Complete triage accounting therefore does not establish complete deep review. Katarina should retain its independent deeper sample and mechanically check any generated plan against its inventory. [Research implementation].
**An exploratory prompt does not ensure independent context.** The planner requests empty knowledge-base references for some exploratory investigations. The assignment builder currently interprets an empty reference set as including all entity and vulnerability entries. This is an implementation mismatch with the intended fresh look, not a measured detection failure. Katarina should make context isolation an explicit, testable property. [Planning prompt], [assignment builder].
**Role names do not imply different models.** Shannon's model host resolves `small`, `medium` and `large` to the same selected model. Capella uses fixed concurrency constants of four triage sessions and two audit sessions. Katarina already exposes independent role models, family budgets and a configurable worker limit. [Model host], [Capella constants].
**Filtering policies can hide relevant risks.** The review prompt broadly excludes resource-exhaustion findings except in modules intended to defend against them. The shared operating principles also exclude many build, test and generated files and assume committed secrets are handled by another scanner. These policies do not fit a general audit-preparation harness. Katarina should preserve explicit scope decisions and treat absence of reproduction as uncertainty, particularly for economic, availability and concurrency risks. [Review policy], [operating principles].
Capella also requires a CWE identifier to accept a finding. Katarina should retain its ability to report an economic or incentive failure without forcing an inaccurate CWE mapping. [Finding collector].
**The navigation layer is deliberately small.** Capella supplies bounded `read`, `find` and `grep` tools, without shell execution or source edits. The inspected implementation is not a compiler-backed whole-program analysis engine. Its architecture and dependency artifacts are model outputs. Katarina can pursue these workflow improvements using its existing source inventory and optional LSP integrations. [Repository tools], [tool policy].
## Adoption and evaluation
| Area | Implemented addition | Evaluation criterion |
|---|---|---|
| 1 | Structured evidence obligations and separate applicability, impact and validation fields | Fewer unsupported confirmations and dismissals; less auditor reconstruction time |
| 2 | Source-cited security model and investigation planner, checked against the inventory | Better cross-file recall without losing baseline coverage |
| 3 | Resumable investigations with configurable depth and independent exploration | Recovery of difficult and initial-scout misses at a measured token cost |
| 4 | Conservative grouping for shared tests, with original observations retained | Fewer duplicate tests without merging distinct defects |
These additions use Katarina's existing Go controller, protobuf worker messages, SQLite state and per-family reservations. No Shannon code is embedded or required at runtime. Evaluate each addition separately on the same vulnerable, repaired and benign snapshots under matched budgets. For Solidity, include mechanisms that are implemented as intended but admit harmful incentives. See the [comparative evaluation protocol].
Solidity economics and incentive review
# Solidity economics and incentive review
Solidity reviews include economic and game-theoretic failure modes in every scouting pass, including when `scan.passes: 1`. This guidance also reaches the challenger, defender, rebuttal, assessor and test writer. A protocol can execute every instruction correctly while rewarding behavior that drains value, creates bad debt or stops a necessary service.
Katarina asks agents to reconstruct the mechanism and its assumptions. It does not compute a formal equilibrium, obtain live market prices, calibrate probabilities or certify economic security. A checklist entry is a question to investigate, not a finding by itself.
## What agents examine
| Area | Questions |
|---|---|
| Actors and incentives | Who pays, earns, bears losses, controls information or can form a coalition? Can participants profit by deviating from the intended strategy? |
| Capital and feasibility | Can capital be flash borrowed or must it stay locked? What collateral, duration, ordering rights or governance power are required? |
| MEV and timing | Can ordering, front-running, sandwiching, delayed inclusion or a race change a user's outcome? |
| Oracles and liquidity | Does manipulation cost less than extractable value? What depth, window, stale-price or external-market assumptions make that possible? |
| Solvency and exits | Can withdrawals, liquidation incentives, bad debt or first-mover advantages create a run or a cascade? |
| Accounting and rewards | Do rounding, share inflation, donations, wash activity or reward farming pay more than they cost? |
| Governance | Can vote borrowing, bribery, concentrated voting or timing defeat the intended economic protections? |
| Liveness and griefing | Are keepers and liquidators still paid enough under stress? Can a low-cost action force a much larger loss or operating cost? |
Ethereum's [MEV documentation] provides background on transaction ordering, arbitrage, liquidations and sandwiching. These mechanics require project-specific evidence before Katarina should report a risk.
## Evidence that survives triage
Economic candidates include an `economics` object alongside the ordinary source location, claim, impact and remediation. This optional object is validated before a finding is accepted and preserved in SQLite, JSON, Markdown and SARIF properties. An economic mechanism may have no suitable CWE; an empty CWE is valid.
```yaml
economics:
actors:
- "Keeper: earns a fixed liquidation reward and pays execution costs."
assumptions:
- "No external keeper subsidy; confirm in integration/deployment documentation."
- "Gas-cost range is unknown from this repository."
sequence:
- "Compare available reward with transaction cost for an eligible liquidation."
- "Decline execution when net compensation is negative."
- "Check whether unpaid liquidation leaves collateral losses with the pool."
capital: "Keeper funds gas; no malicious borrower or flash loan is necessary."
payoff: "keeper_net = reward_value - gas_used * gas_price - other_execution_costs, all in the same unit"
constraints:
- "An enforceable alternative liquidation service could refute the liveness failure."
- "Rewards that rise sufficiently with costs may remove the incentive gap."
violated_invariant: "Required liquidation remains economically viable within the documented operating range."
validation_plan: "Use an isolated multi-actor scenario; vary costs and rewards, track unpaid debt, and compare a repaired reward mechanism."
```
This is an illustrative hypothesis, not a finding about an actual protocol. Unknown inputs stay explicit. Agents should give formulas, units and defensible bounds rather than invented prices or precise profit estimates. Net attacker profit, victim loss and externally motivated griefing are separate quantities. An unprofitable action can still be a griefing risk, but its objective and cost asymmetry must be stated.
Each reviewer is instructed to address the strongest falsifier, capital source, constraints and sensitivity to assumptions. The assessor must distinguish an unintended incentive failure from an explicitly accepted exposure. “Users are allowed to do this” or “the implementation matches the specification” does not establish economic safety. A documented intended mechanism can remain a `log` or `test` decision. Model confidence remains uncalibrated.
## Supply the protocol's economic model
With `analysis.evidence_checks: true`, structured economic findings require explicit `incentives` and `capital` checks alongside reachability, control, guards, invariant, impact and feasibility. Unknown checks must identify the next evidence needed. The assessor records existing authority, additional capability or harm, economic effects and deployment conditions. Intended behavior or existing permission alone cannot justify ignoring unresolved economic harm. See [structured evidence].
Put a project-specific economic model in an included repository file and reference it in configuration:
```yaml
design_notes: [docs/invariants.md, docs/trust-model.md, docs/economics.md]
```
The [economic design-note template] covers participants, accepted exposures, invariants, operating ranges and off-chain assumptions. Resolve its unknowns with your team; comments and documents remain untrusted evidence and are cross-checked against implementation. Do not include credentials or confidential market data you do not want sent to your selected providers.
Economic review guidance is included in the existing role prompts. It increases prompt size, and economic findings can require more context or output tokens. All requests count toward the session budgets. Independent deeper scouting and test revisions have separate [configuration controls]. Increase `max_output_tokens` if providers truncate larger finding documents, accounting for the resulting budget reservations.
## Tests and interpretation
Use the existing configured Foundry commands for deterministic scenarios, fuzzing or invariants against the actual implementation. Test writers are asked to vary relevant parameters, account for transaction costs and asset flows, and include a repaired-mechanism negative control. Claims about real market depth, competition, coalition behavior or human participation may remain unresolved by simulation; log those limits for auditors.
Generated vulnerability-reproduction tests are expected to observe the claimed failure in the original implementation and stop reproducing it after repair. They are distinct from permanent safety regression assertions, which should pass after repair. Command success alone proves neither kind is sound. Keep test discovery, assumptions and assertions in the human review.
Sessions retain the review policy used when they were created. After upgrading to a binary with a different policy, start a new session to apply that policy; reports from existing sessions remain available. See [reports and recovery] for compatibility requirements.
Generated tests and execution
# Generated tests and execution
The assessor can choose `test` only when `tests.commands` is nonempty. The test writer returns a strict plan: summary, configured command key, new test files and the expected observation. Katarina validates it and writes actual test source under `SESSION/tests/FINDING_ID/attempt-N/`.
```yaml
tests:
runner: none
timeout_seconds: 180
max_output_bytes: 65536
allowed_paths: ["src/test/java/**", "test/Katarina*.t.sol", "**/*_test.go"]
commands:
java: [mvn, -B, -Dtest=KatarinaSecurityTest, test]
solidity: [forge, test, --match-path, "test/Katarina*.t.sol", -vvv]
go: [go, test, ./...]
```
`none` generates reviewable tests without running them. `local` enables local execution. `ec2` uses [disposable AWS infrastructure]. With an execution runner enabled, Katarina runs the selected configured command whenever an assessed finding requests a test, without a separate confirmation prompt.
Execution is followed by an independent review of the test and observed output. The reviewer can request a concrete test revision; `max_iterations` limits the total plans/executions per finding (default 2, range 1–5). Every iteration has its own artifact directory, durable execution intent and result. Unchanged test content/command cannot be rerun by merely rewording the plan. `runner: none` generates one plan without execution review. See the [feedback-loop semantics].
## Plan restrictions
- Commands are selected by map key. The model cannot submit executable names, shell strings or arbitrary argv.
- Only new files matching `allowed_paths` are accepted. Existing implementation and test files cannot be overwritten.
- Absolute paths, traversal, hidden path components, duplicate files, credential filenames and NUL-containing paths are rejected.
- At most 12 files and 256 KiB of generated content are accepted.
- The original repository remains untouched; test overlays are written into a fresh copy.
Model prompts ask for assertions against the real implementation that observe the claimed defect and would fail after a repair. These are instructions, not proof that the generated test is sound. Review the actual assertion and run a negative control on the repaired implementation before calling a vulnerability confirmed.
## Shared tests
With `analysis.grouping: true`, related findings can share a plan when every member was individually selected for testing. A shared plan includes `covers` entries mapping every finding ID to an assertion excerpt in a generated file. Proof review records a separate interpretation for every member. Mixed outcomes remain separate, even though execution is shared. Tests are stored under `tests/GROUP_ID/attempt-N/`; individual tests retain `tests/FINDING_ID/attempt-N/`. See [grouping and shared tests].
## Local execution
Katarina copies included regular source files, verifies every SHA-256 digest, and overlays the generated tests. It excludes secrets, symlinks, dependency directories and other excluded inventory entries. No Git hooks or implicit Git checkout is needed.
The command runs in the copy, with a private temporary HOME, no inherited model/AWS keys, a timeout, bounded stdout/stderr and process-group termination. Temporary files are removed afterwards. The report keeps output, exit code, duration, truncation and runner type.
**Local execution is not an OS sandbox.** Code runs with your user privileges, can use the network, and could access other files available to that user. Use this mode for repositories and build tools you trust. Use EC2 for stronger separation. LSP servers and configured analyzer commands have the same local-host consideration.
The snapshot contains only included repository files. Go dependency downloads may require network access; Maven normally sees an empty HOME; Foundry libraries excluded by the scan are absent. Prepare dependencies using one of these approaches:
- Include vendored source dependencies you want analyzed/tested.
- Use a trusted prepared tool wrapper with explicit cache paths, such as `-Dmaven.repo.local=/opt/katarina/m2`.
- Use a prepared EC2 AMI containing the compiler, test tools and offline dependencies.
An example Maven configuration selects one test class. If the writer chooses a different class/file, the command may find no tests or fail: inspect the resulting plan and runner output. Set command naming conventions in your design notes.
## Interpreting results
| Status | Meaning |
|---|---|
| `passed` | The configured command returned exit code 0. Inspect assertions and test discovery. |
| `failed` | The command returned a nonzero exit status; it may be an assertion or setup failure. |
| `timeout` | The command or remote execution exceeded its timeout or was canceled. |
| `error` | Setup, process start, cloud submission or cleanup failed. |
| `indeterminate` | An execution intent exists without a committed result after interruption. |
None of these automatically changes a candidate into an independently confirmed vulnerability. Compilation failures, missing dependencies and “zero tests found” must never be presented as reproduced security issues.
## Rust and C/C++ test commands
These languages use the same validated test overlays and local/EC2 runners. Rust integration tests can usually be added under `tests/` without changing the crate. Record the crate's features, target and public API in design notes:
```yaml
tests:
runner: none
allowed_paths: ["tests/katarina_security.rs"]
commands:
rust: [cargo, test, --offline, --test, katarina_security]
```
Select `local` or `ec2` when ready to execute. The named test file must match the command. Dependencies and the selected toolchain must already be available for offline execution. Cargo projects with `autotests = false`, private-only APIs or explicit target lists may require an existing test hook; Katarina will not rewrite their manifest or production code. For a rustup installation, point PATH at the real toolchain binaries or use a trusted wrapper, as described in [navigation].
For C/C++, configure a project-owned command that compiles the newly overlaid test, links the actual implementation, runs it, and propagates failure. A trusted launcher can configure/build a disposable CMake directory and run a selected CTest target. `ctest` alone does not compile new source or register a new target. Existing CMake/Make build files cannot be overwritten by a generated plan, so prepare test discovery ahead of time. The default `tests/**` path allows C/C++ test sources; narrow it for your project. Sanitizer and fuzz commands use the same operator-configured command map and prepared toolchain.
For economic Solidity claims, see [economic scenario tests]. Reproduction tests should stop observing the defect on a repaired mechanism; permanent safety regression assertions should pass on the repair.
A persisted execution intent prevents an interrupted test from automatically running a second time. Start a fresh session or manually rerun the generated test after inspecting an indeterminate result. For EC2, first run the cleanup command printed in the AWS guide.
Proof-review interpretations are `supports`, `refutes`, `inconclusive` or `revise`. They do not overwrite the original disposition or convert command success into a confirmed vulnerability. Error/timeout/indeterminate execution cannot authorize revision, and incomplete/truncated output cannot support a definitive interpretation. When the revision limit or a budget is exhausted, remaining uncertainty stays visible.
Disposable EC2 test runner
# Disposable EC2 test runner
Katarina uses the AWS SDK directly, so the controller machine does not need the AWS CLI. Credentials come from the standard SDK chain: environment variables, shared AWS credentials/config files, SSO profiles or an assumed role. AWS credentials remain with the controller and are excluded from model worker requests.
## Create the stack
1. [Launch the Katarina stack in Asia Pacific (Seoul)].
2. Review the preloaded `katarina` stack and its [template YAML]. The launch link uses the [public S3 template] and selects `ap-northeast-2`.
3. Supply `OperatorPrincipalArn`: the existing IAM user or role allowed to assume Katarina's operator role. Review and acknowledge IAM creation in AWS.
The website and this manual open CloudFormation's review page directly with the template selected. The same YAML is embedded in Katarina for offline export or manual template upload:
```sh
katarina aws template --out katarina-bootstrap.yaml
```
### Prefilled quick-create links
CloudFormation's `templateURL` uses the S3 HTTPS endpoint; the website URL remains a convenient download. To print the same launch link, or choose a different target region, run:
```sh
katarina aws link --template-url https://katarina-bootstrap.s3.ap-northeast-2.amazonaws.com/katarina-bootstrap.yaml --region ap-northeast-2
```
The command prints a console URL opening the quick-create review page with the stack template preloaded. Sign in to AWS, select the operator principal and acknowledge IAM creation to create the stack. Credentials are configured separately using a profile or environment variables as described below; the link and stack outputs contain no secret keys. See the [official quick-create documentation].
The stack creates a dedicated VPC/public subnet, a security group with no inbound access, an encrypted private S3 artifact bucket, a restricted EC2 instance role/profile, and an operator role. The runner manages instances through SSM, without SSH access.
## Configure credentials and outputs
Use the `OperatorRoleArn` stack output with an AWS profile:
```ini
# ~/.aws/config
[profile katarina]
role_arn = arn:aws:iam::123456789012:role/YOUR-STACK-OperatorRole-...
source_profile = default
region = ap-northeast-2
```
Your existing `default` identity must be allowed to assume that role. Alternatively use your organization’s SSO/role process, or supply `AWS_ACCESS_KEY_ID`, `AWS_SECRET_ACCESS_KEY` and, for temporary credentials, `AWS_SESSION_TOKEN`. The stack's `CredentialsConsole` output links to the relevant IAM role page.
Copy these outputs into `katarina.yaml`:
```yaml
tests:
runner: ec2
timeout_seconds: 180
commands:
java: [mvn, -o, -B, -Dmaven.repo.local=/opt/katarina/m2, -Dtest=KatarinaSecurityTest, test]
allowed_paths: ["src/test/java/**"]
aws:
region: ap-northeast-2
profile: katarina
subnet_id: subnet-...
security_group_id: sg-...
instance_profile: YOUR-STACK-InstanceProfile-...
image_id: ami-YOUR-PREPARED-IMAGE
instance_type: t3.small
bucket: YOUR-STACK-artifacts-...
ttl_minutes: 30
```
Instance types permitted by the template are `t3.small`, `t3.medium` and `t3.large`. Update the template and configuration together for other types. TTL is 5–120 minutes. Allow enough TTL for boot, SSM registration, test timeout and cleanup. The code stops waiting one minute before the launch deadline.
## Prepare the test AMI
Use an x86_64 Amazon Linux 2023-compatible image with:
- An enabled Amazon SSM Agent and AWS CLI (`aws`).
- `bash`, `tar`, `gzip`, `timeout`, `unshare`, `runuser` and `useradd`.
- Your JDK/Maven/Gradle or Solidity/Foundry toolchain, available on `/usr/local/bin:/usr/bin:/bin`.
- Offline dependency caches readable by the unprivileged test user.
- A root volume at `/dev/xvda` compatible with the configured 20 GiB encrypted gp3 mapping.
Build a toolchain image containing the required tools and dependencies, then pin its ID in `aws.image_id`. Each test uses that configured image. If the AMI uses a different device layout or requires larger volumes, adjust the runner before use. Project dependencies must be available offline because the test's network namespace cannot reach external services.
## Lifecycle and boundaries
1. Persist a resource intent and idempotent EC2 client token in SQLite.
2. Copy/hash-check included source, overlay the generated tests, archive regular files, and upload to an encrypted private `sessions/` S3 object. The uncompressed snapshot cap is 128 MiB.
3. Launch one instance with IMDSv2 required, encrypted disposable storage, no inbound access, and Katarina ownership/expiry tags.
4. At boot, schedule shutdown after the configured TTL. `InstanceInitiatedShutdownBehavior=terminate` makes that shutdown terminate the host.
5. Wait for SSM Online, then submit the test command once. An ambiguous SSM submission is not retried automatically.
6. The root SSM setup downloads the archive, then the test runs as an unprivileged user in a separate network namespace. It cannot reach IMDS, SSM or external services through that namespace. This is host separation, not a formal proof against kernel escape.
7. Capture the command result. Request instance termination and delete the source object on success, failure or cancellation. Persist cleanup completion.
SSM inline output has AWS-imposed limits (24,000 stdout / 8,000 stderr characters); Katarina also enforces its own byte limit. Do not rely on the inline output for huge test logs. See [GetCommandInvocation].
## Recover and clean up
```sh
katarina aws cleanup --config katarina.yaml --state ./project/.katarina SESSION
```
The command uses durable client tokens to find instances after a lost launch response. Resume also attempts cleanup before additional EC2 work. Cleanup failures remain visible in `outstanding_resources`; they are not silently treated as successful testing.
If the controller crashes or cannot reach AWS, the in-instance shutdown timer remains. A failed boot, disabled shutdown service or unavailable control plane can defeat that timer; termination is not an absolute guarantee. For an explicit sweep of expired tagged instances in the configured region:
```sh
katarina aws reap --config katarina.yaml
```
The `reap` command requests termination only for instances tagged `ManagedBy=Katarina` with a parseable expired `ExpiresAt` tag. Schedule it through existing operations tooling if periodic cleanup is needed. Model budgets do not cap EC2, EBS, S3 or public IPv4 costs; AWS billing is separate.
The S3 bucket expires session objects after one day and is retained on stack deletion to avoid accidental loss. Empty/delete it explicitly when no longer needed. Stack deletion does not automatically terminate instances launched independently of CloudFormation; run cleanup/reap first.
Validation coverage includes local template checks and mocked runner lifecycle tests. Deployment and live EC2 test execution have not been validated; verify them in a dedicated evaluation account and target region before using the runner for reviews.
Evidence reports and recovery
# Evidence reports and recovery
Each session has a stable ID and lives under the selected state directory:
```text
.katarina/
controller.lock
state.db
state.db-wal # may exist while the database is open
state.db-shm
sessions/SESSION/
config.json # effective configuration, without API keys
inventory.json # included/excluded files, hashes and chunks
report.json # complete report contract
report.md # human handoff
report.sarif # SARIF 2.1.0
events.jsonl # ordered export of committed events
security-knowledge.json # combined source-cited claims, when available
investigation-plan.json # configured/generated questions, when planned
investigations.json # question answers and incomplete records
finding-groups.json # nonempty shared-validation groups
tests/FINDING_ID/attempt-N/... # generated test sources per iteration
tests/GROUP_ID/attempt-N/... # shared tests, with per-member coverage
```
SQLite is authoritative. File exports are snapshots, written atomically at normal completion or a handled interruption. A hard process kill may leave exports stale. Regenerate them from committed state:
```sh
katarina report --state /path/to/.katarina SESSION
```
Do not copy a live SQLite database without its WAL or a SQLite-aware backup. Stop the session first if copying the directory conventionally. The store uses schema version 1 and fails on unsupported versions rather than guessing a migration.
## Contracts
| Artifact | Contract |
|---|---|
| Full report | `schemas/report.schema.json` |
| Assessed finding | `schemas/finding.schema.json` |
| Event record | `schemas/event.schema.json` |
| Generated test plan | `schemas/test-plan.schema.json` |
| File/chunk inventory | `schemas/inventory.schema.json` |
| Shared security knowledge | `schemas/security-knowledge.schema.json` |
| Investigation plan | `schemas/investigation-plan.schema.json` |
| Investigation records | `schemas/investigations.schema.json` |
| Finding groups | `schemas/finding-groups.schema.json` |
| Worker request/response | `proto/worker.proto` |
| Native pi bridge | `internal/piffi/bridge.h` |
JSON Schemas use Draft 2020-12. Exports use `schema_version: 1.3.0`; the schemas also accept 1.0.0, 1.1.0 and 1.2.0 reports. New analysis fields are optional for earlier reports. SQLite uses storage version 1; family-budget and analysis-artifact tables are added when the database is opened if absent. Go validates model output before accepting it, including citation provenance and relationships between group members that cannot be fully expressed by JSON Schema. The report includes:
- Source and configuration digests and session completion status.
- Included/excluded file counts and completed/expected scouting jobs.
- Separate deep-scout coverage, so sampled stronger review is distinguishable from baseline coverage.
- Separate knowledge and question coverage, shared source-cited claims, the committed investigation plan, and completed or incomplete question records. Combined artifacts may be absent when their stage has not finished; completed model jobs still retain their accepted outputs.
- Candidate locations, CWE strings, severity, claim, evidence, prerequisites, impact and remediation.
- Optional structured `finding.economics`: actors, assumptions, strategy sequence, capital, net payoff, constraints, violated invariant and validation plan. All fields are required when this object is present; economic findings need not have a CWE mapping.
- The challenge, independent defense, rebuttal and assessor decision.
- Optional review `checks` and decision `assessment`, with evidence verdict, cited obligations, next evidence, capability analysis and deployment applicability. Quotation matching verifies source provenance, not the correctness of the model's reasoning.
- Optional finding `group_id` and `shared_test_id`, group membership and required assertions. Shared test plans have `covers`; shared proof verifications have per-finding `members`. All individual findings and decisions remain available.
- “By design” evidence, ignored dispositions and uncalibrated model confidence.
- Generated test plans, execution results and output.
- All `test_attempts` with plan, result and optional model verification. Top-level `test_plan`/`test_result` retain the latest attempt for compatibility.
- Job attempts, result text, token usage and estimated-usage flags.
- Ordered events, conservative spend reservations and outstanding cloud resources.
- `model_families` with each configured cap, cumulative reserved tokens, observed input/output usage and an estimated-usage flag. A cap of zero means unlimited. Sessions created before family accounting was introduced have no family ledger; their usage is not reconstructed retroactively.
A failed or canceled scan is `incomplete`, even if some stages have finished. An empty findings array is not meaningful without the coverage and job status fields. Tool exits are captured rather than converted to clean scans. A successful model scan means scheduled stages completed, not that the software is secure.
## Audit handoff
Give auditors `report.md`, `report.json`, `inventory.json`, the exact source revision and generated tests. Ask them to review unresolved candidates, highest-impact findings, assumptions accepted as intended design, and coverage gaps. Keep ignored findings available so the rationale can be challenged.
SARIF keeps the same finding IDs and file locations for code-scanning consumers. Model-recommended ignores are emitted as external suppressions **under review**, not auditor-approved dismissals. Results carry the assessor disposition, rationale, optional economic/evidence assessment and group/shared-test references in properties. Shared execution and individual member interpretations remain in test attempts. A SARIF upload is an operator action; Katarina does not upload reports automatically.
## Sensitive data
Reports can contain proprietary source excerpts, vulnerability details, test output and design documents. The state directory/files are created with private permissions. Existing state directories must have mode 0700, and state.db must be a regular file. Known provider keys are redacted from model/tool text and not included in effective configuration, but this is not a universal secret detector. Exclude confidential files you do not want sent to your configured model provider. A filename blacklist cannot detect credentials embedded in arbitrary code.
## Session compatibility
The configuration digest includes model choices, commands, budgets and the binary's review-policy version. API-key values are excluded, so credentials can be rotated without invalidating a session. Resume requires the same inventory and effective configuration to keep evidence from different review conditions separate.
If an upgrade changes the review policy, start a new session to use it. To continue existing work, use the original binary and configuration. Reports from existing sessions can still be exported without rerunning the review.
Policy `5-source-coverage-and-proof-history` reserves primary chunk context before supplementary material and rejects test revisions that repeat any earlier attempt. New sessions are required to apply these fixes; completed jobs from earlier policies are not retroactively counted as having received the corrected context.
## Limits of recovery
An in-flight model completion can be billed twice if its response was lost. Reservations are retained. Completed jobs are reused. Navigation rounds have separate job IDs and their accepted outputs are reused. A model that repeatedly exhausts its context budget requires a fresh session with adjusted limits.
Test execution has a durable intent before launch. A missing result is `indeterminate` and never silently repeated. EC2 resource intents and client tokens support cleanup after interrupted API calls; verify outstanding resources in AWS when cleanup reports an error. See [AWS recovery].
Development, packaging and evaluation
# Development, packaging and evaluation ## Build Development requirements: - Go 1.24 or later. - Rust `nightly-2026-07-05` (pinned by `ffi/pi-bridge/rust-toolchain.toml`). - A C compiler/linker and platform build tools for cgo and pi's native dependencies. - Network access on the first build to fetch Go and Rust modules. ```sh rustup toolchain install nightly-2026-07-05 --profile minimal make build bin/katarina version ``` `make build` builds the static Rust bridge using Cargo.lock, then links it into `bin/katarina` with the Go `pi` build tag. The first build downloads and compiles pi's dependency graph and can require several minutes and substantial memory and disk space. Subsequent builds reuse the Go and Cargo caches. The linked pi feature set is documented in [architecture]. Linux and macOS are the intended host platforms; build on the target OS/architecture with the corresponding C/Rust toolchains. A single executable does not mean universal libc compatibility: Linux binaries inherit the baseline of the build host. Build releases on the oldest supported target distribution and test them there. Windows users should use WSL; Windows controller locking is explicitly unsupported in this implementation. The application runs from a single executable containing the pi runtime and embedded SQLite. Project tests and optional analyzers/language servers require their own tools. `make build-go` produces `bin/katarina-go`, a Go development build with the `direct` provider engine and synthetic `demo` engine. That build rejects `engine: pi` because it does not include the Rust bridge. ## Tests ```sh go test ./... go test -race ./... go vet ./... # After make ffi: go test -tags pi ./internal/piffi ./internal/provider ``` Tests cover provider request shapes and refusal/truncation handling; typed IPC framing; source chunk coverage and symlink/drift rejection; credential precedence/redaction; concurrent budget reservations and restart recovery; the full scout/debate/judge/test pipeline; language-server protocol exchanges; generated test-path restrictions; local command timeout/output bounds; and mocked EC2 lifecycle/cleanup. FFI tests call the actual linked pi Agent with a deterministic Go provider callback. They exercise success, token accounting and provider failure without paid model calls. AWS lifecycle tests use a mock backend, not real EC2 instances. Live provider and AWS tests require explicitly configured credentials and should be run in a dedicated evaluation account/project. Economic/native-language tests verify that review guidance reaches every triage stage, economic evidence survives SQLite and report export, and mixed Rust/C/C++ LSP requests carry the correct language IDs. Optional local compiler tests reproduce an authorization defect in C, C++ and Rust, then check a repaired negative control using the actual implementation. They skip only when the relevant compiler is unavailable and need no third-party packages. LSP protocol tests use a stub server; they do not establish successful indexing of a real project by rust-analyzer or clangd. Investigation tests verify concurrent agents under the worker limit, recovery of a cheap-scout miss by independent deeper scouting, execution-feedback-driven revision, and resumption without repeating executed attempts. Budget tests race multiple claims against one family cap, check rollback of rejected claims, retain reservations across reopening, and aggregate usage across retries/roles. CLI tests cover `--max-agents`, repeated family budget overrides and the generated resume command. See [comparative evaluation] for the separate security-quality tests still required. Shared-analysis tests cover questions recovering baseline misses, selected shared context versus independent deeper scouting, role inheritance and family accounting, exact citation checks, economic obligations, grouping membership, assertion mappings and mixed member interpretations. An integration test closes/reopens SQLite after an interrupted shared proof review and checks that the execution and completed model calls are reused. Artifact tests reject changed immutable data; replayed assessments preserve committed proof evidence. These use synthetic model/runner fixtures and establish orchestration behavior, not detection quality. To export the richer integration fixture for independent JSON Schema validation, set `KATARINA_SCHEMA_REPORT` to a temporary output directory while running `go test ./internal/engine -run TestSecurityAnalysisSharedProofAndRecovery -count=1`. Validate the resulting report and additional analysis artifacts against their matching Draft 2020-12 schemas. Regenerate protobuf types when changing the worker contract: ```sh go install google.golang.org/protobuf/cmd/protoc-gen-go@v1.36.6 protoc --go_out=. --go_opt=module=katarina.fyi/katarina proto/worker.proto ``` Generated protobuf Go code is checked in, so normal builds do not require protoc. JSON Schema regeneration uses the development helper `python3 scripts/generate-schemas.py`; it is not a runtime dependency. ## Package ```sh make release RELEASE_VERSION=0.1.0-preview.1 ``` This builds the native pi executable and generates `web/downloads/katarina-VERSION-OS-ARCH.tar.gz`, `web/downloads/katarina-VERSION-source.tar.gz` and `web/downloads/SHA256SUMS`. `web/downloads/` is Git-ignored. The packager runs `katarina version` and requires the requested version and linked pi support; it does not substitute a direct-only build for a native release. The source archive includes tracked and non-ignored new source files from the working tree, without Git history, build output, private session directories or download archives. Each archive includes `BUILD.json`, a source-file checksum manifest, dependency metadata, pi's license/rider and collected dependency notices. Notice collection uses installed Go/Cargo metadata and local license files; where a crate omits its license file, it fetches the upstream notice at the crate's recorded Git revision. For declarations offering Apache-2.0 without a packaged notice, it includes the canonical Apache license text and records the declaration/repository. This can require network access. The Rust dependency listing is a conservative resolved-graph inventory, including build/platform dependencies, not a claim that every package survives linking. `BUILD.json` records the version, native target, build tools/settings, source identity, base Git revision and whether local changes were included. A dirty working tree is packaged explicitly as a source snapshot, not falsely identified as a clean Git release. Archive members have deterministic ordering, modes and timestamps. The generated unsigned SHA-256 manifest checks download integrity; it is not a publisher signature. Pin and validate target environments before claiming wider platform support. On Linux, the manifest also records the build host's libc and linked system libraries. To repackage an already built, matching native executable: ```sh go run ./cmd/bundle --version 0.1.0-preview.1 --binary bin/katarina ``` Run native macOS releases on macOS with the corresponding C/Rust tools, then smoke-test them there. Cross-building a Go-only executable would omit pi and is not the release format. Developer ID signing/notarization requires the maintainer's Apple signing setup; no signed or notarized macOS package is claimed by the current Linux preview. Keep downloadable versions and platform availability in `web/index.html`, `docs/installation.md` and README consistent when preparing another release. ## Website The public website files are `web/index.html`, `web/style.css`, generated `web/manual.html`, `web/katarina-bootstrap.yaml` and the generated `web/downloads/` directory. It uses static HTML and CSS with system fonts; the red high heel is Unicode Braille text in a `<pre>` element. Preserve its characters, spacing and line breaks when editing the artwork. Preview the embedded site with: ```sh bin/katarina serve --listen 127.0.0.1:8787 ``` `make docs` renders the manual as escaped text with clickable documentation, download and external links, and copies the embedded deployment template to `web/katarina-bootstrap.yaml`. Rebuild Katarina to update the embedded pages and template. The preview server defaults to loopback. Download archives are deliberately not embedded recursively inside the executable; download links target the public website, and a plain static server can preview the entire upload directory including downloads. Upload the public files and the complete `downloads/` directory to the root of `https://katarina.fyi/`, preserving names and subdirectories. `web/embed.go` is a Go build file and is not needed by the static host. Set ordinary content types for HTML/CSS, YAML and gzip archives; the artifacts need to be downloadable without authentication. The generated file permissions are readable by a static uploader. Upload matching archives and `SHA256SUMS` together; check published checksums before announcing a release. No credentials or application state belong in `web/`. ### Connect the hosted AWS template The public download is `https://katarina.fyi/katarina-bootstrap.yaml`. The launch buttons open CloudFormation's review page for stack `katarina` in `ap-northeast-2`, using `https://katarina-bootstrap.s3.ap-northeast-2.amazonaws.com/katarina-bootstrap.yaml` as the template. To reproduce the link: ```sh katarina aws link --template-url https://katarina-bootstrap.s3.ap-northeast-2.amazonaws.com/katarina-bootstrap.yaml --region ap-northeast-2 ``` Publish the generated `web/katarina-bootstrap.yaml` both with the website and as object `katarina-bootstrap.yaml` in the `katarina-bootstrap` S3 bucket. Keep those copies identical to `deploy/katarina-stack.yaml`; uploading the website does not necessarily update the separate bootstrap bucket. The S3 object must be publicly readable through its HTTPS endpoint before the launch link can create a stack. If the endpoint or launch region changes, update the AWS buttons in `web/index.html` and the manual generator, and the launch link/examples in `docs/aws.md`. Run `make docs`, rebuild and repackage so the source and embedded manual agree. Creating a CloudFormation stack still requires the operator principal, IAM acknowledgment, credentials and a prepared test AMI. ## Evaluate security quality Do not infer security quality from infrastructure tests. Build a versioned benchmark of repositories and known issues you are allowed to analyze: 1. Include vulnerable and repaired versions, with ground-truth issue locations and exploit prerequisites. 2. Include benign designs that resemble vulnerabilities, particularly intentional admin powers, tenant boundaries and Solidity economic assumptions. 3. Run fixed model configurations against the same source snapshots. 4. Measure candidate recall, assessor precision, duplicated findings, false-positive dismissals, test quality, token/cost reservations and human triage time. 5. Check that the test distinguishes vulnerable and repaired implementations while exercising the same property. A proof that asserts the defect occurs should stop succeeding after repair; a safety regression assertion should fail on the defect and pass after repair. Do not accept compilation errors or missing tests as proof. 6. Compare against your existing static analyzers and human audit notes. Tune prompts/models using a training set and retain a separate evaluation set. Use the [comparative evaluation protocol] to assess model routing and review strategies under matched budgets. Measure audit costs and reviewer effort alongside detection quality; orchestration test results alone cannot establish those outcomes. ## Known implementation limits - A bounded, file-oriented review is not whole-program formal verification. Context can be partial; large files/lines and dependencies may be excluded. - Baseline non-Go symbol extraction is heuristic. Java/Solidity/Rust/C/C++ semantic queries need the selected LSP server and a correctly imported project. - Economic review records strategy and payoff assumptions but is not an equilibrium solver or a live market simulation. Finding quality and sensitivity to prompt/model choices need benchmark evaluation. - The LSP subset does not implement an entire editor client or guarantee server indexing has finished when every query is made. - Candidate fingerprints are deterministic. Optional model-proposed grouping preserves all findings and uses bounded windows, so cross-window duplicates may remain. - Local tools/tests are not a sandbox. EC2 isolates hosts and test networking, with operator-prepared toolchains. - Model confidence is uncalibrated. A passing generated test is execution evidence, not independent vulnerability confirmation. - API compatibility targets text Chat Completions and Claude Messages; provider-specific APIs/auth extensions need additional adapters. - Cost reservations depend on operator rates and exclude AWS/tool charges. Interrupted upstream calls may be billed again. - Validation on live providers, large Java/Solidity projects, target-platform releases and AWS deployments is pending.
Integration references
# Integration references The following references document the integration interfaces and research background used by Katarina. The integration references were reviewed in September 2026. ## Runtime, providers and tools - [pi Rust SDK], [SDK source] and [upstream license]. - [OpenAI Chat Completions]. - [Claude Messages]. - [DeepSeek Chat Completions]. - [OpenRouter API overview]. - [Eclipse JDT Language Server]. - [Nomic Foundation Solidity language tools]. - [Slither] and [CLI usage]. - [Language Server Protocol]. - [AWS CloudFormation quick-create links]. - [AWS SSM SendCommand] and [GetCommandInvocation]. - [Microsoft MDASH announcement]. These establish integration contracts and background, not measured Katarina security performance. Model availability, prices, provider schemas and AWS behavior can change; validate the configuration used for each release and evaluation. ## Economic review and native-language tools - [Ethereum MEV documentation]: transaction-ordering background for protocol review. - [rust-analyzer configuration]: initialization options, Cargo project loading, build scripts and procedural macros. - [clangd installation and project setup]: compilation databases and compile_flags.txt limitations.