自动化推理技术助力IAM策略检查优化方法

自动化推理：让IAM策略检查更精准

要做好云环境中的资源访问控制，第一步往往是编写身份与访问管理（IAM）策略。IAM策略语言的功能非常强大，可以创建细粒度策略，精确控制谁可以对哪些资源执行哪些操作，从而将最小权限原则落到实处——也就是只授予任务所需的权限。不过，问题来了：怎么确保这些策略真的满足了安全要求呢？在某机构2023年的re:Invent大会上，他们推出了IAM访问分析器的自定义策略检查功能，专门帮助用户根据自身的安全标准来验证策略。这个功能的核心是，把策略语句转换成数学公式的复杂任务变得简单了，用户不需要具备形式逻辑的专业知识，也能享受自动化推理带来的好处。

在开发流程中，IAM访问分析器的API CheckNoNewAccess是一个关键工具，它能确保在更新策略时不会无意中增加权限。而CheckAccessNotGranted API则允许你明确指定哪些关键权限是开发者不应在策略中授予的。这样一来，安全团队就能把规则前置，防患于未然。

Zelkova：自动化推理的幕后引擎

自定义策略检查是构建在一个叫Zelkova的内部服务上的，它用自动化推理来分析IAM策略。其实，之前不少预防性和检测性的托管控制，比如S3阻止公共访问、IAM访问分析器的公共和跨账户发现，都离不开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"的拒绝语句：

{
    "Version": "2012-10-17",
    "Statement": [{
        "Effect": "Allow",
        "Principal": "*",
        "Action": ["s3:PutObject"],
        "Resource": "arn:aws:s3:::DOC-EXAMPLE-BUCKET"
    },{
        "Effect": "Deny",
        "NotPrincipal": "123456789012",
        "Action": "*",
        "Resource": "*"
    }]
}

虽然这个策略仍然有"Principal": "*"的模式，但实际上不再允许公共访问了。这类复杂情况，正是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访问分析器的自定义策略检查，包含两个预定义的检查：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”)，并搜索策略允许的具有该操作的请求。由于前面的策略允许这个操作，检查会失败，从而阻止该权限被部署。这样一来，你就能根据自己的标准来检查策略了——而不仅仅是依赖那些通用的、广泛适用的检查。

调试失败：找到问题的根源

通过把策略检查民主化——也就是无需昂贵且耗时的人工审查——自定义策略检查能帮助开发者更快地迭代。当策略通过检查时，开发者可以自信地进行更新。如果策略没通过检查，IAM访问分析器会提供额外信息，方便开发者调试和修复。

假设开发者编写了下面这个基于身份的策略：

{
    "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访问分析器会用Zelkova额外解决一些相关问题，把失败定位到策略中的特定语句。对于前面的策略，检查失败的描述会是“新访问出现在索引为1的语句中”，这表明第二个语句包含关键权限。

自动化推理的民主化，关键在于让它的使用变得简单，让属性的指定变得直观。随着更多自定义检查的推出，这项能力会持续帮助用户走上最小权限的旅程。