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

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

• 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:30-13:00 開場
• 13:00-14:00 「自己紹介と今日話せるネタ出し」 by 全員

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

# 自己紹介

## 岡部 @masterq

* 誰？: 昔NetBSDでコピー機を作ってました。今は仕事でSecure-OSを作っています。検証ツールが仕事に生かせたらいいなぁと考えて色々手を出しては手を焼いています。
* 話せるネタ: VeriFast検証器の紹介とRTOSに適用してみた話、ATS言語入門

## つづきたかし @TakashiTsuzuki

* 誰？: 社内SE。SIerのSEからキャリア。品質の向上に役立つ情報が欲しいな。
* 話せるネタ: ないよ!

## おおたまささき @Masaki_Ota

* 誰？: 組み込みC言語エンジニアからはじめた。そのころ静的コード解析してた。R8Cマイコンを使ってた。今はWebアプリケーション。C#やRubyを使う。C++をたまに使う。Rubyは実行時のコード解析の方が重要。C++だと静的コード解析は大事かなと。
* 話せるネタ: ないよ!

## くぅ - kuxu

* 誰？: 大学生だぜ!静的コード解析は言葉を聞いたことがあるぐらい。Coqは名前だけは聞いてた。いつかどちらもやらないと。普段はC#で。コグニティブサービスもさわっている。
* 話せるネタ: ないよ!

## @lumin

* 誰？: 情報セキュリティ。納品されたバイナリの仕様を満たしているかどうか検索。対象:x86バイナリ,ARMバイナリ,Androidアプリ,iOSアプリ。idaproというツール。
* 話せるネタ: 今話したよ!

## よんた @keita44_f4

* 誰？: そもそも管理者に登録されたぞ。大学で関数型言語をやってた。Coqを触ってた。趣味として静的コード解析は趣味で。Qt/C++でアプリを仕事で書いている。
* 話せるネタ: ないよ!

## 黒曜

* 誰？: 会場係。RoR使い。Isabelleをさわった大学時代。
* 話せるネタ: ないよ!

• 14:00-15:00 「ChibiOS/RT開発環境の構築」 by @masterq

メジャーなRTOSの1つであるChibiOS/RTを紹介し、参加者のPCにそのビルド環境を構築します。ビルド構築について詳しくはchibios-verifastリポジトリを参照してください。また本発表資料はGitHubから入手できます。

• 15:00-15:10 休憩
• 15:10-16:10 「STマイクロ製マイコンボード上におけるChibiOS/RTアプリケーションの実行」 by @masterq

メジャーなマイコンメーカの1つであるSTマイクロ製のボードを使って、前タームで構築したChibiOS/RTのアプリケーションを動作させます。

# 反省

会場でハンズオンをして以下のような気付きが得られました。次回に向けて改善しましょう！

* ケーブル不良品多し
* GCCのツールチェーンのダウンロードが遅い(USBスティックで配布すべき)
* GNU makeをインストールしていないcygwinユーザのことを考えろ
* stlinkはハマるのでWindowsとmacOSはバイナリして環境構築した方がいい
* stlinkの公式ドライバがWindowsには必要かも
* Windowsではファームウェアライトは純正ツールの方がマシ
* ツールチェーンにPATHを通す
* 統合開発環境
* Dockerでイメージ配布
* mbed方式のファームウェアライトする方式の方がいいかも
* MSYS/MinGW上ではst-utilが凍る
* make gdbwriteからmake allに依存をはる

• 16:10-16:20 休憩
• 16:20-17:20 「VeriFastによるChibiOS/RTアプリケーションの検証」 by @masterq

前タームで使用したChibiOS/RTアプリケーションのコードに対してVeriFastを使って簡単な検証を行ないます。

• 17:20-18:00 「未定」

当日までに予定が決まらなければ、各自もくもく会になります。参加者が「こんな検証をしてみたい」と提案して、それに対して検証可能かどうか皆で調べるのも面白いかもしれません。また希望があれば来年の計画を立てたいと思います。

しかし会場からの活発な議論があった場合などは柔軟に対応しようと考えています。

会場について

Misoca様に会議室を提供していただきました。ありがとうございます!

当日は森さん(@kokuyouwind)が会場を担当してくれます。 12:30頃には利用可能な状態にしておきますが、ビル自体のシャッターが降りているため、ビル入り口についたら主催者もしくは森さんご連絡ください。

その他会場詳細についてはこちらをご覧ください。

またこの勉強会において困ったことがありましたら 090-3524-7064 まで電話をください。主催者が対応いたします。

アクセス

• 場所 : 名古屋市中村区名駅2-35-22 メビウス名古屋ビル2階 株式会社Misoca 内 セミナールーム「木曽川」 map
• JR/地下鉄/名鉄「名古屋」駅より徒歩5分くらいです。
• 名古屋駅からの経路

スペック

• Wi-Fiあります
• プロジェクタ使えます。HDMI と VGAあります
• マイクとスピーカはありません
• ホワイトボードあります
• 電源潤沢にあります
• ドリンク飲めます。飲酒はご遠慮ください
• 食事はご遠慮ください。飲食可能なコミュニティスペースが同フロアにあります
• 禁煙です
• 弊社及び弥生の紹介やパンフレット配布等のご協力をお願いする場合があります。ご了承ください

協賛

• STマイクロエレクトロニクス様: マイコンボードの提供
• Misoca様: 会場の提供