Formally Verifying Security and Compliance Mandates using AWS Network Access Analyzer

pdf
Abstract: Amazon Web Services (AWS) Customers use the Virtual Private Cloud service to virtually provision networks to connect their cloud-based applications. As customer’s scale their networks in order to meet their business goals it becomes more and more challenging to determine if their applications continue to meet their security and compliance mandates. Late last year AWS launched Network Access Analyzer, an automated reasoning-based service to help customers better understand if their networks satisfy such mandates. In this talk, we will discuss how customers are using Network Access Analyzer to formally prove that their networks meet their network compliance requirements.

 

Dan DaCosta began his career working on advanced networking and software security projects for the defense industry. Inspired by his use of Haskell, he

became interested in advanced type systems. This lead him to study formal logics, interactive theorem provers, model checkers, SAT solving, and other

formal methods topics. He is now an Applied Scientist at AWS where he works on a team that develops tools to statically reason about reachability properties in AWS networks.

Tags:
License: CC-BY-NC-3.0
Submitted by Katie Dey on