CONTRIBUTING.md

Contributing to Mimesis

In the current prototype of Mimesis, it employs S2E for full-system symbolic execution to analyze a given network function program binaries together with the Linux kernel running in a QEMU KVM. We implemented a custom S2E plugin to control the symbolic execution process, combined with a kernel module built with SystemTap to automatically instrument the Linux kernel for (1) injecting a symbolic packet/frame as input, (2) recording the egress packets/frames, and (3) terminating the symbolic execution.

Background

To understand the design of Mimesis, it is encouraged to read through the code directly. However, the following documentations provide some background knowledge of S2E, SystemTap, QEMU, and BDDs, which may be helpful.

• S2E
  • Getting started with S2E
  • Symbolic execution of Linux binaries
  • How to write an S2E plugin
  • Copying files between the host and the guest
  • Using SystemTap with S2E
  • Solving a CTF challenge with S2E
• SystemTap
  • SystemTap documentation
  • Understanding how SystemTap works (Red Hat)
  • SystemTap - filtering and analyzing system data (SUSE)
• QEMU
  • QEMU Documentation/Networking
• BDDs
  • Sylvan documentation
  • Graph-Based Algorithms for Boolean Function Manipulation (IEEE ToC '86)
  • Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams (SAT '16)

Where to start?

Please take a look at the code in an order similar to the following to understand how Mimesis works.

• depends/setup.sh
• scripts/build.sh
• scripts/s2e.sh
• src/sender.cpp
• src/symbolic_ingress.stp
• src/s2e/libs2eplugins/src/s2e/Plugins/Mimesis.cpp
• src/libps/manager.cpp
• src/libps/packetset.cpp
• src/libps/klee-interpreter.cpp
• src/libps/bitvector.cpp
• src/libps/bdd.cpp

Improvements

Note
Please see the project notes for all the updates and action items.

Functional to-do items.

• Parse the SMT constraints into BDD-based packet sets. (ongoing)
• Build the library for BDD-based packet sets. (ongoing)
• Create the NF model class/module. (ongoing)

Performance to-do items.

• Parallelize the analysis.
• Concolic execution.
• State merging.
• Fork profiling.
• (FAQ) Handling path explostion.
• (FAQ) Logging for constraint solving queries.
• Profiling CPU and memory usage.

Participation

To report bugs, fix issues, or provide code changes, please either file an issue or submit a pull request.