静的コード解析とこの勉強会について

静的コード解析をご存知でしょうか。静的コード解析とは、コンピュータのソフトウェアの解析手法の一種で、ソフトウェアを実行することなく解析を行うことです。このような手法には以下のように様々な実装があります:

• ATS, B-Method, CBMC, Coq, Coverity Scan, CSP, Dafny, F*, Frama-C, FreeSafeTy, Infer, Isabelle, SATABS, Spin, Uppaal, VDM, VeriFast, Why3, boogie, cogent, corral, seL4, vcc, その他

しかしこれらの手法は特性が異なります。メモリの安全性しか検査できないものや、実行バイナリを数学的に証明できるものまで幅があるのです。実際の製品に応用する際には「どの手法が製品のどの部分に適しているのか」知っておく必要があります。

また、実際の製品の安全性は単に設計すれば済む問題ではありません。お客様が製品を入手する際に、その製品はどのような検証をなされていて、どの程度の安全性なのか納得していただいた上で、安心して使用していただかねばなりません。そのためにはこれらの手法をわかりやすく初学者に解説できる必要があるのです。

この勉強会は上記のような静的コード解析についての意見交換を目的としています。

発表スタイルと発表者の募集

この勉強会では発表者を毎回募集しています。基本的に発表者は「自分の話したい内容」を「自分の話したい形式」で「自分の意図したレベル」にて発表できます。無理に高度な話をする必要もありませんし、無理に初心者にわかりやすくする必要もありません。

ただし、初心者はわからないところを(ある程度)質問できるものとします。おそらく初学者からは、この勉強会で発表者が宇宙語を話しているように見えるでしょう。ただし、主催者はあまりにも初歩的な質問内容であった場合には任意のタイミングでその質問を打ち切ることができることとします。

発表者は可能であれば当日の発表資料を後日公開してください。勉強会に参加できなかった方々にも知見を共有したいためです。公にしたくない内容を発表する発表者は、事前にその旨を主催者に申告してください。

持ち物

• Windows/MacOS/LinuxいずれかのOSがインストールされ、無線LANに接続可能なノートPC

当日の内容

仮ですが、以下のようなスケジュールを想定しています。

• 12:45 ビル1階のサンクス飲食スペースに集合してください
• 13:00-14:00 「自己紹介と今日話せるネタ出し」 by 全員

せっかく勉強会に集まったので、交流を深めるために自己紹介をしましょう。持ち時間は一人5分以内です。またもし勉強会当日に話せるネタがある場合には「XXXの発表をしたいです」と発言してください。予定を調整します。主催者が発表ネタを作るのに苦しくなってきたので新しいネタを供給していただけると嬉しいです!

## 自己紹介

### @masterq

セキュアOSを作ってました(過去形)
元NetBSD組み込み屋さん
同人誌を書きました

### @ftake

C言語=>SPIN
LLVMさわってた
変更範囲の分析をやったりしている
opensuseのサミットが1ヶ月後にあるよ!準備が大変だよ!
LTはまだ募集してます。
みんな来てね!

### @tohdo

形式手法の学会にいってるよ
Why3を使ってる

### @dooriver

Haskellを最近真面目に使ってる
Standard MLが好きだったのだが。。。
Haskellはライブラリが充実してていいね!
ネタ: callgrindの入門(20分)

### @hanetsuki_y

元RTL設計屋さん
C言語でファームウェア開発が今
VRやってるよ!
adlintを使ってた
Coverityを使おうと思ったが予算が通らなかった。。。
spyglassを使ってHDLを検証してた。でも高い。。。
ネタ: HDLの検証(皆興味ある？)

### @mimura1133

セキュリティ屋さんだよ!
CTF本の著者の1人だよ!
Windowsのカーネルモードドライバをアルバイトで書いてた
x86アセンブラも読めるよ!浮動小数点も脳内実行できるよ!

### @khibino

職業Haskellプログラマ
関数型言語から定理証明に興味が
Coqにも興味が
静的解析はあまり。。。
HRRというDSLを作っていて、Haskell DSLがSQLに変換されるよ。ある程度安全になるよ!

### くぼあき

モデリングツールを支援している
なかなか買ってくれないお。。。
皆使ってほしい!
元は複合機とかも作ってたよ
解析/数学はあまりつっこまないで
今日は会場係りだよ

### @y_taka_23

名古屋から東京に来たよ
Coqから定理証明に入門した
Liquid Haskellを使った経験がある
Liquid Haskell本を発刊したよ!

### @tanaka_akr

Coqの中でSSEを使ってCに変換してRubyから呼ぶ発表
基本はC言語プログラマ
ここ数年Coqを研究で使っている
Alloyを昔使ったことがある
ネタ: Rubykaigiと同じネタならしゃべれるよ(40分)

### @hatsugai

並行システムの検証をしたくてツールを作っている
対話的なモデル検証
SSGというクラウドパワーを使って検証する
pthreadの検証もしたよ
isabelleを使っていて、Coqはあまり。。。
ネタ: 2つあるよ

## ネタ

