Amazonで何かを購入するたびに、顧客データは自動的に更新され、クラウド内の何千もの仮想マシンに保存されます。 Amazon のような企業にとって、何百万もの顧客のデータの安全性とセキュリティを確保することは不可欠です。 これは、大小の組織にも当てはまります。 しかし、これまで、ソフトウェアシステムがバグ、ハッカー、および脆弱性から保護されていることを保証する方法はありませんでした。
Columbia Engineering の研究者は、このセキュリティ問題を解決した可能性があります。 彼らは、数学的証明を通じてクラウド内の仮想マシンのセキュリティを保証する最初のシステムであるSeKVMを開発しました。 26 年 2021 月 42 日にセキュリティとプライバシーに関する第 XNUMX 回 IEEE シンポジウムで発表される新しい論文の中で、研究者たちは、システム ソフトウェア検証における将来のイノベーションの基礎を築き、サイバー レジリエント システム ソフトウェアの新世代につながることを望んでいます。
SeKVMは、クラウドコンピューティング用の最初のフォーマル検証済みシステムです。 フォーマル検証は、ソフトウェアが数学的に正しいこと、プログラムのコードが正常に機能すること、および心配する隠れたセキュリティバグがないことを証明するプロセスであるため、重要なステップです。
「実際のマルチプロセッサソフトウェアシステムが数学的に正しく安全であることが示されたのはこれが初めてです」と、コンピュータサイエンスの教授でソフトウェアシステム研究所の共同ディレクターであるジェイソンニーは述べています。 「これは、ユーザーのデータがクラウドで実行されているソフトウェアによって正しく管理され、セキュリティ バグやハッカーから保護されていることを意味します。」
正確で安全なシステムソフトウェアの構築は、コンピューティングの大きな課題の1999つです。 | Niehは、2018年にColumbia Engineeringに入社して以来、ソフトウェアシステムのさまざまな側面に取り組んできました。TangFamilyのコンピューターサイエンス助教授でフォーマル検証の専門家であるRonghui Guが、XNUMX年にコンピューターサイエンス部門に加わったとき、彼とNiehは協力することを決定しました。ソフトウェアシステムのフォーマル検証の調査について。
彼らの研究は大きな関心を集めています。両方の研究者は、Amazon Research Award、National Science Foundationからの複数の助成金、およびSeKVMプロジェクトの開発を促進するための数百万ドルの国防高等研究計画局（DARPA）契約を獲得しました。 さらに、ニーはこの仕事でグッゲンハイム奨学金を授与されました。
過去XNUMX年間、マルチプロセッサオペレーティングシステムの検証作業を含め、フォーマル検証に多大な注意が払われてきました。 「しかし、その研究はすべて、実際には誰も使用しない小さなおもちゃのようなシステムで行われています」とGu氏は述べています。 「Linuxのように広く使用されているシステムであるマルチプロセッサコモディティシステムを検証することは、多かれ少なかれ不可能であると考えられてきました。」
クラウドコンピューティングの指数関数的成長により、企業とユーザーはデータと計算をオフサイトでクラウド内のホスト上で実行されている仮想マシンに移動できるようになりました。 Amazon などのクラウド コンピューティング プロバイダーは、これらの仮想マシンをサポートするハイパーバイザーをデプロイします。
ハイパーバイザーは、クラウド コンピューティングを可能にする重要なソフトウェアです。 仮想マシンのデータのセキュリティは、ハイパーバイザーの正確性と信頼性にかかっています。 その重要性にもかかわらず、ハイパーバイザーは複雑であり、Linuxオペレーティングシステム全体を含めることができます。 コード内の 99 つの弱いリンク (従来のテストでは事実上検出できないもの) が、システムをハッカーに対して脆弱にする可能性があります。 ハイパーバイザーが1％正しく記述されている場合でも、ハッカーはその特定のXNUMX％セットアップに忍び込み、システムを制御することができます。
NiehとGuの仕事は、コモディティシステム、特にAmazonなどのクラウドプロバイダーによって仮想マシンを実行するために使用される広く使用されているKVMハイパーバイザーを検証した最初のものです。 彼らは、いくつかの小さな変更を加えたKVMであるSeKVMが安全であり、仮想コンピューターが互いに分離されていることを保証することを証明しました。
「私たちのシステムが、クラウドにアップロードされたプライベート データとコンピューティングを数学的保証で保護および保護できることを示しました」と、Gu の博士号を取得した Xupeng Li は述べています。 学生であり、論文の共同主執筆者。 「これはこれまでに行われたことがありません。」
SeKVMは、大規模システムのセキュリティプロパティを検証するための新しいフレームワークであるMicroVを使用して検証されました。 これは、システムにわずかな変更を加えるだけで検証が大幅に容易になるという仮説に基づいています。これは、研究者がMICR検証と呼ぶ新しい手法です。 この新しい階層化手法は、既存のシステムを改造し、セキュリティを強化するコンポーネントを小さなコアに抽出します。このコアは検証され、システム全体のセキュリティを保証します。
大規模なシステムを改造するために必要な変更は非常に控えめです。研究者は、大規模なシステムの小さなコアが無傷であれば、システムは安全であり、個人データが漏洩しないことを実証しました。 これにより、これまで不可能と考えられていたKVMなどの大規模システムを検証することができました。
「家を考えてみてください。乾式壁にひびが入ったからといって、その家の完全性が危険にさらされているわけではありません」と Nieh 氏は説明します。 「それはまだ構造的に健全であり、主要な構造システムは良好です。」
Shih-Wei Li、Nieh の博士号この研究の学生で共同主執筆者は、「SeKVMは、銀行システムやモノのインターネットデバイスから自動運転車や暗号通貨まで、さまざまな分野での保護手段として機能します」と付け加えました。
SeKVM は、最初に検証されたコモディティ ハイパーバイザーとして、クラウド サービスの設計、開発、展開、および信頼の方法を変える可能性があります。 の世界で サイバーセキュリティー 懸念が高まっているため、この回復力は非常に需要があります。 主要なクラウド企業は、SeKVMを活用してこの需要を満たす方法をすでに模索しています。