SkillFortify: Formal Security Scanning for AI Agent Skills and Plugins

§1 TL;DR #

SkillFortify provides the first formal analysis framework for agent skill supply chains: Dolev–Yao attacker model adapted to the 5-phase skill lifecycle, sound static analysis via abstract interpretation over a 4-element capability lattice, SAT-based dependency resolution with capability bounds, and a trust score algebra — achieving 96.95% F1 with 0% FPR on 540 skills.

§2 Q1 / Q2 / Q3 #

Q1 痛点 #

Agent skill ecosystems (OpenClaw 228K stars, Anthropic Agent Skills 75.6K stars) face a supply-chain crisis: ClawHavoc infiltrated 1,200+ malicious skills, MalTool catalogued 6,487 malicious tools, 26.1% of 42,447 scanned skills have vulnerabilities. All 12 existing defense tools (Snyk, Cisco, ToolShield) are heuristic — they detect known patterns but cannot prove absence of malicious behavior. Cisco explicitly warns "no findings does not mean no risk."

• Task class: supply-chain security for agent skill ecosystems (static analysis, not runtime).
• Interaction: CI/CD integration, pre-deployment scanning.
• Autonomy: automated analysis tool, no agent runtime involvement.

Q2 方法 #

Six formal contributions forming a layered defense:

1. DY-Skill attacker model (§3): Adapts Dolev–Yao with 6 operations (intercept, inject, modify, drop, forge-skills, compromise-registries) over the 5-phase skill lifecycle (Install → Load → Configure → Execute → Persist). Maximality theorem (Theorem 3.6): any defense secure against DY-Skill is secure against all symbolic attackers.
1. Sound static analysis (§4): Abstract interpretation over the 4-element capability lattice $(\{\mathsf{NONE}, \mathsf{READ}, \mathsf{WRITE}, \mathsf{ADMIN}\}, \sqsubseteq)$ across 8 resource types. Galois connection ensures soundness: $\mathit{Viol}(s) = \emptyset \Rightarrow$ no concrete execution exceeds declared capabilities (Theorem 4.9).
1. Capability-based sandboxing (§5): Object-capability discipline with transitive attenuation — authority can only decrease along delegation chains. Static confinement theorem (5.6) via structural induction.
1. Agent Dependency Graph (§6): $\mathit{ADG} = (\mathcal{S}, V, D, C, \mathit{Cap})$ extending classical package resolution with per-version capability constraints. SAT encoding adds clause family (C5): $\neg x_{s,v}$ for capability-violating versions. Resolution soundness (Theorem 6.10): SAT satisfiability ↔ secure installation existence.
1. Trust score algebra (§7): Four signals $(T_p, T_b, T_c, T_h)$ with multiplicative propagation $a \otimes b = a \cdot b$, exponential decay $T(s,t) = T_0 \cdot e^{-\lambda(t - t_{\text{last}})}$, and SLSA-inspired graduated levels (L0–L3). Monotonicity theorem (7.12): improvement never decreases trust.
1. SkillFortifyBench: 540 skills (270 malicious, 270 benign), 13 attack types, 3 formats.

核心技术壁垒: The soundness guarantee via abstract interpretation (Theorem 4.9) — if SkillFortify reports no violations, there are no violations in any concrete execution. This is qualitatively different from heuristic scanning and provides the same class of guarantee as Astrée for A380 flight software.

Q3 结果 #

Metric	Value
Detection F1	96.95% (95% CI: [95.1%, 98.4%])
Precision	100% (0 FP across 270 benign)
Recall	94.07% (254/270 malicious)
FP rate	0.00% (95% CI: [0.0%, 1.4%])
1K-skill SAT resolution	92.4 ms
540-skill end-to-end scan	1.378 s
Trust monotonicity	100% (200/200 data points)
Lockfile determinism	100% (10/10 configs)
FN concentration	A11 typosquatting (50%), A12 dependency confusion (0%)

§3 架构 / 方法图 #

