Great writeup. Though combined with the lack of lockfiles for transitive actions, relying purely on static analysis is tough. Linter like zizmor are great, but they struggle with deep composite actions trees and runtime template injection.

I got frustrated with the lack of security to started working myself on an open-source runtime sandbox for GHA: https://github.com/electricapp/hasp

The first check was inspired by the trivy attack. hasp enforces SHA pinning AND checks that a comment (# v4.1.2) actaully resolves to its preceding SHA. That grew into a larger suite of checks.

Instead of just statically parsing YAML it hooks into the runner env itself. Some of its runtime checks mirror what zizmor already does including resolving upstream SHAs to canonical branches (no impostor commits) and traversing the transitive dependency tree. I have a PR up with a comparison document here (hasp vs. zizmor): https://github.com/electricapp/hasp/pull/13/changes#diff-aab...

Furthermore, it sandboxes itself to prevent sensitive exfiltration by acting as a token broker which injects the secret at runtime -- the GH token can only ever be used to call the GH API. It uses landlock, seccomp, and eBPF via Rust, so no docker. The token broker sandbox can also be used to wrap a generic executable giving hasp generic applicability beyond GHA context (i.e. agentic or other contexts, where token runtime injection seems quite in vogue)

I'm using this as a stopgap until GH rolls out some of the features on its roadmap. I'm moving torward treating the runner as a zero-trust or actively malicious environment, so this was my small contribution on that front.