Developers Summit 2020 で使用したスライドです。 言葉というものは曖昧です。複数人が「ともにつくる」システムにおいて、メンバ間で仕様を正しく共有することは非常に重要ですが、一方で言葉の裏側に隠された「暗黙の仮定」を見抜くことは簡単ではありません。このような仕様の曖昧性への対抗手段として、本セッションでは「形式手法」を紹介します。形式手法ではシステムの挙動を数学的に記述することにより、自然言語の持つ曖昧性を排除し、仕様が満たされるかどうかを厳密に検証することが可能になります。あなたの頭の中にある仕様がどのように「数学的な記述」に変換されるのか、具体例を通して体験してみませんか？ イベント概要：https://event.shoeisha.jp/devsumi/20200213/session/2380/

July Tech Festa 2019 で使用したスライドです。 近年、テストを書く文化は広く普及しており、開発フローにおいて自動テストを組み込むことはもはや常識となりました。しかしよく考えてみると、有限個のテストケースが保証しているのは、所詮「特定の有限個の入力に対する出力」にしか過ぎません。では「あり得る全ての入力」に対してプログラムの性質を保証することは果たして可能でしょうか？ この問いに対する答えのひとつが「定理証明」と呼ばれる手法です。定理証明では、数学的な「証明」をプログラム上でエンコードすることにより、真に「全ての入力」を扱うことができます。本セッションではこの定理証明を取り上げ、従来のテストとの考え方の違いや具体的な適用方法について、サンプルを交えつつ解説します。 イベント概要：https://2019.techfesta.jp/speakers#A10

builderscon tokyo 2019 で使用したスライドです。 本セッションでは、形式手法 (formal methods) を用いた分散アルゴリズムの検証について解説しました。形式手法は、数学的な表現を用いて対象となるシステムを定式化することにより、システムの挙動の「正しさ」を厳密に保証するための方法論です。 なお解説として取り上げたのは、AWS による事例論文でも有名なモデル検査器 TLA+ です。講演前半で形式手法の一般論に触れたのち、後半では分散トランザクションを実現するための TCC (Try-Confirm/Cancel) Pattern のモデリングと検証を行いました。 講演概要：https://builderscon.io/tokyo/2019/session/fa356ee3-6be9-4850-ac9e-037bd34aabaa 録画：https://www.y

Cloud Native Meetup Tokyo #4 で使用したスライドです。CNCF プロジェクトのひとつ、Notary についてその役割とアーキテクチャを解説しています。Notary は何らかのデータを安全に配信するためのフレームワークで、同じく CNCF プロジェクトの The Update Framework (TUF) に基づいています。特に Docker の Tag と Digest を結びつけることで Docker image が改竄されていないことを保証でき、Docker Hub でも利用可能です。 イベント概要：https://cloudnative.connpass.com/event/97281/

July Tech Festa 2018 で使用したスライドです。二相コミットを例として、分散アルゴリズムの検証にモデル検査を使用する手法について解説しています。また、代表的なモデル検査ツールである SPIN、TLA+、P について、同じシステムを各ツールで記述してみることでその特定の違いについて学びます。 イベント概要：https://2018.techfesta.jp/speakers#C40 ブログ記事：http://ccvanishing.hateblo.jp/entry/2018/08/01/055608

AWS Dev Day Online Japan 2021 で使用したスライドです。 許可しているはずのインスタンス間でなぜか通信が通らない、逆に意図しないアクセスが許可されていた、そしてこの種のデバッグはかなり辛い…！ そんなときは、通信経路を自動でチェックしてくれる VPC Reachability Analyzer の出番です。この機能が面白いのは、チェックの際に実際に通信を行う必要がなく、いわば設定項目の「意味」を理解した上で結果を「推論」してくれる点。本講演では、背景となる数学的な理論や論文にも踏み込みつつ、AWS ネットワークの意味論を用いた検査技術を解説します。 イベント概要：https://aws.amazon.com/jp/about-aws/events/2021/devday/ ブログ記事：https://ccvanishing.hateblo.jp/entry/20

