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

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

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

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

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

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

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

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

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

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

持ち物

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

当日の内容

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

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

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

# 参加者リスト
## 名前: たけやま @ftake

どんな人: SPIN使ってた。C言語検証してた。ソフトウェア設計改善。OpenSUSEの開発。SUSEのイベントを日本開催したい。
ネタ: あんまりない...

## 名前: かさい @takarakasai

どんな人: ロボットの研究開発。医療機器。複雑な機器を扱う。品質に対する知見を広めたい
ネタ: ないんだぉー

## 名前: とがわ @tos

どんな人: 育児中だぜ!SDN(Software Defined Network)の開発。学生時代は関数型言語をさわってた。SDNは一方泥臭い。
ネタ: callgrindの紹介。実行させて検証する。関数の呼び出し関係を調べることができる。既存資産のサーベイに役に立つことがある。が、、、仕込みが足りないので次回発表したい。

## 名前: 絵面 @ezura

どんな人: iOSエンジニア。プログラミング言語スキー。Swiftの言語仕様外をつつく遊び。Swiftの闇を見つめるのが好き。Swift 3.1はまたバグると思うと楽しみでしょうがない。
ネタ: Swiftまわりで闇のネタを発表したいが、、、次回かなぁ。。。

## 名前: 石橋 @rysh

どんな人: Webサービス。開発プロセス改善をやってる。リファクタリング好き。他人のシステムをリファクタリングするのは危険。静的解析がリファクタリングのヒントになるのでは。自己組織化についても
ネタ: Eclipseのlintプラグイン。

## 名前: たなかあきら @tanaka_akr

どんな人: Rubyコミッタ。C言語プログラマ。産総研。Coqに溺れる日々。CoqでC言語コードを吐き出す
ネタ: Coq=>Cなネタ (30分)

## 名前: えばら @TadashiEbara

どんな人: 分散ファイルシステム。Java。C++。お金を扱うプログラム。C++はSEGVだしまくりだぜー。ひゃっはー。落ちないC++がほしいんだよ。
ネタ: ないんだぜー

## 名前: かわの(総統) @nanbuwks

どんな人: オープンハードウェアカンファレンス。オープンハードセキュリティ。IoTなどインターネットに繋がるけど、80ポート開きっぱなしなどセキュリティの意識が低すぎる。ハードウェアでバッファオーバーランなども防ぐ方法が本当にないのかにも興味がある。疫病など物理攻撃に対する耐性を作るのにも興味がある。子供3人いるよ!一人子供と一緒に来ました。
ネタ: ないんだよー

## 名前: ごとう @eldesh

どんな人: SMLスキー。VeriFastに興味がある。定理証明にも興味がある。
ネタ: VeriFastの停止性証明の紹介ができるよ (30分)

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

• 13:45-14:25「Coq=>Cなネタ (30分)」 by @tanaka_akr (7)
• 休憩 (10分)
• 14:35-15:40 「Third French Japanese Meeting on Cybersecurity参加レポート (30分)」 by @masterq (6)

Third French Japanese Meeting on Cybersecurityという会議に@masterqが参加してきたので、聴講メモを見ながら会議の様子を報告します。

• 休憩 (10分)
• 15:50-16:00「懇親会の調整 (お店を選んで参加人数で予約します) (20分) 」by 全員
• 16:00-16:45 「VeriFastの停止性証明の紹介 (30分)」 by @eldesh
• 休憩 (5分)
• 16:50-17:45 「ATS言語ハンズオン (60分)」 by @masterq (9)

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

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

fun print_int {l:addr} (pat : !int@l | p : ptr l): void = {
  val () = println! (!p)
}

implement main0 () = {
  var v : int = 123
  val p = addr@v
  prval pat = view@v
  val () = print_int (pat | p)
  prval () = view@v := pat
}

• 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

協賛

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

前回の勉強会でのやりたいことメモ

## (誰が音頭取るか置いておいて)やりたいこと
### VeriFast

* VeriFast基礎
* VeriFastのOCamlコード読む会
* VeriFastの停止性検査について
* マイコンそのもので遊ぶ会
* VeriFastで検証済みの非常に単純なゲーム (数当てとかレベル)
* リストのconsを自分で検証してみたい
* デリファレンスの検証とは何なのか根本的に理解したい
* メモリ破壊がないだけでもうれしいよ!
* 簡単な検証対象ってなんどうを考える会
* VeriFastの検証は何がターゲットとして向いてるの？GUIとかI/Oとかあったら？
* 分離論理入門

### CSP

* CSPハンズオン (LTSAを使う？)
* 「並行システムの検証と実装: 形式手法CSPに基づく高信頼並行システム開発入門」を読む

### Isabelle

* http://www.concrete-semantics.org/ 読書会
* 分離論理がIsabelleにもあるらしい

### Boogie

* 某L社で製品検証に使おうとして絶望した話

### ATS

* 前回VeriFastを対象にやったようなハンズオン

## 招待講演してくれる人を探す

* 某Kさん呼ぶか! Hさんが呼んでたよって言えば来るんじゃね？