Webアプリケーション開発プロセスをセキュアに ―DevSecOps実現のポイント―

Share

DevSecOpsは、「DevOps」―開発(Development)チームと運用(Operations)チームが相互協力しながら品質を向上させ続けるサイクル―の一環に、セキュリティ(Security)を組み込むことで、トータルコストを低減しつつ、さらなるクオリティ向上を実現する手法です。セキュアなWebアプリケーション開発プロセスの実現のためには、この考え方が重要です。しかし、多くの企業・組織にとって、DevSecOpsの実現には様々な課題があるのが実情です。 本記事では、開発の現場担当者が感じている課題を整理したうえで、セキュアなWebアプリケーション開発にむけて、どのように取り組むべきかについてご紹介します。

OWASP Top10に新たな項目

2021年9月、「OWASP Top 10 2021」が発表されました。Webアプリケーションセキュリティに関する最も重大な10項目のリスクを取り上げたものです。前回発表された2017年版(OWASP Top 10 2017)から4年ぶりの更新となります。

※OWASP(Open Web Application Security Project)…Webアプリケーションセキュリティに関する国際的コミュニティ

2017年版Top 10の各項目は、2021年版ではそれぞれ順位を上げ下げしつつ、一部統合されて7項目となり、完全に消えたものはありませんでした。そして、新たなカテゴリが3項目追加される形で計10項目となりました。

OWASP Top 10 – 2021

A01:2021 –アクセス制御の不備
A02:2021 –暗号化の不備
A03:2021 –インジェクション
A04:2021 –NEW セキュアでない設計
A05:2021 –セキュリティ設定のミス
A06:2021 –脆弱かつ古いコンポーネントの使用
A07:2021 –識別と認証の不備
A08:2021 –NEW ソフトウェアとデータの整合性の不備
A09:2021 –セキュリティログとモニタリングの不備
A10:2021 –NEW サーバサイドリクエストフォージェリ(SSRF)

NEW」は2021年度版で追加された項目
https://owasp.org/Top10/ より弊社和訳

新設された3項目のうち2つが、システム開発のプロセスにかかわる内容に焦点を当てています。

● セキュアでない設計(Insecure Design)
  ポイント:設計における管理策の欠如、ロジックの検証が不十分である等
  推奨対策:シフトレフトによる開発ライフサイクルの実践 等
● ソフトウェアとデータの整合性の不備(Software and Data Integrity Failures)
  ポイント:安全でないデシリアライゼーション、
  信頼できないコンポーネントの利用、CI/CDパイプラインにおける検証不備 等
  推奨対策:データの整合性チェック、コンポーネントのセキュリティチェック、
  CI/CDのセキュリティ対策

※シフトレフト…開発工程のより早い段階でセキュリティに関する問題に対処する、ソフトウェアの開発や運用の考え方

ここで推奨対策例として出てきた「シフトレフト」と「CI/CDのセキュリティ対策」はアプリケーション開発プロセス手法である「DevSecOps」実現に欠かせません。

アプリケーション開発における「DevSecOps」

DevSecOpsは、「DevOps」―開発(Development)チームと運用(Operations)チームが相互協力しながら品質を向上させ続けるサイクル―の一環に、セキュリティ(Security)を組み込むことで、結果的にトータルコストも削減でき、サービスの価値をさらに向上させる手法です。

DevSecOpsとシフトレフト(Shift Left)について、詳しくは過去記事「前倒しで対処 ー セキュリティを考慮したソフトウェア開発アプローチ「シフトレフト」とはー」をご覧ください。

“セキュリティ”が組み込まれていないと…

DevSecOpsにおけるシフトレフト

DevSecOps実現のためには、「シフトレフト」の考え方が大切になります。セキュリティを開発の最終段階で対応したのではすでに遅く、開発プロセスの全フェーズにおいて常にセキュリティ上の課題を先取りして解決しながら進めることが、テストやリリースといった最終段階での手戻りを防ぎ、結果的にトータルコストの削減と品質の向上に寄与します。

DevSecOpsにおけるCI/CDのセキュリティ対策

“Sec”が入らないDevOpsにおいては、設計・実装を小さな単位で素早く繰り返し実行していく手法(アジャイル開発手法等)が一般的ですが、このスピード感をサポートするのが「CI/CD」です。

CI/CDの説明図

CI(Continuous Integration)は継続的インテグレーション、CD(Continuous Delivery)は継続的デリバリの略です。アプリケーション開発におけるコード、ビルド、テスト、デプロイといった各作業を自動化して継続的にサイクルを回せるようにする仕組みを指します。オンプレミスでもクラウド上でも展開可能で、CI/CDを提供する様々なツールやサービスが提供されています。