* [10] 「CSPによるスケジューラのモデル化と優先度継承プロトコルによる優先度逆転問題への対処と検証 (40分)」 by @hatsugai
* [10] 「モデル検査器によるマルチスレッドプログラムの検証 (40分)」 by @hatsugai
* [5] 「Rubykaigiと同じネタ(CoqでSSE) (40分)」 by @tanaka_akr
* [4] 「Coverityを買えないときの静的コード解析ツール (20分)」 by @masterq
* [3] 「HDLの検証 (20分)」 by @hanetsuki_y
* [3] 「Valaを使った安全なGObjectプログラミング (20分)」 by @masterq
* [2] 「GObject Introspectionをさわってみたよ (30分)」 by @masterq
* [2] 「callgrindの入門 (20分)」 by @dooriver

14:00以降は各自の持ちネタを発表します。途中休憩を10分x2確保しようと思います。現時点で上がっている発表ネタとその発表に必要な時間は以下です:

• 「CSPによるスケジューラのモデル化と優先度継承プロトコルによる優先度逆転問題への対処と検証 (40分)」 by @hatsugai

システムをモデル化する際，大きく分けて2つの方針があります．1つは相互作用の手段が与えられているとしてコンポーネントだけをモデル化する方法，もう1つは加えてオペレーティングシステムも明示的にモデル化する方法です．今回はCSPを使ってOSのスケジューラをモデル化してみました．優先度付きのスケジューラにはいわゆる優先度逆転問題があります．まずはこれを検査で検出できるようにして，次に優先度継承プロトコルを実装して解決できたことを検証します．ツールは SyncStitch を使います．

• 「モデル検査器によるマルチスレッドプログラムの検証 (40分)」 by @hatsugai

C言語とpthreadで書かれたマルチスレッドプログラムを検査する Pthread Program Checker (PPC) というツールを開発しています．このツールではC言語でモデルを書くことができます．検査したい性質もふつうにassertを入れるだけなので簡単です．このツールを使って pthread プログラムのちょっと気になる点をいくつか調べてみたという事例紹介です．

• 「Coverityを買えないときの静的コード解析ツール (20分)」 by @masterq

Coverityは優秀な静的コード解析ツールとして有名です。しかし会社の規模によっては当該ツールの導入予算がつかないケースもあると思います。本発表ではオープンソースの静的コード解析ツールを紹介し、その特性を比較します。

• 「GObject Introspectionをさわってみたよ (30分)」 by @masterq

GObject Introspection は GObject というライブラリを持ちいて、かつ特殊なコメントを埋め込まれたC言語ライブラリへの高級言語バインディングを自動生成する機構です。Haskell言語向けGObject Introspectionの実装である haskell-gi をサーベイした結果を報告します。

• 「Valaを使った安全なGObjectプログラミング (20分)」 by @masterq

ValaはGObjectをベースにした独自の言語でGNOMEのベースとなっているGLibを使ったオブジェクト指向プログラミングを支援します。本発表ではこのVala言語がどの程度安全なプログラミングを支援しているのか簡単なテストプログラムを例にして解説します。

• 「ATS言語ハンズオン (60分)」 by @masterq

ATS言語 (日本語ページ) はOSのカーネルやベアメタルで動作するコードを安全に設計できることが知られています。このハンズオンではATS言語にまったく触ったことのないユーザ向けに、各プラットフォームへのATSコンパイラのインストール方法、最初のATSプログラムの書き方、依存型の解説と簡単な利用方法、線形型の解説と簡単な利用法について説明/ハンズオンを行ないます。

• 「最近のはてなブックマークを見て談話しよう (30分)」 by 全員

@masterqが日々収集しているコード検証に関するブックマークを皆で眺めながら意見交換をしましょう。

• 「懇親会の調整 (お店を選んで参加人数で予約します) (15分) 」by 全員
• 17:45-18:00 「次回の計画 (15分)」 by 全員

会場について

永和システムマネジメント様に会議室を提供していただきました。ありがとうございます!

• 場所 : 〒101‐0041 東京都千代田区神田須田町2-3-1 NBF神田須田町ビル7F map（1階がサンクスのビルです。）

開催日は休日のため、ビル自体が入館制限されており、関係者でないと入れません ので注意ください。

参加者のみなさんは次の段取りに従って入館してください。

• 12:45 に同ビル1階のファミリーマートの飲食スペースあたりに集合してください。
• 入館できる人が引率して、まとまって入館します。
• 遅参した場合は、サンクスに到着したら 主催者のTwitter や同席予定者へ連絡してください。別途入館を支援します。
• 主催・発表予定者で、早めに来たい方には、別途調整しますのでご連絡ください(会場は 12:30 から使えるようにしてあります)。
• 電源、Wi-Fi は自由に使えます。
• 飲食は自由です。自動販売機があります。（ゴミの後始末は各自でお願いします。）
• その他この勉強会において困ったことがありましたら 090-3524-7064 まで電話をください。主催者 が対応いたします。

懇親会

18:30から以下で懇親会を開催します。

• 春天酒坊 03-6206-9200 東京都千代田区神田須田町2-6-2-101

協賛

• 永和システムマネジメント様: 会場の提供