Formal Analysis and Supply Chain Security for Agentic AI Skills

TL;DR

This paper introduces SkillFortify, a formal analysis framework for agentic AI skill supply chains, addressing security vulnerabilities with rigorous guarantees and demonstrating high accuracy and efficiency in detection.

Contribution

The paper presents the first formal analysis framework for agent skill supply chains, including a novel attacker model, static analysis, sandboxing, dependency resolution, and a benchmark suite.

Findings

Achieves 96.95% F1 score with zero false positives on 540 skills.

SAT-based resolution handles 1,000-node graphs in under 100 ms.

Provides formal guarantees for security analysis methods.

Abstract

The rapid proliferation of agentic AI skill ecosystems -- exemplified by OpenClaw (228,000 GitHub stars) and Anthropic Agent Skills (75,600 stars) -- has introduced a critical supply chain attack surface. The ClawHavoc campaign (January-February 2026) infiltrated over 1,200 malicious skills into the OpenClaw marketplace, while MalTool catalogued 6,487 malicious tools that evade conventional detection. In response, twelve reactive security tools emerged, yet all rely on heuristic methods that provide no formal guarantees. We present SkillFortify, the first formal analysis framework for agent skill supply chains, with six contributions: (1) the DY-Skill attacker model, a Dolev-Yao adaptation to the five-phase skill lifecycle with a maximality proof; (2) a sound static analysis framework grounded in abstract interpretation; (3) capability-based sandboxing with a confinement proof; (4) an Agent Dependency Graph with SAT-based resolution and lockfile semantics; (5) a trust score algebra with formal monotonicity; and (6) SkillFortifyBench, a 540-skill benchmark. SkillFortify achieves 96.95% F1 (95% CI: [95.1%, 98.4%]) with 100% precision and 0% false positive rate on 540 skills, while SAT-based resolution handles 1,000-node graphs in under 100 ms.