Formal Analysis of Access Control Mechanism of 5G Core Network [CCS 2023]

发表于 | 分类于

SUMMARY

本文主要讨论了5G核心网络access control的形式化分析，关注NF向NRF请求token，并向其他NF请求服务的过程。 文章提出5GCVerif工具对5G核心网络的访问控制策略进行了形式化验证，定义了4种安全属性，发现了5种可能的安全隐患，提出一些简单的防御措施。

Motivation

5GC以更分散的NF提供服务，NF维护关于UE和5G系统的敏感信息，NF的resource allocation和authorization是非常重要的。 3GPP采用了OAuth 2.0框架作为5GC内NF访问控制的基础，但是目前没有工作对改框架做形式化认证，文章尝试回答如下问题： Is it possible to formally analyze the design of OAuth-based access control mechanism of a 5G Core?

文章认为虽然已有工作分析了4G/5G协议安全性，但是存在以下缺陷：

  • Some approaches have modeled only a single NF (i.e., MME/AMF) as the interface of 5GC by combining all NFs’ functionalities into one. This prevents reasoning about the interactions between NFs.
  • Other methods only model and analyze a subset of the protocol interactions, and quickly run into intractability and scalability issues when faced with more intricate protocol interactions.
    • Additionally, these analyses require manual interventions from human experts to guide the provers, making them less automated and unmanageable for large systems.
    • Moreover, all preceding approaches treat the 5G core network configurations as static, not accounting for changes during network operations. However, 5GC permits dynamic configuration updates.

Challenges

  • Incomplete and non-compliant open-source core: 不同实现可能有区别，所以文章基于标准进行分析；
  • Intractability: 5GC中包含大量的NF，service和operation，并且耦合了动态更新和复杂的授权逻辑，分析的难度大、状态空间爆炸；
  • Ambiguity and underspecification: 标准描述模糊，存在定义不清晰的地方。

文章将问题归为model-checking问题。 However, the highly configurable and customizable nature of the 5G Core turns the problem into an undecidable parameterized model-checking problem.

  • 5GC太复杂了，采用cutoff原则和small model theorem只分析5个NF规模下的表现；
  • 遍历所有可能的配置不可行，随机构造符合规范的配置；
  • 利用符号匹配的方法，迭代寻找配置不满足安全特性的地方。

Background

A Network Repository Function (NRF) allows other NFs to register and discover each other, and is the main focus of this study. The Access and Mobility Management Function (AMF) provides UE registration, connection, and reachability management. The Unified Data Repository (UDR) provides storage for subscriber and policy-related data. The Unified Data Management (UDM) accesses UDR and manages user identity and generates authentication credentials.

OAuth 2.0 is a well-established framework to govern authorization in a virtualized system. It is based on a central authorization server that issues access tokens to clients to grant access for invoking API calls. In a 5G Core, the NRF plays the role of the authorization server.

NF间交互的基本过程如下：

图片

A valid accessTokenRequest includes the consumer’s NFInstanceID, the target service and the corresponding scopes it wishes to access, the NFInstanceID or NFType of the NFP, etc.

Design

图片

5GCVerif包括以下几个步骤：

  • 模型构建：首先，构建一个抽象模型M*，该模型由一组通过认证通信通道进行通信的有限状态机（FSM）组成。M* 抽象了3GPP Release 17 技术规范中定义的5G Core访问控制机制。
  • NF更新：操作管理（OAM）决定NF是否能够成功更新其配置文件。在模型中，允许更新的属性由一组控制参数控制。
  • NF注册：NF在网络中注册并获取唯一标识符。
  • NF发现：在5G Core中，消费者NF通过发送NFDiscoveryRequest消息来发现生产者NF。
  • 授权逻辑：实施授权逻辑时，需要根据授权参数验证请求。授权参数可能包括允许的网络切片、允许的NF类型等。
  • 模型检查过程：在此步骤中，使用符号模型检查器（如nuXmv）来验证M是否满足访问控制属性Φ。如果找到了一个反例，则表明5GC的访问控制策略存在漏洞。
  • 安全属性：将访问控制策略分解为多个简单属性，每个属性仅关注一个授权参数。这有助于简化漏洞的识别和根源分析。

图片

