#静的コード解析の会第7回

2018/05/12(土)12:45 〜 18:00 開催

ブックマーク

#C言語, #初心者

イベント内容

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

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

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

FPGA屋さんになっている。Vivadoなれない。。。

今日のネタ:

* さわって学ぶVCC(VCCチュートリアルの翻訳) 60分

### hatsugai

仕事ないぞ。ひからびる。
趣味のプログラミングに忙しい。
ネタないよ!

### tos

最近仕事に復帰。一週間目!
4月頭からトップエスイーに通いはじめたよ。

https://www.topse.jp/ja/

命題論理/述語論理/ホーア論理など基礎をやってから、静的解析の紹介などがあったよ。
(岡部はちゃんと基礎がないまま勉強会運営しているよ)

### khibino

Haskellで仕事しているよ。
flopsに行ってきたよ。

今日のネタ:

* flopsでわかったことをざっくりでなら話せるよ 30分

### tanimocchi

セキュリティ屋さんだよ。暗号とか。分散やら。

今日のネタ:

* flopsのネタのサポートなら

### ftake

普段はansible屋さんに今なってるよ。
今日のネタ、、、つらみ。。。

今日のネタ:

* 皆で https://sv-comp.sosy-lab.org/2018/ を眺める 20分

### 久保秋 真

UMLのツール作ってるよ。
最近別の仕事で動的解析のツールを試してたよ。
組み込みだと動的解析がつらい。。。
ETロボコンの仕事をしなければ。。。
CygwinのインストールやらITリテラシー教育の重みもデカい。
トップエスイーでモデル駆動開発をやってて、その記事を昔書いたよ。
2018-05-18にC言語の入門本を出版するよ:

https://www.amazon.co.jp/dp/4802611587

### eldesh

ネタないよ。
flopsに行ってきたよ。
機械学習の会社でWebサービスを作っているよ。Rustで。
VeriFastがまだマイブームでキテるよ。
もっと基礎的な教科書を読もうとしていて、ホーア論理を学習中。

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

「皆で https://sv-comp.sosy-lab.org/2018/ を眺める (20分)」
「 http://www.sqlab.jp/FLOPS2018/ でわかったことをざっくりでなら話せるよ (30分)」
「さわって学ぶVCC (60分以上)」 by @masterq

VCCはMicrosoft Research製のC言語静的解析ツールです。C言語に_(foo)という特殊な注釈を挿入して、コードの正しさを検証します。本発表ではVCCのチュートリアルである"Verifying C Programs: A VCC Tutorial"で紹介されたコードをオンラインで実行させながらVCCの使い方を学びます。左記チュートリアルのざっくりとした翻訳もあります。 "5 Object invariants"の後半まで読みました。

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