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

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

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

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

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

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

「勉強会の様子を知りたい」という場合には、発表動画から本勉強会の雰囲気を知ることができます。

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

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

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

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

持ち物

• Windows/MacOS/LinuxいずれかのOSがインストールされ、無線LANに接続可能なノートPC
• マウス
• 少しばかりの好奇心

当日の内容

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

• 13:00-14:00 「自己紹介と今日話せるネタ出し」 by 全員

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

## @masterq

C言語からATS言語へのトランスレータを書きはじめました。
(誰が必要なんだろう？)

* 「KreMLin入門 (30分)」 by @masterq
* 「ATS最新動向 2018年秋 (30分)」 by @masterq
* 「VeriFastの光と闇(FreeRTOS編) (30分)」 by @masterq
* 「C言語からRustへの変換手法比較 (20分)」 by @masterq
* 「TLA+とUPPAALによって設計されたOpenComRTOS概要 (20分)」 by @masterq

## @eldesh

VeriFast楽しい!

ネタなし

## @Kuniwak

DeNAテックコンで検証の話をした。
VDA++とSPIN。SPINいいね!
PlusCalに興味があります。

DeNAテックコンと同じ話ならできるよ
困ってること聞きたい! (ドメイン固有の問題がある。。。)

## @kubo39

D言語いいね!
最近Isabelleをはじめました。
ソフトウェアの基礎をIsabelleで書きなおしている。

ネタなし

## @ゆで卵

Isabelleを最近はじたので、様子見に来たよ!

ネタなし

## @ntanaka-nobuakit

ガイオテクノロジーではたらいてます。
ユニットテスト自動生成ツール。
もうRustじゃないか？
動的テストより、FMEAやらで人間のモデルを分析するツールが今はちょっとドメインが違うかもしれない。

ネタなし

## @_KskSsk

10年前にSPINっぽい何かを作ってた。
Cで検証は辛い。。。
検証は即状態爆発になるのでは。。。
第三の解は存在しないのか。。。

ネタなし

## @takumi-kato

量子コンピュータライブラリ作ってる。
量子コンピュータもコンパイラを作る流れになるのでは。。。
好きな言語はRustです。

ネタなし

## @tohdo

Spark(Ada)を使ってる!
モデル検査はまだnuSMVを使ったことがある。
定理証明系はLeanが好き。
プログラムは書く毎にHaskellを勉強しなおすよ。

ネタなし

## @ftake

昔はモデル検査を応用したツールを作ってたりした。
最近はめっきり。新しい情報はいつでも欲しい。
コベリティじゃない重くないツール欲しいですよね。

ネタなし

## @tanimocchi

最近Inferを使ってる。いいね!
CPAcheckerは関数単位でしか使えなくてつらかった。

過去に発表した抽象解釈を使ったdeep learningの検証/学習

## @tanaka_akr

Rubyコミッタ。Coqを使ってる。

Matzの主張をCoqでデバッグする。
Coqのドキュメントを修正してみた。フォーマルじゃないドキュメントを。

## @hatsugai

CSPいいね! CSPのモデル検査ツールを作っている。
Isabelleで証明を書いたりしています。

ネタなし

## @myuon_myon

定理証明ではIsabelleを良くつかっている。昔はAgdaだった。

Isabelleでsortのアルゴリズムを作ったので、その解説。

## @golden_lucky

鹿野と言います。ラムダノートで出版社。
定理証明の本も作ってるけど、自分で検証はしてないので、今日はROMりに来たよ。

ネタなし

## @khibino

Haskell使ってる。Agda最近はじめました。

ネタなし

## 発表ネタへの投票

v 10 「C言語からRustへの変換手法比較 (20分)」 by @masterq
v 10 Matzの主張をCoqでデバッグする。
v 10 Isabelleでsortのアルゴリズムを作ったので、その解説。
v 9 「TLA+とUPPAALによって設計されたOpenComRTOS概要 (20分)」 by @masterq
v 7 過去に発表した抽象解釈を使ったdeep learningの検証/学習
v 6 DeNAテックコンと同じ話ならできるよ
v 6 「ATS最新動向 2018年秋 (30分)」 by @masterq
v 4 Coqのドキュメントを修正してみた。フォーマルじゃないドキュメントを。
v 5 「VeriFastの光と闇(FreeRTOS編) (30分)」 by @masterq
4 「KreMLin入門 (30分)」 by @masterq

