本ブログは 2021 年 12 月 1 日に公開された Amazon Science Blog “ A gentle introduction to automated reasoning ” を翻訳したものです。 2021 年、Amazon Science は研究領域のリストに 自動推論 を追加しました。この変更を行ったのは、自動推論が Amazon にもたらしている影響が大きいからです。例えば、Amazon Web Services のお客様は現在、 IAM Access Analyzer 、 S3 Block Public Access 、 VPC Reachability Analyzer といった自動推論ベースの機能を直接利用できます。また、Amazon の開発チームが 自動推論ツールを開発プロセスに統合 し、製品の セキュリティ 、 耐久性 、可用性、品質の水準を高めている例も見られます。 この記事の目的は、自動推論についてまったく知識はないものの詳しく学んでみたいと考えている業界の実務者に向けて、自動推論をわかりやすく紹介することです。この記事を理解するために必要な前提知識は、短い C と Python のコード断片を読めることだけです。途中でいくつかの専門的な概念に触れますが、あくまで堅苦しくない形で紹介するにとどめます。最後に、さらに深く学びたい方のために、一般に公開されているおすすめのツール、動画、書籍、記事へのリンクを紹介します。 まずは簡単な例から始めましょう。次の C 関数を考えてみてください。 bool f(unsigned int x, unsigned int y) { return (x+y == y+x); } 少し時間を取って、次の質問に答えてみてください。 「 f が false を返すことはあり得るか?」 これはひっかけ問題ではありません。論点を明確にするため、意図的に簡単な例を使っています。 網羅的テストで答えを確認するなら、次の二重にネストしたテストループを実行するという方法が考えられます。このループは、unsigned int 型のあらゆる値の組み合わせに対して f を呼び出します。 #include<stdio.h> #include<stdbool.h> #include<limits.h> bool f(unsigned int x, unsigned int y) { return (x+y == y+x); } void main() { for (unsigned int x=0;1;x++) { for (unsigned int y=0;1;y++) { if (!f(x,y)) printf("Error!\n"); if (y==UINT_MAX) break; } if (x==UINT_MAX) break; } } 残念ながら、最新のハードウェアであっても、この二重ループは 非常に長い 時間動き続けます。私はこれをコンパイルして 2.6 GHz の Intel プロセッサ上で 48 時間以上実行したところであきらめました。 なぜテストにこれほど時間がかかるのでしょうか。UINT_MAX は通常 4,294,967,295 なので、検討すべき f の呼び出しは 18,446,744,065,119,617,025 通りあります。私の 2.6 GHz のマシンでは、コンパイルされたテストループは f を 1 秒あたり約 4 億 3,000 万回呼び出しました。それでも、この性能で約 1,844 京通りのすべてのケースをテストするには 1,360 年以上かかります。 上記のコードを業界の実務者に見せると、ほぼ即座に、基盤となるコンパイラ/インタープリタとハードウェアが正しく動作する限り f が false を返すことはないという結論に達します。どのようにしてわかるのでしょうか。コードについて 推論 しているのです。学校で学んだ知識から x + y は y + x と書き換えられることを思い出し、 f は常に true を返すと結論づけます。 Amazon Web Services のユーティリティコンピューティング担当 senior vice president、Peter DeSantis による AWS re:Invent 2021 基調講演。Amazon Web Services の自動推論への取り組みについては 15:49 からご覧ください。 自動 推論ツールは、この作業を私たちの代わりに行います。数学における既知の技法を使って、プログラム (または論理式) に関する問いに答えようと試みるのです。この例であれば、ツールは代数を使って x + y == y + x が単純な式 true に置き換えられることを導出します。 自動推論ツールは、対象領域が無限である場合 (例えば、有限の C の int ではなく非有界の数学的整数の場合) でも、非常に高速に動作することがあります。残念ながら、場合によってはツールが 「Don’t know」 (わからない) と答えることもあります。その有名な例は後ほど見ていきます。 自動推論の 科学 は、本質的にこうした 「Don’t know」 という回答の頻度を可能な限り下げることに焦点を置いています。ツールが 「Don’t know」 と報告する (あるいは試行中にタイムアウトする) 頻度が低いほど、そのツールは有用になるのです。 今日のツールは、かつてのツールでは答えられなかったプログラムやクエリに対しても答えを出せるようになっています。明日のツールはさらに強力になるでしょう。この分野では急速な進歩が続いており、だからこそ Amazon ではそこから得られる価値がますます大きくなっています。実際、自動推論の分野でも、Amazon 流の好循環が独自に形成されつつあると考えています。より多くの入力問題がツールに与えられることでツールが改善され、それがツールのさらなる活用を促すのです。 次に、少し複雑な例です。自動推論とは何かの大まかな輪郭がつかめたところで、次の小さな例では、ツールが私たちの代わりにどのような複雑な問題を扱っているのかを、もう少し現実に近い形で見ていきます。 void g(int x, int y) { if (y > 0) while (x > y) x = x - y; } あるいは、非有界整数を扱う同様の Python プログラムを考えてみましょう。 def g(x, y): assert isinstance(x, int) and isinstance(y, int) if y > 0: while x > y: x = x - y 次の質問に答えてみてください。 「 g は必ず最終的に呼び出し元へ制御を返すか?」 このプログラムを業界の実務者に見せると、たいていはすぐに正しい答えを導き出します。ただし一部の人、特に理論計算機科学の成果を知っている人は、 「これは 停止性問題 の例であり、解けないことが証明されている」 という理由で、この質問には答えられないと誤解することがあります。実際には、 このプログラムを含む 特定のプログラム について、停止するかどうかを推論することは可能です。この点については後で詳しく説明します。 この問題を見たとき、ほとんどの業界の実務者が用いる推論は次のとおりです。 y が正でない場合、実行は関数 g の末尾へ飛びます。これは簡単なケースです。 ループのすべての反復で変数 x の値が減少するのであれば、最終的にループ条件 x > y が成立しなくなり、 g の末尾に到達します。 x の値が常に減少するのは、 y が常に正である場合だけです。そのときにのみ x の更新 (すなわち x = x - y ) が x を減少させるからです。そして y が正であることは条件式によって保証されているため、 x は常に減少します。 経験豊富なプログラマーであれば、通常はこの C プログラムの x = x - y という命令でのアンダーフローを心配するでしょう。しかし、 x の更新前に x > y が成り立っているため、アンダーフローは起こり得ないことに気づきます。 ここまでの 3 つのステップを自分で追ってみたなら、コンピュータプログラムについて推論する際に自動推論ツールが私たちの代わりにどのような思考を行っているかを、とても直感的に理解できたはずです。実際には、ツールが向き合わなければならない厄介な細部が数多くあります (例えば、ヒープ、スタック、文字列、ポインタ演算、再帰、並行性、コールバックなど)。しかし、これらやその他のトピックを扱う技法については数十年分の研究論文があり、そのアイデアを実際に活用するさまざまな実用的ツールも存在します。 自動推論はポリシー (上) とコード (下) の両方に適用できます。いずれの場合も、常に真であることについて推論するのが不可欠なステップです。 重要なポイントは、自動推論ツールは通常、上記の 3 つのステップを私たちの代わりに実行しているということです。ステップ 1 はプログラムの 制御構造 についての推論です。ステップ 2 はプログラム内で 最終的に 真になることについての推論です。ステップ 3 はプログラム内で 常に 真であることについての推論です。 なお、AWS のリソースポリシー、VPC のネットワーク記述、さらには makefile のような設定アーティファクトも、コードとみなすことができます。この視点に立てば、C や Python のコードについて推論するのと同じ技法を用いて、設定の 解釈 に関する問いに答えられます。この着想があるからこそ、IAM Access Analyzer や VPC Reachability Analyzer のようなツールが生まれるのです。 テストは不要になるのか? f と g の例で見たように、自動推論は網羅的テストよりも大幅に高速になる場合があります。今日利用できるツールを使えば、網羅的テストで何世代分もの時間を待つのではなく、 f や g の性質をミリ秒単位で示せます。 では、テストツールを捨てて自動推論に移行してよいのでしょうか。そうとは言えません。テストへの依存を大幅に減らすことはできますが、テストを完全になくせる日は、近いうちには来ないでしょうし、そもそも来ないかもしれません。最初の例をもう一度考えてみてください。 bool f(unsigned int x, unsigned int y) { return (x + y == y + x); } バグのあるコンパイラやマイクロプロセッサが原因で、このソースコードから作られた実行可能プログラムが実際には false を返してしまうかもしれないという懸念を思い出してください。言語のランタイムについても心配する必要があるかもしれません。例えば、C の数学ライブラリや Python のガベージコレクターにバグがあり、プログラムが正しく動作しなくなる可能性もあります。 テストに関して興味深く、しかもしばしば見落とされがちなのは、テストが C や Python のソースコードについて教えてくれるだけではないということです。テストはコンパイラ、ランタイム、インタープリタ、マイクロプロセッサなども同時に検証しています。テストの失敗は、スタック内のいずれのツールに起因していてもおかしくありません。 一方、自動推論は通常、そのスタックのうち 1 つの層 – ソースコードそのもの、あるいは場合によってはコンパイラやマイクロプロセッサ – にのみ適用されます。推論が非常に価値あるものだと感じるのは、検査対象の層について、私たちが 知っている ことと 知らない ことの両方を明確に定義できるからです。 さらに、自動推論ツールが用いる周辺環境のモデル (例えばコンパイラや、対象手続きを呼び出す手続き) によって、私たちの前提が きわめて 厳密なものになります。計算スタックの層を分離することで、時間、労力、費用と、今日および将来のツールの能力をより有効に活用できます。 残念ながら、自動推論を使う際には、ほとんどの場合、 何らかのこと について前提を置く必要があります 。例えば、シリコンチップを支配する物理の原理などです。したがって、テストが完全に置き換えられることはありません。前提をできる限り検証するために、エンドツーエンドテストは今後も行うことになるでしょう。 不可能なプログラム 先に、自動推論ツールが 「yes」 や 「no」 ではなく 「Don’t know」 を返すことがあると述べました。また、永遠に実行を続ける (あるいはタイムアウトする) ために、まったく答えを返さないこともあります。ここでは、ツールが 「yes」 や 「no」 を返すことが できない とわかっている、有名な「停止性問題」のプログラムを見てみましょう。 terminates という名前の自動推論 API があると想像してください。この API は、C 関数が常に停止する場合は 「yes」 を返し、関数が永遠に実行され得る場合は 「no」 を返します。一例として、 こちら で説明されているツールを使えば、このような API を構築できます (著者自身の過去の研究成果です)。停止性判定ツールが何をしてくれるかを理解するために、2 つの基本的な C 関数を考えてみましょう。1 つは (前述の) g です。 void g(int x, int y) { if (y > 0) while (x > y) x = x - y; } もう 1 つは g2 です。 void g2(int x, int y) { while (x > y) x = x - y; } 既に述べた理由により、関数 g は常に呼び出し元へ制御を返すため、 terminates(g) は true を返すはずです。一方、 terminates(g2) は false を返すはずです。例えば g2(5, 0) は決して停止しないからです。 ここで難しい関数が登場します。 h を考えてみましょう。 void h() { if terminates(h) while(1){} } これが再帰的であることに注目してください。 terminates(h) の正しい答えは何でしょうか。答えは「yes」ではあり得ません。「no」でもあり得ません。なぜでしょうか。 terminates(h) が「yes」を返すとしましょう。 h のコードを読めばわかるように、この場合は h のコード内の条件文が無限ループ while(1){} を実行するため、関数は停止しません。したがってこの場合、 terminates(h) の答えは誤りとなります。 h は自分自身に対して terminates を呼び出す形で再帰的に定義されているからです。 同様に、 terminates(h) が「no」を返すとすれば、 h は実際には停止して呼び出し元へ制御を返します。条件文の if の条件が満たされず、else 分岐も存在しないからです。この場合もやはり答えは誤りとなります。だからこそ、このケースでは 「Don’t know」 という答えが避けられないのです。 プログラム h は、決定可能性に関する Turing の 1936 年の有名な論文 や、1931 年の ゲーデルの不完全性定理 で示された例の変種です。これらの論文が教えているのは、停止性問題のような問題は「解けない」ということです。ただしここで 「 解ける 」 とは、解法手続き自体が常に停止し、 「yes」 か 「no」 のいずれかを答え、決して 「Don’t know」 とは答えないことを意味します。しかし、それは私たちの多くが念頭に置いている「解ける」の定義ではありません。多くの人にとっては、ときにタイムアウトしたり、ときおり 「Don’t know」 と返すことはあっても、答えを返すときには必ず正しい答えを返すツールであれば十分なのです。 この問題は飛行機での移動に似ています。過去に墜落事故が起きており、将来も起きるであろうことは確実なので、100% 安全ではないとわかっています。しかし、無事に着陸したなら、そのときはうまくいったと わかる のです。航空業界の目標は、原理的には避けられないとしても、失敗を可能な限り減らすことです。 これを自動推論の文脈に置き換えると、 h のような一部のプログラムについては、 「Don’t know」 という答えをなくせるほどツールを改善することは決してできません。しかし、今日のツールが 「Don’t know」 と答えるものの、将来のツールなら 「yes」 や 「no」 と答えられるようになるケースは他に数多くあります。自動推論の専門家にとっての現代の科学的な課題は、実用的なツールが 「yes」 か 「no」 を返す頻度を可能な限り高めることです。現在進行中の取り組みの一例として、CMU 教授であり Amazon Scholar でもある Marijn Heule 氏による コラッツの停止性問題を解く挑戦 をご覧ください。 もう 1 つ覚えておきたいのは、自動推論ツールが日常的に「計算困難な」問題、例えば 複雑性クラス NP に属する問題を解こうとしているという点です。ここでも、停止性問題で見たのと同じ考え方が当てはまります。自動推論ツールは強力なヒューリスティックを備えており、特定のケースでは計算困難性の問題を回避できることがよくあります。しかし、そうしたヒューリスティックは失敗し得ますし (実際に失敗することもあり)、その結果として 「Don’t know」 という答えや、実用に耐えない長い実行時間が生じます。ヒューリスティックを改善してその問題を最小化することが、この科学の役割です。 用語について 科学文献では、相互に関連するトピックを表すために多くの名称が使われており、自動推論はその 1 つにすぎません。簡単な用語集を示します。 論理 とは、何が真であり何が真でないかを定義するための形式的かつ機械的な体系です。例: 命題論理 や 一階述語論理 。 定理 とは、論理において真である命題です。例: 四色定理 。 証明 とは、定理に対する論理上の妥当な論証です。例: Gonthier 氏による 四色定理の証明 。 機械的定理証明器 とは、多くの場合人間が書き下した証明を機械可読な形で表現したものを検査する半自動推論ツールです。これらのツールはしばしば人間の手助けを必要とします。例: HOL-light 。開発者は Amazon の研究者 John Harrison です。 形式的検証 とは、コンピュータシステムのモデルに定理証明を適用して、システムの望ましい性質を証明することです。例: 検証済み C コンパイラ CompCert 。 形式手法 とは最も広い意味の用語で、単にシステムのモデルについて論理を用いて形式的に推論することを指します。 自動推論 は、形式手法の自動化に焦点を置いています。 半自動推論 ツールとは、ユーザーからのヒントを必要とするものの、論理において妥当な証明を見つけるツールです。 このように、この領域で仕事をする際には呼び名の選択肢がいくつもあります。Amazon では自動推論という呼び方を選びました。自動化とスケールに対する私たちの意欲を最もよく表していると考えているからです。実際には、社内のチームの一部は自動推論ツールと 半 自動推論ツールの両方を使っています。私たちが採用してきた科学者は、完全自動の推論におけるヒューリスティックが失敗しかねない場面でも、半自動推論ツールを使って成功させられることが多いからです。外部のお客様向け機能については、現在は完全自動のアプローチのみを使用しています。 次のステップ この記事では、ごく小さなトイプログラム (例示用の簡単なプログラム) を用いて自動推論という考え方を紹介しました。ヒープや並行性を含む現実的なプログラムの扱い方には触れていません。実際には、自動推論のツールと技法は非常に多岐にわたり、中にはかなり狭い領域もありますが、多種多様な領域の問題を解いています。それらすべてと、この分野の数多くの系統や下位分野 (例えば「充足可能性モジュロ理論 (satisfiability modulo theories、SMT) の求解」「高階論理の定理証明」「分離論理」) を説明するには、数千本のブログ記事と書籍が必要になるでしょう。 自動推論の起源は、コンピュータの初期の発明者たちにまで遡ります。そして論理そのもの (自動推論が解こうとしている対象) には数千年の歴史があります。この記事を簡潔に保つため、ここで筆を置き、さらに読むべき資料の紹介に移ります。なお、この分野を深さ優先で読み進めると細部に迷い込みやすく、始めたときより混乱してしまう可能性があります。1 つの側面だけを深く学ぶのではなく、深さを制限した深さ優先探索のアプローチで、さまざまなツールや技法をそれぞれ少しずつ順に見ていき、次へ進むことをお勧めします。 おすすめの書籍 Handbook of Practical Logic and Automated Reasoning Temporal Verification of Reactive Systems Decision Procedures Model Checking Software Foundations Specifying Systems Introduction to Static Analysis Logic in Computer Science: Modelling and Reasoning about Systems Functional Algorithms, Verified! Handbook of Satisfiability The Calculus of Computation 国際会議・ワークショップ https://etaps.org/2020/tacas https://ijcar2020.org/ https://popl21.sigplan.org/ http://smt-workshop.cs.uiowa.edu/ ツールコンペティション http://termination-portal.org/wiki/Termination_Competition https://sv-comp.sosy-lab.org/2020/ https://smt-comp.github.io/2020/ http://www.satcompetition.org/ ツールの例 AGREE: http://loonwerks.com/tools/agree.html Alloy: https://alloytools.org/ Aprove: https://aprove.informatik.rwth-aachen.de/ BioModelAnalyzer: https://biomodelanalyzer.com/ Boogie: https://github.com/boogie-org/boogie.git CBMC: https://www.cprover.org/cbmc/ Checked C: https://plum-umd.github.io/projects/checkedc.html Checker Framework: https://checkerframework.org/ CoCoSim: https://github.com/NASA-SW-VnV/CoCoSim Coq: https://coq.inria.fr/ CPA Checker: https://cpachecker.sosy-lab.org/ CVC4: https://cvc4.github.io/ Dafny: https://github.com/dafny-lang/dafny Dreal: https://github.com/dreal/dreal4 HOL light: https://www.cl.cam.ac.uk/~jrh13/hol-light/ Infer: https://fbinfer.com Iris: https://iris-project.org/ Isabelle: https://isabelle.in.tum.de/ Java PathFinder: https://github.com/javapathfinder JKind: https://github.com/loonwerks/jkind KeYmaera X: https://keymaerax.org/ Kind2: https://kind.cs.uiowa.edu/ KLEE: https://klee.github.io Lean: https://leanprover.github.io/ MiniSat: http://minisat.se/ Nagini: https://github.com/marcoeilers/nagini P: https://github.com/p-org/P PRISM: https://www.prismmodelchecker.org PVS: https://pvs.csl.sri.com Rosette: http://emina.github.io/rosette/ Rust プログラミング言語: https://www.rust-lang.org/ [Rust でプログラミングすることは、本質的に型システムの中でメモリ破壊が起こらないことを証明していることになります (unsafe 領域を使用していない場合)] Sally: https://github.com/SRI-CSL/sally SAW: https://github.com/GaloisInc/saw-script SeaHorn: http://seahorn.github.io/ SMACK: https://smackers.github.io Soot: http://soot-oss.github.io/soot/ SPIN: http://spinroot.com/spin/whatispin.html T2: https://mmjb.github.io/T2/ TLA+: https://lamport.azurewebsites.net/tla/tla.html Vampire: https://vprover.github.io/ VCC: https://github.com/microsoft/vcc Verifast: https://github.com/verifast/verifast Z3: https://github.com/Z3Prover/z3 自動推論の活用について語る Amazon スタッフへのインタビュー Byron Cook PLDI’20 Ask Me Anything Byron Cook on The CUBE Neha Rungta on The CUBE Neha Rungta が AWS Config ルールにおける制約ベースの推論ツールについて語る Serdar Tasiran CAV’21 Ask Me Anything LogMeIn: How LogMeIn Automates Governance and Empowers Developers at Scale お客様と業界に向けた AWS の講演 Automating Compliance Verification on AWS Using Provable Security 。AWS のコンプライアンス担当 VP である Chad Woolf と、コンプライアンス監査企業 Coalfire の CEO である Tom McAndrew 氏による講演 An AWS Approach to Higher Standards of Assurance w/ Provable Security 、Byron Cook Dive Deep into IAM Access Analyzer 。Andrew Gacek 他による講演 The Evolution of automated reasoning Technology at AWS 。AWS のセキュリティ担当 VP である Eric Brandwine による講演 AWS の CISO 兼セキュリティ担当 VP である Steve Schmidt による、AWS における形式的/制約ベースのツールの開発と活用に関する 講演 AWS re:Invent 基調講演 、CTO ワーナー ヴォゲルス 自動推論の科学コミュニティに向けた AWS の発表 Debugging Network Reachability with Blocked Paths 、CAV’21 Embedded World 2021: Formally Verifying the FreeRTOS IPC Mechanism 、Embedded World ’21 Formal reasoning about the security of Amazon Web Services 、FLoC 2018 基調講演 Formal reasoning about the security of Amazon Web Services 、OOPSLA/SPLASH 2018 基調講演 How I learned to stop worrying and start applying automated reasoning 、FACC’21 (その他の関連発表は FACC のウェブサイト をご覧ください) On automated reasoning for compliance certification 、Formal Approaches to Certifying Compliance (FACC) に関する CAV ワークショップ Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning 、CAV’21 Provable Security at AWS 、USENIX Enigma 2019 [30 分の箇所までスキップしてください]: SideTrail: Verifying Time-Balancing of Cryptosystems Stratified abstraction of access control policies 、CAV’20 Verified Cryptographic Code for Everybody 、CAV’21 What is automated reasoning? How Is it Used at AWS? AWS のブログ記事と解説動画 A simpler way to assess the network exposure of EC2 instances: AWS releases new network reachability assessments in Amazon Inspector AWS CTO による自動推論グループについてのブログ記事: Proving security at scale with automated reasoning AWS CTO が S3 の整合性について語る AWS ポッドキャストのインタビュー: Provable security podcast: Byron interviews Moshe Vardi AWS ポッドキャストのインタビュー: Next Generation Security with automated reasoning, an Artificial Intelligence Technology AWS Config アップデート – S3 バケットをセキュアに管理する新しいマネージド ルール 。IAM ポリシーに対する自動的な制約解決技法を活用した AWS Config のイベント駆動チェックについて解説しています。さらに 詳細はこちら 新しい Amazon S3 暗号化 & セキュリティ機能 。Amazon Web Services の S3 コンソールにおける、ポリシーに関する制約ベースの推論の活用について解説しています ブログ 1 、 2 、 3 : Galois と協力して、Amazon の暗号インフラストラクチャコンポーネントである s2n の正しさを証明した取り組みについて解説しています Chad Woolf (AWS のコンプライアンス担当 VP) が、コンプライアンス認証を簡素化し水準を高めるために自動推論を活用することへの関心について語る Daniel Schwartz-Narbonne が、AWS のブートコードにおける証明可能なセキュリティの実現に自動推論がどのように役立っているかを紹介 How automated reasoning helps us innovate at S3 scale How automated reasoning improves Prime Video experience How AWS SideTrail verifies key AWS cryptography code How AWS uses automated reasoning to help you achieve security at scale Jeff Barr による IoT 設定検証ツールの紹介 新機能 – VPC Reachability Analyzer Zelkova ベースの新しい AWS Config ルール s3-blacklisted-actions-prohibited と bucket-policy-not-more-permissive がリリース Podcast: AI tech named automated reasoning provides next-gen cloud security Amazon Macie で用いられている制約ベースの IAM ポリシー分析の詳細については、 こちら を参照してください Tightening application security with Amazon CodeGuru Using Formal Methods to validate OTA Protocol … その他の AWS ブログ Amazon Scholar として Amazon と協働する大学教授による講義ノート https://courses.cs.washington.edu/courses/cse507/21au/ http://www.cs.cmu.edu/~mheule/15816-f21/ https://www.cs.cmu.edu/~mheule/15217-f21/ とっておきの深掘りトピック 今日私たちが使っている自動定理証明器に見られるアルゴリズムの一部は、1959 年にまで遡ります。この年に Hao Wang 氏が自動推論を用いて証明したのは Principia Mathematica の定理です。 著者について Byron Cook Amazon の vice president 兼 distinguished scientist である Byron Cook は形式的検証分野のリーダーであり、SAT (充足可能性問題)、SMT、記号的モデル検査への貢献と、生物システム、コンピュータのオペレーティングシステム、プログラミング言語、セキュリティへの応用で知られています。Byron が Amazon で進めてきた自動推論の取り組みは、クラウドにおけるより高い水準の保証と、新たなお客様向け機能をもたらしています。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。

