技術ブログを開設する
ログイン
もっと気軽にアウトプットできる技術ブログプラットフォーム

Formal Reasoning About the Security of Amazon Web Services

形式手法に関するトップカンファレンスであるCAV 2018にて,AWSから講演(Invited Paperの発表)がありました.

そこでの発表からAWSは形式手法にかなり力を入れている印象を受け,割と重要な内容かなと思い,単なる箇条書きですが抜粋・まとめてみました. 月並みですがAWSも中の人達もまじすごい.

著者(発表者)/所属機関

Byron Cook (Amazon Web Services, University College London)

出典

FLoC 2018 (CAV 2018)

内容

  • AWSでは分散アルゴリズムの設計に形式手法(TLA+)を使用 (2014)
  • その後も継続的に形式手法を取り入れいているようで,本論文では特にセキュリティへの形式手法適用事例を紹介

Security of the Cloud: Where Formal Reasoning Fits In

  • AWS内部の開発,特にセキュリティレビューで定理証明やモデル検査(symbolic model checking)の利用が増えている
  • 2017年だけでも下記の事例にて定理証明やモデル検査を適用
  • OSSを活用しつつ使う上で生じた変更をフィードバックしており,例えば下記を利用+貢献
    • CBMC: C/C++向けのbounded model checker
    • SAW: CやJabaでの特定性質の検証
    • SMACK: Cプログラムに対するアサーション検証
  • s2nなど一部プロジェクトでは形式検証ツールをCI/CDに組み込み,継続的検証を実施
  • SMT-basedのツールで設定ミス防止を図っている
  • 形式手法の利用はコードを書く前から始まっている=プロトコルやアルゴリズムの設計段階から利用

Securing Customers in the Cloud

その他

  • 他社事例(文献)として以下に言及 (抜粋)
    • IBM, Google @ Dagstuhl Seminar 2013
    • Microsoft @ SOSP 2015 分散システムの検証
    • Facebook @ LICS 2018 codebaseの継続的検証

感想

  • TLA+の適用に始まり,AWSは形式手法の適用に対し継続的に力を入れいている印象
  • 特に今回は,形式検証のトップカンファレンスであるCAVにて2本の論文採択+Invited talkをしており抜きん出ている
  • こういった会議でプレゼンスを上げることで,AWS利用時の安心度・信頼感が高まる素晴らしい取り組み
  • これだけセキュリティチームで形式手法が利用される/開発者もTLA+などを使えるところを見るに,中の人がちゃんとComputer Scienceの素養を持っていて優秀な模様

関連記事

この記事へのコメント

まだコメントはありません
0
@jagijagijag1の技術ブログ
0
このエントリーをはてなブックマークに追加