• 「懇親会の調整 (お店を選んで参加人数で予約します) (15分) 」by 全員

• 「KreMLin入門 (30分)」 by @masterq

F*のサブセットで、C言語にコンパイルできるLow*のコンパイラを、KreMLinユーザマニュアル http://fstar-ja.metasepi.org/doc/kremlin-book/ を読みながら入門します。

• 「ATS最新動向 2018年秋 (30分)」 by @masterq

一時期話題になったATS言語。2018年に入って「ATS3の設計開始宣言」と「Vanessa‍ McHaleがATS使いになった」ことでATS言語界隈は大きく変わる兆しがありました。ATS3の最新動向とVanessa‍が設計したツール群について簡単に紹介します。当日の資料はこちらです。

• 「VeriFastの光と闇(FreeRTOS編) (30分)」 by @masterq

@masterqがFreeRTOSのタスクを少しだけVeriFastで検証してみました。その結果実感したVeriFastの良い面と悪い面について共有します。当日の資料はこちらです。

• 「C言語からRustへの変換手法比較 (20分)」 by @masterq

C言語からRustへの変換手法としてcorrodeとc2rustが広く知られています。前者は純粋なHaskell実装で、後者はRust+Clang+Emscriptenで実現されています。両者の比較のためにBSD catコマンドを両ツールでRustに変換してみました。変換してcorrodeの結果とc2rustの結果が得られました。変換結果を眺めながらCFGの特性などを比較します。また発表者は変換結果をrustcでコンパイルできなかったので助言がいただけると助かります。

• 「TLA+とUPPAALによって設計されたOpenComRTOS概要 (20分)」 by @masterq

OpenComRTOSというRTOSはTLA+とUPPAALという2つのツールによって設計されています。TLA+はモデル検査に、UPPAALは性能モデル検証に用いられています。Formal Development of a Network-Centric RTOSというレポートを読みながらモデル検査のRTOSへの適用事例と発表者の感想を共有します。

• 17:45-18:00 「次回の計画 (15分)」 by 全員

会場について

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

• 場所: 東京都中央区日本橋2-7-1 東京日本橋タワー
• 別途メールにて連絡する手順で入館してください
• 電源、Wi-Fi は自由に使えます。
• 飲食は自由です。
• その他この勉強会において困ったことがありましたら 090-3524-7064 まで電話をください。主催者 が対応いたします。

懇親会

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

建設的な議論のために

主催者自身が建設的な議論を阻害しがちなので、議論のやり方についてルールを導入しようとしています。 今回の勉強会では具体的なルールを制定しませんが、参加者一人一人が以下の文書を読むことを推奨します。

また本勉強会で困ったことなどご意見がありましたらMetasepiメーリングリストまでご連絡ください。対応いたします。

Rust行動規範

コミュニティに参加する全員が尊守すべきルールです。 この文書はRustコミュニティに向けたものですが、本勉強会が大規模化するにあたり、参考にして独自の行動規範を導入する予定です。

はじめてのBillGレビューのこと

ビル・ゲイツは仕様書のレビューの際に以下のように語ったそうです。

「これをどうやって実現するのか本当に詳細に調べた者が誰かいるのか? たとえば、日付と時刻に関するあのたくさんの関数だ。Excelには日付と時刻の関数がすごくたくさんある。Basicが同じ関数を持つようになるのか? それが全部同じように動くようになるのか?」

私達は研究者ではありません。製品を設計する技術者です。理学ではなく工学に属するのです。 また論文に書いてあることや有識者の見解を鵜呑みにすることは実際の製品を作る上で危険です。「この技術は本当に動くのか？」という疑念を常に持ちましょう。 実際に技術に触れ、使ってみて、実装を読まなけれ真実は見えません。

ファスト＆スロー

人間の脳は素早い判断を行なうシステム1と熟慮して論理的に考えるシステム2があるそうです。 システム1ではなくシステム2で考えてから発言することを心掛けましょう。 (もっとも主催者自身がシステム1ばかり使ってしまう傾向があるのですが。。。)

協賛

• サイボウズ株式会社様: 会場の提供