根据 https://www.usenix.org/system/files/conference/nsdi15/nsdi15-paper-fogel.pdf
记录batfish项目背景以及对实习内容进行记录
Batfish 运作流程
将网络配置和环境转换为Datalog的变体，并且还使用此语言来表示正在配置的各种协议的行为。
执行所得的Datalog程序会产生表示数据平面的逻辑关系以及计算中各种关键概念的关系，例如，由特定协议确定的到达目的地的最佳路线。我们使用自动约束求解器来检查结果数据平面的属性，并生成违反这些属性的具体数据包。最后，这些数据包会反馈到我们的声明性模型中，从而引发更多的关系事实（例如，采用的路径，沿途遇到的ACL规则）。
我们的多路径一致性属性要求在存在多路径路由的情况下，流的数据包要么沿着它们经过的所有路径被丢弃，要么沿着所有路径到达目的地。
Batfish 产生的原因
网络通过一系列路由器和交换机转发数据包。每个设备的数据平面状态确定如何处理具有给定报头的数据包（例如，丢弃，转发到特定邻居或跨多个邻居进行负载平衡）。此状态由控制平面生成。在当今的网络中，控制平面是通过设备配置指定的，设备配置使用特定于供应商的语言，并且包括诸如以下方面：指定数据包过滤策略的ACL，直接连接的IP地址前缀的静态路由以及一个或多个路由的协议（目标网段、掩码、下一跳、度量值、Tag、Community等）。所有设备的配置，结合当前拓扑和相邻设备之间交换的动态信息，确定当前数据平面。
由某些管理实体管理的网络称为自治系统（AS）。在AS内，使用内部网关协议（如OSPF [23]）来交换有关网络拓扑和连接目标的信息，OSPF是一种计算成本最低的路径的协议。 BGP [29]是一种适应策略约束的协议，已在多个AS之间使用。路由器宣布它们愿意将来自相邻AS的流量传送到的目标IP地址前缀。本地策略确定接收到的公告是否可接受（例如，是否可以信任播音员具有到达目标前缀的路径），以及应该选择多个用于同一前缀的公告中的哪一个（例如，基于商业关系）。
实例：
考虑图2顶部所示的网络N，其中有两个相邻的AS。 P是大型提供者AS，C是拥有两个目标前缀的客户AS。路由器n2直接连接到前缀为10.0.0.0/24的内部专用网络。运营商希望该网络可用于C，但不可用于P以及不为C服务的N的其他部分。
图2的底部显示了实现此规范的配置片段，大致基于Cisco的IOS语言。 n1的配置的前两行指定它在将其连接到n2和n3的接口上运行OSPF，每条路由的成本度量为1。接下来的两行指定它运行带有c2的BGP，并且仅接受与前缀匹配的公告。前缀列表PL_C。路由器n2的配置类似，除了它还会通过OSPF重新分配（即通告）连接的网络。路由器n3配置为接受来自p1的所有前缀通告，并将所有静态配置的网络重新分发到OSPF。为了将前缀10.0.0.0/24与C路径之外的节点隔离，操作员将安装静态丢弃路由，并在n3（第6行）处进行日志记录。此路由已重新分配（第4行），因此n4不必直接知道此路由。此设置可防止P和n4（及其后面的主机）访问10.0.0.0/24，并使操作员能够发现任何尝试。
Batfish的四个阶段
-
建模控制面
Batfish的第一阶段将配置文件和网络拓扑作为输入，并输出一个控制平面模型，该模型捕获网络执行的分布式计算。首先将输入信息解析为中间数据结构，然后将其转换为一组逻辑事实，每个逻辑事实都与特定关系相关联。
-
构建数据面
网络的数据平面是每个节点的转发信息库（FIB）。 FIB确定数据包到达特定接口时要采取的适当措施。出于本文的目的，该动作是将数据包转发到一个或多个接口之外，接受该数据包或丢弃该数据包。 Batfish的第二阶段会为每个用户指定的环境生成一个数据平面。
FIB的规则如下。当数据包到达接口时，规则首先检查接口是否具有传入的ACL。如果是这样，并且如果该ACL不允许数据包的标头，则该数据包将被丢弃。 否则，如果将标头的目标IP地址分配给该节点的任何接口，则将接受该数据包。否则，规则将检查RIB中是否存在与报头的目的IP地址的前缀最长匹配的网络的条目。对于每条这样的路由，与该路由的下一跳相对应的接口的确定如下：如果该路由直接连接在接口上，则选择该接口。否则，规则将递归地使用与原始下一跳地址最长前缀匹配的路由下一跳，直到找到直接连接的路由为止。最后，如果接口的传出ACL允许，则将数据包转发到该接口，否则将其丢弃。
