学術協力がアマゾンの顧客に現実世界のセキュリティをもたらす方法
アマゾンの科学者とスタンフォード大学研究者の協力により開発されたオープンソースツールcvc5は、AWSで毎日約10億回の自動推論チェックを実行し、セキュリティを強化しています。
キーポイント
アマゾンとスタンフォード大学の学術協力により、オープンソースの自動推論ツールcvc5が開発された
cvc5はAWSで1日約10億回の自動推論チェックを処理し、IAMアクセスアナライザーやAmazon Bedrockの機能など顧客セキュリティ向上に貢献
学術研究と実世界応用の成功例として、研究助成から技術協力、最終的には研究者のアマゾン採用に至る長期的協力関係を確立
影響分析・編集コメントを表示
影響分析
この記事は、学術研究と産業界の協力が具体的なセキュリティ向上と製品開発につながる成功事例を示している。特に、SMT（充足可能性モジュロ理論）を基盤とする自動推論技術の大規模実装は、クラウドセキュリティの信頼性向上に寄与し、オープンソースツールとして業界全体にも価値を提供している。
編集コメント
学術研究の実世界応用における成功事例として、長期的な協力関係の構築と具体的なビジネス価値創出の両面から参考になる内容。
学術連携がいかにしてアマゾンの顧客に現実世界のセキュリティをもたらすか
アマゾンの科学者とスタンフォード大学の研究者たちによる初期の会合が、cvc5というオープンソースツールの開発につながりました。このツールは現在、AWS全体で毎日約10億件の自動推論チェックを支えています。
共有 共有 リンクをコピー
バイロン・クック: 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)
原文を表示
How academic collaboration delivers real-world security to Amazon customers
An early meeting between Amazon scientists and Stanford researchers led to cvc5, an open-source tool now powering approximately one billion automated-reasoning checks across AWS every day.
Share Share Copy link
Byron Cook: Formal Reasoning about the Security of Amazon Web Services In the keynote, Cook described how his team was using an open-source software tool called cvc (cooperating validity checker) to identify logic problems in code and fix them. Sitting in the audience was Stanford University professor Clark Barrett, who had been working on cvc for almost 20 years.
Cvc had been developed to analyze verification problems encoded as satisfiability modulo theory (SMT) problems. SMT is a mainstay of formal methods — the use of automated reasoning to prove that a program or system will behave as intended. By applying SMT at scale, cvc can detect logical errors in code and in systems such as those used for authentication and access management.
“I was kind of stunned. It was really exciting,” Barrett says. “And this really started with this exciting moment of realizing, Hey, our work is being used by Amazon.”
The encounter between Cook and Barrett ultimately led to a years-long research collaboration that culminated in Barrett’s becoming an Amazon Scholar in 2023. Initially, Amazon provided small grants to Barrett’s lab at Stanford’s School of Engineering through the Amazon Research Awards program; those grew into larger funding commitments as the research progressed. This funding supported foundational research that — together with deep technical collaboration between the two teams — enabled the development of cvc5, the latest version of the open-source software. Cvc5 has delivered significant value for both Amazon customers and the broader industry, while simultaneously advancing academic research.
As one example, cvc5 is used in Automated Reasoning checks, a new Amazon Bedrock feature that verifies natural-language content against organizational policies. It powers access-policy analysis tools, including Identity and Access Management (IAM) Access Analyzer, a service that helps customers securely manage access to AWS resources. More recently, Amazon has begun deploying cvc5 for specification analysis and test generation in Kiro, a new agentic development environment. Across these applications, cvc5 now processes approximately one billion solver calls every day, enhancing security, reliability, and durability for AWS customers.
How Academic Collaboration Delivers Real-World Security to Amazon Customers
A meeting of minds
Working with Barrett on the project is Robert Jones, a senior principal applied scientist at AWS who shared an advisor with Clark when both were Stanford PhD students. Also involved in the project over the years were many students and postdocs keen to test their skills. More than a few have since joined Amazon to develop new implementations and applications, extending work that began when they were student researchers.
“What's really fun about it is that people who have just finished their PhD, for example, often bring fresh insight to long-standing research challenges because they're thinking about them in a different way,” Jones says. “And I find that the best part of collaboration is that different people tend to build different mental models for the same problem. When those come together, you often have new insight into how to think about the problem or how to map it to a different problem you already know how to solve.”
A successful coupling of academic research and commercial funding can have great impact, but as Barrett points out, there needs to be a focus on achievable goals. It’s easy to get caught up in an interesting project idea that leads to a practical dead end, Barrett says.
“If you're in your ivory tower, building your tools, and you don't have access to the real problems, it's very easy to build the wrong tool. And I've actually made this mistake,” he says. “You build a hammer, and then you go around looking for a nail, and you can't quite find anything that fits. You get excited about a particular approach but don't think about what that approach could be good for. So I actually now much prefer the opposite, where I go find a real problem, and then I take a step back and say, ‘What approach can we actually use to solve that?’”
When you change code, he says, “Eighty percent of the time it does better, and 20 percent of the time it does worse. This is actually not so great in some contexts.” Sorting the wheat from the chaff is essential to producing robust and scalable code, he adds, and large-scale testing is needed to find and fix issues that can be inadvertently introduced as the code changes.
Analyzing interactions at that level requires multiple minds, and the more the merrier, Jones says. The old adage “many hands make light work” is particularly useful when mixing public research and practical applications.
“I really like to work on hard problems that require multiple people to solve. I enjoy the collaboration involved in science,” he says. “I've always found that more minds working on the same problem together are better than one.”
Barrett and Jones agree that what makes this work is a willingness to see from both points of view — the scholastic and the commercial. Sometimes a pure research goal can have very beneficial results, sometimes not, but melding these two approaches together to address serious issues can deliver huge benefits.
And communication is key, both agree.
“One of the hard things about academia is knowing which problems are the most important to work on and how those problems might impact the real-world problems that are being encountered in industry,” Jones says. “Having the ability to be much more open about the kinds of problems that we're struggling with and Clark telling us about his research agenda helps both of us. It enables Amazon to indicate areas of interest, and it helps Clark understand concrete problems that we encounter day to day as we try to apply these tools and techniques in practice.”
Automated reasoning
Academic collaborations
Amazon Web Services (AWS)
関連記事
今日のまとめ
AI日報で今日の重要ニュースをまとめ読み