Security audit

openmath-open-theorem

Security checks for vulnerabilities and agentic risk

Overview

This skill is a disclosed OpenMath theorem discovery/downloader with some normal setup persistence and remote-source risks that users should understand before building downloaded projects.

Installers should be comfortable with the skill reading or creating an OpenMath preferences file and contacting the documented OpenMath API. Prefer project-local config, avoid storing submission or auth fields unless needed, do not set custom OpenMath endpoint environment variables unless you trust them, and review downloaded Lean/Rocq source before compiling or proving it.

A.I.G

Vulnerability Patterns

Insecure Skill Coding PracticesFinds exploitable flaws such as hardcoded secrets or command injection
Skill Instruction HijackingAlters the agent's session goals or safety constraints when the skill loads
Agent Memory PoisoningWrites attacker-controlled rules into memory that affect later sessions
Remote Payload Retrieval and ExecutionFetches external code whose behavior can change after review
Embedded Malicious CodeShips malicious scripts inside the skill and executes them locally

Findings (1)

T09 · Insecure Skill Coding Practices

Warning

Location: scripts/openmath_env_config.py:197
Finding: Unvalidated API Endpoint Can Supply Executable Theorem Source
Content: View full analysis
str: env_override = normalize_url(os.environ.get("OPENMATH_API_HOST")) if env_override: return env_override return default_openmath_api_host() ``` `scripts/openmath_api.py:73-84`: ```python def fetch_theorem_detail(theorem_id: int) -> TheoremRecord: try: api_host = resolve_openmath_api_host() except OpenMathEnvConfigError as exc: raise RuntimeError(str(exc)) from exc url = f"{api_host}/api/v1/theorems/{theorem_id}" result = fetch_json(url, "openmath-open-theorem/fetch_theorem_detail.py") ensure_success(result) theorem = result.get("data") if not theorem: raise RuntimeError(f"Theorem with ID {theorem_id} not found.") ``` `scripts/download_theorem.py:112-116`: ```python def scaffold_lean(project_dir: Path, theorem: TheoremRecord) -> str: module_name = lean_module_name(theorem.theorem_id) theorem_file = project_dir / f"{module_name}.lean" theorem_code = theorem.theorem_code or f"-- TODO: Fill in theorem {theorem.theorem_id}\n" theorem_file.write_text(theorem_code.rstrip() + "\n", encoding="utf-8") ``` The equivalent Rocq path writes remote theorem source verbatim at `scripts/download_theorem.py:132-135`. ### Technical Analysis The `OPENMATH_API_HOST` environment variable is accepted after only trimming whitespace and a trailing slash. The code does not: - Restrict the URL to HTTPS. - Verify that the hostname belongs to an approved OpenMath domain. - Require confirmation before using a custom endpoint. - Authenticate the returned ...[truncated 2605 chars]
Remediation: View remediation

SkillSpector

Vulnerability Patterns

Rogue AgentSelf-Modification, Session Persistence
MCP Least PrivilegeUnderdeclared Capability, Wildcard Permission, Missing Permission Declaration
MCP Tool PoisoningHidden Instructions, Unicode Deception, Parameter Description Injection
Prompt InjectionInstruction Override, Hidden Instructions, Exfiltration Commands
Data ExfiltrationExternal Transmission, Env Variable Harvesting, File System Enumeration

Findings (4)

Tp4

High

Category: MCP Tool Poisoning
Confidence: 98% confidence
Finding: The declared purpose is theorem discovery and download, but the skill behavior also includes configuration inspection and persistence in local or home directories, which is more sensitive than the description suggests. This mismatch can mislead reviewers and users about what data is accessed and stored, making consent and risk evaluation weaker and enabling unexpected exposure of local preferences or auth-related fields.
Content: No source excerpt is available for this finding.

Undeclared Tool Scope

Medium

Category: MCP Least Privilege
Confidence: 86% confidence
Finding: The skill directs use of environment variables, local/shared config files, networked API calls, and local workspace scaffolding, but it declares no explicit tool scope or permissions boundaries. That omission increases the chance an agent can read/write files or reach network endpoints without clear least-privilege constraints, especially because endpoint overrides via environment variables could redirect traffic to attacker-controlled hosts.
Content: No source excerpt is available for this finding.

Session Persistence

Medium

Category: Rogue Agent
Confidence: 78% confidence
Finding: The skill explicitly asks to create and persist shared configuration under the workspace or the user's home directory, creating session persistence across runs. Even though the stored fields appear limited, the instructions also mention possible submit/authz fields later, so persistent storage could retain sensitive data longer than necessary or in a broadly accessible location.
Content: Scanner excerpt · SKILL.md (reported line 19)May include surrounding context.
md
This gate is mandatory. If `openmath-env.json` is missing, or if it exists but `preferred_language` is missing, stop. Do not query the OpenMath theorem list, theorem detail, or download APIs until setup is complete. If no config exists, stop and ask the user where to create it, then collect at least: - `preferred_language`: `lean` or `rocq` - config visibility / save scope: `./.openmath-skills` or `~/.openmath-skills`

Session Persistence

Medium

Category: Rogue Agent
Confidence: 60% confidence
Finding: Skill establishes unauthorized persistence across sessions via cron jobs, startup scripts, or state files. Session persistence allows an attacker to maintain access beyond the current interaction.
Content: Scanner excerpt · scripts/openmath_env_config.py (reported line 108)May include surrounding context.
python
f"First-time setup guide: {setup_doc_path()}", f"Example config: {example_config_path()}", "", "If no config exists, stop and ask the user where to create it:", f"- ./{PROJECT_CONFIG_DIRNAME}/{ENV_CONFIG_FILENAME} (recommended for project-specific settings)", "- ~/.openmath-skills/openmath-env.json (recommended for reusable settings)", "",

Static analysis

No suspicious patterns detected.