# apkeep-impl

**Repository Path**: gdtongji/apkeep-impl

## Basic Information

- **Project Name**: apkeep-impl
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2020-10-13
- **Last Updated**: 2021-03-12

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# APKEEP-IMPL
Contains 3 layers referred from APKeep paper figure 3.
### Network layer: 
A data structure to store the FIB and topology of physical network. Basic view:
```
Network: {Device}

Device: {Port}, {Rule}

Port: {Peer} // the link is represented by this structure.

Rule: {Ip, prefix, out_port}
```
Different dataset need to write it's own parser to fit the network layer data structures. For internet2, Main.java is an example.

### Model layer:
The model layer maintains a PPM and a portToPred structures, since ports and preds are many-to-many relation.
When a rule is add to the network layer, the model update is triggered. See addRule function of `network.Network.java`.
```
Model: <PPM, PredToPorts>
PPM: Port -> {Pred}
PredToPorts: Pred -> {Port}
```
The model relies on singleton of BDD instance, which is implemented in BDDEngine.java. Be sure we use the same bdd manager to compute bdd.

### Verifier layer:
The verifier layer takes the delta forwarding graph from an update result of model layer, the function `checkInvariants` will check loop and blackholes. 

For reachability check, we first construct a set of properties (see `verifier.Property.java`), which takes a string as regular expr and construct automata (see `verifier.Automata.java`).

### Main.java
This file contains full process to verify internet2 by adding rules one by one, on each update it do checkInvariants, and comments are listed in the code.