Network Software Verification

The EPFL Network Architecture Lab is developing a tool to verify network dataplane software (such as middlebox functions: NAT, DPI, application acceleration, etc.)

If you had such a tool, which properties would you want to check with it?

Please use the whole range of priorities.

	High priority	Medium priority	Low priority
Crash freedom: prove that the software cannot crash under any circumstances (e.g., no null pointer dereference, no segfault, no division by 0, etc.)
Liveness: prove that every packet is eventually processed
Worst-case execution time: compute the upper bound on the number of instructions executed per packet
Worst case energy consumption: compute the upper bound on the max amount of energy consumed per packet
Correctness wrt a spec: prove that the code conforms to a spec. written in a formal language
Other: specify below

Please enter one response per row

Would you like to check any other property?

This is a required question

Which language would you be willing to write line-rate packet-processing software in?

Pure C99
C99 with some safety restrictions (e.g., no void* casts)
Pure C++
C++ with safety restrictions (e.g., no raw pointers, no implicit type conversion)
A type-safe memory-safe language (e.g., Go, Rust, D)
Managed code (e.g., Java, C#, Python)
Any of the above but with programmer-provided annotations (e.g., loop invariants, no-null qualifiers)
Other:

This is a required question

We would like to keep you updated on our progress. [optional]

Please provide your contact information, and we will notify you when the tool is ready to try out. We promise not to send more than a couple of messages a year.

Name:

This is a required question

E-mail:

This is a required question