自动化推理助力IAM策略检查

自定义策略检查助力自动化推理民主化新的IAM Access Analyzer功能使用自动化推理确保用IAM策略语言编写的访问策略不会授予意外访问权限。通过Amit Goel,Jeremiah Dunham2023年12月8日阅读时间7分钟为了控制对某机构云中资源的访问客户可以编写身份与访问管理IAM策略。IAM策略语言富有表现力允许创建细粒度策略控制谁可以对哪些资源执行哪些操作。这种控制可用于强制执行最小权限原则仅授予执行任务所需的权限。但如何验证IAM策略是否符合安全要求在2023年re:Invent大会上宣布推出IAM Access Analyzer自定义策略检查帮助用户根据安全标准对策略进行基准测试。自定义策略检查将策略语句转换为数学公式的任务抽象化使客户无需具备形式逻辑专业知识即可享受自动化推理的好处。自定义策略检查在开发流程中的作用IAM Access Analyzer APICheckNoNewAccess确保在更新策略时不会无意中添加权限。通过CheckAccessNotGrantedAPI可以指定开发人员不应在其IAM策略中授予的关键权限。自定义策略构建在一个名为Zelkova的内部服务上该服务使用自动化推理来分析IAM策略。此前使用Zelkova构建了预防性和探测性托管控制例如某服务S3 Block Public Access以及IAM Access Analyzer的公共和跨账户发现。现在随着自定义策略检查的发布可以设置安全标准并阻止不符合该标准的策略被部署。Zelkova的工作原理Zelkova通过将策略转换为精确的数学表达式来建模IAM策略语言的语义。然后使用称为可满足性模理论SMT求解器的自动化引擎来检查策略的属性。可满足性SAT求解器检查是否可以给布尔变量分配真值或假值以满足一组约束SMT是SAT的推广包括字符串、整数、实数或函数。使用SMT分析策略的好处在于它的全面性。与针对给定请求或一小部分请求模拟或评估策略的工具不同Zelkova可以针对所有可能的请求检查策略的属性。考虑以下某服务S3存储桶策略{Version:2012-10-17,Statement:[{Effect:Allow,Principal:*,Action:[s3:PutObject],Resource:arn:aws:s3:::DOC-EXAMPLE-BUCKET}]}Zelkova将此策略转换为以下公式(Action s3:PutObject) ∧ (Resource arn:aws:s3:::DOC-EXAMPLE-BUCKET)在此公式中∧是数学符号表示“与”。Action和Resource是代表任何可能请求中的值的变量。仅当请求被策略允许时该公式才为真。这种精确的数学表示非常有用因为它允许全面回答有关策略的问题。例如可以询问策略是否允许公共访问得到的答案是肯定的。对于上述简单策略可以通过手动审查判断是否允许公共访问策略语句中的Principal: *意味着任何人公众都被允许访问。但手动审查容易出错且不可扩展。或者可以编写简单的语法检查来查找Principal: *等模式。然而这些语法检查可能会遗漏策略的细微差别以及策略不同部分之间的相互作用。考虑对上述策略进行如下修改添加一个带有NotPrincipal: 123456789012的Deny语句该策略仍然具有Principal: *模式但不再允许公共访问{Version:2012-10-17,Statement:[{Effect:Allow,Principal:*,Action:[s3:PutObject],Resource:arn:aws:s3:::DOC-EXAMPLE-BUCKET},{Effect:Deny,NotPrincipal:123456789012,Action:*,Resource:*}]}利用Zelkova中策略语义的数学表示可以精确地回答有关访问权限的问题。使用Zelkova回答问题以一个相对简单的问题为例。通过IAM策略可以授予对要共享的资源的跨账户访问权限。对于敏感资源希望检查是否不可能进行跨账户访问。假设要检查上述策略是否允许账户123456789012以外的任何人访问S3存储桶。正如将策略转换为数学公式一样可以将要询问的问题或要检查的属性转换为数学公式。要检查所有允许的访问是否都来自自己的账户可以将属性转换为以下公式(Principal 123456789012)为了证明该属性对策略成立现在可以尝试证明只有(Principal 123456789012)的请求才被策略允许。数学中常用的一种技巧是反转问题。不是试图证明属性成立而是通过找到不满足该属性的请求来证明它不成立——换句话说满足(Principal ≠ 123456789012)的请求。为了找到这样的反例寻找对变量Principal、Action和Resource的赋值使得以下公式成立(Action s3:PutObject) ∧ (Resource arn:aws:s3:::DOC-EXAMPLE-BUCKET) ∧ (Principal ≠ 123456789012)Zelkova将策略和属性转换为上述数学公式并使用SMT求解器高效搜索反例。对于上述公式SMT求解器可以生成一个反例表明此类访问确实被策略允许例如Principal 111122223333。对于之前修改的带有Deny语句的策略SMT求解器也可以证明结果公式无解并且策略不允许来自账户123456789012外部的任何访问(Action s3:PutObject) ∧ (Resource arn:aws:s3:::DOC-EXAMPLE-BUCKET) ∧ (Principal 123456789012) ∧ (Principal ≠ 123456789012)策略中带有NotPrincipal: 123456789012的Deny语句被转换为约束(Principal 123456789012)。通过检查上述公式可以看到它无法被满足来自策略和属性的Principal约束是矛盾的。SMT求解器可以通过彻底排除解来证明这一点以及更复杂的公式。自定义策略检查为了让Zelkova的使用民主化需要在更易访问的接口背后抽象数学公式的构建。为此推出了IAM Access Analyzer自定义策略检查包含两个预定义检查CheckNoNewAccess和CheckAccessNotGranted。通过CheckNoNewAccess可以确认在更新策略时不会意外添加权限。开发人员通常从更宽松的策略开始并随着时间的推移将其完善到最小权限。现在通过CheckNoNewAccess可以比较策略的两个版本以确认新版本不会比旧版本更宽松。假设开发人员更新了本文中的第一个示例策略以禁止跨账户访问但同时添加了一个新操作{Version:2012-10-17,Statement:[{Effect:Allow,Principal:123456789012,Action:[s3:PutObject,s3:DeleteBucket],Resource:arn:aws:s3:::DOC-EXAMPLE-BUCKET}]}CheckNoNewAccess将两个版本的策略转换为公式Pold和Pnew。然后搜索公式(Pnew ∧ ¬Pold)的解这些解代表新策略允许但旧策略不允许的请求“¬” 是数学符号表示“非”。由于新策略允许主体123456789012执行旧策略不允许的操作检查失败安全工程师可以审查此策略更改是否可接受。通过CheckAccessNotGranted安全工程师可以通过指定要针对策略更新检查的关键权限来更具规范性。假设要确保开发人员不授予删除重要存储桶的权限。在前面的示例中CheckNoNewAccess仅因为权限是通过更新添加的才检测到这一点。通过CheckAccessNotGranted安全工程师可以指定s3:DeleteBucket作为关键权限。然后将关键权限转换为公式(Action s3:DeleteBucket)并搜索策略允许的具有该操作的请求。由于前面的策略允许此操作检查失败从而阻止该权限被部署。通过能够将关键权限指定为CheckAccessNotGrantedAPI的参数现在可以根据自己的标准检查策略——而不仅仅是针对现成的、广泛适用的检查。调试失败通过民主化策略检查无需昂贵且耗时的手动审查自定义策略检查帮助开发人员更快地行动。当策略通过检查时开发人员可以放心地进行更新。如果策略未通过检查IAM Access Analyzer会提供附加信息以便开发人员进行调试和修复。假设开发人员编写了以下基于身份的策略{Version:2012-10-17,Statement:[{Effect:Allow,Action:[ec2:DescribeInstance*,ec2:StartInstances,ec2:StopInstances],Resource:arn:aws:ec2:*:*:instance/*},{Effect:Allow,Action:[s3:GetObject*,s3:PutObject,s3:DeleteBucket],Resource:arn:aws:s3:::DOC-EXAMPLE-BUCKET/*}]}再假设安全工程师指定了关键权限包括s3:DeleteBucket。如上所述CheckAccessNotGranted在此策略上失败。对于任何给定的策略有时很难理解检查失败的原因。为了让开发人员更清楚IAM Access Analyzer使用Zelkova解决额外的问题将故障精确定位到策略中的特定语句。对于上述策略检查失败并显示描述“新访问位于索引为1的语句中”。此描述表明第二个语句包含关键权限。自动化推理民主化的关键是使其使用简单且易于指定属性。通过额外的自定义检查将继续支持客户在最小权限之路上前进。FINISHED更多精彩内容 请关注我的个人公众号 公众号办公AI智能小助手或者 我的个人博客 https://blog.qife122.com/对网络安全、黑客技术感兴趣的朋友可以关注我的安全公众号网络安全技术点滴分享