ただし、CI/CDはセキュリティ上のリスクにもなりえます。CI/CD環境に脆弱性が潜んでいて不正アクセスされるようなことがあれば、そこを発端に組織全体が危険にさらされる恐れもあるのです。このため、DevSecOps実現のためには、CI/CDのセキュリティ対策が不可欠です。

セキュアでない設計によるリスク

では、シフトレフトが意識されていない、セキュアでない設計にはどのようなものがあるでしょうか。ユーザの認証に用いられる情報がIDと生年月日である場合、生年月日は他者が容易に知りうる情報なので、本人確認の仕様としてはふさわしくないことがわかります。例えば、補助金の申請システムにおいて、申請者の本人確認や申請内容の検証が甘いために容易に複数の虚偽申請を許してしまうようでは、実用に耐えるとはいえないでしょう。

こうしたセキュリティについて考慮されていない設計は、弊社の脆弱性診断でも相当数検出されています。アカウントロックアウトが設定されていない、Webサーバからのレスポンスにクレジットカード番号のような重要情報が含まれている、個人情報が暗号化されないまま送信されている、といった例は多々見受けられます。放置しておくと、個人情報や機密情報の漏洩を引き起こしかねません。

プライバシーマーク推進センターによって報告された、2020年度「個人情報の取扱いにおける事故報告集計結果」によると、誤送付や紛失・盗難によらない情報漏洩のうち、プログラムやシステムにおける設計・作業ミスを原因とするものは102件あったとのことです。大した件数ではないようにも見えますが、インシデント1件あたりの漏洩件数が増加傾向にあるとの報告もあり、影響の大きさに注意が必要です。また、これらはあくまで報告があったものだけの数ですので、セキュアでない設計によるアプリケーションが人知れず稼働したままになっている危険性は大いにあるでしょう。

一般財団法人日本情報経済社会推進協会(JIPDEC)プライバシーマーク推進センター
2020年度「個人情報の取扱いにおける事故報告集計結果」(2021年10月15日更新)より

CI/CDパイプラインにおける検証不備によるリスク

コードカバレッジツールへのサイバー攻撃の概要図

CI/CDパイプラインに起因するリスクの方はどうでしょう。2021年にあるインシデントが発生しました。ソースコードのテスト網羅率を計測するコードカバレッジツールがサイバー攻撃を受けた結果、このツールを使用していた国内企業のCI環境に不正アクセスされ、重要情報を含む1万件以上の情報漏洩につながったというものです(右図参照)。

自動化、高効率化ツールによる利便性を享受するためには、そこに係るすべてのツールや工程におけるセキュリティチェックを行う必要があるのです。

DevSecOps実現を阻む壁

さて、安全なWebアプリケーション開発の重要性は認識できているとしても、実現できなければ意味がありません。とはいえ、DevSecOps実現には、多くの企業・組織において様々な障壁があるものと思われます。今回は主な障壁を「組織」と「技術」のカテゴリに分類し、それらの問題点および解決の糸口を考えていきます(下図参照)。

DevSecOps実現のためにできること

DevSecOpsに特化したガイドラインが存在しないというのも、対応を難しくしている要因の1つかもしれません。とはいえ、Webアプリケーション開発におけるセキュリティ対策の課題を考慮すると、鍵となるのはやはりシフトレフトです。シフトレフトを意識しながら、システム開発プロセスに組み込まれたセキュリティ対策を実践する例として、以下のようなイメージが考えられます。

Webアプリケーション開発におけるセキュリティ対策実施の背景には、Webアプリケーションの規模や利用特性ばかりでなく、開発組織の業務習慣や文化等、様々な事情があることでしょう。例えば、セキュアコーディングのルール整備やスキルの平準化が不十分という課題があれば、まずは現場レベルでそこから取り組んでいくといったように、信頼されるWebアプリケーション構築のために、少しずつでもDevSecOpsの実装に近づけていくことが肝要です。

【参考】システム開発プロセスのセキュリティに関するガイドライン・資料等

●NIST
 Security Assurance Requirements for Linux Application Container Deployments
 https://csrc.nist.gov/publications/detail/nistir/8176/final

●OWASP
 OWASP Application Security Verification Standard
 https://github.com/OWASP/ASVS

●内閣サイバーセキュリティセンター(NISC)
  情報システムに係る政府調達におけるセキュリティ要件策定マニュアル
  https://www.nisc.go.jp/active/general/pdf/SBD_manual.pdf

セキュリティレポート資料ダウンロードページボタン

年二回発行されるセキュリティトレンドの詳細レポート。BBSecで行われた診断の統計データも掲載。

サービスに関するお問い合わせボタン

サービスに関する疑問や質問はこちらから
お気軽にお問合せください。


SQAT® Security Serviceページへのバナー

BBSecコーポレートサイトへのバナー



Share

前倒しで対処 ー セキュリティを考慮したソフトウェア開発アプローチ「シフトレフト」とはー

Share

