#静的コード解析の会 第7回
イベント内容
静的コード解析とこの勉強会について
静的コード解析をご存知でしょうか。静的コード解析とは、コンピュータのソフトウェアの解析手法の一種で、ソフトウェアを実行することなく解析を行うことです。このような手法には以下のように様々な実装があります:
- 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 全員
会場について
永和システムマネジメント様に会議室を提供していただきました。ありがとうございます!
- 場所 : 〒101‐0041 東京都千代田区神田須田町2-3-1 NBF神田須田町ビル7F map(1階がファミリーマートのビルです。)
開催日は休日のため、ビル自体が入館制限されており、関係者でないと入れません ので注意ください。
参加者のみなさんは次の段取りに従って入館してください。
- 12:45 に同ビル1階のファミリーマートの飲食スペースあたりに集合してください。
- 入館できる人が引率して、まとまって入館します。
- 遅参した場合は、ファミリーマートに到着したら 090-3524-7064 まで電話してください。別途入館を支援します。
- 主催・発表予定者で、早めに来たい方には、別途調整しますのでご連絡ください(会場は 12:30 から使えるようにしてあります)。
- 電源、Wi-Fi は自由に使えます。
- 飲食は自由です。自動販売機があります。(ゴミの後始末は各自でお願いします。)
- その他この勉強会において困ったことがありましたら 090-3524-7064 まで電話をください。主催者 が対応いたします。
懇親会
18:30から以下で懇親会を開催します。
- 春天酒坊 03-6206-9200 東京都千代田区神田須田町2-6-2-101
協賛
- 永和システムマネジメント様: 会場の提供
注意事項
※ 掲載タイミングや更新頻度によっては、情報提供元ページの内容と差異が発生しますので予めご了承ください。
※ 最新情報の確認や参加申込手続き、イベントに関するお問い合わせ等は情報提供元ページにてお願いします。
新規会員登録
このイベントに申し込むには会員登録が必要です。
アカウント登録済みの方はログインしてください。
※ ソーシャルアカウントで登録するとログインが簡単に行えます。
※ 連携したソーシャルアカウントは、会員登録完了後にいつでも変更できます。
![connpass](https://files.techplay.jp/JI32Z7OO7/images/top/apilogo_connpass.png)