お知らせ ビープラウド、「90日で稼げるプログラマーに」オンライン学習サービス「PyQ(パイキュー)」を販売開始

このエントリーをはてなブックマークに追加

11月

19

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

ATS/VeriFast/Infer/Frama-C/seL4などなどについて発表しまくるんだ!

ハッシュタグ :#metasepi
募集内容

ホモ・サピエンス

無料

先着順(抽選終了)
15/25

イベントの説明

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

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

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

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

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

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

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

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

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

当日のスケジュール

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

  • 12:45 ビル1階のサンクス飲食スペースに集合してください
  • 13:00-14:00 「並行システムの理論 CSP の紹介」 by @hatsugai

CSP (Communicating Sequential Processes) は並行システムの振る舞いを記述し,その性質を議論するための理論です.並行システムとは複数の構成要素からなるシステムで,各構成要素が並行に動作し,互いに作用を及ぼしあいながら協調して全体として目的の仕事をするシステムです.現在我々が目にするコンピュータを使ったシステムの多くは並行システムです.このようなシステムの開発に必要な基盤は,我々がよく知っている逐次的なプログラムとは異なっています.CSP はその基盤を提供してくれる理論です.今回はまず逐次的なプログラムの開発基盤を5つのポイントで整理・レビューし,それと対比させる形で CSP および並行システムについて紹介していきたいと思います.最後に CSP に基づく並行システムの検証の方法とツールをご紹介します.使用する資料はこちらからダウンロードできます.もし疑問な点がありましたら事前に hatsugai@principia-m.com までお知らせいただければ幸いです.時間が限られていますので,すべてにお答えできるかどうかわかりませんが,資料の手直しや説明の準備の参考にさせていただきたいと思います.

  • 14:00-14:10 休憩
  • 14:10-15:10 「Prologを使えば君も天才になれます」 by @h_sakurai

自動検証を構築するには基礎となる理論の理解が必要です。しかし論文に乗っているような数式は、それなりの教育を受けていない人にとって非常に難しく見えます。関数型言語による言語の構築は高速で確実に動きますがそれなりの規模になってしまいます。実のところ、評価や型検査、型推論の推論規則は一種の論理型言語にすぎません。論理型言語でよく知られているPrologを使えば推論規則をトライ&エラーで実行しながら試してみることができます。今回はPrologの基本的な使い方から初め、関数型言語的に四則演算のある言語を作成し、それを徐々に論文の形に近づけた後、ラムダ計算を実装し、型推論、Fether Weight Javaの実装、ATSの基礎となる線形論理型言語のインタプリタの実装やInferの理論的な基礎となるホーア論理を使った簡単な検証システムをなどを紹介します。

  • 15:10-15:20 休憩
  • 15:20-15:35 懇親会の調整 (お店を選んで参加人数で予約します)
  • 15:35-16:35 「TPPMark2016を解きながら学ぶVeriFast」 by @eldesh

VeriFastは分離論理に基づくCとJava言語の検証器です。 分離論理とは手続き型言語の挙動を理解するための方法の一つであるホーア論理を拡張したもので、ポインタを用いた高度なメモリ操作を含むプログラムを記述する事ができます。 本発表では定理証明器に関する会議であるTPP2016で出題された問題であるTPPMarkを題材として、VeriFastによる注釈と検証の方法の入門的な解説を0から行います。 TPPMarkの要求の形式化から始め、そのために必要となる仕様の定義を行い、その実装を組み上げながら、検証に必要な注釈を付けていきます。

  • 16:35-16:45 休憩
  • 16:45-17:10 「Inferは契約プログラミングの夢をみるか」 by @masterq

InferはObjective-C,Java,Cコードを対象にした静的自動検証器で、Facebookが買収したことで話題になりました。任意のC言語コードをこのツールにかけることで表明を書かずにメモリ関連の欠陥などを自動的に検出してくれます。一方、古くから契約プログラミングが提唱され、動的な事前条件と事後条件をコードに埋め込むことによってその品質を向上させることが知られています。この発表ではInferを使うことで静的に検証可能な事前条件と事後条件を表明することができることを示し、またその利用の限界についても言及します。

  • 17:10-17:40 徹底討論「テーマ: 静的コード解析を国際標準化するには」

お客様は製品を手にする際「この製品はどんな検証をされていて、どの程度安全なのだろうか?」と疑問を持つのではないでしょうか。一方で、ホーア論理や分離論理などの理論的背景を全ての人類に理解させることも困難です。ちょっと想像してみましょう。もし「様々な静的コード解析を包括した国際標準があったら」この問題を解消することはできるでしょうか?すなわち安全性をうたう製品には全て当該の国際標準にそったグレードや種別がマークで記載されていたとしたら、お客様に「この製品はどの程度安全なのか」たやすく実感していただくことができるのではないでしょうか。そのような国際標準を作ることは本質的に可能なのかブレインストーミングしてみましょう。

  • 17:40-18:00 次回の計画

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

