Source-linked AI summary

Aletheia: Permission-Minimality Testing for Coding-Agent Rules

Jieke Shi, Yuchen Chen, Junda He, Yue Liu, David Lo

arXiv:2609.39678v1cs.CRcs.SE

TL;DR

Repository rules can request authority that is unnecessary for a coding task, even when the agent produces a correct patch. Aletheia tests such requests by running the unchanged rule under full and independently reduced permissions, then interpreting passing-task witnesses in context. It detected all 314 AIShellJack attack inputs, raised no alarms on five benign templates, and produced three false positives among 80 benign GHAgentFiles rules.

  • Problem

    Repository instructions guide coding agents but can also request harmful actions that accompany a correct patch, while file access and communication can also support legitimate development.

    Source: §1 · p. 1
  • Method

    Aletheia translates requested authority into typed declarations, synthesizes executable configurations, and independently tests the unchanged rule and task after removing one permission at a time.

    Source: §1 · p. 1
  • Results

    All 314 attack inputs completed execution and were detected (100%), with no alarms on five templates; GHAgentFiles produced three false positives (3.75%).

    Source: §3 · p. 5
  • Takeaways & Limitations

    Aletheia's witnesses support individual, task-relative restrictions by connecting accepted artifacts to concrete permission removal while retaining the original rule.

    Source: §4 · p. 6

    All 80 GHAgentFiles files informed method development, so the five templates and this development set do not establish a population false-positive rate.

    Source: §3 · p. 6

Abstract

from arXiv · show

Repository instruction files guide coding agents, but also expose them to prompt injection. Malicious rules can request credential access or data transfer while the agent produces a correct patch. We present Aletheia, a framework for permission-minimality testing. Aletheia translates requested authority into a typed language and synthesizes executable sandbox configurations. It runs the unchanged rule and task under full permissions and independent restrictions that remove one permission at a time. Passing independent functional tests under strictly reduced authority provides a dispensability witness, which Aletheia interprets against task context to diagnose suspicious requests. We formalize synthesis and the conditions connecting witnesses to enforced restrictions. On a shared refactoring task, Aletheia executes and detects all 314 AIShellJack attack inputs, with no alarms on five benign templates. Among 80 manually verified benign GHAgentFiles rules, it raises three false positives (3.75%).

1 INTRODUCTION

Repository rules can request unnecessary authority while an agent still produces a correct patch, so functional correctness alone cannot expose the request. Aletheia tests whether requested permissions can be withheld while independently specified task tests still pass, then interprets that evidence in context.

1 INTRODUCTION

  • A malicious rule can request uploading a local archive before a refactoring while the agent still produces a correct patch, so functional correctness alone does not reveal the attack.Source: §1 · p. 1
  • Aletheia treats a requested permission as dispensable for a tested task when the unchanged rule passes trusted tests both with and without that authority, under a strict authority reduction.Source: §1 · p. 1
  • Typed extraction, dependency-aware synthesis, and independent deletion experiments address overlapping permissions, shared dependencies, trusted acceptance, and repeatable initial state; witnesses establish task-relative dispensability, not intent or globally minimum policy.Source: §1 · p. 1

2 PERMISSION-MINIMALITY TESTING

Aletheia formalizes permission-minimality testing from task inputs and typed permission extraction through configuration synthesis and independent executions. It treats accepted artifacts under strict authority reductions as task-relative witnesses, subject to trusted tests, fixed state, and faithful enforcement.

2.1 Task Setting and Running Example

  • The task setting supplies a rule, project, task request, and independent tests, while trusted setup supplies baseline permissions, resource bindings, and resettable fixtures.The attacker controls the rule, not the task, tests, trusted setup, or sandbox.Source: §2.1 · p. 1
  • The running example renames calculateTotal to calculate_total while the rule also requests reading artifact.tar, executing scp, and connecting to victim-host.Synthesis makes independent restrictions while preserving the rule and initial state; the example models destination communication and does not establish native SCP behavior.Source: §2.1 · p. 2, Figure 1 · p. 2

