Blog

Tech

参加レポート

2016.9.24

ICFP及び関連イベント参加レポート – ICFP 2日目 –

κeenです。ICFPに参加するために奈良に来ています。これはICFP本体の2日目のレポートです。会場が奈良公園の中にあるので一歩外に出たら鹿がいます。

Our Jouney to Find Bugs in JavaScript Web Applications in the Wild

Talker: Sukyoung Ryu

2日目のキーノートはJavaScriptの検証器を作っているryuさんから。これまでの自分のキャリアの話を交えつつJavaScriptの検証器の変遷を話しました。

飛び跳ねたり"In The Wild v(._.)v" したり楽しそうに喋ってました。

因みにJavaScriptについては"i don’t like javascript"とのこと。まあ、ICFPでの講演なのでちょっとバイアスの掛かった発言が多いですね。

学部生の頃はCでポインタに苦しめられました院生の時に使ったSMLは形式的に定義されてるしSML/NJの静的解析器が素晴しくて感銘を受けて、OCamlは標準がなくてちょっと残念。因みに「こういうちゃんとした言語を経験したならJavaScriptを扱わされてつらいんじゃない？」とよく言われるそうですが、そんなことはなく"I’m enjoying"だそうでです。

ハーバードに言ってからはアセンブリの世界に飛び込んで "new world in debbuging" を経験しました。

次は Sun MicrosysetmでJava/Scalaを経験しましたFortressの話、Guy Steeleの話、言語設計、Javaの型検査器の仕事は3年掛かったけどScalaは1年で終わた話、などなど。「Guy SteeleはSchemeやLispにも明るかった」って言ってて、うんそりゃそうだよね。って思ってました。

KAISTに戻った後はJavaScirptの検査器に従事しました。Webで使われている技術なので色々な所で使われています。

jQueryのサブセットを見せて"Show how bad it is"って言ってました。関数の即時呼び出しで名前空間を作ってるだとかそこからexportするのにグローバル変数に触ってるだとか extend 関数で実行時にjQueryオジェクトを拡張してるだとか。

なんでJavaScriptでやってるかというと様々なところ、Samsung Smart TVとかでも使われているので影響力が強いのと"almost freestyle"なのでちゃんと面倒見てあげないといけないとのこと。なんかこの辺で跳ねてました。かわいい。

あと、空港のディプレイがundefined undefined undefinedになってる画像を見せて笑いを取ったり。

あとは実世界のアプリケーションについての話もしてました。JavaScriptを触ったらすぐに「これが現実か」ってなるそうです。

"Web Application In The Wild v(._.)v"

JSにはHTML/DOMがあったりプラットフォームの多様性があったりダイナミックだったりしますからね。アカデミックな所で使われるのはせいぜい 10K行程度のJSですがFacebookとかだと1M行くらいになるそうです。

さて、検査器でなにを検査するかというと、健全性の検査は停止しません。バリデーションや型エラー/脆弱性の発見などだそうです。

最初の検査器はコントロールフローグラフベースです。一応サブセットの検査は出来るものの産業界からはサブセットじゃ意味がないなんか言われたそうです。

さて、次はWebアプリケーションのJSの検査です。実用的にDOMをモデリングしたそうです。

その次はJavaScript Web Application in the Wild v(._.)v です。 Web APIやWeb IDLとの整合性の検査など。ここでJSのdisが結構多かったです。引数がundefinedになるだとか云々。巨大なJSのコードをどうやって検査するかの問題だとかも話してました。なんか非健全なコードでも実用上問題がないとか云々。

静的にJavaScript Web Application in the Wild v(._.)vをしようと思うと、900くらいファイルがあって絶望したけどよくよく調べてみたらテストとかロケールファイルとかが多くて実際にブラウザに読まれるのは1ファイルだけだったとか。

そしていよいよ実アプリケーションを解析してみました。Wikipediaを解析したら === を使うべきところで == を使っているバグを発見して、論文を書いたそうです。因みにその件についてWikipediaに載ったそうです。

そこで使った検査器については github: sukyoung/safe comming soonとのこと。

