Name
Abstract | ||
|---|---|---|
Cloud computing provides on-demand access to IT resources via the Internet. Permissions for these resources are defined by expressive access control policies. This paper presents a formalization of the Amazon Web Services (AWS) policy language and a corresponding analysis tool, called ZELKOVA, for verifying policy properties. ZELKOVA encodes the semantics of policies into SMT, compares behaviors, and verifies properties. It provides users a sound mechanism to detect misconfigurations of their policies. ZELKOVA solves a PSPACE-complete problem and is invoked many millions of times daily. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.23919/FMCAD.2018.8602994 | 2018 Formal Methods in Computer Aided Design (FMCAD) |
Keywords | Field | DocType |
AWS access policies,SMT,cloud computing,on-demand access,Amazon Web Services policy language,access control policies,semantic-based automated reasoning,Internet,IT resources,ZELKOVA,policy properties verification | Automated reasoning,World Wide Web,Computer science,Theoretical computer science,Access control,Amazon web services,Semantics,The Internet,Encoding (memory),Cloud computing | Conference |
ISBN | Citations | PageRank |
978-1-5386-7567-0 | 2 | 0.37 |
References | Authors | |
9 | 9 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| John Backes | 1 | 2 | 0.37 |
| Pauline Bolignano | 2 | 2 | 0.37 |
| Byron Cook | 3 | 60 | 5.08 |
| Catherine Dodge | 4 | 2 | 0.37 |
| Andrew Gacek | 5 | 252 | 16.87 |
| Kasper Luckow | 6 | 2 | 0.37 |
| Neha Rungta | 7 | 563 | 27.72 |
| Oksana Tkachuk | 8 | 2 | 0.37 |
| Carsten Varming | 9 | 2 | 0.37 |