SkillFortify: Formal Analysis and Supply Chain Security for Agentic AI Skills

Abstract

The rapid proliferation of agentic AI skill ecosystems—exemplified by OpenClaw (228,000 GitHub stars as of February 2026) and Anthropic Agent Skills (75,600 stars at the same date)—has introduced a critical supply chain attack surface. The ClawHavoc campaign (January–February 2026) published hundreds of malicious skills to the OpenClaw marketplace, while MalTool synthesised 1,300 standalone malicious tools and 5,727 tools with embedded malicious behaviour that evade conventional detection. In response, a dozen reactive security tools emerged, yet the ones we surveyed rely on heuristic methods that provide no formal guarantees. We present SkillFortify, a 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) a capability model with a static confinement proof, and a runtime enforcement design; (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.15% F1 with 100% precision and a 0% false positive rate on this 540-skill benchmark, while SAT-based resolution handles 1,000-node graphs in a median 27 ms. We also report a negative result: information flow analysis detects no skill that pattern matching alone does not, so on this corpus its contribution to coverage is zero. Tool: pip install skillfortify | Code: https://github.com/qualixar/skillfortify Preprint: arXiv:2603.00195 --- Version 2.0 changes --- Corrects the bibliography: 22 entries in v1 carried author lists that did not match the papers at the cited arXiv identifiers. All verified against the arXiv API and corrected; affected authors notified. Corrects three external claims against primary sources: - MalTool reports 1,300 standalone and 5,727 embedded malicious tools, not 6,487. - CVE-2026-25253 is authentication-token exfiltration via an unvalidated gatewayUrl, credited to depthfirst and fixed in 2026.1.29 on 30 January 2026 — not remote code execution through a crafted skill package on 27 January. - ClawHavoc counts are 341, later 824, and 1,184 depending on source and date, not "over 1,200". Re-measures all experiments against the released v0.6.0 implementation using harnesses now committed to the repository, which record each measurement with the machine it was taken on. Detection accuracy is unchanged (F1 96.15%, precision 100%, recall 92.59%). E3 reverses to a negative result: information flow analysis adds no detections over pattern matching on this corpus. States the soundness theorem's scope explicitly, no longer conflating it with the zero false-positive rate, which is an empirical result on this benchmark. Softens priority claims where prior work was not exhaustively surveyed.