さて、JSはプラットフォーム毎にデバイスAPIを持っています。つらいですね。さらにはWebViewみたいにJavaとの連携があるやつも考え始めたら大変です。 Androidのマニュアルにも"use with extreme care"とあるそうです。しかしそのextreme careを肩代わりするのが検査器なので頑張るとのこと。 gihtub: wala/WALAという解析フレームワークがあるそう。MethodNotFoundだとかIncompatibleTypeConversionの発見だとか、あるいはプライベートなデータが漏れてないかの検査だとか。

そして巨大なコードの解析の話。Our Jouney with JS Web Apps in the Wild。グローバルな解析だとスケールしないのでどうにかする必要があります。こういうのは関数型言語のコミュニティで色々と議論されてきたのでそれが助けになったそう。アルゴリズムについても複数(CFA2, PDCFA, AAC, P4F)、部分検査とその合成についても色々と知見を借りたとか。

で、まだ旅はまだ半ばでまだ関数型コミュニティからの助けが必要とのこと。"Analyze crazy language with crazy techneque"。サムスンのSmart TVがトップシェアを誇るので脆弱性あったらまずいよねーとか。

"it’s hard to change existing system but extend is possible"。これについてはGuy Steeleがjavaのバイトコードに型を付けるべきだと言ったのに対してMartin Oderskyがそれじゃ産業界に受け入れられないから既存の物は変えるべきではないといったという話をしていました。

ということでJavaScript Web Application in the Wild v(._.)vを解析する話でした。

A Glimpse of Hopjs

Talker: Manuel Serrano, Vincent Prunet
Paper: A glimpse of Hopjs

普通、Webアプリケーションはサーバサイドとクライアントサイドに分かれるけど1つのシステムで全部賄いたいよね、そいういの作ったよ、というもの。

JSもHTMLもサーバサイドコードもクライアントサイドコードも1つのシステムで書けます。PHPやNode.js, react.jsなんかを引き合いに出してました。

;; a single language
H ::= JavaScript
  | <tag> .. ${H} ... </tag>
  | service[id] (id, ...){H; ...}
  | ~{H} ; client side program
  | ~${H}

;; a single language

H ::= JavaScript

| <tag> .. ${H} ... </tag>

| service[id] (id, ...){H; ...}

| ~{H} ; client side program

| ~${H}

記法とかはreact.jsに似せているよう。

サーバ記法とクライアント記法があって、サーバ記法の中にクライアント記法を書いたりなんたりと複雑なことも出来ます。デモではクライアント記法の中にクライアント記法を書いてボタンを押す度に新たなボタンが増えるやつを書いてました。

あとはクライアント-サーバだけでなくサーバ-サーバ間の通信の話なんかもしてました。

Experience Report: Growing and Shrinking Polygons for Random Testing of Computational Geometry Algorithms

Talker: Ilya Sergey
Paper: Experience report: growing and shrinking polygons for random testing of computational geometry algorithms

これはExperience report、つまり事例紹介です。

「多角形って育ったり切れたりするんだぜ」から始まりました。

やったこととしては学部2年生の1週間のグループ課題として適切な難易度の適切な教材が欲しくてそれを用意したというお話。

実際に用意したのは「美術館全体に目が届くように警備員を配置するにはどこにどれだけの警備員を配置すればいいか？」という問題。

例えば

+------+
|      |
+---+  |
    |  |
+---+  +--+
|         |
+---------+

+------+

| |

+---+ |

| |

+---+ +--+

| |

+---------+

のような形なら

+------+
|    x |
|      |
+---+  |
    |  |
+---+  +--+
|    x    |
+---------+

+------+

| x |

| |

+---+ |

| |

+---+ +--+

| x |

+---------+

のように2箇所に配置すれば見渡せそうです。実はこれNP完全な問題。なので最適解を求めるのはつらく、ヒューリスティックが必要になるのでそれで競わせようといもの。

で、運営側としては

様々な特徴のある問題の生成
オンラインでフィードバックする添削システム
それら全てが動くことの確認

