情報科学科の先輩に聞く!

現役学生OBインタビュー「先輩たちの仕事の原点」各界で活躍する先輩たちが教えてくれる“仕事の本質”

座談会トップへ戻る

論理学で企業に活躍

FireEye|平井洋一さん (情報科学科30期)
インタビュー年月日
平成28年 3月 15日
平井洋一 
2013年博士課程修了。萩谷研究室出身。独立行政法人産業技術総合研究所 セキュアシステム研究部門研究員を経て、2014年、FireEye社に、Formal Verification Engineerとして入社。
内藏理史、崔正行(情報科学科三年)
学部時代
情報科学科を選んだ理由を教えてください。

入試では理Iを受けました。興味をひかれるものがいろいろあり、たとえば、学部一年の頃は生物の実験室に遊びに行き、実験の真似ごとみたいなことをさせてもらいました。そのうち、だんだんとロジックや論理学めいたことをやりたいという思いが少しづつ自分の中でかたまっていきました。そうすると、数学科、情報科学科、文学部の哲学科の3学科が候補となりました。その中で、万が一挫折したとしても、残りの人生に引きずらないのが情報科学科と思い、学科を選択しました。

情報論理はどうでしたか。

情報論理は、他の人がすごく苦労しているのに、自分は不思議と、すんなりできました。人によって得意不得意が違います。情報科学科で、いろいろな課題をこなしていくと、どうしようもなく苦手なこともあるし、結構得意なこともあるし、そうでもないこともあると自覚できました。あと、周りと比べてどうかということもわかりました。たとえば、自分はC言語で簡単にコーディングができ、かなり得意なつもりでしたが、周りには自分よりもっと得意な人がたくさんいました。逆に自信があまりなかった数学関連の話では、周りの人がすごく苦労していることを自分は比較的簡単にこなせました。いろいろな分野に挑戦できるので、自分と同級生の能力を比較し、自分の強いところと弱いところが理解できてよかったです。

研究室は?

研究室は萩谷研を選びました。何がしたいのかが決まってなかったので、院試のときも、ロジックを使って面白いことがしたいですと言った記憶があります。一番ほったらかしにされそうな、一番枠のなさそうなところを選びました。

演習3の他の2つの研究室はどちらに行かれましたか。

須田研と細谷研に行きました。演習3は(萩谷研を含めて)その三箇所を回りました。演習3では、「たぶん行かないだろう」と感じていた研究室もあえて選択しました。多分行かないだろうと思っていても、実は演習3で三週間行ったら、ものすごく楽しいかもしれません。その楽しさを味わう機会がないと損すると思って、このようなところにも行ってみました。その先生がたまたま授業でしゃべることと、その先生の研究室でできる研究というのは違うことが多いと思います。演習3だと、研究していることを見たり、実際に手を動かしたり、体験したりできる。普段の授業だけで判断せず、演習3で体験するのは大事だと思います。

自分も参考にしてみます。萩谷研ではどういうことをしていましたか。

大雑把な興味としては、並行計算や分散計算で、参加者によって知っていることが違うような状況をうまく扱う枠組みがほしいと思っていました。論理式の恒真や充足可能性を問う問題がありますよね。卒論では、与えられる論理式を証明したい人と反対したい人がいる2人ゲームに翻訳して、証明したい人が勝ったら、翻訳元の論理式が証明可能だということをやろうとしました。そのとき、先のゲームをペトリネットにしました。これが私の卒論でした。何かいい定義ができたという話ではないが、他の人が見たことないことを見ようとしてあがいてたような気がします。自分の卒論と修論と博士論文を比べると、実は卒論が好きです。自分の興味の原点みたいのが現れている気がします。国際学会に出せた、論文になったということはないですが、やろうしていることに面白みがあるような気がします。
大学院の研究
修士論文は、認識論理の話でした。認識論理では、普通の論理式と違って、「XさんがAを知っている」という形の論理式が出てきます。これをネストすることもできて、もちろんネストした内側で、「ならば」を入れることもできます。「私が、「この人がAを知っている」ならば、「その人がAを知っている」ことを知っている」のような形の論理式を使う論理を認識論理と言います。ここには昔からたくさんの違う公理系があって、どのような性質を認めるのかは系によって違います。例えば、KAは「Aを知っている」という意味で、「KA → KKA」(「Aを知っている」ならば「「Aを知っている」ことを知っている」)で表して、これを公理として認めています。もう少し微妙な例としては、「(¬KA) → (K¬KA)」で、「Aを知らない」ならば、「「Aを知らない」ことを知っている」となるかどうかという話があります。これは人によって違いそうですよね。いろいろな系の中に、S5という公理系があります。これは「KA → KKA」も「(¬KA) → (K¬KA)」も両方認めます。S5の認識論理で、論理式に意味をつけようとすると、参加者全員の認識の状態をある瞬間でスナップショットを撮って、そこで意味を付けるしかない。認識論理を最初に開発したときは、人間の世界の認識を扱っていて、人と人が喋った直後に認識の状態のスナップショットをこの四人で撮りましょうと言っても構いませんが、計算機の世界だと、スナップショットを光のスピードで撮れたとしてもすごく遅いです。認識論理を使って分散計算のネットワークでつながっているたくさんの計算機の認識を扱おうとすると、スナップショットを光のスピードで撮れたとしても、どこで切ればいいかよくわからないです。そのようなふわふわしたところに議論をのせなければいけないので自分はS5のことがあまり好きではありませんでした。