セキュリティにおける 「シフトレフト(Shift Left)」 とは、より早期の段階でセキュリティに関する問題に対処する、ソフトウェアの開発や運用の考え方です。元々この概念は仕様を満たしているか等の検証に対するソフトウェアテストのジャンルで使われていた言葉ですが、近年セキュリティの世界で注目されています。

ソフトウェア開発の主要工程である「設計」→「開発」→「検証」→「運用」の各プロセスは、計画書や図などで、通常左から右に向けて記載されます。図の左側(レフト)、すなわち時間軸の早い段階で脆弱性を作り込まない対策を施した開発を行えば、セキュリティリスクを低減させるだけでなく、品質向上、期間短縮、トータルコスト低減などの効果があります。

セキュアなWebアプリケーション開発を推進する国際NPO「OWASP(Open Web Application Security Project)」もシフトレフトを推奨しており、Googleをはじめとする先進IT企業ではこの考え方を採用したシステム開発を行っています。

「シフトレフト」と「セキュリティ・バイ・デザイン」「DevOps」「DevSecOps」との違い・関係

シフトレフトと関連する言葉に、「セキュリティ・バイ・デザイン」「DevOps(デブオプス)」「DevSecOps(デブセックオプス)」などがあります。

「セキュリティ・バイ・デザイン(SBD:Security by Design)」とは、開発の企画・設計段階からセキュリティを考慮することです。

「DevOps(デブオプス)」は、ソフトウェア開発チーム(Developer)と運用チーム(Operations)が互いに協力し合い、ソフトウェアとサービスのクオリティを向上させます。「DevSecOps(デブセックオプス)」は、開発チームと運用チームに、セキュリティチーム(Security)が加わり、セキュリティを含めトータルコストを低減しつつ、さらなるクオリティ向上を実現する仕組みです。

セキュリティ・バイ・デザインは概念、DevSecOpsは体制運用、そしてシフトレフトは工程管理の考え方ですが、いずれも、事故やトラブルが起こってから、あるいは脆弱性が見つかってから、といった事後対応のセキュリティ対策ではなく、事前対応、すなわち前倒しで実践する点で一致しています。

シフトレフトによって向上する品質

たとえば、ビルを建てた後になってから、建物の基礎部分に問題が見つかったら改修は容易ではありません。また、社会的な信頼も大きく損なうことでしょう。ソフトウェアも同じで、問題発見が早いほど、改修に必要な労力、費用、時間は少なくてすみますし、信用失墜の危険性も軽減できます。

リリース直前の脆弱性診断でWebアプリケーションに脆弱性が発見されたら、手戻り分のコストがかかるだけではなく、リリース日の遅れや、機会損失の発生を招き、ステークホルダーのビジネスにまで影響を及ぼしかねません。シフトレフトの考え方でセキュリティに配慮しながら開発を進めれば、こうしたリスクを低減でき、ソフトウェアの信頼度が高まります。

シフトレフトによるトータルコスト低減メリット

セキュリティに配慮せず開発を行えば、短期的にはコストを抑え、開発期間を短くすることができるでしょう。しかし、リリース後の運用過程で、もしサイバー攻撃による情報漏えいや知的財産の窃取などが起こったら、発生した損失や対応費用など、長期的に見たコストはより大きくなるでしょう。

こうしたトータルコストの低減効果こそ、シフトレフトによるセキュアな開発および運用の真骨頂です。

シフトレフトとは、発生しうるトラブルに事前に備えるということです。病気にならないように運動をしたり、食生活に気をつけたりといった、ごくごくあたりまえのことです。

つまり、これまでのソフトウェア開発は、その当たり前をやっていなかったとも言えます。シフトレフト、セキュリティ・バイ・デザイン、 DevSecOpsという言葉がいろいろな場面で見られるようになったことは、開発現場が成熟してきた現れでもあります。今後、こういった開発プロセスが新常識となっていくことでしょう。

シフトレフトを普及させた裁判の判決とは

ここで、セキュリティ視点でのシフトレフトの考え方を日本に普及させるきっかけのひとつになったとされる、2014年の、ある裁判の判決をご紹介します。

とある企業の開発依頼で納品されたオンラインショッピングのシステムに、SQLインジェクションの脆弱性があったことで、不正アクセスによる情報漏えい事故が発生しました。依頼した企業は、開発会社がセキュリティ対策を怠っていたことを債務不履行として提訴、東京地方裁判所がそれを認め、開発会社に約2200万円の損害賠償支払いを命じました( 平成23年(ワ)第32060号 )。ただし、全面的に開発会社の落ち度としたわけではなく、発注会社側が責務を果たしていない点については、相当程度の過失相殺を認めています。

