As cloud environments continue to explode in complexity, formal methods have started to gain attention for their potential to secure clouds at scale. AWS undoubtedly pioneered this space by developing Tiros + Zelkova and pushing their capabilities across the shared-responsibility boundary in the form of point-solutions (ex. Access Analyzer). We’ll start by briefly discussing how your organization can find easy wins on existing infrastructure with these point-solutions. However, the killer use-case for formal-methods is applying them pre-deployment, ensuring the cloud is “correct-by-construction”. While Zelkova can be leveraged to do exactly this for IAM, it is not directly available for some customers. To address this, we implemented a simplified IAM policy parser which determines relative permissiveness using an SMT solver based on the original Zelkova paper.

We’ll take you through this process to explore what makes IAM policies difficult to evaluate, how Zelkova works, and discover Zelkova’s quirks (are there instances where Zelkova can’t compute permissiveness before timeout?). More importantly, we’ll go through policy reasoning examples to argue that Zelkova’s use of automated reasoning and formal guarantees are likely unnecessary for the problem space. To conclude the talk, we’ll discuss what makes a good specification for Zelkova to verify. After all, your verification is only as strong as your specification. In doing this, we’ll demonstrate why Zelkova’s relative permissiveness API makes writing broad specifications difficult.

Ultimately, the audience will be encouraged to adopt formal method tooling such as Zelkova for their cloud environment, while remaining prudent about the value formal methods provide for their organization.