が必要で、Scalaを使って作ったとのこと。確か準備期間が2ヶ月とかだった気がします。

1.の様々な特徴のある問題の生成については、とりあえず（凸とは限らない）複雑な多角形を用意する必要があります。手法は基本的な多角形を用意してそれらを回転、拡大/縮小して貼り合わせてどんどん大きくしていったとのこと。

動作確認はScalaCheckを用いて行なったとのこと。その過程でJoe-Simpsonのアルゴリズムのバグを見付けたりCGAL(Computational Geometry Algorithms Library)の不自然な挙動を見付けたりしたとのこと。

Corrections to Lee’s visibility polygon algorithm | SpringerLink

次はshrinkingの話。上記のようにバグを見付けたら、simplest caseを作りたいので多角形を切って、簡単にしていきます。これは作成と逆の手順、つまり、どこかに貼り付けられた多角形を剥がしてあげればその子の多角形ごと切り落とせます。

最後に実際に走らせてみた話です。

94名、24チームが参加して5日間で2360回の提出がありました
サーバは24時間5日間ずっと稼働しました。特にクラッシュもなく、バグが見付かった時もサーバダウンなしにデプロイ出来たとのこと。
ほとんどのチームは教科書のアルゴリズムを多少改良したものだったとのこと
優勝チームは問題をSet Cover Problemに還元してそれを線型計画法で解いたとのこと。すごい。

Think Like a Vertex, Behave Like a Function! A Functional DSL for Vertex-Centric Big Graph Processing

Talker: Kento Emoto, Kiminori Matsuzaki, Zhenjiang Hu, Akimasa Morihata, Hideya Iwasaki
Paper: Think like a vertex, behave like a function! a functional DSL for vertex-centric big graph processing

高速な大規模グラフ処理ライブラリにGoogleのPregelというのがありますが、命令的で気に食わないのでFunctionalなDSLを作ってそれでPregelを叩けるようにしたよ、というお話。 CF Pregel: a system for large-scale graph processing

細かい記法を変えただけでなく、例えば到達可能ノードを調べるのには隣接ノードに色を塗っていって塗れるノード全てに色がついていたらループ終了、のようなアルゴリズムになるかと思いますが、それだとメインの計算と終了判定が密結合してしまっているのでよくないのでそれをFixpointと捉えて計算と終了条件を分離した、などの話もありました。

今回作ったFregelはpregelにコンパイルする他純Haskellなインタプリタもあるとのこと。手元で試すのに便利そう。

で、パフォーマンスについては素のPregelに比べて大分遅くて、メッセージのやりとりが多いよう。あとは終了条件がlocalだったのがglobalなpropertyになってるのも関係するのかな？

Datafun: A Functional Datalog

Talker: Michael Arntzenius, Neelakantan R. Krishnaswami
Paper: Datafun: a functional Datalog

要点は型レベルで単調性やfixpointを追えるdatalogインスパイアドなDatafunという言語を作ったというもの。

文法的に単調な関数と離散な関数を区別していたりそれらの合成からまた単調性を導出したり、あとは型がただのSetではなくてPartially Ordered Setだったり（さらにSemiLatticeな型もある）します。

Datfunが生きる例としてリレーションの合成だとか到達可能性だとかCYKパーシングだとかを挙げていました。l

Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong)

Talker: Eric L. Seidel, Ranjit Jhala, Westley Weimer
Paper: Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong)

型エラーが起きたプログラムはどこかが間違っていますが、どこで問題が起きるのかは初心者にはぱっとは分からないという問題。それに対してとりあえずそれっぽい入力を食わせてみて、不整合が起きた部分を示してあげることで分かりやすくしようというのがモチベーション。

モチベーションが分かりやすくしよう、なので色々と苦心していて、出来る限り本質的な部分で不整合が起きるようにしたり問題が起きるまでのステップ全部を見せるのではなくて重要そうな部分を見せるようにしたりしていました。あとはWebUIも作ってたり。

実際に学生でABテストをした結果、有為にこのツールを使わせたチームの方がデバッグ力が上がったそうです。

Automatically Disproving Fair Termination of Higher-Order Functional Programs

