Epinoia-有状态网络的意图验证模块，略读

Epinoia relies on a unified model for NFs by leveraging the causal precedence relationships
that exist between NF packet I/Os and states.

这句话的意思是：“Epinoia依靠一种统一的网络功能（NF）模型，通过利用存在于 NF 包输入/输出和状态之间的因果先行关系。”
unified model for NFs: 这里所说的“unified model”指的是把不同类型的网络功能（Network Functions，NFs）进行抽象和统一建模的模型。通过将不同 NFs 统一建模，可以更好地管理和操作它们。
causal precedence relationships: 因果先行关系，表示某个事件（或操作）在时间上先于另一个事件发生，且有可能导致后者发生。这里可能指的是 NF 数据包的输入/输出操作和状态之间的因果关系，即某个操作可能会导致状态的改变。

1.有状态网络

《Epinoia: Intent Checker for Stateful Networks》是2021年提出的“网络意图检查器”，用于有状态网络的网络意图检查。有状态网络是指包含有状态NFs (stateful Network Functions)的网络，较传统交换机、路由器而言，其数据包处理行为也需依赖之前的数据包，越来越流行。有状态网络的例子：防火墙，允许属于已建立的连接的数据包直接入站； 网络代理（proxy）服务，缓存热门的网页内容。

2.意图检查系统需要具备的特性

1. Vendor-agnostic model specifications: 这个要求指的是意图检查系统应该支持跨不同供应商的网络功能（NFs）和配置。具体做法为，使用OpenConfig YANG models表示NFs的配置。

• Completeness to support end-to-end intent checking: 这个要求强调系统需要完整性，能够支持从端到端的意图检查。它需要考虑到网络中的所有环节，包括由 NFs 执行的数据包头修改和路由动态性。这是因为网络中的流量可能会经过多个网络功能，每个功能都可能对数据包进行修改，因此检查必须确保意图在整个流程中得到满足。具体做法为，使用意图分解。
• Incremental checking: 这个要求提到系统应该支持增量检查，以高效地验证正确性，而不是在每次变更时都进行完整的检查。这是为了避免对每次变化都执行完整的检查，从而节省计算资源和时间。系统可以根据变更的程度，只验证与变化相关的部分，以减少不必要的工作量。具体做法为，使用一种新的因果图记忆技术表示有状态NF包的操作逻辑，对所有检查结果进行检查。

• 3.现有意图验证方法 recent work

  1. 定制方法： 定制方法，如HSA[10]和其实时版本NetPlumber[9]，会识别受网络变化影响的数据包集，并利用定制的基于路径的算法来计算它们的新的转发路径。这种方法不能模拟来自网络其他部分的额外数据包序列，因此无法用于有状态网络。换句话说，它只关注受变化影响的数据包的路径，忽略了其他可能影响这些数据包的因素。
• 求解器方法： 求解器方法，如Minesweeper[4]和VMN[17]，使用一阶逻辑编码了网络中所有可能的数据包行为；为了实现与现代求解器（如SAT和SMT）的可扩展性，它们依赖于优化方法来识别逻辑上独立的网络片段。这种方法更加全面，考虑了网络中所有可能的数据包行为，但为了应对大规模的网络，需要使用求解器进行逻辑分析，需要一些优化策略来降低计算复杂度。

• 总的来说，定制方法关注于受变化影响的数据包的路径计算，而求解器方法则考虑了整个网络中数据包的各种可能行为。每种方法都有自己的优势和限制，选择适合的方法取决于网络的规模、复杂度和需求。

  either only ensures correct NF traversal assuming all instances of each type of NFs are equally
  and correctly configured [10] [8] [4], or only checks NF configurations in a restricted scope that may lose end-to-end expressiveness and accuracy [17]

  最近关于网络控制平面配置(例如BGP配置)的综合[7]和验证[4]的工作表明，路由器之间的路由发布可以使用布尔变量有效地建模。

  Epinoia extends the intent specifications in PGA [19].

  Epinoia并不是为了检查无状态交换结构的正确性，因为已经有很多解决方案[9]-[11]，[28]。同时，通过去除交换结构，网络图的大小要小得多(将大小降低至少50%[23])