Jun. 2023No.99
Interview
「安全性」を積み上げるゼロトラスト
システムの「振る舞い」を定義する形式検証のインパクト
スマートフォンやタブレットのみならず、多くの家電、車までもがインターネットにつながるIoT時代。リスクも高まる中で、どのようにシステムの信頼性を保つのか。科学技術研究機構（JST） CREST「形式検証とシステムソフトウェアの協働によるゼロトラストIoT」（研究代表者：竹房あつ子）が実現する「安全性」のあり方について聞いた。
石川 裕ISHIKAWA, Yutaka
国立情報学研究所
アーキテクチャ科学研究系 教授
竹房 あつ子TAKEFUSA, Atsuko
国立情報学研究所
アーキテクチャ科学研究系 教授
ゼロトラストを支える形式検証理論
――自動運転への期待と同時に、安全性や信頼性への懸念も高まっています。先生のご研究はどのようなものですか。
竹房 安全なIoTシステムを作るためのソフトウェアシステム技術を作り上げることであり、そのために形式検証理論の力を活用することです。
――お二人はここまで、どのように歩んでこられたのでしょうか。
竹房 大学では情報科学を専攻しました。数学に近い理論から工学に近いプログラミングまで、幅広く学べて選べる環境でした。ちょうどインターネットが普及してきた時期だったのでネットワークコンピューティングに関心を持ち、卒業研究でもテーマにしました。その時の大学の研究室が、産業界や実社会での応用に関する研究を行っている研究機関や大学と共同研究をしており、刺激と影響を受けながらグリッドコンピューティングや超分散処理の研究を行うようになりました。
当時のその世界には、「センサーグリッド」という概念がありました。モノや実験装置を全部ネットワーク化してデータを集めることです。現在のクラウドコンピューティングやIoTに近い研究は、その時から始めていたと言えます。
石川 私はシステムソフトウェアやOSに関心がありました。最初はUNIXを使っていましたが、1980年代後半にパソコンで動くUNIXが現れはじめ、1990年代にはLinux が世界の一大ブームになりました。1997年頃には、パソコンと高速ネットワークを組み合わせ、システムソフトウェアを工夫することによりスーパーコンピュータ並みの性能が出せる状況になりました。米国の学会で我々が研究開発したシステムソフトウェアとPCクラスタのデモを行ったところ大変注目を受けました。
その当時、いろいろなところで我々のソフトウェアが使われていました。自然の流れでスーパーコンピュータの開発に携わり続け、「富岳」の開発でもプロジェクトリーダーを務めました。1980年代後半頃は検証技術に興味を持っていましたが、当時はシステムソフトウェアの開発に使える技術として成熟していなかったためその後距離をおいていました。
――社会のシステムの複雑さ、制御できなかった場合の影響の大きさは、文字通りの「桁違い」ではないかと思います。
竹房 これまでも、目の届きにくいIoTデバイスや人が手元で管理していない計算機が、外部から侵入されて大きな被害を発生させたりしています。自動運転車の実用化が視野に入ると、さらに大きなリスクが発生するでしょう。対策が困難だからこそ、安全にしなくてはなりません。安全にするためには、どういう管理をすればよいのか？ ということです。まず、ネットワーク上に何があってどう守らなくてはならないのかを明らかにし、その状態が保たれていることを確認し続けます。同時にシステムを把握し続け、システムへのアクセスが信頼できることを保証し続けます。これが、私たちが安全を保証するための考え方です。
――未知の危険に完全に対策することは可能なのでしょうか？
石川 対応できる危険であるかどうかは、システムの脆弱性や存在しうる危険性によります。そこに脆弱性がなくても、外部からの何らかのアタックによって、ネットワークサービスの一部が影響を受けてパフォーマンスが低下する可能性もあります。その時、どう判断してどう対応すればよいのか。あらかじめ、検討して決めておきます。
例えば自動運転車の場合、走行に関係しないサービスなら「そのサービスをオフにして運転し続ける」。自動運転「レベル３」で走行している場合、走行に悪影響を与える危険性を検知すれば「自動運転を解除し、運転者に運転を代行してもらう」といった対応が考えられます。実際には、システムの設計段階で分析を行い、分析結果に基づいて対策を講じておく必要があります［1］。このために必要な形式検証理論を、蓮尾先生たちと共に追求しています。
――安全性のためにネットワーク上のあらゆるものを完全には信用しない「ゼロトラスト」が必要なのは当然ですが、性能が犠牲になることはないのでしょうか？
竹房 もちろん、性能と安全性のトレードオフはあります。システムを作る側が最初に、何をどこまで安全にするのかを考えるわけですが、システムの運用が開始されれば、さまざまな変化が起こったり持ち込まれたりします。その変化が、現在の研究対象の一つです。
まず、システムをモデル化し、モデルが安全であることを保証してから、システム実装に反映します。システムが変化するということは、モデルも変化するということです。変化したモデルの安全性を検証してからシステムに反映すれば、システムの安全性は維持され続けるはずです。
基礎研究によって実際の開発を支援
――最初の設計段階での品質保証は、運用開始後の変化に対応して安全性を確保し続けるためにも重要そうですね。
石川 私たちは製品やサービスを作っているわけではありませんが、確かな手法や頼れる解析ツー
ルを作り上げるための基礎研究を行うことによって、実際の開発を支援することがミッションです。自動運転車の場合、自動車がインターネットに接続され、ネットワーク経由で多様なサービスを利用しています。ネットワークサービスを提供する側だけではなく、自動車の方でも多様なソフトウェアが動いています。サイバーセキュリティ的な脆弱性があってアタックされた時、そもそも脆弱性があるのかないのか。それを形式検証の手法を使って解析し、今後、開発したツールを公開していきます。さらにプラットフォーム側で、竹房先生たちと連携しています。
竹房 すべての変化に対して求められる対応が可能であるとは限りませんが、それでも、変化を検出することは重要です。
例えば災害対策には、大きく分けて「災害を事前に完全に防止する」という考え方と、「災害の発生は避けられないので、発生した場合に被害を食い止めて復旧を容易にする」という考え方の2種類があります。私たちは後者、すなわちレジリエンスが実現されるIoTシステムを目指しています。リスクを予測して備えることは重要ですが、受け止めきれないリスクや予測できないリスクが発生した時にも安全に確実に、かつ全体で緩やかに対応することが大切でしょう。それは、システムソフトで可能になると考えています。
――そこで重要な役割を担うのが形式検証であり、数学のパワーだと理解しています。
石川 システムのモデルを設定してモデルを検証すること、そのモデルが発生させうるすべての可能性を検証することを、数学的に行うのが形式検証です。考え方自体は昔から存在し、限られた分野で使われてきましたが、徐々に応用範囲が広がってきたと思っています。
すべての可能性を数え上げて検証するわけですから、現実的な、ある程度のサイズと複雑さのあるモデルでは、「組み合わせ爆発」が起こります。ふんだんにメモリを搭載した高性能コンピュータが使えるようになったので、ある程度は、組み合わせ爆発が起きても検証が続けられるようになりました。組み合わせ爆発を抑えながら、現実を反映した大きく複雑なモデルをどこまで検証できるのか。まだまだ、これからです。
竹房 モデルを設定して検証することと、プログラムを作成して実行することの間には、大きなギャップがあります。そこを、どう折り合わせて修正していけるのか。言い換えれば、「形式検証の研究者が作ったモデル化手法をシステムソフトウェア研究者が活用できるようにするには、どうすればよいのか？」という課題でもあります。
研究成果がNII提供のサービス向上につながる
――過去になかった応用の可能性、近未来に実現されそうな夢には、どのようなものがあるでしょうか？
竹房 NIIは学術機関に対してサービスを提供しています。その中で、IoTシステムのためのミドルウェアも提供しています［2］。私たちの今の研究成果は、そこに統合されて使っていただくことになるでしょう。まずは学術機関の皆さんが、IoTシステムを安全に作ることを支援したいです。
IoTの応用範囲は、非常に広いです。例えば各家庭にスマートメーターを備え付け、その情報を都市の電力削減に応用することも可能です。まずは、Society5.0のための基盤技術として使っていただけるようにすることが課題です。
それが実現すると、「各家庭の情報を隠して電力供給を全体最適化する」ということも可能でしょう。例えば、「地域の自治体単位で自動的に、かつ快適に節電を行う」といった応用も可能かもしれません。社会に根付く道筋としては、学術機関でのIoTシステム開発だけではなく、企業との共同研究を進めて使っていただくことも考えられます。
いずれにしても、外的な要因による変化もありえますから、先行き予測は難しいです。地道に研究を行い、地道に普及活動をしていくことが重要だと考えています。
――期待が高まる一方で、社会から見た懸念はどうしても残りそうです。
竹房 だからこそ、「ゼロトラスト」なのです。すべてに対して「これで大丈夫だろう」と落とし込むのではなく、「今、ここで、大丈夫かどうか」を積み上げていく考え方です。IoTデバイスを対象とした研究で開発した技術は、サーバをはじめ、多様な範囲に適用できます。たとえば小型、かつ人が手元で管理できない場合の多いIoTデバイスに対するソフトの開発と「ゼロトラスト」の実現は、幅広い範囲に応用できるでしょう。
システムの「振る舞い」を数学がモデル化
石川 さらに、私たちの研究では数学の威力が発揮されます。システムの振る舞いを数学的にモデル化し、抽象的に表現することによって、システムの振る舞いが明瞭となりサイバー攻撃の可能性を洗い出すことが可能となります。サイバー攻撃の可能性が見つかれば事前に防御方法を検討しシステムを修正します。修正したシステムの振る舞いを同様に検証することにより「問題がないことを証明した」という説明が可能になります。漏れや取りこぼしなく説明責任を果たせるようになる意義は大きいと考えています。
そのためには、開発者がシステムの振る舞いを適切に抽象化し、証明を可能にする必要があります。ここが難しいところですが、開発者は、守るべき資産（例えばIoT機器が扱っているデータ）がどのように扱われているかを我々が開発するツールで記述してもらいます。今までは安全性を検 証する人が 開発 者にインタビューしてシステムの挙動を理解してモデル化して安全性を証明していました。ソフトウェアを開発する側で「問題ありません」という証明ができるようになることには、大きな社会的インパクトがあります。
―――安全なシステムと未来の自動運転車に、ますます期待が高まります。
（取材・構成 みわ よしこ、photo 今村 拓馬）
[1]自動車の場合は、設計と評価に関する国際規格に基づいて分析を行う。