27 November 2018

The Theory and Math Behind Data Privacy and Security Assurance (SEC301)

by mo

Neha Rungta

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


reasoning engine

  • audits
  • checks
  • identifies
  • detects
    • 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?

regex scanner:

- *
- *:*
- 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

SMT solvers

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


  • audit
  • check changes
  • identify policy statements
  • detect misconfiguration


devops security