Diary?

(23:33)

Caty は何度か書いてるとおりデフォルトで HTML 特殊文字のエスケープを行うのだが、流石にもうそれを余計なお世話とか言い出すダメエンジニアに関しては「死ね」と返していいよな。そもそも今後の予定として、セッションやファイルなどにデータを書き込む処理を検出してある種の脆弱性（例えば CSRF など）への対策を示唆するメッセージと手法を表示するとか、そういうのも考えているんだが。 Caty スクリプトで使われるコマンドはすべて独自の型宣言を持っており、ファイルなどへの書き込みを行うかどうかをその宣言から判断できるので、そういった処理の作成者にユーザ認証やトークンチェックをするようアドバイスするのは十分可能なはずだ。

これは汎用的に使えるセキュリティ対策コマンド群（セッション ID の埋め込みコマンドと Cookie の値との照合コマンド）を用意すれば割と実用的になりそうだ。あとセッション ID の埋め込みと照合コマンドを使えば、 CSRF などに関してはスクリプトの入力の型からパイプライン全体がセキュアかどうか判断できる。

実際には次のような使い方になるんじゃなかろうか。

//入力フォームの出力
some_command | print form.html | add_session_id
 
//入力を受け取る側
translate SomeInputType & SessionToken | when {
    OK => check_token  | when {
        OK => //以降はファイルなどへの書き込み処理
        NG => //未ログインとみなしてログインページにリダイレクトとか、まあ適宜適切な処理を
    },
    NG => //入力エラー処理
}

SessionToken は例えばこんな型。

type SessionToken = object {
    "sessionID": string
};

この時 check_token の型は SomeInputType & SessionToken -> @OK SomeInputType | @NG ErrorInfo に推論できる。あるいは translate 自体にチェック機構を入れてしまってもいいかもしれない。まあこのあたりのやり方はいろいろあるので、一番ユーザの負担にならなそうなやり方を模索するか。あと俺が実装を頑張って translate も型推論させれば、次のようになる。

translate | when {
    OK => check_token | when {
        OK => //以降はファイルなどへの書き込み処理
        NG => //未ログインとみなしてログインページにリダイレクトとか、まあ適宜適切な処理を
    },
    NG => //入力エラー処理
}

この時推論の一部の流れを切り取ると、

1. 2番目の when 節の入力型が @OK X | @NG ErrorInfo となる。ここで X は正常処理の型とする
2. check_token の型は _T & SessionToken -> @OK _T | @NG ErrorInfo で、 _T が X となる
3. translate の型は WebInput -> X & SessionToken に推論される

って感じかなあ。まあどこまでやるか、そもそも本当にできるか、できたとして穴は無いか、穴がある場合にどのような対策をユーザに取ってもらうかなど、考えるべき事は腐るほどあるんだが。