Slides are not available for this talk.

Abstract: Applications of formal methods (FM) usually focus on analyzing the possible executions of a system that start in a desirable state and evolve according to the system logic. As long as the system stays within a set of desirable states along all possible transitions, the analysis allows us to conclude that system invariants are maintained on every execution of the system. On the other hand, these techniques may find a possible bad execution that leads the system to an undesirable state (a system invariant is violated). In such a scenario we usually do the following: i) turn the system off, ii) apply changes to the system that preclude executions from entering similar undesirable states, iii) turn the system back on, and iv) restart the analysis. However, in reality, many systems need to stay operational while in an undesirable state and remain operational as we attempt to restore the system to a desirable state. The recovery problem is how to get the system back into a desirable state, i.e., restore the system invariants. This is a challenge as the core business logic of the system is rarely designed with recoverability in mind.In this talk, I will share the experience from a proactive effort that scientists and engineers at AWS Identity [1] undertook to apply formal methods techniques to analyze AWS Identity and Access Management (IAM [2]) service’s incident recovery tools. The analysis aimed at ensuring that recovery scenarios do not cause unintended or unexpected state changes in IAM. I will present some of the properties of the IAM service and what the IAM service does w.r.t potential issues that arise in recovery scenarios. I will show some key safety properties, our analysis approach, and some of the challenges we faced towards formally guaranteeing the safety of IAM’s recovery tools.

Aleks Chakarov is an Applied Scientist in the Automated Reasoning group in Identity at Amazon Web Services (AWS). For the past year and a half, Aleks has been applying automated reasoning techniques in the identity and access management domain. Before joining AWS, Aleks was a Senior Research Scientist at Phase Change Software LLC where he applied program analysis and logic-based AI to develop programmer productivity tools. Aleks holds a PhD in Computer Science from the University of Colorado Boulder.

References

1https://aws.amazon.com/identity/
2https://aws.amazon.com/iam/