会場について

永和システムマネジメント様に会議室を提供していただきました。ありがとうございます!

  • 場所 : 〒101‐0041 東京都千代田区神田須田町2-3-1 NBF神田須田町ビル7F map(1階がサンクスのビルです。)

開催日は休日のため、ビル自体が入館制限されており、関係者でないと入れません ので注意ください。

参加者のみなさんは次の段取りに従って入館してください。

  • 12:45 に同ビル1階のサンクスの飲食スペースあたりに集合してください。
  • 入館できる人が引率して、まとまって入館します。
  • 遅参した場合は、サンクスに到着したら 主催者のTwitter や同席予定者へ連絡してください。別途入館を支援します。
  • 主催・発表予定者で、早めに来たい方には、別途調整しますのでご連絡ください(会場は 12:30 から使えるようにしてあります)。
  • 電源、Wi-Fi は自由に使えます。
  • 飲食は自由です。自動販売機があります。(ゴミの後始末は各自でお願いします。)
  • その他この勉強会において困ったことがありましたら 090-3524-7064 まで電話をください。主催者 が対応いたします。

懇親会

18:30から以下で懇親会を開催します。

発表者

資料 資料をもっと見る/編集する

フィード

masterq

masterqさんが資料をアップしました。

2016/11/19 23:19

masterq

masterqさんが資料をアップしました。

2016/11/19 23:18

masterq

masterqさんが資料をアップしました。

2016/11/19 23:18

masterq

masterqさんが資料をアップしました。

2016/11/19 23:18

eldesh

eldeshさんが資料をアップしました。

2016/11/19 22:39

久保秋 真

久保秋 真 さんが書き込みました。

2016/11/19 12:11

会場はスタンバイできました。机と椅子のレイアウトをしたほうがよいでしょう。

h_sakurai

h_sakuraiさんが資料をアップしました。

2016/11/19 10:26

masterq

masterq さんが書き込みました。

2016/11/18 21:55

とりあえず現地近辺でお店を何件かピックアップしておこうと思います。

久保秋 真

久保秋 真 さんが書き込みました。

2016/11/18 11:01

あ、投稿に使うアカウント間違えました…。

東京青高同窓会

東京青高同窓会 さんが書き込みました。

2016/11/18 11:00

懇親会の手配を何方かにお願いできませんか。

masterq

masterqさんが資料をアップしました。

2016/11/14 17:57

masterq

masterq さんが書き込みました。

2016/11/08 00:20

会場のEthernetでRTMPが通ればYouTubeで生放送できるかもしれません。

masterq

masterqさんが資料をアップしました。

2016/10/27 19:51

masterq

masterq さんが書き込みました。

2016/10/25 09:04

気が早いですが、次々回の日程調整をしています。参加されたい方/発表したい方は参加できる日程を入力していただけないでしょうか。よろしくお願いします / #静的コード解析の会 第1回 日程調整 https://chouseisan.com/s?h=489b5d18b0fe4682b3154f94295a0137

masterq

masterq さんが #静的コード解析の会 第0回 を公開しました。

2016/10/07 21:25

「静的コード解析 第0回」 を公開しました!

グループ

Metasepi

組み込み/関数型プログラミング/コード検証などの話題を扱うコミュニティです

イベント数 10回

メンバー数 83人

終了

2016/11/19(土)

12:45
18:00

募集期間
2016/10/11(火) 00:00 〜
2016/11/18(金) 22:00

会場

永和システムマネジメント コワーキングスペース

東京都千代田区神田須田町2-3-1 NBF神田須田町ビル7F

永和システムマネジメント コワーキングスペース

参加者(15人)

eldesh

eldesh

I joined 静的コード解析の会 第0回!

masterq

masterq

静的コード解析の会 第0回 に参加を申し込みました!

TakeshiHori

TakeshiHori

静的コード解析の会 第0回 に参加を申し込みました!

久保秋 真

久保秋 真

#静的コード解析 の会 第0回 に参加を申し込みました!

hatsugai

hatsugai

#静的コード解析の会 第0回に参加を申し込みました!

autotaker1984

autotaker1984

#静的コード解析の会 第0回 に参加を申し込みました!

TadashiEbara

TadashiEbara

#静的コード解析の会 第0回に参加を申し込みました!

h_sakurai

h_sakurai

#静的コード解析の会 第0回 に参加を申し込みました!

sm0kym0nkey

sm0kym0nkey

#静的コード解析の会 第0回 に参加を申し込みました!

mhayashi

mhayashi

I joined #静的コード解析の会 第0回!

参加者一覧(15人)

キャンセルした人(7人)