修論でやりかったのは、そこまでの労力をかけてグローバルなスナップショットを撮らなくても、認識と論理式に意味がつくような論理の構築です。そのようなモチベーションで、直感主義論理の上に認識の要素をつけた論理を作りました。ここでは、上の「KA → KKA」が常に成り立つが、下の方の「(¬KA) → (K¬KA)」は常に成り立たないという新しい認識論理を作りました。新しい論理を作る時は、2つの論理式を計算的に比較しやすいなど、その新しい論理に客観的に良い性質があると証明しないといけません。

いい性質があるということを何か言わないといけないですか。

そうです。この修論の場合には、この認識論理を使うと、共有メモリの「Sequential Consistency」、つまり一貫性を記述しやすいことを主張しました。共有メモリのSequential Consistencyという性質は、どのコアからReadコマンドやWriteコマンドをどんな順番でたくさん出しても、すべてのReadコマンドとWriteコマンドが必ずある順番で一列に並んでいると思い込んだプログラムを書いてもいいということです。

問題を解く前に「コア1がAを知っていて」「コア2がBを知っている」ような状況で、 問題を解いた後に「実現してほしい状態」があるという課題を、「コア1がAを知っていて」「コア2がBを知っている」「ならば」「実現してほしい状態になる」と論理式で書けます。Sequential Consistencyを表す論理式を使って証明できるような「ならば」を実現できるプログラムがある事は分かっているので、「ならば」の形の論理式を証明できるかどうかで、この課題が解けるかどうかを判定することができます。この「ならば」は厳密には古典論理の「ならば」とは違うので、修論では、この「ならば」の意味もきちんと作りました。結構面白かった気がします。博士論文では、修論で論理を作り、これが直観主義に近い論理なので、ラムダ計算を付けてみました。修論の続きみたいな感じです。どうしてわざわざ博士課程まで行ったのかを説明すると、修論をまとめていて、構築した認識論理をきちんと研究として完成させたい、そのためにラムダ計算をつけたい、そのためにはもう少し時間がほしかったので、博士課程に行きました。

卒論や修論を書くのは大変でしたか。

どれも時間をたくさん使いました。卒論を書いているときに、結構夜遅くまで毎日やっていました。僕が居た部屋は、七号館の二階にある化学東館に行く廊下の一番化学東館よりの部屋です。七号館には外から中庭に抜ける通路がありますよね。僕の部屋の真下がその通路だったので、冬の夜中までいると寒かった。卒論を書いたときは、萩谷研の同期で一緒に残る人が結構多かったので、そんなに大変ではありませんでした。あと、テーマの決め方ですが、卒論はどうせ時間がないとわかっていたので、えいやと決めました。修論は、気になる問題を見つけようとして、論文をたくさん読むのに使った時間が長かったです。でも、最終的に自分が選んだテーマは、どの論文の続きでもありませんでした。あちこちに行き、話を聞き、色々な論文を読んでいるうちに、たまたまあの話とこの話が繋がるではないかと思いついたことがあり、その思いつきをもとに研究を始めました。ある程度量に触れることが大事だと思います。指導教員によってテーマの決め方が違うと思います。修論なら、たぶん良いテーマをもらい、それをきちんと仕上げることも多いと思います。僕の場合は、他の研究室にいけば、配属の時点で分野が大分絞られるので、テーマを選びやすそうだという事はわかっていましたが、それが嫌なので、萩谷研を選びました。だから、テーマを決めるには時間がかかりましたが、自業自得ですね。
研究所の研究員としての仕事
平井さんが産総研(産業技術総合研究所、AIST)に所属していたときの仕事を教えていただけますか。

