ClawHub
Back to skill

Security audit

Formal Methods

Security checks for vulnerabilities and agentic risk

Overview

The skill is upfront about running local formal verification tools, but Lean and Coq inputs are executed without a documented sandbox or constrained environment.

Install only if you are comfortable running Lean and Coq code with the permissions of your local user account. Prefer using it for your own trusted proofs, and avoid checking third-party Lean or Coq files unless the runtime is wrapped in a container or other sandbox with a cleaned environment and restricted filesystem access.

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

Error
Location
SKILL.md:35
Finding

Unsandboxed Execution of User-Controlled Lean and Coq Source

Content
View full analysis
/`), runs the prover binary with `cwd` set to that directory, captures stdout/stderr, and applies a 60-second timeout. The exact commands are: - Lean: `lean ` — may read Lean 4 stdlib and elan-managed toolchains from `~/.elan/` - Coq: `coqc ` — may read Coq stdlib and opam-managed packages from the opam switch - Z3: `z3 ` — self-contained, only reads the input file. Accepts declarative SMT-LIB2 format only. **Filesystem access:** The skill itself only writes to the temp directory. However, Lean and Coq read their installed standard libraries and search paths (managed by elan/opam) as part of normal operation. The skill does not explicitly constrain `--include` paths or environment variables. **Network access:** The skill does not make network requests. However, if Lean source contains `import` of unresolved packages, `lake` tooling could theoretically attempt a fetch — this is a Lean runtime behavior, not initiated by the skill. To prevent this, avoid `lakefile.lean` or `lake-manifest.json` in the temp directory (which the skill does not create). ``` The affected tool definitions accept source text directly: ```markdown ### lean_check Type-check Lean 4 code. **Parameters:** - `code` (string, required): Lean 4 source code - `filename` (string, optional): Source filename (default: `check.lean`) ``` ```markdown ### coq_check Check a Coq proof for correctness. **Parameters:** - `code` (string, required): Coq source code - `filename` (string, optional): Source filename (default: `check.v`) ``` ### Technical Analysis The skill documentation states that caller-supplied Lean and Coq source is written to a tem ...[truncated 3278 chars]
Remediation
View remediation

SkillSpector

Vulnerability Patterns
  • Prompt InjectionInstruction Override, Hidden Instructions, Exfiltration Commands
  • Data ExfiltrationExternal Transmission, Env Variable Harvesting, File System Enumeration
  • Privilege EscalationExcessive Permissions, Sudo/Root Execution, Credential Access
  • Supply ChainUnpinned Dependencies, External Script Fetching, Obfuscated Code
  • Excessive AgencyUnrestricted Tool Access, Autonomous Decision Making, Scope Creep

Static analysis

No suspicious patterns detected.