この判決は、これまで技術者がいくらセキュリティの必要性を説いても首を縦に振らなかった、セキュリティよりも利益を重視していた「開発会社の経営管理層」と、セキュリティよりもコストと納期を重視していた「発注者」の考えを変えるインパクトを持っていました。

将来事故が起こらないよう、トータルコストを抑えセキュリティに配慮した開発を行う有効な方法としてシフトレフトが採用されたのは、ごく自然なことといえるでしょう。

シフトレフト視点での開発上の注意

シフトレフトに基づく開発におけるセキュリティ対策の実施例は以下のとおりです。

●セキュリティ・バイ・デザイン
まず、セキュリティ・バイ・デザインの考え方に基づいて、企画・設計段階からセキュリティを考慮しましょう 。

●セキュアな開発環境
開発は、脆弱性を作り込まないようにするフレームワークやライブラリなど、セキュアな開発環境を活用して行います。

●ソースコード診断
開発の各段階で、プログラムコードに問題がないかを適宜検証するソースコード診断を実施します。

●脆弱性診断
もし、どんなセキュリティ要件を入れたらいいかわからなくても、独立行政法人情報処理推進機構(IPA)などの専門機関がいくつもガイドラインを刊行しています。「このガイドラインを満たすような開発を」と依頼して、それを契約書に記載しておけばいいでしょう。ガイドラインの中身を完全に理解している必要はありません。

リリース前や、リリース後の新機能追加等の際には、必ず事前に脆弱性診断を行います。また、脆弱性が悪用された場合、どんなインシデントが発生しうるのかを、さらに深く検証するペネトレーションテストの実施も有効です。

シフトレフト視点での発注の仕方

シフトレフトは主に開発者側の考え方です。では、ソフトウェア開発を依頼する発注者はどうすればいいのでしょうか。

まず、発注の際には必ずセキュリティ要件を入れましょう。納品されたシステムやWebアプリケーションにセキュリティの問題が発見された際に対応を要求しやすくなります。

もしそれによって見積額が上がったら、トータルコストのこと、シフトレフトというこれからの新常識のことを思い出していただきたいと思います。

・安全なウェブサイトの作り方(IPA)
https://www.ipa.go.jp/security/vuln/websecurity.html

シフトレフトが変えるセキュリティの未来

とはいえ、今回ご紹介したシフトレフトの考え方が社会に広く普及するまでには、もう少し時間がかかりそうです。

SQAT.jp を運営する株式会社ブロードバンドセキュリティが、リリース直前のWebサービスに脆弱性診断を行うと、山のように脆弱性が発見されることがあります。

その脆弱性の中には、2014年の裁判で開発会社の債務不履行とされたSQLインジェクションのような、極めて重大なものが含まれていることも多くあります。

業界が成熟し、シフトレフトによるセキュリティ対策が実践されていけば、脆弱性診断というサービスの位置づけ自体が将来変わることすらあるかもしれません。たとえば自動車のような、安全規格に基づいて設計製造された製品における出荷前の品質チェック、あるいは監査法人による会計監査のように、「きちんと行われている前提」で実施する広義のクオリティコントロール活動の一環になるかもしれません。

SQAT.jp は、そんな未来の到来を少しでも早く実現するために、こうして情報発信を行い続けます。

まとめ

・シフトレフトとは上流工程でセキュリティを組み込み、トータルコストを抑えるという考え方
・セキュリティを考慮せずにWebサービスを開発し提供するのは、たとえるなら建築基準法を考慮せずにビルを建ててテナントを入居させるようなもの
・セキュリティをコストととらえ費用を惜しむと、将来的により高い出費を余儀なくされる可能性がある
・シフトレフトによるセキュリティ対策には、セキュリティ・バイ・デザイン、セキュリティ要件の明示、セキュアな開発環境、早期段階から適宜に実施する各種セキュリティ診断等がある


年二回発行されるセキュリティトレンドの詳細レポート。BBSecで行われた診断の統計データも掲載。
サービスに関する疑問や質問はこちらからお気軽にお問合せください。

Share

Frama-Cのもたらすセキュリティ

Share

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)で7段階規定され、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に相当するけれども、ツール自体はなんとオープンソースである。

ソフトウェアの信頼性が、セキュリティと何の関係があるのかと思う方もおられるかもしれない。マルウェアがソフトウェアのバグや脆弱性を突いて感染を拡大することを見ればわかるように、ソフトウェアの信頼性を向上させバグの混入を防ぐことは、セキュリティの言葉に翻訳すると「攻撃者に付け込む隙を与えない」ことを意味する。理屈としては攻撃者だけではなく、ペンテスターに対しても付け込む隙がなくなる。攻撃者/ペンテスターが「脆弱性の1本釣り」であるならば、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メンバー


年二回発行されるセキュリティトレンドの詳細レポート。BBSecで行われた診断の統計データも掲載。
サービスに関する疑問や質問はこちらからお気軽にお問合せください。

Share