Skip to content
/ neo Public
forked from netarch/neo

A network testing tool combining formal model checking and container-based emulation that covers in-network non-determinism

License

Notifications You must be signed in to change notification settings

al0wner/neo

 
 

Repository files navigation

Neo

GitHub workflow Codecov GitHub repo size

Neo is a network testing tool based on the Plankton verification framework. It combines explicit-state model checking and emulation techniques to achieve high-coverage testing for softwarized networks with middlebox components.

Table of Contents

Environment setup

The following dependencies are needed for Neo.

  • Clang
  • LLVM
  • libnl
  • libelf
  • zlib
  • spin
  • Docker

depends/setup.sh can be used to automatically set up the environment, but it only supports Arch Linux and Ubuntu at the moment. Pull requests are appreciated.

Since Neo requires Linux version to be at least 5.4 for per-packet drop monitoring, and Ubuntu 18 ships Linux 4.15 by default, it is recommended to use at least Ubuntu 20.04. Otherwise newer kernel versions will need to be manually installed.

Build and install Neo

cd neo
./scripts/configure.sh
./scripts/build.sh

The executable will be at build/neo. Optionally you can install Neo to system paths if desired.

sudo DESTDIR=/ ./scripts/install.sh --prefix /usr

Usage

Neo options:
  -h [ --help ]                Show help message
  -a [ --all ]                 Verify all ECs after violation
  -f [ --force ]               Remove output dir if exists
  -j [ --jobs ] arg (=1)       Max number of parallel tasks [default: 1]
  -e [ --emulations ] arg (=0) Max number of emulations
  -d [ --drop ] arg (=timeout) Drop detection method: ['timeout', 'dropmon',
                               'ebpf']
  -i [ --input ] arg           Input configuration file
  -o [ --output ] arg          Output directory

Examples:

sudo neo -afj8 -i examples/00-reverse-path-filtering/network.toml -o output

Note
Note that root privilege is needed because the process needs to create virtual interfaces, inject packets, manipulate namespaces, and modify routing table entries within respective namespaces.

About

A network testing tool combining formal model checking and container-based emulation that covers in-network non-determinism

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • C++ 84.1%
  • C 5.1%
  • Shell 4.4%
  • CMake 2.8%
  • Python 2.3%
  • Promela 0.6%
  • Other 0.7%