…(2019) による論文 "Formal Foundations of Serverless Computing" を軸にしています。この論文はサーバーレスコンピューティングに対して操作的意味論の定式化を行うものであり、プログラミングの国際学会 OOPSLA '19 の Distinguished Paper を受賞しています。 なお、同様のテーマは AWS Dev Day 2022 でも登壇しています。スライドも大部分は共通ですが、解説が不足していた点を具体的に補足したり、…

… Jangda らの論文、Formal foundations of serverless computing について解説しました。OOPSLA '19 の Distinguished Paper にも選出されています。 解説したのはこの論文のうち前半部分、具体的には Section 4 まで相当です。イベントの参加者の大半はこのような形式化には慣れていないことを考え、後半部分のより現実的かつ複雑な意味論を諦める代わりに「操作的意味論とはなにか」「推論規則の読み方」「双模倣…

…されている 2 本の論文をベースにして解説を行いました。VPC Rechability / Network Access Analyzer は内部的には AWS Tiros と呼ばれるエンジンがクエリ処理を担っており、さらにそのバックエンドとして SMT ソルバの MonoSAT を使用しています。これに加え「不通の原因部分を含む完全な経路」をユーザに提示するため、与えられた制約をいくつかのクラスに分類し、段階的に Minimal Correction Subset (MCS…

…的な基礎付けを与えた論文 "Formal Foundations of Serverless Computing" を発表しました。今回の講演はこの論文、特に前半部分に焦点を当てたものです。上記の「プラットフォームの都合」を織り込んだサーバーレスの意味論、およびより直感的な挙動を表現した単純化された意味論の 2 種類を定義し、両者が弱双模倣の関係となる条件を記述するところまでを解説しました。 今回の講演の主眼は論文紹介ではありますが、あくまでも計算機科学に馴染みがない参加者に…

…す。 元になっている論文は以下です。 ieeexplore.ieee.org July Tech Festa は 20 分しか枠がないこともあり、スライドの最後のほう、論文に述べられた SMT エンコーディングを解説する部分がちょっと消化不良になってしまいました。この反省点は、次に挙げる CI/CD Conference 2021 で活かされています。 ccvanishing.hateblo.jp なお、この発表はログミー Tech にて書き起こしが掲載されています。 log…

…ジン Tiros の論文 [Bac19] を解説することです。そのための道筋として、Section 1 で VPC Reachability Analyzer の機能を簡単に紹介した後、Section 2 でその要素技術である SMT ソルバの仕組みを解説し、最後に Section 3 として VPC ネットワークの意味論を SMT ソルバ用にエンコーディングする方針について解説します。 VPC Reachability Analyzer AWS 上でネットワークが意図通りの…

…およびその元となった論文について発表してきました。公募 CFP 枠です。 発表の大筋は、少し前に July Tech Festa 2021 で登壇した際のものと共通です。関連リンク集などは以下の記事にまとめてあるので、よかったらこちらも合わせてお読みください。 ccvanishing.hateblo.jp 内容面では、前回の発表時間 20 分に対して今回は 40 分の枠をもらっていたので、 Level 1-3 として定式化した「検査水準」とツールの対応を明確にすること Zel…

…関する情報は、以下の論文に基づきます。 ieeexplore.ieee.org 参考リンク IAM Access Analyzer IAM Access Analyzer 自体は無料で利用することができます。いくつかのリソースに対してアクセス権限の検査ができるようになっていますが、実験する場合は S3 Bucket の Bucket Policy で試すのが最も簡単で、結果もわかりやすいと思います。 docs.aws.amazon.com aws.amazon.com 例えば…

…この一般化を利用して論文中では、分岐時間的 (branching-time) な性質、すなわちここまで見てきたような状態の直線的な無限列ではなく、状態をノードとするような木構造に対して定義された性質についても、従来と類似の分解定理が成立することが示されている。 定理：任意の分岐時間的な性質は、existentially safe な性質と existentially live な性質の共通部分、universally safe な性質と universally live の共…

…いている時点ではまだ論文を充分読み込んでいないので何とも言えませんが、内容がきちんと把握できたら改めてどこかのイベントで発表したいと思います。 Scheduler Extender github.com スケジューリング処理の一部分を JSON Webhook で外部サーバに委譲するための仕組みが Extender です。 Extender が設定できる処理は以下の 4 か所で、Scheduler 起動時の設定ファイルに外部サーバのエンドポイントなどを記述することで有効になり…

…なっているのは以下の論文で、発表中取りあげた TLA+ による形式化もこれに基づきます。 www.microsoft.com アブストラクトを読むとわかる通り、実はこの論文は二相コミットに関するものではありません。「トランザクションコミットに Paxos を使用した」というのが趣旨で、二相コミットは単なる引き立て役です。とはいえ今回の発表と無関係というわけでもなく、Paxos を用いたコミットについても TLA+ コードが載っているので、興味がある人は読んでみると面白いでしょ…

…いて検証する、という論文が見つかったので参考までに読んでみました。 Zahoor E., Asma Z., Perrin O. (2017) A Formal Approach for the Verification of AWS IAM Access Control Policies. In: De Paoli F., Schulte S., Broch Johnsen E. (eds) Service-Oriented and Cloud Computing. ESOC…

…に特化せず、参照した論文中で述べられている AWS 内での取り組みをもう少し前面に出そうかと思っていました。スライドの途中で TLA+ の名前が出てくるのは名残です。 ただ TLA+ は完全にオートマトン型の典型的なモデル検査器であり、AWS を 使う側 とは相性があまり良くなかったため、具体的な内容は結局すべて外してしまいました。その分 Alloy についてはこの発表を聞いた人がとりあえず触ってみる程度のことは説明できたので、まあ結果オーライかなとは思います。 ところで、今…

…Java を導入した論文はここで読めます。今回の LT では時間の都合上細かい内容をほとんど述べていないので、もし興味があればぜひ元論文に目を通してみると面白いと思います。なお LT で扱ったのは第 2 章で述べられている（ジェネリクスを持たない）FJ の部分です。 スライドの補足 型付け規則と簡約規則について、時間の制限もあり LT の中では例を 1 つずつ挙げるだけに留めました。しかしそのせいでスライド 25 ページ目の主張で "two impolite rules" と…