Correctness of source code extension for fault detection in openflow based networks

Software Defined Networks using OpenFlow have to provide a re- liable way to detect network faults and attacks. This technical report shows a formal analysis of correctness for an automated code extension technique used to extend OpenFlow networks with a logging mecha- nism that is used for the detection of faults and attacks. As presented in a companion paper, we applied the code extension techniques for a framework that can extend controller programs transparently, making possible on-line fault management, debugging as well as off-line and forensic analysis