自定义策略检查推动自动化推理技术普及

新推出的IAM访问分析器功能利用自动化推理技术，确保使用IAM策略语言编写的访问策略不会授予意外访问权限。

为了控制对某中心云平台资源的访问，用户可以编写IAM策略。IAM策略语言具有丰富表达能力，允许创建细粒度策略来控制用户对资源执行的操作。这种控制可用于实施最小权限原则，仅授予执行任务所需的权限。

但是如何验证IAM策略是否符合安全要求？在某中心的2023 re:Invent大会上，推出了IAM访问分析器自定义策略检查功能，可帮助用户根据安全标准对策略进行基准测试。自定义策略检查抽象了将策略语句转换为数学公式的任务，用户无需具备形式逻辑专业知识即可享受自动化推理的好处。

开发流程中的IAM访问分析器自定义策略检查

IAM访问分析器API CheckNoNewAccess确保在更新策略时不会意外添加权限。通过CheckAccessNotGranted API，可以指定开发人员不应在其IAM策略中授予的关键权限。

自定义策略检查基于名为Zelkova的内部服务构建，该服务使用自动化推理来分析IAM策略。之前已使用Zelkova构建预防性和检测性托管控制，例如某对象存储服务的阻止公共访问和IAM访问分析器的公共及跨账户发现。现在，通过发布自定义策略检查，用户可以设置安全标准并阻止不符合此标准的策略部署。

Zelkova工作原理

Zelkova通过将策略转换为精确的数学表达式来建模IAM策略语言的语义，然后使用称为可满足性模理论求解器的自动化引擎来检查策略属性。可满足性求解器检查是否可以为布尔变量分配真值或假值以满足约束集；SMT是SAT的推广，包括字符串、整数、实数或函数。使用SMT分析策略的好处是全面性，与针对给定请求或少量请求集模拟或评估策略的工具不同，Zelkova可以检查策略对所有可能请求的属性。

考虑以下某对象存储服务存储桶策略：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

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

Zelkova将此策略转换为以下公式：

1
2

(Action = "s3:PutObject") 
∧ (Resource = "arn:aws:s3:::DOC-EXAMPLE-BUCKET")

在此公式中，"∧“是"和"的数学符号。Action和Resource是表示任何可能请求值的变量。仅当策略允许请求时，该公式才为真。这种策略的精确数学表示很有用，因为它允许我们全面回答有关策略的问题。

对于简单策略，可以执行手动审查来确定是否允许公共访问：策略语句中的"Principal”: “*“意味着允许任何人访问。但手动审查容易出错且不可扩展。

或者，可以为模式编写简单的语法检查。然而，这些语法检查可能会忽略策略的微妙之处以及策略不同部分之间的交互。考虑上述策略的以下修改，添加了带有"NotPrincipal”: “123456789012"的Deny语句；策略仍然具有"Principal”: “*“模式，但不再允许公共访问：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

{
   "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存储桶。正如将策略转换为数学公式一样，可以将要询问的问题转换为数学公式。要检查所有允许的访问是否来自账户，可以将属性转换为以下公式：

1

(Principal = 123456789012)

要证明该属性对策略成立，可以尝试证明只有具有(Principal = 123456789012)的请求才被策略允许。数学中常用的技巧是翻转问题，不是试图证明属性成立，而是通过查找不满足它的请求来证明它不成立。要找到这样的反例，需查找满足以下条件的变量赋值：

1
2
3

(Action = "s3:PutObject")
∧ (Resource = "arn:aws:s3:::DOC-EXAMPLE-BUCKET")
∧ (Principal ≠ 123456789012)

Zelkova将策略和属性转换为前述数学公式，并使用SMT求解器高效搜索反例。对于前述公式，SMT求解器可以生成反例，显示此类访问确实被策略允许。

对于之前带有Deny语句的修改策略，SMT求解器还可以证明结果公式无解，并且策略不允许来自账户外部的任何访问：

1
2
3

(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，现在可以比较策略的两个版本，以确认新版本不比旧版本更宽松。

假设开发人员更新本文的第一个示例策略以禁止跨账户访问，但同时添加了新操作：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14

{
   "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)的解，这些解表示被新策略允许但不被旧策略允许的请求。由于新策略允许账户中的主体执行旧策略不允许的操作，检查失败，安全工程师可以审查此策略更改是否可接受。

通过CheckAccessNotGranted，安全工程师可以通过指定要针对策略更新检查的关键权限来更具规范性。假设要确保开发人员未授予删除重要存储桶的权限。在前面的示例中，CheckNoNewAccess仅因为权限随更新添加而检测到这一点。使用CheckAccessNotGranted，安全工程师可以将s3:DeleteBucket指定为关键权限。然后将关键权限转换为公式，并搜索策略允许的具有该操作的请求。由于前述策略允许此操作，检查失败并阻止权限部署。

通过能够将关键权限指定为CheckAccessNotGranted API的参数，现在可以根据标准检查策略，而不仅仅是进行通用的广泛适用检查。

调试失败

通过普及策略检查，无需耗时费力的手动审查，自定义策略检查帮助开发人员更快地移动。当策略通过检查时，开发人员可以自信地进行更新。如果策略检查失败，IAM访问分析器提供附加信息，以便开发人员调试和修复它们。

假设开发人员编写以下基于身份的策略：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

{
   "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的语句中的新访问”。此描述表明第二个语句包含关键权限。

普及自动化推理的关键在于使其简单易用且易于指定属性。通过附加自定义检查，将继续支持客户在实现最小权限的旅程中前进。