wirespec型安全なプロトコル記述言語

ワイヤフォーマット・ステートマシン・コーデックを一つのDSLで定義し、安全なC/Rustパーサーを生成。TLA+でプロトコルを検証。

安全なプロトコル定義

バイナリプロトコルの構造を宣言的に記述するだけで、バッファオーバーリードやエンディアンミスのない安全なパーサー/シリアライザーが生成されます。

従来は数百行の C コードを手書きしていたプロトコル処理を、数十行の .wspec 定義に置き換えます。

1 つの定義から C11・Rust のコードを生成。バックエンド追加で新しいターゲット言語にも対応可能。

QUIC、TLS 1.3、MQTT、BLE、IPv4、TCP — 実際のプロトコル仕様を wirespec で記述し、生成コードのラウンドトリップテストで正確性を確認しています。

TLA+ モデル検査でプロトコルのステートマシンを検証。デッドロック、活性違反、ガード競合をコンパイル時に検出。

ASN.1 エンコーディングされたフィールドを埋め込み、rasn による自動デコード/エンコードに対応。UPER、BER、DER、APER、OER、COER をサポート。