每个步骤的关键设计点如下：

  • 模型构建：在构建抽象模型时，需要确保模型能够捕捉到5G Core访问控制机制的核心特征，同时还要考虑可扩展性和可定制性。
  • NF更新：在设计模型时，需要考虑如何有效地控制允许更新的属性，以便在模型中分析不同的配置文件更新场景。
  • NF注册：需要确保在模型中正确地实现NF注册的过程，以便在网络中正确地识别和管理各个NF。
  • NF发现：在实现NF发现过程时，需要考虑如何处理不同的NF之间的通信，以及如何在模型中实现这些通信。
  • 授权逻辑：实现授权逻辑时，需要考虑如何在SMV语言中实现复杂的条件语句，例如使用决策表或if-else结构。

Findings

文章发现了以下几类可能的漏洞，并进行了验证：

图片

  • Confused Producer Attack：一个恶意消费者可以伪装成另一个消费者，从而使生产者无法正确验证权限。
  • Token Reuse Attack：一个被攻击的消费者NF可以重用先前保存的未过期的访问令牌来访问原本不应该访问的受害者NF。
  • Default Overprivilege Attack：在OAM（操作维护）存在的情况下，它需要批准攻击者删除其sNssais。这可能导致攻击者获得更多权限。
  • Authorization Bypass Attack：NRF（网络功能实例注册）在处理NFDiscoveryRequest时，未对NFDiscoveryRequest和消费者NFProfile的权限参数进行交叉检查，可能导致未经授权的访问。
  • Parameter Misuse Attack：一旦被攻击的消费者NF在合法切片中获得对生产者NF的访问令牌，它也会隐含地被授予访问同一NF内其他切片中的相同操作。攻击者只需提供相应的查询参数，即可从他们不应访问的切片中检索、创建或更改信息。

Discussion

  • Confused Producer Attack：accessToken已经包含一个属性producerSnssaiList，该属性指定了消费者有权访问的sNssais列表。NFP可以使用此列表来验证消费者是否被允许访问其服务，以防止困惑的生产者攻击。然而，3GPP定义了producerSnssaiList是可选的，因此NFP不能依赖此属性来验证消费者的授权。我们建议在accessToken中强制加入producerSnssaiList。
  • Token Reuse Attack：目前，OAuth 2.0令牌没有描述撤销机制。一个合理的解决方案是启用NFP来检查NFC是否使用过时的accessToken。为此，NFP可以在从NFC接收 NFServiceRequest时通过新的API调用TokenVerificationRequest(accessToken) 查询NRF。RFC 7662中也讨论了类似的解决方案。然而，为每个NFServiceRequest引入NFP和NRF之间的额外网络交互可以显着提高NRF和NFP的性能，并击败缓存accessToken 的目的。另一种解决方案是向accessToken引入新的属性时间戳，它表示发行时间。此外，NFP 应该维护一个属性lastUpdateTime，以跟踪最近的关键NFProfile更新。如果accessToken中的时间戳比NFP的lastUpdateTime更早，NFP将拒绝 NFServiceRequest。
  • Default Overprivilege Attack：为了减轻这种攻击，OAM必须在授予配置文件更新之前验证对关键NFProfile属性的更新。此外，在每个accessTokenRequest中NRF应该根据NFC的NFProfile中的相关属性验证NFP的NFProfile的授权参数。避免所有关键属性的允许默认策略也很重要，包括sNsais。相反，应该强制执行deny-bydefault 策略。但是，如果各方没有都修复，实施此修复可能会导致互操作性问题。
  • Authorization Bypass Attack：在NRF验证NFDiscoveryRequest期间，强制在请求者ssaisnfDisc消息和sNs之间执行交叉检查。
  • Parameter Misuse Attack：一种方法是NRF在accessTokenRequest验证期间检查输入参数，并且只将验证值附加到accessToken。然而，这种方法需要对现有的accessToken设计进行重大修改，并可能导致系统开销增加。它还限制了accessToken缓存，并可能导致通信瓶颈。或者，如果NFP 进行验证，NFP将需要有关NFC（例如 NFProfile）的附加信息，并且可能需要对NRF进行额外的查询，从而导致大量延迟。

作者与GSMA分享了这些findings，并且获得CVD-2023-0069编号。

Link to paper: Formal Analysis of Access Control Mechanism of 5G Core Network