これは何ですか？
SPECA は、書かれたコードが「仕様どおりに動いているか」を自動で確認するツールです。
従来のコード診断ツールとの違い
静的解析やリンター (eslint など) は「コードの書き方のルール」をチェックします。「変数の型は正しいか」「使っていない変数がないか」といった類です。これらは便利ですが、「仕様で定められた振る舞い」までは検証しません。
SPECA は逆方向から考えます。まず仕様書を読んで「ここでこういう処理が必要」と判定し、実装されているコードと照らし合わせて「ズレ」を探します。コードの見た目ではなく、仕様が要求することを出発点にする点が異なります。
仕様を基点とする発想
たとえば、あるシステムの仕様に「ユーザー認証の後にのみ、機密データへのアクセスを許可する」と書かれていたとします。SPECA は以下の手順で確認します。
- 仕様を読んで「これは重要なセキュリティ要件だ」と認識する
- コードのどこがこの要件を実装しているかを探す
- すべての実行経路で「認証 → データアクセス」の順が守られているか証明してみる
- 証明できない部分 (穴) があれば、それを脆弱性の候補として報告する
想定ユーザー
- セキュリティ監査を担当している: 仕様書とコードを手作業で突き合わせる手間を減らしたい
- バグバウンティに参加している: 大規模なコードベースから実装の穴を効率よく見つけたい
- 自分たちの開発品質を確かめたい: 要件どおりに実装されているか定期的に確認したい
次のステップ
仕組みをもう少し詳しく知りたい場合は、「どうやって動く？」へ進んでください。