静的コード解析の会#9

(会場と日程を変更しました) #静的コード解析の会 第9回 - connpass に行ってきました。今回も何らかの発表は出来ず。
どこかで宣伝したらしく、前回から人数が大幅に増えて14~5人くらいの参加者でした。

参加者の傾向としては:

  • なぜかIsabelle使いが多い。
  • モデル検査勢が(人数的に)優勢。
  • 他は各々の好みでいろいろ。

といった感じでした。

RustでマルチスレッドWebサーバを作る例を写経

Final Project: Building a Multithreaded Web Server - The Rust Programming Languageを写経した。
標準ライブラリのみを使って簡単なマルチスレッドWebサーバを書く例。
スレッドプールを作ってacceptするたびに「htmlを応答する関数」をJobとしてチャンネルで配る。

最終的にちゃんと各Workerスレッドを終了させるところまで作る。

思ったよりかなり簡単に書けてしまった印象。設計がいいからだろうか?

歯が痛くて倒れていた

8月中旬頃、突然奥歯(の中の神経)に激痛が起こりました(結局明確な原因は不明)。
2週間くらいしてようやく普通の生活が出来るようになりました。あまりに酷い状態だったので書き留めておきます。


どんな状態だったかというと:

  • 常に痛い。何もして無くても神経が痛い。でも痛くてじっとしてもいられないので家の中を徘徊し続けた。ただし歩いても痛い。詰みじゃん。
  • 食べられない。4日間くらいお茶とポカリだけで生きていた。痛い以外の感情がないからか空腹感全くは感じない。今にして思うとちょっとやばいな。
  • 痛み止めが効いている間は大体普通の生活が出来る。ただし効果は4〜5時間で切れ、かつ1日3錠までなので、任意の9時間(24 - (5 * 3))はのたうち回ることが確定。朝4時から5時間くらいうろうろし続けるのは心折れそうだった。
  • 寝られない。痛いと寝られないんですね。初めて知りました。心配しなくても起きる方も痛み止めが切れる時刻にちゃんと起きます。人体って凄いね(^q^)。


他:
症状が出たのがコミケ直後だったので、会社でコミケで調子のってぶっ倒れたヤツみたいな扱いだったのが悲しかった。
原因はよく分からないから無関係という主張も出来ないんだけど…。

terraformのチュートリアルを読んだ

terraformのチュートリアルを一通り読んで実行した。

  • チュートリアルを実行するのに必要な知識が全てチュートリアル内にあり、かなり分かりよい
  • ほぼ写経で動く(1度AWSのよく分からないエラーが出たけど)
  • 記述が古い箇所がある(動きはする)
  • その時点でのconfiguration全体に自信が持てないことがある(remote backends(最後の節)は特に)

terraformの感想

便利そう。途中でエラーが出ても(何かを修正してやり直せば)設定通りの状態にしてくれる(はずな)ので安心感がある。

静的コード解析の会#6で発表してきた

静的コード解析の会#6VeriFastによる停止性検査について発表してきました。(資料作って徹夜してしまった…)



前回も同じテーマでしたが私の理解も資料も十分でなかったため(α)としてました。
が、今回の発表では多重集合、整礎関係、実際の処理系で検査できるコードについての説明まで入れることが出来たので、これで一通りの内容を盛り込めたと思います(ただしシーケンシャルなプログラムに限る…)。
参照している論文はModular termination verificationです。


(多分)怪しげな記述や展開のよく分からないページがありますが、がんばって作ったので興味がある人は是非眺めてみて下さい。
個人的なおすすめはStatic Recursionパターンの検証方法のあたり(資料の末尾の方)です。


会場からは、

  • 処理系が(もっと)がんばれ
  • 発表の構成が悪い(直接そうは言われてないけど)

という感じの反応が得られました…orz。

感想

これまで何度かVeriFastに関する発表をしてるし、(呑みながら)議論もしてきたので聴衆の理解度が高くて非常に楽しい発表になりました。ありがとうございました。

また、懇親会でマルチスレッドの扱いについて質問がありました。通常の(部分正当性の)検査では問題無くスレッドが扱えますが、停止性検査については全く把握できていないので基本的なアイディアだけでも押さえておきたいと思っています。
参照した論文のTR版にマルチスレッドに関する議論があるようです。

SMLでSHA2アルゴリズムを実装しました

SMLでSHA2(Secure Hash Algorithm)というハッシュアルゴリズムを実装しました。
https://github.com/eldesh/sha2_sml.gitに公開してあります。現在のところSML/NJで動作を確認しています。
#こういう基本的な部品から実装して行くのが重要です。たぶん。

実装内容

RFC6234を実装しました。

SHA224 SHA256 SHA384 SHA512 SHA512/224 SHA512/256
実装


SHA224,SHA256,SHA384,SHA512を実装してあります。他にSHA-512/224とSHA-512/256というのがありますがこちらは未実装です。
また入力として文字列とバイト(Word8.word)列しか受け取れず、(8の倍数で無い)ビットの列は入力できません。

インストール方法

readme.rstに書いてあります。
各コマンドの詳細を知りたい方は先日のエントリ(SMLUnitのインストールを通してSML/NJ向けのライブラリのインストール方法を解説する)を参照して下さい :)

使用例

インストールが出来たとして、使用する様子を紹介します。

sha2_sml$ sml
- CM.make "libsha2sml.cm";
(* ... snip ... *)
val it = true : bool
- Sha256.hashString "abc";
val it = - : ?.Sha256.word Sha256.t
- Sha256.toString it;
val it = "BA7816BF8F01CFEA414140DE5DAE2223B00361A396177A9CB410FF61F20015AD"
  : string

念のためsha256sumコマンドで確認します。

$ echo -n "abc" | sha256sum | tr [:lower:] [:upper:]
BA7816BF8F01CFEA414140DE5DAE2223B00361A396177A9CB410FF61F20015AD  -

やりました。

テスト

NISTのCAVPのshort/longのケース全て。それに加えてNESSIE*1のテストベクタの一部を使っています。*2

全部パスしてるので、まぁ大体正しく実装出来てるんでしょう。きっと。
あとは処理系的に入力サイズが大きいとき不安。4GB超えた辺りとか。

まとめ

実装に思いの外時間がかかりました。ダメですね。RFCは分かりづらいような気もする

超重要なアルゴリズムなんですがRFCの日本語訳が見つからなかったのが意外でした。あと、NISTのサイトにもSHA2の定義はあるんですが、RFCの方が大分冗長ですね。

*1:ネッシー

*2:NESSIEさん、テストベクタのこのフォーマットはちょっと酷いんじゃ無いですかね…