Talker: Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi
Paper: Automatically disproving fair termination of higher-order functional programs

用語が色々と多いので難しい内容。普通の停止性はどのような実行でも停止することですが、Fair-terminationは’fair’な実行は全て停止することを指します。 Fairな実行はイベントAが起こるなら同じくらいの頻度でBも起こること。直感的には悪いことAが何回か起こるけど必ずいつかは嬉しいことBが起こる、ようなものです。例えば標準入力から乱数が与えられて1が出たら停止するようなプログラムとか。

で、それをdisproveなのでfairな実行であるにも関らず、停止しないケースを捜す問題。それを高階な関数型言語でやる、と。なんか高階モデル検査で重要らしく、ω-regular temporal property（日本語に直すとω-正規時相性？）や線型時相論理の検査はfair-terminationの検査問題に還元出来るとのこと。

こんな感じとのこと。

[fairness constraint]   [functional program]
      |                         |
      V                         V
[reduction to higher order model checking]<--------(Abstraction Types)
      |                         |                        ^
      V                         V                        |
[Tree Automaton]        [Tree Geretate Program]   [predecate discovery]
      |                         |                        ^
      V                         V                        |
      [Higher Order Model Checking]----(rejct)--->(counterexample)
         |
         V
      (accept)=disproved

[fairness constraint] [functional program]

| |

V V

[reduction to higher order model checking]<--------(Abstraction Types)

| | ^

V V |

[Tree Automaton] [Tree Geretate Program] [predecate discovery]

| | ^

V V |

[Higher Order Model Checking]----(rejct)--->(counterexample)

(accept)=disproved

分岐の枝が一杯あると扱いづらいのでexist-nodeとかforall-nodeを導入した抽象木に一旦変換した後にモデル検査をしているようです。

あとはモデル検査で反例があったら反例がinfiniteなので扱いに困ったので工夫しただとか。

ということで健全ではあるが完全でないアルゴリズム自体は(入力がfair-terminatingな時に)停止しない手法を開発しました、と。停止しない問題はfair-terminationの検査器はあるのでそれを一緒に走らせればよい、とのこと。しかし完全ではないのでnon-fair-terminatingな場合に困りそうな気がするんですが大丈夫なんですかね。

実装についてはMoCHiを拡張して、高階モデル検査にはHorSatPに反例生成器を乗っけたと。あとはZ3も述語抽象と述語発見のバックエンドSMTソルバとして使ったとのこと。

この辺に詳しい人がいないのか珍しく質問者がいませんでした（座長仕事しろよ）

Higher-Order Ghost State

Talker: Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
Paper: Higher-order ghost state

やりたいことは明確で、Rustの安全性を証明したい。RustBeltというプロジェクトからきているようです。 Rustは高階関数を持ちつつもメモリアロケーションやデータレイアウトを制御出来、線形型(アフィン型なんだけどなぁ)やリージョン推論、並行性を持つので証明に使うロジックもちゃんと準備しないといけないとのこと。

Rustの証明のために並行分離論理に高階量化子とCustom ghost state両方を入れたいのですが既存の拡張ではやりたいことが満足に出来ないので作ったというもの。Irisというロジックがベースになっているそう。

高階量化子はいいとして、Ghost Stateというのはプログロムの中には現れないけど証明の中で必要になる状態のことだそうです。そしてハイレベルなGhost Stateを表すには部分可換モノイドを使うと具合がいいらしいです。

んで、今回やりたいのはGhost Stateの中に高階分離論理述語を入れたい。ので、部分可換モノイドを拡張したCMRAという代数的構造を開発してHigher-Order Ghost Stateを可能にしたという内容。因みにCoqで形式化もしてあるとのこと。

モチベーションとかは単純明快で分かりやすいのですが周辺知識がなくて追っていけないのが悔しい。

Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data

Talker: Jesper Cockx, Dominique Devriese, Frank Piessens
Paper: Unifiers as equivalences: proof-relevant unification of dependently typed data

