SQAT® Security Report 2020年春夏号
株式会社ブロードバンドセキュリティ
エグゼクティブ・フェロー※
安藤 一憲
※取材当時の役職になります。
本稿はC言語のわからない方も、ゆくゆくは一般に「プログラミング言語」に適用できそうな話だと思って読んでいただきたい。ソフトウェアのバグで航空機が飛べなくなり、航空機メーカーの業績にも影響する昨今、ソフトウェアの品質管理はどの会社にとっても重要な課題である。すでにソースコード診断でセキュリティや品質を担保しているお客様も多い中、本稿ではエアバス社等で使用されているソースコードの検証ツールを紹介する。
C言語のソースコード解析ツールFrama-C
「ソフトウェアはソースコードに書いた通りに動作するのか？」という命題にはさまざまな答えがあろう。コンパイルエラーが出るもの、実行時にエラーで止まるものもある。ソースコードの脆弱性をチェックするツールはすでに弊社診断サービスにも使われているが、さらに精度を上げて厳密にやろうとすると、定理証明支援系と呼ばれるツールが存在する。
数理論理学では、正しい定理から演繹的に推論を積み重ねて得られる定理は正しいといえる。定理とは証明の与えられた命題である。したがって、ソースコードにおいて、命題に相当する「型」と証明に相当する「プログラム」が与えられていれば、そこから演繹的に積み上げていった型とプログラムは正しいセット、すなわち正しいソースコードといえることとなる。こうしたツールで最も有名なのはたぶんフランスのINRIA*1で開発されたCoqであろう。CoqはOCamlという言語で書かれており、「命題の証明」を積み上げていって、証明できたものに関してはOCaml言語でプログラムが抽出できる。しかしながら、我々の目の前にあるのは例えばC言語などのソースコードであり、プログラマは必ずしも抽象化された命題の証明を書きたいわけではない。数理論理学の言うように、命題が「型」であり証明が「プログラム」に対応するのであれば、C言語などのソースコードはそもそも証明の一部を成すはずであり、それが論理的に正しい(ソースコードの記述に不具合がない)かどうかをチェックできればことは足りる。つまりバグがないことを数学的に証明できればよい。
そこで登場するのが、同じフランスの原子力・代替エネルギー庁のCEA-LIST*2で開発された、Frama-Cである。Frama-CはCoqと同様にOCamlで書かれているが、Coqとは違って「C言語のソースコード解析ツール」であり、C言語(C99)のソースコード解析のためのプラグインの集成という体裁が取られている。ソースコードのチェックツールではあるが、そのプログラムを実行せずに実行エラーを検知したり、変数の取り得る値をチェックしたりできる。
簡単な使い方としては、C言語のソースコードをそのままEvaプラグインでチェックすることで、実行時エラーがないことを確認できる。これだけでも脆弱性を大幅に減らすことができるだろう。Frama-Cのサンプルサイトには、わざと問題があるgzip-1.2.4などのソースコードがサンプルで集められているが、Evaプラグインに食わせてみると、ソースコードに問題がある部分がオレンジ色のバルーンで示される。カバーできなかったコードは赤で表示される。動作するようになったプログラムを、これでチェックしてみるだけでも十二分に価値がある。
さらに、論理的あるいは数学的な検証を動作させるのに必要なのは、C言語のソースコード自体と、ソースコード中にコメントの形で追加するACSL(The ANSI/ISO C Specification Language)で記述された関数やループ構造の動作前提条件や仕様である。検証を受け持つのはWpプラグインである。この「Wp」という名称は1967〜69年にロバート・フロイド、エドガー・ダイクストラ、アントニー・ホーアらが提唱しその後改良が重ねられて来た「Weakest Preconditions calculus（最弱事前条件計算）」にちなんで名付けられている。Wpプラグインの下には、推論的プログラム検証プラットフォームWhy3を介して、前述のCoqやSMTソルバー*3(prover)を複数配置することができる。
ちまたではAIがバズワードになっているけれども、SMTソルバーはなかなか表には出て来ないものの、人工知能分野の成果物のひとつである。Frama-Cでデフォルト利用されるproverはAlt-Ergoであるが、前述のCoqやマイクロソフトリサーチ製のZ3や、スタンフォード大学とアイオワ大学等の共同プロジェクトでGoogle、Amazon Web Service、DARPA、Intel、NASA等のサポートを受けるCVC4など、著名なSMTソルバーを外部proverとして並列に利用することができる。Wpプラグインのマニュアルにも「Coq、Gappa、Z3、CVC3、CVC4、PVSその他の多くのproverがWhy3を介してアクセス可能」と書いてある。まだまだいろいろなものが使えるようだ。すべてのproverがWhy3の下に配置されたのは最新バージョン(20.0 Calcium)からのようで、ネット上で検索にかかる古いバージョンの説明文書は役に立たないが、Alt-ErgoやCoqやZ3やCVC4を直接知らなくても、それらを動作させて検証結果を得ることができる。動作させたいSMTソルバーはコマンドラインオプションで選択指定が可能だ。Frama-CはGUIを備えているがコマンドラインでも使える。実際に動く簡単なプログラムを書いて検証してみた。
試しにACSLで書くべき前提条件や仕様をまったく書かずに、これをframa-cのWpプラグインに食わせてみると、5件の固有性の検証(goal)が走り、そのうち1件しか正当(valid)と判定されなかった。検証されると緑のバルーン、検証失敗だとオレンジのバルーン、proverがタイムアウトするとハサミのアイコンが表示される。さすがにソースコードだけでは論理的な検証をするには情報不足のようだ。どの部分がどのような検証に失敗したのかは、GUIからドリルダウンできるようになっている。
GUIの表示を見るとswap()という関数が検証できていないようなので、その関数の直前にACSLで動作前提条件を加えて、もう一度frama-cのWpプラグインで検証してみる。加えたのは以下3行のACSL記述である。
すると、9件の固有性の検証が走りすべてが正当と判定された。Wpプラグインのマニュアルの例をもとに、実際に動くように書いたプログラムではどう検証されるのかを確かめるために用意したショボいプログラムではあるが、たった3行のACSL記述を加えただけで、人工知能分野の成果物である複数のSMTソルバーが動員されて「正当」という判定結果が出てしまった。ちなみにFrama-CのサイトにあるACSL-1.14のマニュアルは118ページしかない薄い本である。論理演算子なんかはすべてC言語と同じ。おかげで関数の仕様を書いたコメントだと思って読めば前提知識がなくてもなんとなく読めてしまう。ただし、まだ泣き所もあってstrlenやstrcpyなど文字列操作関数を記述するためのACSL側の道具立てが弱い。まぁ今後何らかの改善がされてくるだろうけれども、このWpプラグインでの検証は、Evaプラグインでの検証と違ってプログラムが実行できなくても、関数単位で実施できるのが味噌である。
このように論理的にソースコードをチェックする手法はFormal Method(形式手法)、あるいはLight-Weight Formal Method(軽量形式手法)と呼ばれる。Frama-CはCEA-LIST製のオープンソースツールで、ライセンスはほぼLGPLv2互換であり、商用ライセンスも用意されている。作っているのは重要インフラのど真ん中にいる人たちということになる。原子炉の制御プログラムが脆弱性だらけとかいう事態だけは勘弁願いたいという思いは世界共通であろう。実は2000年に策定されたISO/IEC 61508は電気・電子分野における「機能安全」と呼ばれる国際規格だが、この中で安全度基準(SIL)が4段階規定され、レベル2以上でこの「形式手法」の利用が推奨されている。ISO/IEC 15408はIT製品のセキュリティに関する国際標準で、Common Criteriaと言った方が知っている方は多いかもしれない。情報セキュリティの実現度は評価保証レベル(EAL)で７段階規定され、EAL5以上で軽量形式的な設計記述が要求され、EAL6で軽量形式手法による検証、EAL7で形式手法による検証が要求される。EAL5以上は「軍用や特殊用途向け」と言われていて、一般になじみがないのはそのせいかもしれないが、これら形式手法のツールが原子力関連や航空機関連で使われているのは、規格上の必然でもある。*4
Frama-C自体はmacOS上で開発されているようで、HomebrewとOCaml系ソフトウェアのパッケージ管理ツールopamを使うと、あっさり最新版(20.0 Calcium)がインストールできる。Ubuntuなどでもパッケージでインストールすることもできるが、Frama-C自体のバージョンが古く、最新の機能が使えず、プラグインの構成も異なるため、この記事を書くにあたってはmacOS上で動作する最新バージョンで動作確認している。
ソフトウェア信頼性向上とセキュリティ
Formal Methodの歴史は古いこともあって、Frama-C以外のチェックツールもいくつも存在している。マイクロソフトは、Windowsのデバイスドライバをマイクロソフトリサーチ製のSLAMというチェックツールで検証しており、そうすることでWindowsのセキュリティ向上に貢献しているという記述も見つかる。さらに検索してみると案の定、SLAMの精度とパフォーマンスを上げるためにZ3を使っているという情報も見つかる。*5
プログラムだけではなく、TLS 1.3のプロトコル安全性の検証にもFormal MethodなチェックツールProVerifやCoqが併用されたことはよく知られている。
さらに、 Amazon Web Serviceは、Leslie Lamport先生(LaTeXの原著者で現在マイクロソフトリサーチ所属)作のTLA+という形式手法を実現する言語で、サービスに使用するプログラムをチェックしている。たまに「似たような機能を実現しているプログラムなのに Amazon Web Serviceで使用しているプログラムにだけ脆弱性がない」という事象を目にすることがあるが、その理由のひとつはこのTLA+を含む検証の成果であろう。代表的なところでAmazon S3はこのツールによる検証を経て作られている。*6
クラウドベンダーのソフトウェア信頼性向上にこれらのFormal Methodな検証ツールが使われていることは一般には意外と知られていないが、航空機の安全性だったり、OSの安全性だったり、暗号化プロトコルの安全性だったり、クラウドサービスの安全性だったり、クリティカルなソフトウェアの安全性を向上させるために実際に利用されている。20年以上の歴史があるのに、これらが表にはなかなか出て来ないのは、これらのツールの多くが、プログラマから見ると飛びつきにくい代物にしか見えないことに起因していると思われる。しかし、世の中にはC言語プログラマに優しいFrama-Cのようなツールがあり、使う気になればいつでも使えるということは知っておいた方が良い。TLA+の仕様などを含めて、筆者の頭の中にあった「形式手法による検証はひたすら面倒くさい」という先入観は、Frama-Cであっさりと打ち砕かれた。実際エアバス社では、航空機を飛ばすためのプログラムを、すべてFrama-Cでチェックしていると聞く。これは作りたての実験的なものではなく、実戦で使われて何年もかけてアップデートされているツールである。検査の実現レベルは軍か特殊用途向けとされるEAL5に相当するけれども、ツール自体はなんとオープンソースである。
ソフトウェアの信頼性が、セキュリティと何の関係があるのかと思う方もおられるかもしれない。マルウェアがソフトウェアのバグや脆弱性を突いて感染を拡大することを見ればわかるように、ソフトウェアの信頼性を向上させバグの混入を防ぐことは、セキュリティの言葉に翻訳すると「攻撃者に付け込む隙を与えない」ことを意味する。理屈としては攻撃者だけではなく、ペンテスターに対しても付け込む隙がなくなる。攻撃者／ペンテスターが「脆弱性の１本釣り」であるならば、Formal Methodによるソフトウェア検証は「脆弱性の底引き網」に相当する。
現状を見てみると、せっかくFormal Methodでチェックされたコードで作られたサービスを利用していても、その上で自前の未チェックコードを動作させることで、セキュリティ上の問題が発生することは多々あるようだ。チェック済みのコードで構成されたクラウドサービス上で、自前のソフトウェアを併用して同レベルの安全性を確保しようと思う場合には、Formal Methodなチェックツールの利用は解のひとつになり得る。もちろん開発の初期段階から利用することで、最初から不用意なバグの混入を防ぐ使い方が推奨される。この手のツールはいわば究極の「シフトレフト」を実現するツールである。なお、本稿に登場させたSMTソルバーの調査過程で、Java、C++、Pythonなど、各言語のプログラムのチェックに利用できるツールの存在もいくつか目に入った。これは各言語でプログラムの信頼性を高めようと努力している人たちがいるという証左である。Formal Methodを使ってプログラムの信頼性を確保しようという試みはC言語とFrama-Cだけに限った話ではない。Formal Methodのチェックツールの裏で、SMTソルバーを使うこと自体がトレンドになっているようだ。それらも含めて今後の動きに注目したい。ただ、Frama-Cはそれらのチェックツールの中でも抜群にかっちょいい。
おわりに
実は本稿を書くにあたって与えられたお題は、「クラウドのセキュリティ」だった。多くの記事がそれを題材にしながら、 Amazon Web ServiceやMicrosoftやGoogleが地道にやっているソースコードレベルでのセキュリティ対策を取り上げてこなかった。大声で「シフトレフト」を叫んでいる方面からも、「形式手法」という声は聞こえて来ない。クラウドのセキュリティは 、 実は「軍や特殊用途向け」として一般には目が向けられてこなかった方法で担保されているのである。それを記事にするかどうかでも悩んだ。検索しても日本語で出て来るのはせいぜい国立情報学研究所の先生の研究プロジェクトくらいだ。しかも、クラウドベンダーの使っているツールを見ると、お世辞にもプログラマとの親和性が高いとは言い難い。多くは論理記号を使ってプログラムとは別に仕様を書き下すタイプのものだ。それらの取り組みを紹介するだけでは、開発の現場に対してあまり現実味がない。どうしたものかと思案しているところにレジリエンスな研究室の門林先生からFrama-Cの紹介があって、この記事になった。聞くと笑顔で作者が知り合いなのだと言う。さすがの知見の広さとタイミングの良さに感謝したい。クラウドに限らず、ツールが進化することでこういった技術が身近になり、形式手法であらかた脆弱性がつぶしてあるルータやIoT機器等の製品が増えてくることに期待したい。
株式会社ブロードバンドセキュリティ
エグゼクティブ・フェロー※ 安藤 一憲
※取材当時の役職になります。
学生時代からネットワーク／サーバ管理に30年以上従事。
古くはメーリングリストサービスから多言語での携帯サイト構築、携帯向けメール配信、ディレクトリハーベスティング対策、サーバ負荷分散、独自のDDoS対策などを考慮した規模の大きなサーバシステムなどを数多く設計構築。
1999-2006年まで8年間、InternetWeekのメール系チュートリアルの講師を勤める。
古くはsendmail (MTA)のエキスパートとして知られるが、現在は社外との共同研究やM3AAWG等国際会議に参加しつつ海外動向と先端技術担当を勤めている。
＜プロジェクト担当実績 (BBSecのみ)＞
・2005年 メールASP (AAMS)を企画設計構築し事業化
・2009年 CrackerDetect EXOCETを企画立ち上げ
・2012年 メールASPにアカウントの乗っ取り検知実装を主導
・2014年 Dovecot Pro/Scalityの導入を主導
・2015年 Splunk SIEM導入を主導
・2018年 AI搭載自動脆弱性診断サービスの監修
＜その他＞
・WIDEプロジェクト研究員
・奈良先端科学技術大学院大学等との共同研究窓口
・M3AAWGメンバー
