T09 · Insecure Skill Coding Practices
Error
- Location
- SKILL.md:36
- Finding
- Untrusted Lean Source Executes in a Shared Privileged Service Runtime<![CDATA[ ## Vulnerability Details **File Location**: `SKILL.md:36` **Additional Locations**: `SKILL.md:194`, `SKILL.md:217-235`; `schema.md:289-300`, `schema.md:428-448` **Vulnerability Type**: Trusted code execution without effective isolation **Risk Level**: High ### Vulnerable Code Snippet ```markdown - Lean submitted to `certify_from_lean`, `export_provider_programs`, or `execute_locally` runs as `trusted_direct_v1` inside the private Cloud Run service container. IAM authenticates callers, but Lean shares the service filesystem, network, and service identity; this is not untrusted-code isolation. Submit only internally trusted Lean. The receipt fields `execution_mode` and `untrusted_code_isolation` are the machine-readable authority. ``` The corresponding schema accepts source code as a general string: ```json "lean_source": { "description": "Complete CircuitSpec authoring fragment defining spec. Use search_lean with authoring_only=true and a worked .lean corpus example when authoring. Maximum 1048576 characters.", "required": true, "type": "string" } ``` ### Technical Analysis The Skill explicitly states that user-supplied Lean source is executed directly within a shared Cloud Run service container and that it shares the service filesystem, network connectivity, and service identity. IAM authenticates the caller but does not isolate the submitted program from service-level resources. The instruction to submit only “internally trusted Lean” is an administrative warning rather than a technical security boundary. The exposed input schema only establishes that `lean_source` is a string; it does not demonstrate enforced syntax restrictions, capability restrictions, module allowlisting, filesystem isolation, network isolation, or per-request identities. This execution model exceeds the minimum privileges required to compile or verify a quantum-circuit specification. A least-privilege implementation would not grant submitted source access to a sha ...[truncated 1765 chars]
- Remediation
- <![CDATA[ ## Remediation Suggestions 1. Execute every submitted Lean program in a fresh, ephemeral sandbox rather than the shared service container. 2. Use a dedicated request-scoped service identity with no default permissions; grant only the minimum capabilities required for proof compilation. 3. Disable network access by default. If limited network access is indispensable, enforce an explicit destination allowlist through a controlled proxy. 4. Mount an empty, request-specific filesystem and expose only immutable compiler libraries required for the operation. 5. Prevent access to metadata services, service credentials, Unix sockets, host paths, and artifacts belonging to other requests. 6. Enforce a strict server-side allowlist of admitted Lean imports and declarations. Do not rely on prompt instructions or caller trust. 7. Apply CPU, memory, process, output-size, and wall-clock limits to every request. 8. Destroy the sandbox and all temporary files after completion. 9. Return verifiable receipt fields identifying the sandbox policy, egress policy, runtime image digest, and request-scoped identity. 10. Until isolation is implemented, disable the source-execution actions for externally supplied or agent-generated Lean and accept only normalized declarative circuit representations. ]]>