Abstract: This project proposes the investigation of techniques for the consistent composition of programs in programmable data planes. The use of techniques for formal verification in programmable networks is necessary to ensure the resilience of future computer networks, which are strongly based on software abstractions, regarding configuration errors. This project investigates the need to support the detection and handling of configuration errors arising from the insertion/removal of software on the network, and the interaction between these software components. In particular, this project has as main contributions: (a) Conducting a state-of-the-art survey in the area of composition and verification of programmable networks; (b) Investigation and definition of mechanisms for the efficient composition of programs in programmable data planes; (c) Investigation and definition of formal verification mechanisms to ensure consistency, both of individual switches and the network as a whole, in a P4 network; (d) Implementation of a system that allows the correct and consistent composition of modules in P4 programs, with a focus on the composition of security functions.
Ano Inicio: 2019
Ano Fim: 2023
Coordenador Local: Alberto Schaeffer-Filho
Agência de Fomento: FAPERGS
