VerifiableAuthPlatformとは
VerifiableAuthPlatform は、パスワード認証の動きを、仕様、実装、テスト、ログで確認できるようにするポートフォリオです。パスワード認証では、ログインIDとパスワードを使って本人かどうかを確認します。
「ログイン成功」「パスワード間違い」「アカウントのロック」「ログアウト」のような認証という機能は、画面だけ見ても正しいかどうかを判断しにくい領域です。たとえば、ログインに失敗したとき、ただ「失敗」と表示するだけでは、失敗回数が増えたのか、ロックされたのか、ログに残ったのかが分かりません。VerifiableAuthPlatform は、そのような見えにくい動きを、仕様と実行結果の両方から確認できるようにする技術実証です。
画面構成
掲載している画面は、TUI と監査ログ・メトリクスの確認画面です。TUI は Terminal User Interface の略で、ターミナル上で操作する画面のことです。
この画面では、Cエンジンを操作し、登録、ログイン、パスワード変更、ログアウトなどの動きを確認します。Cエンジンとは、C言語で作った中核処理のことです。
TUI は、認証の動作を手で試すための入口です。利用者は、ユーザー登録、ログイン、ログアウト、パスワード変更のような操作を選びます。ただし、TUI 自体が認証ルールを判断するわけではありません。TUI は操作を受け取り、Cエンジンへ渡し、返ってきた結果を表示します。
監査ログでは、「いつ」「どの操作が」「どの結果になったか」を確認します。メトリクスでは、全体として失敗が増えていないか、ロックアウトが何回起きたか、成功と失敗の傾向がどうなっているかを確認します。
技術構成
VerifiableAuthPlatform は、役割ごとに4つの層に分かれています。認証処理では、画面、ルール、実行処理、確認手段が混ざると、どこで間違いが起きたのか分かりにくくなります。そのため、役割を分けて確認できる構成にしています。
主な技術構成は次のとおりです。
- Lean: 仕様を数学的に書いて確認するための言語です。ここでは、認証のルールや不変条件を書いています。なお、不変条件とは、処理の前後で必ず守られてほしい条件です。
- Cエンジン: 実際に認証処理を動かす中核部分です。ユーザー登録、ログイン、ログアウト、パスワード変更などを扱います。
- JSON CLI: JSON形式で結果を返すコマンド操作口です。
- Go TUI: ターミナル上で操作するための画面です。
- observability: 観測可能性のことです。観測可能性とは、ログや数値を通じて、内部で何が起きたかをあとから確認できる性質です。
- E2Eテスト: End to End test です。利用者の操作に近い流れで、最初から最後まで正しく動くかをテストします。
処理の流れは、次のようになります。
Leanで認証ルールと不変条件を書く
↓
Cエンジンで同じ動きを実装する
↓
JSON CLIで実行結果を決まった形式にする
↓
Go TUIで操作しやすい画面を作る
↓
監査ログで操作履歴を残す
↓
メトリクスで成功・失敗・ロックアウトを数値化する
↓
E2Eテストで一連の動きを確認するこの流れで重要なのは、仕様と実装を別々に置くだけで終わらせないことです。Lean で書いたルールが、Cエンジンの動き、JSON CLI の出力、TUI の表示、テストの期待値と対応するようにしています。対応が追えると、あとから仕様を変えたときに、どの実装やテストを見直すべきか分かりやすくなります。
また、JSON CLI を間に置くことで、TUI とテストが同じ形式の結果を読めるようになります。画面だけのために特別な形式を作ると、テストと画面の見ている情報がずれる可能性があります。JSON という共通の形式にすることで、確認の入口をそろえています。
設計上の決定事項
1つ目の決定は、Lean で仕様を書くことです。Lean は、プログラムと数学的な証明を近い形で扱える言語です。ここでは、ログインIDが重複しないこと、ロックされたユーザーはログインできないこと、ログアウトではユーザー一覧を変えないことなどを確認します。
2つ目の決定は、Cエンジンを認証処理の中心にすることです。ここでは、固定長配列、パスワードハッシュ、salt などを扱います。固定長配列とは、あらかじめ大きさが決まっているデータの入れ物です。パスワードハッシュとは、パスワードをそのまま保存せず、復元しにくい形に変換した値です。salt とは、同じパスワードでも同じハッシュになりにくくするために加える値です。
3つ目の決定は、Go TUI に認証ルールを重複して書かないことです。TUI は Cエンジンの結果を操作・表示する役割にします。これにより、画面側では成功扱いなのに、エンジン側では失敗扱いになるようなずれを減らしています。
4つ目の決定は、JSON CLI を公開境界にすることです。公開境界とは、外部の部品がどの形で結果を受け取るかを決める境目です。結果を JSON で返すことで、TUI、テスト、ログ確認が同じ結果を読みやすくなります。
5つ目の決定は、仕様と実装の対応表を持つことです。対応表とは、「Lean ではこのルール、Cではこの処理、テストではこの確認」という関係を確認する文書です。これにより、仕様だけ、実装だけ、テストだけが独立してしまうことを防ぎます。
6つ目の決定は、監査ログとメトリクスを最初から設計に含めることです。認証処理では、動いたかどうかだけではなく、あとから説明できることが重要です。失敗回数が増えた理由、ロックアウトが起きたタイミング、想定外の操作がなかったかを確認できるようにしています。
現時点の位置づけ
現時点では、Lean 仕様、Cエンジン、Go TUI、JSON CLI、監査ログ、メトリクス、E2Eテストをつなげて確認できる状態です。
これは本番利用できる完成済みの認証基盤ではありません。仕様、実装、テスト、観測可能性を対応づけて、認証処理を検証しやすくするための技術実証です。そのため、作り方や考え方が成立するかを実証することが目的です。
公開用の説明では、認証の正しさを「画面が動くか」だけで見せるのではなく、「ルールがあり、そのルールに沿った実装があり、実行結果をログとテストで確認できる」という構成を見せることを重視しています。
Github
ソースコードは GitHub で公開しています。GitHub は、ソースコードや開発履歴を公開・管理できるサービスです。