April 26, 2025

30: Formally verified cloud-scale authorization

34 minutes

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

...more

By ichizerofm