Data privacy and security are top concerns for customers in the cloud. In this session, the AWS Automated Reasoning group shares the advanced technologies, rooted in mathematical proof, that help provide the highest levels of security assurance in today’s data-driven world. The Automated Reasoning group co-presents with Bridgewater, a customer that has leveraged these technologies to help confirm that security requirements are being met, an assurance not previously available from conventional tools.
- multiple forces are impacting cloud security
- next gen sec tech, provable security
- customer: security in the lcoud
- aws: security of the lcoud
- non compliance changes
Identifies unintended privilege escalation.
Zelkova drove the
public badge in the S3 console.
Feature: Block public access feature on S3 AWS config integrates with Zelkova eval changes to resources and comply with best practicies is server side enc enabled? is lambda resource restrictured
ability to formally prove a policy in aws enables automation that can provide an accurate holistic view of access in your env.
Data Privacy Zelkova Math | Logic
what does math and logic do for me?
- * - *:* - s3:* - ForAllValues:StringEquals
IAM is a sound and robust lanugage that makes static analysis difficult to catch all policy violations.
George Boole -> logic
not x or (y and z)
either x is fale or y and z are true (or both)
x = false, y = true, z = false is satisfiable not x and x is unsatisfiable
turn the problem and turn it into an SMT formula.
Zelkoa lambda engine.
principal, action resource
only primcipal 7777 has 23:get* access to docks/secret.pdf
bridgewater use case
- worlds largest hedge fund. conneticut
- 250 largest global clients
we want to protect our data
- check changes
- identify policy statements
- detect misconfiguration