はじめに 1. 注目した次世代ツールの魅力 1.1 Oxlint ── 「今すぐ、設定ゼロで爆速化」 1.2 Biome ── 「これ 1 つで全てが片付く、究極の一本化」 1.3 Deno ── 「セットアップ不要、最高にクリーンな開発体験」 1.4 Ezno ── 「型チェックまで Rust 化する、超未来のコンパイラ」 2. Vue特有の壁： の静的解析問題 3. チームでの議論：「設定ファイル2つは本当に必要か？」 4. 結果 5. 今後の展望 まとめ はじめに フロントエンドエンジニアをしている伊藤と申します。 昨今は、Rust 製のツールが数多く生み出されており、Linter もその波に乗っていると思います。 弊社でも移行をしたブログを書いており、是非下記の記事も読んでみてください。 https://tech.revcomm.co.jp/ai-lint-formatter-oxc 史上稀に見る大波が来ている時代に、私も颯爽と波に乗ろうとしました。 そしてどういった結論に至ったかご紹介させていただきます。 注: 本記事の検証は2026年9月10日時点、Oxlint v1.82.0 / Biome v2.5.12 で行っています。この領域は変化が速いため、お読みいただく時点では状況が変わっている可能性があります。 1. 注目した次世代ツールの魅力 1.1 Oxlint ── 「今すぐ、設定ゼロで爆速化」 最大の魅力：既存のプロジェクトにノーリスクで追加できる メリット ESLint の 50〜100 倍高速 ： 数万行のコードも一瞬でスキャンが終わります。 設定ファイルが不要 ： インストールして実行するだけで、プロ級のバグ検出ルールが最初から動きます。 既存の ESLint と併用可能 ： 重い処理（バグチェック）は Oxlint に任せ、複雑なカスタムルールだけ ESLint に残す「いいとこ取り」ができます。 1.2 Biome ── 「これ 1 つで全てが片付く、究極の一本化」 最大の魅力：Linter と Formatter が融合したオールインワン構造 メリット ESLint と Prettier の多くの用途を一本化できる ： 個別にプラグインを組み合わせる煩わしさから解放されます（ただし後述の通り、Vue の <template> 部分は現状 ESLint との併用が前提になる場面が残っています）。 設定の衝突ゼロ ： Linter と Formatter が同じ思想で作られているため、「Linter と Prettier のルールがバッティングして動かない」という定番のストレスがありません。 圧倒的な構文解析の正確さ ： エラーがあっても壊れたコードを器用にパースし、親切なエラーメッセージを出してくれます。 1.3 Deno ── 「セットアップ不要、最高にクリーンな開発体験」 最大の魅力：最初からすべてが揃っている「環境」そのもの メリット ： ツール選定やインストールの手間がゼロ ： deno lint と deno fmt が最初から内蔵されています。 package.json に大量の依存関係を書く必要がありません。 標準で Web 標準に準拠 ： ブラウザと同じ API をそのままサポートしているため、環境ごとの差異に悩まされません。 Node.js との互換性も強力 ： 近年は Node.js のパッケージもそのまま動くため、敷居が非常に低くなっています。 注意: Deno は Linter 単体のツールではなく、ランタイムとツールチェーンそのものです。既存の Node.js プロジェクトに deno lint だけを差し込むのではなく実行環境ごと移行する話になるため、Oxlint / Biome / Ezno とは比較の土俵・移行規模が異なる点に注意してください。 1.4 Ezno ── 「型チェックまで Rust 化する、超未来のコンパイラ」 最大の魅力：JavaScript の限界を超える、圧倒的に賢く高速な型解析 メリット ： TypeScript（tsc）より遥かに高速 ： 現在、フロントエンド開発で一番時間がかかる「型チェック」のプロセスを Rust で爆速にします。 型推論がスマート ： コードの型をより深く、正確に推論してくれるため、開発者が型定義を細かく書く手間を減らせます。 バグを未然に防ぐ先進性 ： 副作用（Side Effects）の検知など、従来の TypeScript よりもさらに一歩進んだ安全なコード検証が可能です。 注意: ただし Ezno は本記事執筆時点（2026年9月）でまだ feature-complete ではなく、tsc との完全互換を目指しているわけでもありません。既存の大規模プロジェクトの型チェックをそのまま置き換えられる段階ではなく、将来性に注目したい実験的プロジェクトという位置付けです。 どれも高速性を売りにしており、React では非常に乗り換えやすく恩恵も受けられます！ 実際に私もローカルでBiomeの設定を試してみましたが、かなり早かったです。 ではそのまま導入して、Rust の恩恵を受けようとしました。 ただ、Vue になると少し話が変わってくるんです・・・ 2. Vue特有の壁： の静的解析問題 Vue は、HTML5 の標準仕様である <template> を、独自の便利な形に拡張して使っています。 要素に v-if や v-for を付けたり、 <template> を .vue ファイルの枠組みとして使ったりしています。 普段の開発をしている中で、 v-if や v-for を使わないケースはほぼないと思います。 当然ですが、それらの値もチェックしてくれると思っていました。 ただ、 <template> 内は、Oxlint, Biome ともにチェックしてくれないんです。 実際に最新版（Oxlint v1.82.0 / Biome v2.5.12、2026年9月時点）で試した結果を、以下のサンプルコードとあわせてご紹介します。 <template > < div > <!-- ❌ 1. 壁：Linterがここを見ないため、存在しない変数（タイポ）をスルーする --> < p > {{ userNema }} </ p > <!-- ❌ 2. 壁：Linterがここを見ないため、「下で使われている」と認識できない --> < p > {{ unusedMessage }} </ p > </ div > < / template> <script setup lang="ts"> import { ref } from 'vue' const userMessage = ref ( 'こんにちは' ) // 🔴 <script> 内は見ているので、「定義したのに使われていない！」と怒られる // （実際には上の template で使いたいのに、Linterが template を読めないせいで孤立する） const unusedMessage = ref ( 'これはエラーになります' ) < / s cript> Oxlint（v1.82.0） デフォルトでも vue-plugin オプションを付けても、このサンプルに対しては何も警告を出しませんでした。 userNema のタイポも unusedMessage の誤検知も発生しない代わりに、テンプレート側の静的解析自体がまだ行われていない、というのが実態でした。 Biome（v2.5.12） デフォルト設定ではスクリプト側の noUnusedVariables ルールが .vue ファイルにも適用され、 userMessage・unusedMessage の両方を「未使用」としてエラーにします( unusedMessage は実際にはテンプレート側で使われているので、これは誤検知です)。 ただし html.experimentalFullSupportEnabled を有効にすると、Biomeはテンプレート内での参照を認識できるようになり、 unusedMessage の誤検知は解消されました(本当に未使用な userMessage は引き続き正しく検出されます)。 一方で、フラグを有効にしてもテンプレート内の userNema のようなタイポを検出するルールはまだ無く、不正な変数参照を見逃す問題は解消されません。 上記の検証からわかる通り、テンプレート内の静的解析はRust製Linter単体ではまだ完結できません。Biomeは実験的フラグ付きで一部の誤検知を解消できるようになってきていますが、テンプレート内のタイポ検出のような踏み込んだチェックまでは、依然として eslint-plugin-vue に頼る必要があります。 つまり、必要なVue固有のルールと各ツールの対応状況次第では、OxlintまたはBiomeとESLintを併用する必要があるということです。 3. チームでの議論：「設定ファイル2つは本当に必要か？」 Rust製Linter を導入するか、一旦は ESLint のままにするか。 どちらを選択するか検討するため、メリット・デメリットを出してみました。 メリット 圧倒的な高速化 ： 従来のJavaScriptなどで書かれたLinter（ESLintなど）に比べ、数倍〜数十倍高速に動作します。大規模なコードベースでも ミリ秒単位 で処理が終わるため、CI/CDの実行時間を大幅に短縮し、開発者の待ち時間をほぼゼロにします。 開発の快適化 ： 保存時の自動整形や pre-commit フックでの実行が劇的に速くなります。 簡単な導入 ： Rust製ツールはコンパイル済みのシングルバイナリとして配布されることが多いため、環境構築やCIでのセットアップが非常にシンプルになります。 デメリット 二重管理 ：（一番の懸念） Rust製フロントエンドLinter（BiomeやOxcなど）は、 .vue ファイルの構文（HTMLテンプレートやVue固有の構文ルール）を完全にサポートしていません。 そのため、Vue固有のルール（ vue/valid-template-root など）をチェックするには、結局従来の ESLint（eslint-plugin-vue） を残さなければならなくなります TypeScript/JavaScript部分： 爆速のRust製Linter（Biomeなど）でチェック Vueファイル・テンプレート部分： 従来のESLintでチェック プラグインエコシステムの未熟さ ： 歴史のあるESLintなどのように、コミュニティが作った無数のサードパーティ製プラグインを自由に追加することが難しい場合があります。独自のルールを追加したい場合のハードルが高めです。 ルールや構文の追従ラグ： 言語（特にJavaScript/TypeScriptやPython）の新機能や新しい構文が登場した際、Rust側でのパーサ（構文解析器）の対応にわずかなタイムラグが生じることがあります。 4. 結果 結果は、デメリット部分の二重管理の懸念部分が大きく、現状のESLint（eslint-plugin-vue）で管理する方を選びました。 手元の計測で速度については、申し分ないことが立証済みでした。 導入するメリットも大いに感じているものの、2つのLinterを併用する点を上回るほどではないと判断しました。 5. 今後の展望 Biome は既に html.experimentalFullSupportEnabled フラグで Vue SFC の実験的サポートを始めており、Oxlint も vue-plugin オプションなどVue向けの機能を増やしてきています。 「サポートされるのを待つ」というよりも、「実験的サポートがどこまで安定するか・テンプレート内のタイポ検出のような踏み込んだチェックまでカバーされるか」を継続的にウォッチしていく、というのが今の立ち位置です。 各プロジェクトの現状を、ご紹介いたします。 Biome v2.4(2026年2月)で Vue・Svelte・Astro 対応を実験的機能からプロダクション標準に近づける取り組みが発表されました。既存のリンティングルールを強化し、HTMLライクな言語でも機能するようにする方針です。 https://biomejs.dev/ja/blog/roadmap-2026/#2026-roadmap Oxlint 公式ドキュメント上の制限の記載に、Vue も含まれており、改善してくれるはずだと思います。そして、改善のための issue があり開発が進められているのがわかります。 https://github.com/oxc-project/oxc/issues/23207 https://oxc.rs/compatibility.html そしてなんといっても、Oxlint の開発を支援しているのが Vue の開発者である Evan You さんが立ち上げた VoidZero という会社なんです。 現在のフロントエンドの「ツールの断片化（Linter、Formatter、テストツール、ビルドツールがバラバラで設定が面倒かつ遅い）」という課題を根本から解決するためVite+（ヴィートプラス）が開発され、その中に Oxlint も含まれています。 Vue の開発者が、Vue を見放すはずがないんです！弊社が Oxlint にするのも近いですね！ まとめ Rust 製のツールは非常に高速で、すぐにでも乗り換えたいと思ってしまいます。 ただ、メリット・デメリットや今後の展望を踏まえて、検討するのが大事だなと今回の移行作業を通じて感じました。 どのツールにするかもしっかり検討したいです。 AI で開発を行うと、簡単に実行できるため、検討するのをサボりがちになってしまいます。 そういう意味でも今回はいい勉強になったと思います。 お読みいただきありがとうございました。 次は、Oxlint に移行した話でお会いしましょう。

