30: Formally verified cloud-scale authorization

AWSがDafnyという言語を用いてIAMの仕様検証と実装の置き換えを行った件について、解説論文をネタに雑談しています。後半は次期Pythonで実装されると思われるt-stringという新しいリテラル表記について話しました。

• Formally verified cloud-scale authorization - Amazon Science
  • AWS re:Inforce 2024 - Proving the correctness of AWS authorization (IAM401)
  • 以前紹介した記事 An unexpected discovery: Automated reasoning often makes systems more efficient and easier to maintain | AWS Security Blog 
• PEP 750 – Template Strings

Chapters:
(00:00) Opening
(03:28) Formally verified cloud-scale authorization 論文の概要
(12:28) Dafny言語
(19:10) shadowテスト
(25:15) PEP 750 Template String