Reachability Analysis for AWS-Based Networks

Introduction

• Tiros
  • 使用现成的自动定理证明工具对使用AWS API构建的虚拟网络进行正式分析
  • Tiros将AWS网络概念的语义编码为逻辑，然后使用各种推理引擎来验证与安全相关的属性
  • 可以使用的工具：Souffle ́, MonoSAT, and Vampire
  • 静态执行分析
  • SMT encoding ： similar in design to Anteater and ConfigChecke