なんかすごそうだけどやっていることがよく分からなかったやつ。依存型のユニフィケーションには問題があって、どうにかしたいけど型理論もclassical、Syntactic、HoTTと一杯あるし汎用的なフレームワークを考えたい。突き詰めていくとユニフィケーションが返す単一子に問題があって、ただ単一化子を返すんじゃなくてユニフィケーションのエビデンスを等価性の形で返してあげるとよい、ということかな？等価性を差し替えることで様々な理論に対応出来ると。

Elaborator Reflection: Extending Idris in Idris

Talker: David Christiansen, Edwin Brady
Paper: Elaborator reflection: extending Idris in Idris

大抵の言語はリッチな表層言語からコア言語に変換する時にElaborateのプロセスを挟みますが、そのElaboratorをユーザからも見えるようにしたよ、というもの。

Elaboratorはユニフィケーションを持っているので証明とかも使えるそう。

今回の論文ではIdrisに %runElab という拡張を入れて遊んでるみたいです。

Partial Type Equivalences for Verified Dependent Interoperability

Talker: Pierre-Evariste Dagand, Nicolas Tabareau, Éric Tanter
Paper: Partial type equivalences for verified dependent interoperability

依存型と単純型をいったり来たりする話。Coqで依存型を使って書いたコードをOCamlにextractするとSEGVが起きる例を示しつつどうにかしたいよね、という話をしていました。

型同士に部分等価性を定義してあげて、両者を行き来出来るようにしてました。あとはList aからVec n aに変換するのにコンストラクタを辿って頑張ってたり。変換に失敗したらOptionにするか実行時例外にするかを選べるそう。

Depedent Iteroperabilityの話ということでDICoqというライブラリとして実装しているそうです。

http://coqhott.github.io/DICoq

Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory

Talker: David Darais, David Van Horn
Paper: Constructive Galois connections: taming the Galois connection framework for mechanized metatheory

プログラムの検証の分野で抽象解釈というのがあるそうです。普通の証明ともまた違うよう。その分野でガロア連結というのが使われるそうです。抽象解釈そのままだと公理の定義が必要で、公理があるということはそこで計算が止まってしまいます。クライスリガロア連結というのを使うと公理は必要なくなりますが、それでもまだ計算が途中で止まってしまいます。で、この論文では計算も出来る構成的ガロア連結を作りました、というもの。

An Abstract Memory Functor for Verified C Static Analyzers

Talker: Sandrine Blazy, Vincent Laporte, David Pichardie
Paper: An abstract memory functor for verified C static analyzers

またフランス人英語でスライドの字が薄くて伝わりにくかったやつ。INRIAがあるしフランス人英語にも馴れないといけないなーと思う今日この頃。

さて、やっていることは凄くて、Cのメモリの扱いやポインタ演算、配列、構造体、共用体などを含むプログラムがランタイムエラーを起こさないことを静的解析するツールを作って、Coqで証明したとのこと。

その他

ICFPのプログラムレポートとかICFPのプログラミングコンテストのレポートとかがありました。一位のチームが圧倒的でした。

その後はBanquetがありました(忘れてましたが初日にもレセプションがありました。おいしい日本酒と天ぷらがあったので一杯やってたら「20代とは思えない」って言われました。)。偶々今回のICFPのプログラムチェアをしている住井先生と同席したので運営の話を聞いてました。因みに住井先生はICFPくらいなら発表の内容はほとんど分かるそうです。POPL（プログラミング言語の基礎理論のカンファレンス）は半分くらい怪しいそうです。POPL怖い。

SIGPLAN Awardsもあって、

Most Influential Paper AwardsにSimon Peyton JonesさんたちのSimple unification-based type inference for GADTs(2016)が
Programming Languages Achievement AwardにSimon Peyton JonesさんのGHCが
Robin Milner Young Researcher AwardにStephanie Weirichさんが
Distinguished Service AwardにPhil Wadlerさんが

選ばれてました。おめでとうございます。ワドラーさんは「モナドはただの自己関手の圏におけるモノイド対象だよ。何か問題でも？」の人ですね。

最後に

折り返し地点にきました。まだ長いので頑張ります。

Author

admin