日々の流転

λ. Cryptol, the language of cryptography

[Haskell-cafe] ANNOUNCE: Cryptol now freely available

Cryptol is a domain specific language for the design, implementation and verification of cryptographic algorithms, developed over the past decade by Galois for the United States National Security Agency. It has been used successfully in a number of projects, and is also in use at Rockwell Collins, Inc. Cryptol is implemented in Haskell.

Cryptolは暗号アルゴリズムの設計・実装・検証に用いるためのHaskell風DSLだとか。面白そう。

ビット列や行列等の操作が便利に行えるようになっているようだ。 それらを扱うための型があり、例えば8bitが2つ並んだものが3つ並んでいるという型は [3][2][8]Bit となる(最後のBitは省略可能)。 型の中に現れるサイズには定義済みの変数も使えるようだ。

以下は列の総和を計算する関数の例。 並列内包表記(ParallelListComp)を使ったHaskellとほぼ同じなのが分かる。

sum xs = last ys
  where
    ys = [0] # [| x + y || x <- xs || y <- ys |];

ホワイトペーパーにC言語が低レベル過ぎる例として載っていた以下の点はなるほどと思った。確かに暗号アルゴリズムを考えるときに、そういった細部は気にしたくはないものだ。

The code that implements 4-bit vectors will be radically different from the code that implements 48-bit vectors, and is usually forced to be highly dependent on conditional compilation constructs or awkward preprocessor macros.