Jan

20
#静的コード解析の会第6回
発表募集中です!

Hashtag ：#metasepi

Registration info	ホモ・サピエンス Free FCFS 12/18

Description

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

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

ATS, B-Method, CBMC, Coq, Coverity Scan, CSP, Dafny, F*, Frama-C, FreeSafeTy, Infer, Isabelle, SATABS, SPARK, 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

今はフリーランスでSSLのポーティングの仕事をしています
最近はVeriFast検証器に興味があります
今日のネタ: VeriFastのパーサをまともにした話 他

### @hatsugai

検証ツールを作っている。
前回pthreadの検証の続きの話
仕事紹介してほしい!
Isabelleやっているよ
トップエスイーでCSPの講義やるよ
今日ネタなし!

### @tos

今日はひさびさに技術にふれる機会だ!
検証そのものは好き。
今日はネタなし!

### @eldesh

SMLが好きです。
組み込みっぽいプログラマです。
最近VeriFastの勉強中。
今日のネタ: VeriFastの停止性の話ができるよ

### @oganao

MySQLの5.7のxprotocolのクライアントドライバをHaskellで作ってる。
構文解析的な話が聞けるかと思って来たよ!

### 久保秋

仕事で動的解析をしています。
場を提供する仕事が今日だよ!
会社としてはUMLのツールを販売している。
永和システムのコワーキングスペースを皆も使って交流してね!

### @ftake

ソフトウェア設計社内コンサル。
設定ファイルを相手にすることが多め。
今日は仕事/趣味のネタが得られればいいな。

### @khibino

Haskellで趣味も仕事も。
メンテナンスの仕事多め。
HRRライブラリをSQLデータベースを安全にするために作ってるよ。

### @tanaka_akr

Coqユーザです。
CoqからCコードを吐くプラグインを書いています。

## ネタ

* 3 VeriFast検証器ハンズオン
* 6 VeriFastの停止性の話ができるよ
* 6 GObject Introspectionをさわってみたよ
* 5 VeriFastのパーサをまともにした話
* 0 ATS言語ハンズオン
* 0 Valaを使った安全なGObjectプログラミング

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

「VeriFast検証器のパーサをマシにする話 (30分)」 by @masterq

VeriFast はC言語コードのコメントに注釈を付けることでバッファオーバフローや関数の事前/事後条件を静的に検査することができます。しかしそのパーサはC99互換ではないために、これまでは検証のためにVeriFast向けのヘッダとビルド用ヘッダを二重管理し、前者に注釈を書き込むスタイルで検証することを強いられてきました。本発表ではNetBSD kernelのC言語コードに直接注釈を挿入可能にするために、当該パーサの互換性を向上させる試みを紹介します。

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

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

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

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

「VeriFast検証器ハンズオン (60分)」 by @masterq

VeriFast はC言語コードのコメントに注釈を付けることでバッファオーバフローや関数の事前/事後条件を静的に検査することができます。主催者が個人的に注力している技術の1つです。新しい参加者はこの検証器の概要を知らないかもしれません。そこで、本ハンズオンでは VeriFastチュートリアルを読みながら実際に検証器をさわってみます。より高度な機能については主催者には荷が重いので、どなたか代役とつとめていただけると助かります。

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