A specification-by-example toolkit that generates formal network specifications using only input-output examples.

Many modern computer systems run on networks like cloud clusters or distributed systems. However, the network protocols that support the operation and security of these systems are notoriously difficult to debug. Formal network specifications provide a solution to a wide variety of network related tasks such as verification, analysis, and debugging. However, very few network engineers possess expertise in both network operation and writing formal specifications, creating a significant barrier to the adaptation of said specifications.

NetSpec is a toolkit that synthesizes highly expressive formal network specifications using input-output example pairs. It is best-first search algorithm is scalable to large networks and can automatically query the user for additional input-output examples in the case of ambiguous specifications. This implementation makes synthesis of formal specifications available to users without prior expertise.

NetSpec generates formal network specifications such as declarative logic programs that can be verified with tools like Vericon and Flowlog. It has been tested on a set of twenty-three different network protocol types and synthesizes solutions at similar or better performance levels as existing solutions while also requiring fewer computer resources. The algorithm optimizes a score based on the fraction and number of tuples in the synthesized network. In each round of optimization, NetSpec either introduces new rules, introduces new literals to existing rules, or aggregates operators. The search algorithm continues until no new programs provide an improvement over the current solution.

• Capable of synthesizing specifications for twenty-three benchmarks while existing solutions only work on less than half
• Runs faster or at similar speed for individual benchmarks on a single thread while existing solutions are multi-threaded
• Only requires input-output examples and no network specification expertise from the user
• Queries the user for additional inputs in the case of ambiguous specifications