The Janitor — Research Contributions & Grant Brief
This document bridges The Janitor's production security capabilities to the research dimensions required for grant evaluation by OpenAI Researcher Access, Google AI Futures Fund, and Anthropic alignment programs.
Research Contribution
1. IFDS-Backed Taint Analysis Across 23 Language Grammars
The Janitor implements a custom Interprocedural Finite Distributive Subset (IFDS) solver over tree-sitter abstract syntax trees. The analysis spans 23 grammars simultaneously — including Rust, Go, Python, TypeScript, Solidity, Swift, Kotlin, Zig, Lua, GDScript, Objective-C, GLSL, Bash, Nix, HCL/Terraform, and Java — to prove source-to-sink taint reachability across language and serialization boundaries.
Research contribution: IFDS over polyglot ASTs with cross-language ABI edge semantics.
The cross-language memory safety witness (crates/forge/src/lcm.rs) is the first
open-source IFDS-backed detector that traces raw-pointer ownership across C/Rust FFI
boundaries using AhoCorasick multi-pattern matching in a ±20-line sliding window without
a full program graph — enabling sub-second detection at PR-gate latency.
2. Kani-Proven Boolean Predicates for Security Gate Correctness
Every critical detection predicate in The Janitor is verified under Kani bounded model
checking (crates/forge/src/reflexive_assurance.rs). Each predicate (e.g.,
ffi_deref_unguarded, session_tool_intent_drift, proof_obligation_missing,
oidc_scope_missing_audience) is proven panic-free and overflow-absent across all
possible boolean input states.
Research contribution: Security detection logic expressed as formally verified pure Boolean functions with Kani symbolic execution proofs. This is a reproducible, machine-checkable form of detection correctness that eliminates the false-positive variance inherent in confidence-scored ML approaches.
3. Z3 SMT Constraint Solving for Exploit Witness Synthesis
The Janitor's exploitability layer (crates/forge/src/exploitability.rs) uses an rsmt2
Z3 interface to generate symbolic path constraints from IFDS taint traces, refining
candidate findings into concrete curl reproduction commands only when the Z3 model is
SATISFIABLE. Unsatisfiable paths are suppressed before reaching the bounty ledger.
Research contribution: Automated exploit witness generation (AEG) from IFDS taint
evidence using SMT constraint refinement — a formal bridge between static analysis and
practical reproduction payloads. This directly implements the principle of
"no proof, no submission" enforced by the proof obligation gate
(crates/forge/src/proof_obligation.rs).
Alignment Surface
AI-Agent Tool-Intent Firewall (P2-22)
crates/forge/src/agent_intent.rs implements an AI-agent deception detector that fires
when a tool dispatch expression appears within ±15 lines of a privilege-escalating
operation without an explicit read-only/sandbox intent suppressor. The Kani-proven
predicate session_tool_intent_drift(has_tool_sink, has_escalation, has_suppressor) is
the first formally verified gate against autonomous agent privilege escalation in
open-source static analysis.
The alignment claim: an AI agent cannot escalate from observer to mutator without the escalation being structurally visible in the code and formally flagged. This is a deterministic enforcement of the "minimal capability" principle without relying on runtime RLHF or model self-reporting.
Bayesian LLM Hijack Detection
crates/forge/src/bayesian_taint.rs applies Bayesian conditional probability over
AhoCorasick pattern matches to detect unbounded prompt concatenation and LLM context
hijacking at the source level — before deployment. This is an interpretable,
auditable alternative to behavioral runtime monitoring that cannot be
jailbroken at inference time.
Formal Proof That Tool-Grant Escalation Requires Operator Authorization
The proof obligation gate (crates/forge/src/proof_obligation.rs) enforces that no
KevCritical finding reaches the bounty ledger without carrying a ProofClass variant
(ReachabilityProof, InvariantViolationProof, or LatticeGapProposal). This is a
mechanically enforced "constitutional" constraint: the system cannot emit a
high-severity claim without a cryptographically-adjacent proof artifact.
Societal Impact
False-Positive Elimination at Scale
The Structural Eradication Law prohibits suppressing commercial false positives with prose annotations — they must be eliminated by writing a deterministic AST guard in the engine. This produces quantifiable false-positive reduction: detectors are provably correct on the test corpus or they are not shipped.
Quantified: 33,000 pull requests audited across 22 enterprise repositories on an 8GB laptop. The actuarial ledger records per-PR categorical billings — every intercepted threat is documented, not aggregated. This is a reproducibility-first approach to security measurement.
Zero-Upload, On-Device Execution
The Janitor never transmits source code to a remote server. Analysis runs entirely
in-memory via memmap2 zero-copy file access. This is a structural privacy guarantee
for academic institutions, national security research environments, and healthcare
providers who cannot permit code exfiltration to cloud SAST vendors.
Open-Source Formal Methods for Security
All Kani harnesses, IFDS lattice structures, and Z3 constraint templates are open-source under the project's license. Researchers can reproduce, extend, and formally verify every security claim. This contrasts with opaque ML-scored SAST tools whose false-positive rates are untestable.
Fairness
The Janitor's scoring model is deterministic, not confidence-scored. A finding either satisfies the structural predicate (proven by Kani) or it does not. There is no probabilistic threshold that produces disparate outcomes across code styles, author demographics, or language ecosystems. The same formal rule applies to Rust, Go, Python, Solidity, and TypeScript identically — eliminating the ML bias variance documented in AI code review tools trained on pre-AI, predominantly English-language codebases.
Grant Metrics
| Metric | Value | Source |
|---|---|---|
| Pull requests audited | 33,000+ | .janitor/bounce_log.ndjson actuarial ledger |
| Enterprise repositories | 22 | Production deployments |
| Analysis latency | 6.7 s/PR | Benchmarked on 8GB Dell Inspiron (WSL2) |
| Language grammars | 23 | crates/polyglot/src/lib.rs |
| Kani-verified predicates | 12+ | crates/forge/src/reflexive_assurance.rs |
| Detectors with TP/TN test coverage | 100% | CI enforced — no detector ships without tests |
| False-positive rate on Godot Engine PRs | <5% | Structural Eradication Law enforcement |
| SLSA compliance level | Level 4 | justfile verify-reproducible |
| PQC attestation | FIPS 204 + FIPS 205 | ML-DSA-65 + SLH-DSA-SHAKE-192s dual key bundle |