2021 年のアウトプットを全部一気に思い出す
こんにちは、チェシャ猫です。2021 年中は大変お世話になりました。
今年もいくつか外部で発表を行いましたが、その中には登壇報告の形でこのブログに載せていなかったり、スライドとして公開していないものがあります。自分自身の記録も兼ねて、本記事では 2021 年のアウトプットを一覧としてアーカイブしておきたいと思います。
2021 年の活動実績
2021 年の登壇は 9 件でした。うち（先着や抽選ではなく）CFP に応募して採択されたものは 5 件 です。傾向として以前よりも LT の割合が少なくなり、比較的長尺の登壇がメインになりました。
- CockroachDB から覗く型式手法の世界【CFP 採択】
- ポリシエンジン Kyverno 入門
- containerd をソースコードレベルで理解する
- containerd をソースコードレベルで理解する（再演）
- Infrastructure as Code の静的テスト戦略【CFP 採択】
- Kubewarden を使って任意の言語でポリシを書こう
- AWS セキュリティは「論理」に訊け！ Automated Reasoning の理論と実践【CFP 採択】
- 君のセキュリティはデプロイするまでもなく間違っている【CFP 採択】
- ネットワークはなぜつながらないのか 〜インフラの意味論的検査を目指して〜【CFP 採択】
また、登壇報告以外に単独の記事を 1 件 書きました。Zenn デビュー作です。今後はこちらも拡充していければと思います。
以下、個々の内容について簡単な解説コメントを交えて振り返ります。
CockroachDB から覗く型式手法の世界
July Tech Festa 2021 winter での発表です。録画はこちら。
CockroachDB の Parallel Commit の設計に TLA+ が使用された事例について、形式手法が必要とされる理由、Parallel Commit のプロトコル、および実際に使用されている TLA+ の言語機能について解説しています。
内容は CloudNative Days Tokyo 2020 で話した同タイトルのスライドをほぼ踏襲していますが、時間が 10 分伸びたため、CockroachDB 以外の TLA+ 採用事例や分散システムにおける Chaos Engineering の位置付けについて解説を追加しました。
本当は TiDB や Azure Cosmos DB、elasticsearch などの話を盛り込んで「データベースと形式手法」的なコンテンツにする予定だったのですが、時間との兼ね合いで最終的には CockroachDB に絞ることになりました。
ポリシエンジン Kyverno 入門
Kubernetes Meetup Tokyo #40 での発表です。録画はこちら。
Kubernetes 向けに Policy as Code を実装する場合、現状では Open Policy Agent (OPA) とその関連ツールがデファクトスタンダートになっています。しかし OPA はポリシの記述に Prolog ベースの Rego 言語の知識を要求するため、組織内で横展開しようとすると学習コストの高さが問題になります。
この学習コスト問題をどうにかしようとして登場したツールの一つが Kyverno です。Kyverno ではポリシを YAML で記述します。YAML なのでロジックの表現力には劣りますが、Rego よりも手軽に記述することができます。さらに、Rego の記述を文字列として Manifest に埋め込む OPA と異なり、YAML であれば Kubernetes のリソースとして自然な統合が可能です。
という話をしようと思ったのですが、なんとちょうど前日に 別の方が他のイベントで Kyverno に関する LT をされていた ため、自分からは特に説明する内容がなくなりました。まあ人生、そんな日もあります。
containerd をソースコードレベルで理解する
CloudNative Days Spring 2021 ONLINE での発表です。録画はこちら。
Pod を起動させる際、Kubernetes は Container Runtime Interface (CRI) というインターフェスに従い、gRPC 経由で外部ランタイムに処理を移譲します。containerd や CRI-O は CRI ランタイムの例です。
この発表では、containerd の CRI 関連部分に絞って、Pod 起動の際に辿る処理の流れをソースコードベースで解説しています。
ソースコードの構造を理解する上で鍵になるのは、containerd の Modular Monolith 的なアーキテクチャです。バイナリとしては一つにまとめてビルドされていますが、各モジュールが処理を他のモジュールに移譲する際、直接相手のメソッドを呼ぶのではなく、クライアントを経由してあたかも外部サーバへのアクセスであるかのように呼び出します。
containerd をソースコードレベルで理解する（再演）
Kubernetes Internal #7 での発表です。録画はこちら。
解説の流れは上記の CloudNative Days Spring 2021 ONLINE とほぼ同じです。
スライドの表紙が「ちょっと詳しい版」となっていますが、実際にはスライド自体にはほとんど差はありません。Kubernetes Internal は Discord を使用し双方向で進めることができるので、聴衆の反応を反応を見つつ、アドリブで追加説明を入れたり GitHub 上の関連プロジェクトなどを紹介したりしています。
Infrastructure as Code の静的テスト戦略
DevOpsDays Tokyo 2021 での発表です。
内容・スライドは CloudOperatorDays Tokyo 2020 でお話しした内容をおおむね踏襲し、細かい部分に時間経過に伴う更新を入れました。
「Infrastructure as Code を実践しようとしたが、なかなかスムーズにいかなくて辛い」というのは大なり小なり覚えがあるところだと思います。
発表の前半ではこの問題を言語化するために「予測可能性」という考え方を導入しました。さらに後半では AWS を取り上げ、予測可能性を担保するための方法論や具体的なツールの適用について解説しています。
この発表は、ものすごく久しぶりのオンサイト登壇になったという意味で、個人的には思い出深いものです。マイクを持って物理的に対面して話すのことの効果は大きく、久々に自分の本来のペースが出せたので非常に良かったです。
なお、この発表はログミー Tech にて全 3 回に分けて書き起こしが掲載されています。
Kubewarden を使って任意の言語でポリシを書こう
Kubernetes Meetup Tokyo #42 での発表です。録画はこちら。
Kyverno に引き続き、Kubernetes 向け Policy as Code に関する発表の第二弾です。
ポリシを YAML で記述する Kyverno と異なり、Kubewarden は WebAssembly で記述します。そのため、WebAssembly が生成できる言語なら何でも（理屈の上では）利用可能で、タイトルに「任意の言語で」と入れたのはこれを意図しています。スライド中では Go (TinyGo) で書く場合を例として取り上げました。
AWS セキュリティは「論理」に訊け！ Automated Reasoning の理論と実践
July Tech Festa 2021 での発表です。録画はこちら。
SMT ソルバ Z3 を利用して AWS の権限周りを検査する推論エンジン、Zelkova について解説しました。
Zelkova は AWS IAM Access Analyzer や AWS Config に統合されており、危険なアクセスを許可していないかを自動で保証することができます。
元になっている論文は以下です。
July Tech Festa は 20 分しか枠がないこともあり、スライドの最後のほう、論文に述べられた SMT エンコーディングを解説する部分がちょっと消化不良になってしまいました。この反省点は、次に挙げる CI/CD Conference 2021 で活かされています。
なお、この発表はログミー Tech にて書き起こしが掲載されています。
君のセキュリティはデプロイするまでもなく間違っている
CI/CD Conference 2021 での発表です。録画はこちら。
July Tech Festa 2021 と同じく、Zelkova による AWS 上のセキュリティ検証の仕組みを解説しています。
前回が 20 分枠だったのに比較してこちらは 40 分枠なので、同じ題材でもより分かりやすく解説することができたと自負しています。特に後半、IAM Policy の意味論を SMT ソルバ用にエンコードする部分について、順を追って必要な仕組みを整理してあります。
ネットワークはなぜつながらないのか 〜インフラの意味論的検査を目指して〜
AWS Dev Day Online Japan 2021 での発表です。録画はこちら。
SMT ソルバを利用して AWS のネットワーク周りを検査する推論エンジン、Tiros について解説しました。
Tiros はこの登壇時点で VPC Reachability Analyzer や Amazon Inspector に統合済みでした。2021 年 12 月には VPC Network Access Analyzer も提供されており、単なる到達性だけでなく、ネットワークが無闇に解放されていないかどうかをセキュリティの観点から確認することもできるようになっています。
元になっている論文は以下です。
この論文では、AWS のネットワークを検査する上で採用するエンジンとして、Datalog の処理系 Soufflé、SMT ソルバ MonoSAT および一階述語論理の自動定理証明器 Vampire の三種類を比較をしています。実際に採用されたのは MonoSAT で、MonoSAT はグラフについての理論が実装されている点が特徴です。
Alloy 6 の新機能 Mutable Field と線形時相論理
仕様記述言語 Alloy に関する新機能の紹介記事です。
v6 より前の Alloy には時間発展を記述する機能がありません。そのためユーザが「時間に従って変化する仕様」を記述する際には、明示的に時間をシグネチャとして導入する必要がありました。実際のシステムの仕様を記述する上で時間発展は頻出であり、慣れれば難しくはないのですが、細かいはまりどころがあったりして不便です。またビジュアライザがそれ用に作られているわけではないので、結果が見づらいという問題もあります。
2021 年 11 月にリリースされた Alloy 6 は、Mutable Field と呼ばれる記法を導入することでこの問題を解決しました。また、ビジュアライザにも状態遷移の前後が並べて表示できるなどの改善が加えられました。さらに、検査したい述語として線形時相論理式が使用できるようになっています。
まとめ
以上、本記事では 2021 年の登壇 9 件と記事 1 件について、簡単なコメントと共に振り返りました。
記事 1 件はやや寂しいですね。実は Alloy 以外にも Zenn に載せる用に検証を進めていた題材がいくつかあったのですが、結局どれも問題があって記事化には至りませんでした。
- 文章を書くタイプのアウトプットにもう少しウェイトを振る
- どこかのイベントで発表するだけでなく、自分自身が保有する情報発信チャンネルを確立する
あたりが来年の活動方針かなと考えています。
それでは、2022 年も張り切っていきましょう。よろしくお願いいたします。