みなさん、こんにちは。ソリューションアーキテクトの戸塚です。今週も 週刊AWS をお届けします。 9月に入り、秋の気配を感じ始めた方も多いのではないでしょうか。今週は AWS Interconnect への Microsoft Azure 接続プレビューや Amazon Linux 2027 のパブリックプレビューなど、幅広いアップデートが揃いました。さて、ちょっと変わったイベントのお知らせです。5体の AI エージェントでチームを組み、自然言語で戦術を指示してサッカーの試合で対戦する「 AWS Agentic Football Cup 」のバーチャルリーグが 9/14（月） に開幕します。Amazon Bedrock AgentCore を使ったマルチエージェント体験を楽しみながら、勝ち上がると AWS re:Invent （11/30〜12/4、ラスベガス） の決勝に招待され、渡航費サポートに加えて優勝賞金 30,000 USD の賞金プールも用意されています。参加無料・コーディング経験不問ですので、腕試しにぜひ登録してみてください。 それでは、先週の主なアップデートについて振り返っていきましょう。 2026年8月31日週の主要なアップデート 8/31(月) Automated Security Response on AWS がカスタム修復向け AI Toolkit を追加 AWS ソリューションの Automated Security Response on AWS (ASR) がバージョン 4.0.0 (2026 年 8 月 26 日リリース) で 4 つの新機能を追加しました。任意の AI アシスタントで ASR 準拠のカスタム修復を生成できる AI Remediation Toolkit、Amazon Inspector / GuardDuty / Macie の検出結果の自動修復、アカウント・OU・リージョン・タグ単位でスコープ設定できる強化版 Web コンソール、Email / Slack / Jira / ServiceNow 向けのマルチチャネル通知アダプターです。カスタム修復の開発期間は数週間から数時間に短縮され、100 以上のセキュリティコントロールを Web コンソールから一元管理できます。 AWS Workload Credentials Provider が Linux および Windows 向けにワンクリックインストールで利用可能に AWS Secrets Manager は、AWS Workload Credentials Provider (AWCP) のワンクリックインストールを発表しました。AWCP は Secrets Manager のシークレットをメモリ内にキャッシュし、ローカル HTTP エンドポイント経由でアプリケーションに提供するエージェントで、AWS Certificate Manager (ACM) からの証明書取得にも対応します。従来は GitHub リポジトリのクローンから Rust でのビルドまで約 6 ステップが必要でしたが、Amazon Linux 2023 では dnf コマンド 1 つでインストールできるようになりました。Linux (x86_64、ARM64) と Windows (x64) 向けのコード署名済みビルド済みバイナリも公開ダウンロード URL から取得できます。Secrets Manager が利用可能な全リージョンで、Secrets Manager の標準料金以外の追加費用なしで利用できます。 Amazon WorkSpaces Applications が新たに 3 つの AWS リージョンで利用可能に Amazon WorkSpaces Applications (旧 AppStream 2.0) が、チューリッヒリージョン、大阪リージョン、カルガリーリージョンの 3 リージョンで利用可能になりました。これにより利用可能リージョンは GovCloud を含む従来の 20 リージョンから 23 リージョンに拡大します。アプリケーションストリーミングはネットワークレイテンシーの影響を受けやすく (推奨 250 ms 以下、100 ms 未満が最良)、エンドユーザーに近いリージョンへの展開で操作の応答性が改善されます。また、日本、スイス、カナダ西部のデータレジデンシー要件やコンプライアンス要件への対応にも利用できます。 AWS Interconnect – Microsoft Azure とのマルチクラウド接続をプレビューで発表 AWS は、AWS Interconnect – multicloud の接続先として Microsoft Azure をパブリックプレビューで追加しました。AWS Interconnect – multicloud は、AWS の VPC と他のクラウドプロバイダーのプライベートネットワークを、マネージド型のプライベート接続で結ぶサービスです。従来はコロケーション施設や自前ルーターを組み合わせた DIY 構成が必要でしたが、AWS Management Console、CLI、API から数分で冗長構成の接続をプロビジョニングできます。すでに OCI と Google Cloud は一般提供 (GA) されており、Azure の追加により主要 3 クラウドとの接続が単一の管理体験に統合されます。プレビューはバージニア北部、北カリフォルニア、シドニー、フランクフルトの 4 リージョンで利用できます。 一元的なエージェント検出とガバナンスのための AWS Agent Registry が一般提供開始 AWS Agent Registry が一般提供 (GA) になりました。組織内のエージェント、ツール、スキル、MCP サーバー、カスタムリソースを登録・承認・検索できるプライベートカタログを提供するフルマネージドサービスです。GA では、プレビューの機能に加えて、AWS CloudFormation・Terraform・AWS CDK による IaC 管理、タグ付け、AWS RAM によるクロスアカウント共有、AWS Organizations 全体での AgentCore リソース自動検出、Amazon Quick 連携が追加されました。バージニア北部、オレゴン、アイルランド、東京、シドニーの 5 リージョンで利用できます。料金は従量課金で、月間 5,000 レコード、Search API 100 万回、List + Get API 200 万回までの無料枠があります。 Amazon Aurora serverless が 最大 30% の性能向上とスケーリング改善を追加リージョンで利用可能に Aurora serverless のプラットフォームバージョン 4 が、ニュージーランド、タイ、ケープタウン、ミラノ、メキシコセントラル の 5 リージョンで追加提供されました。プラットフォームバージョン 4 は、バージョン 3 と比較して最大 30% の性能向上と、複数タスクがリソースを奪い合うワークロードに対応する改良版スケーリングアルゴリズムを含みます。Aurora PostgreSQL と Aurora MySQL の両方が対象で、追加費用はかかりません。新規クラスター、リストア、クローンは自動的にプラットフォームバージョン 4 で起動し、既存クラスターは保留中のメンテナンスアクションの適用、停止と再起動、または blue/green デプロイのいずれかでアップグレードできます。 9/1(火) Anthropic の新しいフロンティアモデル Claude Fable 5.1 が AWS で利用可能に Anthropic の最上位フロンティアモデル Claude Fable 5.1 が AWS で一般提供を開始しました。コンテキストウィンドウ 1M トークン、最大出力 128K トークンで、数時間規模のコーディングやエージェントワークロード、ナレッジワークに向けた設計です。アクセス経路は Amazon Bedrock と、Anthropic が運用する Claude Platform on AWS の 2 つがあります。本モデルは「Covered Model」に指定されており、利用には 30 日間のデータ保持と AWS レビューへのオプトインへの同意が必須です。30 日間のデータ保持を受け入れられないお客様向けには、監視用データを自社管理の AWS 環境に保持したまま利用できる Enterprise Frontier Safeguards (EFS) が、対象のお客様から 2026 年秋以降段階的に展開される予定です。 AWS Marketplace がプライベートオファーの自動更新に対応 AWS Marketplace で、プライベートオファーに自動更新 (auto-renewal) 条件を設定できるようになりました。契約期間の満了時に、交渉済みの価格と契約条件を引き継いだ新しい契約が自動的に作成されるため、再交渉や再購入の手続きが不要になります。販売者は「価格据え置き」「固定率の値上げ」「範囲内での値上げ」の 3 種類から更新時の価格ルールを選択でき、購入者はオファー承諾時および更新決定期限までの間、自動更新のオプトイン/アウトを変更できます。契約価格 (contract pricing) を使う直接プライベートオファーが対象で、すべての商用リージョンで追加設定なしに利用できます。 9/2(水) Amazon SageMaker Unified Studio CI/CD がノートブックプロモーションと AI 支援によるマニフェスト生成を追加 Amazon SageMaker Unified Studio (SMUS) のオープンソース CI/CD ツールキット (aws-smus-cicd-cli) に 2 つの機能が追加されました。1 つ目は generate-bundle-manifest エージェントスキルで、プロジェクトの接続・ストレージ・ワークフローを読み取り専用で調査し、デプロイマニフェストを自動生成します。2 つ目はネイティブ SMUS Notebook のプロモーション機能で、開発・テスト・本番の各環境へノートブックを冪等に同期し、実行履歴を保持したまま更新できます。どちらもオープンソースとして GitHub で公開されており、SMUS が利用可能なすべてのリージョンで使用できます。 Amazon Connect Customer が agentic CX designer の一般提供を開始 Amazon Connect Customer は、AI を活用したセルフサービス体験を設計・展開するためのノーコードキャンバスである agentic CX designer の一般提供を開始しました。ビジュアルキャンバス上で、LLM が推論する agentic なステップと、適格性判定やコンプライアンス開示など正確さが必須の deterministic なステップを 1 つの会話の中で組み合わせられます。設計、外部システム統合、テスト、本番デプロイまでを同一の場所で完結でき、業務チームがコードを書かずに数週間で本番稼働まで到達できます。本機能は AWS が 2026 年に買収した会話型 AI 企業 NLX の技術を基盤としており、2026 年 6 月 22 日のプレビュー発表を経て GA となりました。東京リージョンを含む 9 リージョンで利用できます。 Amazon Quick がコネクタ向けの新しいツール設定と Model Context Protocol (MCP) 同期サポートを追加 Amazon Quick のコネクタに、ツール単位の有効化/無効化、ツール実行前の同意 (consent) を制御する権限設定、外部 MCP サーバーの変更を自動反映する MCP sync の 3 機能が追加されました。コネクタは Outlook、Slack、Salesforce、Jira や自社開発の MCP サーバーを、チャット、エージェント、アプリ、フロー、ディープリサーチから利用するための仕組みです。従来は MCP サーバー側でツールが追加・変更されるとコネクタを削除して再作成する必要がありましたが、MCP sync によりこの運用が不要になります。管理者とコネクタオーナーは、承認済みツールのみをエンドユーザーに公開するガバナンスを構成できます。Amazon Quick が利用可能なすべてのリージョンで利用できます。 9/3(木) Amazon SES が S/MIME メール署名のサポートを開始 Amazon SES が S/MIME (Secure/Multipurpose Internet Mail Extensions) によるメールのデジタル署名に対応しました。署名用証明書を AWS Certificate Manager (ACM) に保存し、送信 ID に関連付けたうえで設定セットの S/MIME 署名を有効化すると、SES が送信時にサーバー側で自動的に署名を付与します。従来は送信者がメッセージを SES に渡す前に自前で署名する必要がありましたが、この作業が不要になります。受信者は From アドレスの保持者本人が送信したこと、および本文が転送中に改ざんされていないことを検証できます。本機能は SES が利用できるすべての AWS リージョンで利用できます。 Amazon Linux 2027 のパブリックプレビューを発表 AWS は Amazon Linux の次期メジャーバージョンである Amazon Linux 2027 (AL2027) のパブリックプレビューを公開しました。AL2023 をベースラインとして、カーネル 7.1、GCC 16.1、Python 3.14 など主要コンポーネントを刷新し、SELinux をデフォルトで enforcing モードに変更しています。ポスト量子暗号 (PQC) がデフォルトで有効になり、AWS-LC による暗号処理の高速化と AWS Neuron ドライバのサポートも含まれます。プレビュー AMI は全商用リージョンで x86-64 / ARM の両アーキテクチャ向けに提供され、コンテナベースイメージは Amazon ECR Public Gallery から取得できます。サポート期限は 2032 年までと案内されており、AL2023 (2029 年 6 月サポート終了) からの移行先となります。 Amazon Quick Max を発表: Quick を最大限活用するパワーユーザー向けに 5 倍の使用量を提供 Amazon Quick に新しい上位プラン「Quick Max」が追加されました。Max は Plus プランの 5 倍の使用量と 5 倍のインデックスストレージ (10 GB → 50 GB) を提供し、月をまたいで大規模なワークロードを中断なく実行したいパワーユーザーを対象としています。料金は年払いで月額 100 USD/ユーザー、月払いで月額 125 USD/ユーザー です。既存の Plus ユーザーは画面左ナビゲーション下部のユーザー名から「Upgrade plan」を選択するだけで切り替えでき、アップグレードは即時に有効になります。 9/4(金) AWS MCP Server が AWS Lambda 関数向けの serverless capability を追加 AWS MCP Server に serverless capability が追加され、Claude Code や Kiro などのコーディングエージェントが Lambda 関数とその接続リソースの障害を診断できるようになりました。エージェントは 1 回のツール呼び出しで、7 日間ベースラインとの比較によるメトリクス異常検知、ログの構造化サマリー、デプロイ済み設定、変更タイムライン、X-Ray トレースの分析結果を取得できます。複数の API 呼び出しをエージェント側で組み立てる場合と比べて、トークン消費を抑えられます。serverless capability は追加料金なしで利用でき、AWS MCP Server 自体はバージニア北部リージョンとフランクフルトリージョンで稼働します。 Amazon Bedrock Managed Knowledge Base がデータソースコネクタの自動同期スケジュールに対応 Amazon Bedrock Managed Knowledge Base で、データソースコネクタの自動同期スケジュールを設定できるようになりました。従来はソースデータの変更のたびに手動で同期を実行するか、EventBridge Scheduler などでカスタムの仕組みを構築する必要がありました。今回のアップデートにより、日次、週次、月次の 3 種類の頻度をデータソース単位で設定でき、Confluence や SharePoint、Amazon S3 などのネイティブコネクタ全てに適用できます。同期は増分処理のため、前回同期以降に追加、変更、削除されたドキュメントのみが処理されます。RAG アプリケーションのデータ鮮度維持にかかる運用作業を削減できます。 Amazon Bedrock Managed Knowledge Base が SharePoint、OneDrive、Confluence データソースのユーザー管理セットアップを導入 Amazon Bedrock Managed Knowledge Base の SharePoint、OneDrive、Confluence データソースで、ユーザー管理セットアップ (3LO: 3-legged OAuth) が利用できるようになりました。従来はサービスアカウント方式 (2LO) の認証情報を第三者システム側で発行する必要があり、管理者権限を持たないユーザーは IT 部門との調整が必要でした。本アップデートにより、既存の Microsoft 365 アカウントや Atlassian アカウントでサインインするだけで、数分でデータソースの接続を完了できます。ただし 3LO は文書レベルのアクセス制御 (ACL) に対応しないため、本番ワークロードには引き続き Entra ID App-Only などのサービスアカウント方式が推奨されます。 今週は AWS Agent Registry の GA や Amazon Quick の新機能追加など、エージェント関連のアップデートも目立ちました。エージェントの検出・ガバナンスからツール管理まで、エージェント開発の土台が着実に整ってきている印象です。年末の re:Invent（11/30〜12/4）に向けてさらにアップデートが加速しそうですね。来週もお楽しみに！ それでは、また来週お会いしましょう！ 著者について 戸塚 智哉(Tomoya Tozuka) / @tottu22 飲食やフィットネス、ホテル業界全般のお客様をご支援しているソリューション アーキテクトで、AI/ML、IoT を得意としています。最近では AWS を活用したサステナビリティについてお客様に訴求することが多いです。 趣味は、パデルというスペイン発祥のスポーツで、休日は仲間とよく大会に出ています。