Abstract

As more and more devices are connected to the network, the importance of Network functions, including switches, is increasing. Switches have the function of connecting networks and users' devices, and it is important to design safe software switches even for software switches which are easy to manage. However, since network disturbance often occurs in software switches due to bugs and errors, we have to verify the operation of them. An interactive theorem prover language, called Coq, can prove some defined functions and formulas on the program. In this paper, a software switch controlling the MAC addresses of each device is designed and implemented using Raw Socket, which is one of the packet handling mechanisms. Especially, we verified the operation of the MAC addresses management in Coq. As a result, formally validated fundamental implementation of the software switch was realized.

Top