flowchart TD subgraph Engines SA[Static Analyzer
Abstract Interpretation
4-element capability lattice] DR[Dependency Resolver
SAT-based ADG
Lockfile generation] TE[Trust Engine
4-signal scoring
Exponential decay] end TKB[Threat Knowledge Base
DY-Skill taxonomy
Pattern signatures] --> SA TKB --> DR TKB --> TE SA -->|Cap_I, findings| CLI DR -->|Secure installation, lockfile| CLI TE -->|Trust scores, levels| CLI CLI -->|SARIF/JSON/terminal| Output

Three engines share a Threat Knowledge Base. The Static Analyzer performs three-phase analysis: (1) capability inference via abstract interpretation, (2) dangerous pattern detection, (3) capability violation check $\mathit{Cap}_I(s) \sqsubseteq \mathit{Cap}_D(s)$.

§4 作者证明 #

Check	Status	Location
DY-Skill maximality (Theorem 3.6)	Proven via simulation construction	§3.4, Appendix A.1
Analysis soundness (Theorem 4.9)	Proven via Galois connection + structural induction	§4.4, Appendix A.2
Capability confinement (Theorem 5.6)	Proven via structural induction on code syntax	§5.4, Appendix A.3
Resolution soundness (Theorem 6.10)	Proven via bidirectional equisatisfiability	§6.8, Appendix A.4
Trust monotonicity (Theorem 7.12)	Proven by direct computation	§7.5, Appendix A.5
Runtime confinement (Theorem 5.7)	Design theorem — no implementation	§5.4

All five main theorems have complete formal proofs in the appendix. Trust decay half-life inconsistency: §7.3 states $\lambda = 0.01$ (half-life 69 days), but §9.6 uses $\lambda = 0.005$ (half-life 139 days).

§5 实验与数据 #

E1 Detection Accuracy (Table 4–6): 100% detection on 9 of 13 attack types. Weaknesses: A11 typosquatting (50% — requires external corpus), A12 dependency confusion (0% — fundamentally relational). MCP format recall lower (82.22%) vs Claude/OpenClaw (100%) due to compact configs.

E3 Combined Analysis (Table 7): Pattern matching detects 246/270; information flow adds 8 more (steganographic multi-step exfiltration A7). No skill caught by info flow alone.

E4 Scalability (Table 8): Sub-linear per-skill cost. 1,000 skills in 92.4 ms; enterprise deployments (200–500 skills) under 30 ms.

E5 Trust Properties: Monotonicity verified on 200 data points without exception. Weight sensitivity CV = 0.18. Active skills maintain $T > 0.70$ over 180 days; abandoned skills decay to 0.31 at 180 days.

E7 End-to-End (Table 9): Full scan of 540 skills in 1.378 seconds. Suitable for pre-commit hooks (<100 ms), CI/CD, and IDE integration.

§6 论证链 #

Step	Claim	Evidence	Depends on
1	Agent skill supply chain has a structural security gap with no formal defenses	ClawHavoc (1,200+ skills), CVE-2026-25253, MalTool (6,487 tools)	—
2	DY-Skill is maximally powerful among symbolic attackers	Theorem 3.6 (simulation proof following Cervesato 2001)	Step 1
3	Sound static analysis proves absence of capability violations	Theorem 4.9 (Galois connection + fixpoint)	Step 2
4	Capability confinement prevents escalation along delegation chains	Theorem 5.6 (structural induction)	Step 3
5	SAT-based resolution produces provably secure installations	Theorem 6.10 (equisatisfiability)	Steps 3, 4
6	Trust algebra incentivizes improvement (monotonicity)	Theorem 7.12 (direct computation)	Step 5
7	Combined system achieves 96.95% F1 with 0% FPR	E1–E7 on SkillFortifyBench (540 skills)	Steps 2–6

§7 实现 cross-reference #

2,567 lines of Python, 44 source files, 473 automated tests (including Hypothesis property-based tests). MIT license. pip install skillfortify. GitHub: https://github.com/varun369/skillfortify.

关键实现细节:

1. Typosquatting and dependency confusion are architectural blind spots — A11 (50%) and A12 (0%) detection rates are inherent limitations of local static analysis. These require external registry comparison (Levenshtein distance, namespace verification) planned for future work.
2. Runtime confinement (Theorem 5.7) is a design theorem with no current implementation — the static analysis (Theorems 4.9, 5.6) provides current defense; runtime sandbox enforcement is specified but not built.