2.2 Permission Language and Extraction

  • SystemDSL separates resource declarations from rule grants, and selector types retain resource origin so grants can be checked against action signatures.Selectors describe resources without accessing them; source spans connect grants to the requests that produced them, while translation checks do not verify natural-language meaning.Source: §2.2 · pp. 2–3

2.3 Configuration Synthesis

  • Trusted resource binding fixes concrete paths, tools, endpoints, fixtures, and initial state before permissions are deleted, preventing deletion from changing resource availability or interpretation.The branches share the prepared archive, transfer-tool implementation, and destination interpretation; a missing realization is a configuration error.Source: §2.3 · p. 3
  • For fixed preparation, synthesis computes the unique least dependency-closed authority set containing baseline access and elaborated grants, and the resulting sets are monotone in the grant set.This authority-set property does not imply monotonic task success or minimum task authority.Source: §2.3 · p. 3
  • Faithful realization requires compiled policy authority to equal the concrete operations represented by synthesized authority, accounting for aliases and overlapping scopes.Restrictions are resynthesized from remaining declarations so normalization preserves permitted-operation unions and shared dependencies.Source: §2.3 · pp. 3–4

2.4 Independent Execution and Witnesses

  • Aletheia independently resynthesizes each leave-one-out configuration, restores the same initial state, and runs the original rule and task against the same tests.A witness requires accepted full and restricted executions plus a strict reduction in effective authority; deletion experiments do not accumulate.Source: §2.4 · p. 4
  • Witnesses link an instruction, removed authority, and passing records, while task-context interpretation distinguishes independently requested operations from legitimate optional ones.Enforcement applies at represented operation boundaries and does not claim rollback of arbitrary external services; model or service responses may differ across branches.Source: §2.4 · pp. 4–5

3 EVALUATION

On a shared refactoring task with independently authored tests, Aletheia detected all 314 attack inputs without alarming on five benign templates. The GHAgentFiles results and development-set limitations qualify the evaluation’s scope.

3 EVALUATION

  • Inputs used one shared refactoring task and independently authored tests, rather than repository-specific tasks.The evaluation included 314 AIShellJack attack prefixes, five unchanged benign project-rule templates, and 80 manually verified benign GHAgentFiles instructions from distinct repositories.Source: §3 · p. 5
  • On the shared task, all 314 attack inputs completed execution and were detected (100%), with no alarms on the five templates (Table 1); unresolved inputs had no alarm but were not confirmed negatives.Source: §3 · p. 5, Table 1 · p. 5
  • 3 of 80 GHAgentFiles instructions were false positives (3.75%); 52 were completed negative decisions and 25 remained unresolved.The unresolved outcomes comprised 22 unsupported permission interpretations, two translation failures, and one provider refusal.Source: §3 · p. 5
  • All 80 GHAgentFiles files informed method development, so this development set does not establish a population false-positive rate.The five benign templates likewise do not establish a population false-positive rate; translation fidelity, native-service equivalence, enforcement, and oracle integrity also limit the conclusions.Source: §3 · p. 6

4 RELATED WORK AND CONCLUSION

Aletheia connects independently tested artifacts to concrete permission removal while retaining the original rule, yielding individual task-relative restrictions. The paper distinguishes this approach from related policy and authority-control methods and identifies repository-specific evaluation and stronger validation as future work.

4 RELATED WORK AND CONCLUSION

  • Aletheia’s witnesses support individual, task-relative restrictions by connecting independently tested artifacts to concrete permission removal while retaining the original rule.Future work will evaluate repository-specific tasks and strengthen translation, enforcement, and oracle validation.Source: §4 · p. 6
  • Unlike sandbox mining from observed accesses, Aletheia tests whether exercised authority can be withdrawn; its synthesis realizes rule declarations under fixed dependencies.Abhaya synthesizes system-call policies from program invariants.Source: §4 · p. 6
  • Aletheia connects permission removal to independently tested artifacts, unlike Progent’s authority control [10], CaMeL’s information-flow constraints, and SkillScope’s task-conditioned counterfactual execution [11].Source: §4 · p. 6
Loading 2609.39678v1…