Developers Summit 2023 Summer で使用したスライドです。 サーバーレスアーキテクチャは強力ですが、同時に冪等性やトランザクションなど特有の考慮事項が必要であり、高い設計力が求められます。ところで、安全なプログラムを書く上で、静的型付き言語は広く利用されていますね。型はいわば実行前に間違いを検出できる仕組みであり、その背後には「プログラムの正しさ」を厳密な数式で記述し分析する理論が存在します。では、同様に「サーバーレスの正しさ」も厳密な数式で記述することは可能でしょうか？本講演ではAWS Lambdaを用いた設計を例として取り上げながら解説します。 イベント概要：https://event.shoeisha.jp/devsumi/20230727/session/4486/ ブログ記事：https://ccvanishing.hateblo.jp/entry/20

July Tech Festa 2021 winter で使用したスライドです。 バグのない分散システムの設計は果たして可能でしょうか？ この問いに対する一つの答えとして、CockroachDB では形式手法ツール TLA+ を用いて分散トランザクションの正しさを担保しています。 形式手法はシステムの挙動を数学的に解析する技法で、「ノードが特定のタイミングで故障した場合にのみ発生するバグ」といった再現困難な問題を確実に検出することができます。 本講演では、CockroachDB の事例を通して、形式手法が実世界で活用されている様子をお伝えします。 イベント概要：https://techfesta.connpass.com/event/193966/ ブログ記事：https://ccvanishing.hateblo.jp/entry/2021/01/24/185819 録画：https:/

CI/CD Conference 2021 で使用したスライドです。 S3 オブジェクトを不必要に公開してしまったり、あるいは遮断されるべきネットワークが繋がってしまったりといったセキュリティ上の設定ミスは、可能な限り避けたいものです。 このようなインフラ層に対するテストを従来の CI/CD の一部として組み込む場合、「個別の設定項目が条件を満たすことを確認する」または「実際にデプロイした環境に対してアクセスしてみる」といった形でテストを行うことが一般的でしょう。 しかしセキュリティ設定には、「複数の設定項目が絡み合った結果、最終的なアクセス可否が定まる」かつ「実際にデプロイする前に影響範囲を知りたい」といった要求があり、上にあげたテストの形式とはあまり相性が良くないのが事実です。 この問題に対して有効な手法の一つが Automated Reasoning です。Automated Rea

AWS Dev Day 2022 Japan で使用したスライドです。 AWS Lambda を初めとするサーバーレスコンピューティング基盤には、 * 複数の関数が同時に実行され共有リソースにアクセスしうる、本質的に並行システムである * Warm Start により関数インスタンスが内部状態を残したまま再利用されうる * 一つのリクエストに対して複数回の実行が行われうる、いわゆる At-Least-One 特性 といった特性があり、通常のプログラムと比較して実行モデルが複雑かつアンコントローラブルな要素を多く含みます。関数を実装する側はこのような「プラットフォームの都合」を考慮して冪等性など細かい挙動に気を配りつつプログラムを書くことになり、これは一般にかなりの実装コストになります。また、アンコントローラブルな要素は、関数の実装から実際の挙動を静的に検査することを難しくしています。 この

CloudNative Days Tokyo 2019 で使用したスライドです。 Kubernetes は既にコンテナオーケストレータのデファクトを獲得し、多種多様なアプリケーションがデプロイされるプラットフォームとなりました。この流れの中で、従来の機能ではカバーできない複雑なコンテナ配置ロジックや、リソース集積率の最適化に対する需要も高まっています。本講演では、カスタマイズの手法から次世代の特殊スケジューラまで、Kubernetes におけるコンテナ配置のすべてをお話しします。 イベント概要：https://cloudnativedays.jp/cndt2019/ ブログ記事：https://ccvanishing.hateblo.jp/entry/2019/07/30/112634 録画：https://www.youtube.com/watch?v=EsZLJT5uQ5E

DevOpsDays Tokyo 2021 で使用したスライドです。 Infrastructure as Code を導入してみたはいいけれど、デプロイしてみたらなぜか上手く動かない。そんな経験はありませんか？ 本セッションでは、実際の環境を構築する「前」に、IaC のコード自体に対してテストを行う手法について解説します。 ご存知の通り Infrastructure as Code (IaC) は、インフラをコードで定義することを通し、アプリケーション開発のベストプラクティスをインフラ領域にも輸入しようとする方法論です。IaC の考え方は近年急速に普及し、開発フローの一部として種々の IaC ツールを利用することは半ば常識のような状態にあります。 しかし同時に、IaC は銀の弾丸ではありません。特に組織的な導入を考えようとすると、得てして「なぜか上手くいかない」「余計に運用が辛くなってしま