Glucat

Blog

Tech

Life

AWS基于模型的网络验证

云中的安全性与本地数据中心安全性相似，但没有设施和硬件维护成本。在云中不必管理交换机，防火墙，物理服务器或存储设备。相反，租户需要使用基于软件的安全工具监控和保护进出云资源的信息流。AWS有一个ARG（Automated Reasoning Group）团队，他们借助自动推理技术，即运用数学逻辑来检测可能潜在暴露脆弱数据的各类配置错误，为AWS云本身和云中的安全性都提供了更高的保障。本文简单介绍ARG研发出的两个工具：Tiros和Zelkova。更多的详细资料可以在AWS官网 Provable Security 上查看。

下图是一个典型的三层网络APP架构，图中显示这两个工具验证的领域。攻击者可能会根据S3 Bucket Policy或者IAM Policy的漏洞去访问S3，或者尝试通过ssh暴力去访问登陆用户的EC2等等。

  • 用户可以使用Zelkova工具去验证下发的S3 Bucket policy。
  • 用户可以使用Tiros工具去验证该EC2是不是可以被外网访问ssh端口。

Tiros

Tiros 是 Amazon Inspector 服务中最近推出的验证网络可达的功能。它不需要在真实网络中发包，而是使用现成的自动化定理证明工具来识别（EC2）网络配置错误或安全漏洞。例如，用户想验证有没有外网的IP能够访问本地的数据库服务。验证的结果能够表明是否可从外网（通过 Internet 网关，包括 Application Load Balancer 或 Classic Load Balancer 后的实例）、VPC 对等连接或 VPN（通过虚拟网关）到达用户指定的服务端口。这些结果还强调了潜在恶意访问的网络配置（如管理不当的安全组、ACL、IGW 等）。

Tiros对AWS网络进行建模，可以分成两部分：

  • 形式化规格（Formal specification）：通过具有明确数学定义的文法和语义的语言TQL（Tiros Query Language），对AWS网络中的组件进行描述。例如路由表是如何转发流量的？防火墙安全组里的规则是按照什么顺序匹配的？负载均衡是如何将流量分发到多个服务器的？
  • 快照（Snapshot）：网络拓扑和网络中的一些细节信息。例如包含了实例，子网，VPC里的路由表。

Tiros提供了许多规则用法，例如list:instance-has-subnet(Inst, Sn)，有点类似于SQL语言 select (Inst, Sn) from aws where instance-has-subnet(Inst, Sn)。同时也允许用户可以自定义一些规则，例如：

def in-data-zone(Inst, Vpce) = 
instance-has-subnet(Inst, Sn) && subnet-has-rtb(Sn, Rtb) && atom/vpce-route(Rtb, Vpce, _pl, _rtstate)

当用户想找出在VPC：vpce-dz123 里有哪些实例能够被外网ssh访问，可以输入：

list:in-data-zone(Inst, vpce-dz123) && internet-can-ssh-to-instance(Inst).

结果返回有可能是空或者找到满足条件的实例 {"Inst": “i-xyzzy”}

Tiros使用了三个求解器：

  • Datalog solver Souffle
  • SMT solver MonoSAT
  • First-order theorem prover Vampire

参考论文：Reachability Analysis for AWS-based Networks

Zelkova

Zelkova 策略分析引擎可以自动检测各种类别的资源配置错误，例如 AWS Identity and Access Management (IAM) 策略，Amazon Simple Storage Service (S3) 策略。正确配置的策略是组织安全状况的关键组成部分之一。策略配置不当也是云客户最为关心的安全问题之一。Zelkova翻译策略成SMT约束公式，然后使用Z3，Z3AUTOMATA和CVC4求解器进行证明是否能够满足Ture，或者返回一个反例满足为False。

下图为例，使用Zelkova检查S3的每个bucket是否会被外网访问，确保没有授权的用户是不能够读或者写你创建的bucket。当bucket被标志位Public代表有些公共的请求能够访问你的bucket，标志位Not public说明所有公共的访问将被拒绝。

策略是用 JSON 来描述的，主要包含 Statement，也就是这个策略拥有的权限的陈述。可任意理解为谁在什么条件下能对哪些资源的哪些操作进行处理。以下是某个用户编写的S3 bucket policy，目的是禁止111122223333访问：

{
    "Effect": "Allow",
    "NotPrincipal": { "AWS": "111122223333" },
    "Action": "*",
    "Resource": "arn:aws:s3:::test-bucket"
}

但是这造成了被其他没有授权用户访问的风险，因为该bucket几乎被公开访问。当用户下发这个策略后，S3会对这个bucket打上public标签提醒用户，这是怎么做到的呢？Zelkova翻译该策略转换为数学公式，仅当其左侧和右侧均为真时才为真。Resource和Principal是变量，就像在代数类中使用x和y一样。

(Resource = “arn:aws:s3:::test-bucket”) ∧ (Principal ≠ 11112222333)

下一步是要确定此策略公式是否允许公共访问，Zelkova通过对比两个策略（zelkova_compare）决定哪个策略更宽松（permissive）。

zelkova_compare(aws_policy1, aws_policy2)
returns 
	‘equivalent’
	‘more-permissive’
	‘less-permissive’
	‘incomparable’
	‘unknown’

以下图为例，左边是candidate的策略，右边是benchmark策略。通过比较后得出左边的策略更为宽松。

Zelkova使用解决方案是如果P1和P2是策略公式，然后假设公式P1⇒P2为真。此箭头符号表示当P1为true时，P2也必须为true。因此，每当P1接受请求时，策略2也必须接受该请求。因此，策略2至少与策略1一样宽松（permissive）。假设公式P2⇒P1是不正确的。这意味着存在一个使P2为真而P1为假的请求。P2允许该请求，但P1拒绝该请求。结合所有这些结果，P1的允许严格程度低于P2。

Zelkova具有一项特殊的策略，该策略允许未经授权的匿名用户访问S3资源。Zelkova将用户下发的策略​​与此策略进行比较。如果用户的政策更为宽松（permissive），则表明政策允许公共访问。如果用户的策略严格限制访问，例如基于源VPC endpoint（aws：SourceVpce）或源IP地址（aws：SourceIp），那么用户的策略就不会比这个特殊策略更为宽松，因此Zelkova认为用户的策略不允许公共访问。

Tiros和Zelkova在workflow里的位置：

参考论文：Semantic-based Automated Reasoning for AWS Access Policies using SMT

comments powered by Disqus