学術協力がアマゾンの顧客に現実世界のセキュリティをもたらす方法

学術連携がいかにしてアマゾンの顧客に現実世界のセキュリティをもたらすか アマゾンの科学者とスタンフォード大学の研究者たちによる初期の会合が、cvc5というオープンソースツールの開発につながりました。このツールは現在、AWS全体で毎日約10億件の自動推論チェックを支えています。 共有 共有 リンクをコピー ![](https://assets.amazon.science/dims4/default/657cefc/2147483647/strip/true/crop/200x200+0+0/resize/295x295!/quality/90/?url=http%3A%2F%2Famazon-topics-brightspot.s3.amazonaws.com%2Fscience%2F88%2F18%2F968db03bd0dba1b5567c4c55315a%2Fhow-academic-collaboration-delivers-real-world-security-to-amazon-customersqrcode) 2018年7月16日、アマゾンの著名な科学者バイロン・クックは、オックスフォード大学で開催された連合論理会議（FloC）で基調講演を行っていました。これは1996年から4年ごとに開催されているコンピュータ論理の集まりです。 バイロン・クック: Amazon Web Servicesのセキュリティに関する形式的推論 基調講演で、クックは彼のチームがcvc（cooperating validity checker）というオープンソースソフトウェアツールを使用して、コード内の論理問題を特定し修正している方法を説明しました。聴衆の中には、スタンフォード大学のクラーク・バレット教授が座っており、彼はほぼ20年にわたってcvcの開発に携わっていました。 Cvcは、充足可能性モジュロ理論（SMT）問題としてエンコードされた検証問題を分析するために開発されました。SMTは形式的手法の主力であり、プログラムやシステムが意図した通りに動作することを自動推論を用いて証明するものです。SMTを大規模に適用することで、cvcはコードや、認証やアクセス管理に使用されるようなシステム内の論理エラーを検出できます。 「私はある種、呆然としました。本当に興奮しました」とバレットは言います。「そしてこれはまさに、『おや、私たちの仕事がアマゾンで使われている』と気づいたこの興奮の瞬間から始まったのです。」 クックとバレットの出会いは、最終的には数年におよぶ研究協力関係につながり、2023年にバレットがアマゾン・スカラーとなることで頂点を迎えました。当初、アマゾンはアマゾン・リサーチ・アワードプログラムを通じて、スタンフォード大学工学部のバレット研究室に小規模な助成金を提供しました。研究が進むにつれ、それらはより大きな資金提供の約束へと成長しました。この資金は基礎研究を支え、それが両チーム間の深い技術的協力と相まって、オープンソースソフトウェアの最新版であるcvc5の開発を可能にしました。Cvc5は、アマゾンの顧客と業界全体の両方に大きな価値をもたらすと同時に、学術研究も前進させています。 一例として、cvc5は「Automated Reasoning checks」で使用されています。これは、自然言語のコンテンツが組織のポリシーに準拠しているかを検証する、Amazon Bedrockの新機能です。また、IAM Access Analyzerを含むアクセスポリシー分析ツールを支えています。これは、顧客がAWSリソースへのアクセスを安全に管理するのに役立つサービスです。さらに最近では、アマゾンは新しいエージェント型開発環境であるKiroにおいて、仕様分析とテスト生成のためにcvc5の導入を開始しました。これらのアプリケーション全体で、cvc5は現在、毎日約10億件のソルバー呼び出しを処理しており、AWS顧客のセキュリティ、信頼性、耐久性を高めています。 学術連携がいかにしてアマゾンの顧客に現実世界のセキュリティをもたらすか 知性の出会い このプロジェクトでバレットと共に働いているのは、AWSのシニアプリンシパル応用科学者であるロバート・ジョーンズです。彼とクラークは、ともにスタンフォード大学の博士課程学生だった頃、同じ指導教官に師事していました。また、このプロジェクトには長年にわたり、自分のスキルを試したいと考えた多くの学生やポスドクも関わってきました。そのうちの少なからぬ人々がその後アマゾンに加わり、学生研究者だった時に始めた仕事を拡張する、新たな実装やアプリケーションの開発に携わっています。 「これの本当に楽しいところは、例えば博士号を取得したばかりの人々が、長年続く研究課題に対して新鮮な洞察をもたらすことがよくあるということです。彼らはその課題を違った方法で考えているからです」とジョーンズは言います。「そして、協力関係の最も良い部分は、異なる人々が同じ問題に対して異なるメンタルモデルを構築する傾向があることだと思います。それらが一つになるとき、その問題の考え方や、すでに解決方法を知っている別の問題にどうマッピングするかについて、新たな洞察が得られることがよくあります。」 学術研究と商業資金の成功した結合は大きな影響力を持つ可能性がありますが、バレットが指摘するように、達成可能な目標に焦点を当てる必要があります。実用的な行き詰まりにつながる興味深いプロジェクトのアイデアに夢中になるのは簡単だ、とバレットは言います。 「象牙の塔の中にいて、自分のツールを構築し、現実の問題にアクセスできない場合、間違ったツールを作ってしまうのは非常に簡単です。そして私は実際にこの間違いを犯したことがあります」と彼は言います。「ハンマーを作り、それから釘を探し回るが、ぴったり合うものがなかなか見つからない。特定のアプローチに興奮するが、そのアプローチが何に役立つかを考えない。だから私は実際、今ではその逆をずっと好んでいます。つまり、現実の問題を見つけに行き、一歩下がって『それを解決するために実際に使えるアプローチは何か？』と言うのです。」 コードを変更すると、彼は言います、「80％の確率で良くなり、20％の確率で悪くなります。これは実際、状況によってはあまり良くありません。」もみ殻から小麦を選り分けることは、堅牢でスケーラブルなコードを生み出すために不可欠だと彼は付け加え、コード変更の際に不注意に導入される可能性のある問題を見つけて修正するためには、大規模なテストが必要だと述べています。 そのレベルの相互作用を分析するには複数の知性が必要であり、多ければ多いほど良い、とジョーンズは言います。「多くの人手があれば仕事は楽になる」という古い格言は、公的研究と実用的応用を混ぜ合わせる際に特に有用です。 「私は、複数の人々を必要とする難しい問題に取り組むのが本当に好きです。科学に伴う協力関係を楽しんでいます」と彼は言います。「私は常に、一人よりも多くの知性が同じ問題に一緒に取り組む方が良いと感じてきました。」 バレットとジョーンズは、この仕事を成り立たせているのは、学問的視点と商業的視点の両方から見ようとする意思であることに同意しています。純粋な研究目標が非常に有益な結果をもたらすこともあれば、そうでないこともありますが、これら二つのアプローチを融合させて深刻な問題に取り組むことは、巨大な利益をもたらすことができるのです。 そして、コミュニケーションが鍵だと、二人は同意します。 「学界の難しいことの一つは、どの問題が取り組むべき最も重要な問題であるかを知り、それらの問題が業界で遭遇している現実世界の問題にどのように影響する可能性があるかを知ることです」とジョーンズは言います。「私たちが苦労している問題の種類について、もっとオープンに話せる能力を持つこと、そしてクラークが彼の研究計画について話してくれることは、私たち両方にとって役立ちます。それはアマゾンが関心のある領域を示すことを可能にし、クラークが私たちがこれらのツールや技術を実際に適用しようとする際に日々遭遇する具体的な問題を理解するのに役立ちます。」 自動推論 学術連携 Amazon Web Services (AWS)

学術協力がアマゾンの顧客に現実世界のセキュリティをもたらす方法

背景や根拠まで確認しますか？

調べる

選ぶ

サイト