チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

CI/CD Conference 2021 で Zelkova の論文について話してきました

こんにちは、チェシャ猫です。

先日開催された CI/CD Conference 2021 で、AWS の IAM Access Anazlyer のバックエンドとして使用されている検査エンジン Zelkova、およびその元となった論文について発表してきました。公募 CFP 枠です。

発表の大筋は、少し前に July Tech Festa 2021 で登壇した際のものと共通です。関連リンク集などは以下の記事にまとめてあるので、よかったらこちらも合わせてお読みください。

ccvanishing.hateblo.jp

内容面では、前回の発表時間 20 分に対して今回は 40 分の枠をもらっていたので、

  • Level 1-3 として定式化した「検査水準」とツールの対応を明確にすること
  • Zelkova による IAM Policy の SMT エンコードについてより具体的に述べること

の 2 点を中心に内容の整理・再構成を行いました。特に後者についてはスライドの構成に大幅に手を入れたので、前回よりかなり分かりやすいプレゼンになったのではないかと自負しています。

なお、スライド中にも宣伝を入れた通り、AWS の「もう一つの推論エンジン」であるネットワーク検査エンジン Tiros については、AWS Dev Day Online 2021 で詳しくお話しする予定です。Z3 のみをバックエンドとする Zelkova と異なり、Tiros では MonoSATSoufflé、そして Vampire という複数のソルバを組み合わせて推論を行うのですが、それはまた別の話。

aws.amazon.com