[Bug][Security]: Lean character literal scanner accepts newlines, enabling code injection

[morluto]

Summary

_skip_quoted_literal advances through any character that isn't a backslash or the delimiter, including newlines. An input like by exact True.intro\n'\n#eval <IO action>\n' makes the scanner consume everything through the second quote, hiding the #eval directive from the proof-axiom validator.

Evidence

src/jacobian/lean_frontend/proof_axioms.py L371-380:

def _skip_quoted_literal(source: str, index: int, length: int, delimiter: str) -> int:
    index += 1
    while index < length:
        if source[index] == "\\":
            index += 2
        elif source[index] == delimiter:
            return index + 1
        else:
            index += 1
    return index

Root cause

The quoted-literal scanner has no newline rejection. Lean character literals are single-character and cannot contain raw newlines, so a newline inside a char literal is always malformed.

Scope

Reject newlines inside _skip_quoted_literal when the delimiter is ' (char literal), raising a malformed-literal error instead of consuming across lines.

Source

• Fix Lean character literal token scanning #809 (comment)

Generated with Devin

[morluto]

Revalidated against current main: _skip_quoted_literal() now rejects \r/\n both directly and after an escape, rejects a trailing escape, and rejects unterminated quoted literals. The reported scanner-hiding path no longer exists. Closing as completed.

[morluto]

Confirmed as the concrete security bypass under the canonical owner #1038. The immediate fix should reject raw newlines and malformed escapes in character literals, with a regression proving the hidden #eval remains visible/rejected. #1038 owns the systemic repair: proof-term category parsing and elaboration by the pinned Lean frontend, hermetic execution, elaborated declaration/dependency policy, and demotion of the Python scanner to bounded defense-in-depth rather than acceptance authority.

[morluto]

Canonical security owner opened: [Security Architecture]: Enforce Lean source policy on a parser-owned syntax boundary, not a hand-written literal scanner.

This issue remains the executable regression for the raw-newline character-literal bypass. The immediate newline rejection is appropriate defense in depth, but closure should also require that ordinary proof capabilities parse a narrow term/tactic category with the exact pinned Lean frontend, apply a positive syntax policy, wrap it in a server-owned module, and sandbox elaboration. The hand-written scanner must no longer authorize execution.