TypeScriptで交差型を使って静的型に状態的な型を動的に付与していきます。 これによりサニタイズ済/未サニタイズ、エンコード済/未エンコード、不変/可変、通常文脈/エラー文脈、Truthy/Falsyといった状態を複合的に扱えるようになります。 さっそく試してみましょう。
この記事はTypeScript アドベントカレンダー2015 2日目の記事です。
サニタイズ済みである文字列のみを受け取る型を作ってみます。
declare class Sanitized {
private id;
}
function sanitize<T>(data: T): Sanitized&T {
return <Sanitized&T>data; // any processing
}
var plain = '';
var secure: Sanitized&string = plain; // type error
var secure: Sanitized&string = sanitize(plain); // ok
たったこれだけです。たったこれだけで信頼境界の内側と外側を分離できるのです。もはやただの文字列は安全な文字列を要求する型に入れることができなくなりました。
見た目が通常の型宣言とよく似ているためアノテーションとしても利用できます。それでいて、この手法は型のみで実現され実装に影響を及ぼさないためまったく何のオーバーヘッドもありません。
信頼境界を越えるときに安全な文字列に変換し、境界内では安全な文字列だけ使うように制限すればプログラムが確実に安全なデータだけを使っていることが保証されるようになります。
苦労して経路を網羅しなくても受け取り側が型を見て不正なデータを拒否するので、境界内が要件を満たさない不正なデータで汚染されることはありません。
信頼境界内は常に安全なデータだけで満たされているクリーンな領域となります。
このような状態付きの型を定義する方法は他にもいくつかありますが、ここで紹介した交差型を使用した方法はその中でも汎用性が高く開発者の負担が小さいものです。今日からでも使い始められるでしょう。
上記のコードは最低限の機能しかないので、以下の条件を追加してもう少し実用的にしてみます。
- 二重に状態を付与しようとした場合はvoidとなる。
export declare class Sanitized {
private SANITIZED;
}
export function type<T>(target: Sanitized&T): void
export function type<T>(target: T): Sanitized&T
export function type<T>(target: T): Sanitized&T {
return <Sanitized&T>target;
}
export function extract<T>(target: Sanitized&T): T {
return <T>target;
}
プリミティブ型の次はデータ型にも対応できるようオブジェクトに状態を持たせてみましょう。
すいません動くコードロストして再実装できなくてロストテクノロジーになりました。以下のコード実装できた方いたら教えてください(泣)。
データ型については信頼できるデータのみを保持する信頼境界内用の公称型を用意して信頼性を確保してください。
declare class Sanitized {
private id;
}
function sanitize<T>(data: T): Sanitized&T {
return <Sanitized&T>data; // any processing
}
class Data<T> {
constructor(public value: T) {
}
public sanitize(this: Data<Sanitized>): void
public sanitize(): Data<Sanitized&T>
public sanitize(): Data<Sanitized&T> {
return new Data(sanitize(this.value));
}
}
var plain = new Data('');
var secure: Data<Sanitized&string> = plain; // type error
var secure: Data<Sanitized&string> = plain.sanitize(); // ok
var secure: Data<Sanitized&string> = plain.sanitize().sanitize(); // type error
これまでは信頼境界内の信頼性を境界通過時の検査のみで担保・依存し、ひとたび境界内に入ればあとはフリーパスになって不正なデータが混入しても検出できないという状態に甘んじていたこともありましたが、型に状態を持てるようにすることで要求される状態を持たない値が境界内で誤って使われようとしても要件を満たせず拒否される信頼性の高い領域を構築できます。
これまで境界線という線で確保していた信頼性と安全性を境界内の空間全体というより高い次元で確保できるようになったのです。より応用的には個々のデータのうち特に信頼性を求める場合は専用に公称型のデータ型を用意することでさらに確実な操作を行い、それ以外のデータは状態の要件により信頼性を確保するといったアプローチが望ましいでしょう。
今回の内容は単純な状態遷移をモデルへ部分的に適用しただけなので形式的証明と呼べるほどのものではありませんでしたが*1、実装に高水準の信頼性を与える方法として形式的証明と同様非常に効果的なものです。
外部と通信を行うアプリケーションは規模の大小にかかわらずサニタイズと正規化を厳しく要求されるため本稿で紹介したように形式的に信頼性を保証する方法が非常に重要となってきますので、これを期にぜひ自身のプロダクトの信頼性と品質の向上に取り組んでみてください。
TypeScriptアドベントカレンダー2015、需要と余裕があれば次回は状態遷移モデルの形式的証明を行う並行処理および並列処理の形式的証明（状態遷移編）です。予定は未定。
*1:形式的証明は未証明部分で破綻していては意味がないので原則として証明対象の全機能を証明します