セキュアシステム研究部門に配属されました。セキュアシステム研究部門は40人ぐらいの研究者がいて、その中にいろんな研究グループがありました。私が所属した研究グループは8人程度の研究者がいました。論理やモデル検査を使って、ソフトウェアの安全性と信頼性を高める研究をしている人たちが主で、あとはRubyのコミッターの人もいました。産総研は面白いところだとおもいます。誰がどの仕事をするのか役割分担が曖昧な気がします。産総研は、論文を書くだけでなく、企業ではできないような研究をするとか、国際規約を作るとか、本当にいろいろな仕事を担っています。それだけに、「この仕事は誰の分担」といったことを、上から決められることは少なくて、自分がやりたいことを頑張り、その結果、周りの人を引き込んでゆくことができさえすれば、必ずしも論文という形で成果をあげる必要はありません。たとえば、新聞に載るような仕事も成果として認められます。評価の軸が論文執筆という1次元ではなく、高次元で、面白い所です。僕は1年間でしたが、いろいろなことをかじってみました。論文を書いて、ワークショップで発表したり、企業にお金を出してもらっているプロジェクトでの研究をしたりしました。そうすると、打ち合わせが結構フォーマルになって、相手方がスーツ着用なので、こちらもスーツを着ていました。学生時代には経験しなかったことで、大学とは違う雰囲気で、面白かったですね。

僕自身は、今のソフトウェアの作り方に結構不満があります。きちんとやるところはテストをきちんとやりますが、悪意のある攻撃者の攻撃を防ごうとすると、テストでバグをいくらとっても、たとえ毎年毎年バグを十分の一に減らしても、どうせバッファオーバーフローなどがどこかで起こっていて、攻撃されます。型システムでも証明でもランタイムで防ぐのでも何でもいいので、人間が間違えても大丈夫にできるような仕組みが欲しいと思っていました。

産総研にいた頃は、データベースシステムを形式的に検証することを考えていました。研究の取っ掛かりとしては、文字列をパースしたりプリントしたりするところで間違いが入りやすいため、データを文字列にプリントする関数と文字列をパースしてデータに戻す関数のペアと、プリントしてパースしたら元に戻すという証明とを、全部組にして扱うライブラリを作りました。全部組にするライブラリを作るために、「リバーシブルプリントパーサー」と呼ばれる数字1文字のためのライブラリから始めて、小さいものから大きいものへ組み立てていくように作っていこうとしました。しかし、このようなことをやっているうちに、自分が求めるものはそれではないような気がしはじめました。今言ったようなリバーシブルプリントパーサーのライブラリを作るようなことは、それほどに難しいことではないのです。むしろ難しいのは、作ったものを広く使われるところまで持って行くことです。例えば、Webアプリケーションを作る人が間違えるとSQLインジェクションが起こりますが、それは安全にSQL文を作るライブラリが存在しないからではありません。実際、そのようなライブラリは存在します。例えばRuby on Railsならそれのおすすめの方法に従ってSQL文を作っていれば、SQL文を自分で書いたりしない訳で、穴になりません。しかし、SQLがただのアスキーの文字列なので、SQLを文字列として自分で作りたい人がどうしても現れてしまいます。そういう問題なので、良いライブラリを作りますというやり方が、適しているかどうかわからなくて悩んでいました。
海外に活躍
今はFireEyeという海外の会社にお勤めですが、どんな仕事をなさっているでしょうか。

今の仕事の肩書はFormal Verification Engineerで、形式検証をやるプロジェクトのために雇われています。検証する対象は小さいOSです。この仕事に応募して面接を受けたときに、「この小さいOSにはPOSIXインターフェイスはないですよね」ということを確認して、ないと言われて、「それなら証明を書けるかもしれない」と言った覚えがあります。小さい単純なOSのカーネルについて証明を書いて、形式検証するという仕事です。研究の内容と近いかというと、産総研での研究と多分方向は似ています。卒論修士論文博士論文はただのロジックの研究ですので、あまり関係ない気がします。

