AWSでの形式手法の利用
MaruyamaFujio
2020/05/05 マルレク「AWSでの形式手法の利用」概要
今回のマルレクのテーマは、「AWSでの形式手法の利用」です。
この間、 形式手法を開発者に広めたいと思って、いろいろ試行錯誤をしてきたのですが、開発者にとって形式手法が身近なものに感じられていないことが大きなネックだと感じていました。今回のマルレクは、多くの開発者にとってはとても身近なAWSでの形式手法の「応用事例紹介」です。
セミナーの第一部では、2011年から始まっていたというAWSの形式手法導入の取り組みを紹介します。S3, ESB, EC2,….といったAWSの代表的なサービスの多くの設計に形式手法が用いられています。
また第一部の後半では、AWSでの現在の形式手法導入の取り組みが、それによってクラウドの安全性を担保するという、クラウド・セキュリティの中心環として位置付けられていることを紹介したいと思います。
AWSでの取り組みを知ることで、「どこでも形式手法なんか使ってないのでは？」という形式手法に対する開発者の心理的なバリアが、すこしでも低くなればいいと思っています。また、形式手法が、「正しいプログラムを作る」という開発の方法論だけではなく、「セキュアなシステムを作る」というシステム・セキュリティの課題と結びついていることを伝えたいと思います。
セミナーの第二部では、AWSの形式手法の受容で大きな役割を果たした、レズリー・ランポート（2013年チューリング賞受賞）の「形式仕様言語」TLA+ の概要を紹介したいと思います。
「はじめに」から
多くのIT技術者にとって、「形式手法」は、身近なものとは感じられていないだろう。それにもかかわらず、それは我々の近くに、すでに「事例」として存在している。
小論は、現代のIT技術者には極めて身近なクラウドの中で、意外なことに 「形式手法」の利用が急速に進んでいることを、IT技術者に知ってもらうことを一つの目的としている。
クラウドが利用する技術についてのIT技術者の間の認識のギャップは、ある意味、自然のことのようにも見える。我々は、基本的には、クラウドのサービスの「利用者」としてクラウドに接する。サービスを利用するのに、クラウド・システムの全体を理解する必要はない。クラウドは、もともとそういうものとして作られている。それはクラウドのメリットでさえある。
クラウドは、現代の最も大規模で最も複雑な情報システムである。しかも、それは日々、拡大している。その技術の詳細を把握するのは、誰にとっても難しいことだ。
小論には、もう一つの目的がある。それは、クラウドで「形式手法」が受容され始めているという「事実」を知ってもらうだけでなく、その「理由」をIT技術者に考えてもらうきっかけを提供することである。
小論のターゲットであるAWSにおいてさえ、「形式手法」の受容は、この10年間の間に起きたものである。それは、新しい流れ・新しい変化なのである。ただ、それは急速に拡大し、しかも、経営層のサポートを得て、成功しているように見える。
重要なことは、その「理由」が、我々が普段扱うシステムとクラウドとの見かけ上の違いを超えて、我々にも理解できるものだということである。
我々はみな、「バグのないセキュアなシステムの開発」を望んでいる。それは、また、AWSが「形式手法」をオプションの一つとして選択した最大の理由でもある。AWSが「形式手法」を選択した「理由」は、我々にとっても、とても身近な問題に関係しているのだ。
最後に述べておきたいことは、今回のセミナーで紹介するAWSが利用している「形式手法」は、TLA+にしてもZelkova/SMTにしても、この間、丸山が興味を持って紹介してきた CoqやDeep Specificationのアプローチとは、かなり異なったものであるということである。
それでも構わないと丸山は考えている。具体的な手法は異なっているのだが、大規模で複雑なシステムの開発・ 検証・運用に、ソフトウェアとコンピュータ・システムの形式的特徴（それは、数学的・論理的特徴と言っていい）に注目し、それを活用するという点では、同じアプローチだと思う。
アプローチは多様だが、こうしたアプローチをとることによって、大規模で複雑なシステムの開発・ 検証・運用に、本格的に機械＝コンピュータを投入できるようになる。ソフトウェアもシステムも、もちろんコンピュータも、その振る舞いは、「抽象化」すれば、数学によって形式的に記述されうるからだ。
いつか時代の駒が大きく進んだ時、主要には、多くの人間の直感と経験の集合知で開発を進めるという現在の開発スタイルは、大きく変わるだろう。現在、クラウドで起きていることは、その先駆けなのだと僕は考えている。
講演ビデオ
- Part I 「大規模なシステム障害はなぜ起きるのか？」
- Part II 「Amazon Web Servicesでの形式手法の導入と拡大」
- Part III 「Amazon Web Servicesのセキュリティについての形式的推論」
Part I 「大規模なシステム障害はなぜ起きるのか？」
Part II 「Amazon Web Servicesでの形式手法の導入と拡大」
Part III 「Amazon Web Servicesのセキュリティについての形式的推論」
講演資料 「Amazon Web Servicesでの形式手法の利用」
- Part I 「大規模なシステム障害はなぜ起きるのか？」
- Part II 「Amazon Web Servicesでの形式手法の導入と拡大」
- Part III 「Amazon Web Servicesのセキュリティについての形式的推論」
- Appendix TLA+
- Appendix Zelkova / SMT
講演資料 Part I 「大規模なシステム障害はなぜ起きるのか？」（ダウンロード）
講演資料 Part II 「Amazon Web Servicesでの形式手法の導入と拡大」（ダウンロード）
講演資料 Part III 「Amazon Web Servicesのセキュリティについての形式的推論」（ダウンロード）
講演資料 Appendix TLA+ （ダウンロード）
講演資料 Appendix Zelkova / SMT （ダウンロード）
参考資料
- 参考資料１: 「Amazon Web Services はどのように形式⼿法を利⽤したか」
- 参考資料 2：「Amazon Web Servicesのセキュティについての形式的推論」
- 参考資料 3：「ワンクリック形式手法」