今の仕事は具体的にどのようにやっていらっしゃるのですか。

今の会社では、やることを自分で決める必要がありません。会社の偉い人がカーネルの形式検証に挑戦したいと考えて、そのために必要な人を募集して雇いました。だから、何をするのかが決まっていて、後はそれをどのぐらいうまくやるかという話なので、あまり悩む必要がありません。毎日の仕事はすごく単純で、家を9時20分に出て、歩いて職場に着くのは9時40分頃です。一日一回、みんなで朝集まって話し合って、まだこれが出来てないとか、次はこれをやらなければならないという相談をして、後はずっとそれをやっています。バージョン管理システムを使って、きちんとお互いのレビューをしながら証明を書いたり、プログラムを書いたりしています。昼は、同僚と一緒に食堂に歩いて行って食べることが多いです。

海外生活はどうですか。

ドイツは働くにはいいところです。みんな一日8時間しか働かないからです。ドレスデンでは、家賃が安いので割りと職場の近くに住むことができます。僕の最初の上司は、毎朝8時頃に来て、毎日4時頃に帰って行き、家で1時間ぐらいメールをチェックするというスタイルでやっています。上司がそれをやっていると、自分もそれができるので楽です。しかし、同じ会社でも、アメリカ本社では文化が違って、9時間や10時間働く人もいます。ドイツだと、それが許されないので、そのような人はいません。勿論、締め切り前に少し頑張って長くいることもありますが、その分、次の月曜日を休んだりします。働くにはいい話をもう1つ。それは有給休暇です。一年に何十日を、何に使ってもいい休みを必ず取ります。例えば、休暇中に病気になれば、有給休暇だった休みが病欠に変わって、病気の分遊べなかった分の休みをあとで取ることができます。

きちんと自由時間が確保されているという感じです。

働くにはいいです。国によって習慣が違うので、チャンスがあったら、出張や旅行などをする事を勧めます。特に海外で働く希望がある人は、インターンシップをやってもいいし、出張に行ってもいいと思います。地域によって、働き方や人の態度が違うので、知らないと損すると思います。なので、あちこちに行ってみるのは大事だと思います。

今ドイツの職場で何語で話していますか。

最初は完全に英語でした。ドイツ人が2人しかいなくて、あとはアルゼンチン人、イギリス人、日本人なので、英語でしたが、最近オフィスにドイツ人が増えてきて、彼らがドイツ語で話すことが増えてきたので、ドイツ語を勉強しています。しかし、大事な仕事の話は勿論全部英語です。
最後に
最後に何かアドバイスをお願いします。

自分の好き嫌いと、得意不得意を早めに知るのは大事です。人によって、好き嫌いが全然違うからです。僕はきちんと寝ないと生きていけないですね。一日8時間ぐらいきちんと寝たくて、かつ自由時間に好きなこともしたいので、一日に8時間しか働かないところにいると幸せですね。そうでなくて、力の限り日々勝負してその代わりにたくさん稼ぎたい人もいるでしょう。人によって好みが違うので、自分の好き嫌いを知っていることは重要です。いろいろなことをやると自然と自分の好き嫌いがわかるようになります。情報科学科の学生は課題でいろいろなことをやらされるので、そこできちんと好き嫌いを覚えて、将来嫌いなことをやるはめになりそうであれば、やらないですむようにするとか、味方を増やすとか、対応を考えられるようになると思います。

あと、普段会わない人に会うチャンスがあれば使ったほうがいいと思います。例えば、僕は修士の頃に、国家公務員試験を受けて、霞が関に面接を受けに行ったことがあります。そうすると、普段会わない人に会うから面白いし、役所の中を見るとみんな机の上に紙が山積みになっていて、昭和時代の映画のような雰囲気も面白かったです。行ってみないとわからないことや、会ってみないとわからないことはたくさんあるので、普段会えない人に会えるチャンスというのは、使った方がいいと思います。それで、気に入らないとか、好みではなければ、そのあと避ければ良いのです。特に、若いうちです。若くて、しかも情報科学科の学生だと、就活でも人気があるため、結構いろいろな人が会ってくれると思います。普段なら会えない人に会って話を聞き、この人と一緒に働きたいか働きたくないかを自分で決めていくのが、大事だと思います。