Cyber attacks have been continuously becoming more frequent and powerful in modern computer networks, which interconnect a huge number of devices, including mobile ones. A main reason explaining the effectiveness of the attacks lies in the errors introduced by human administrators in the configuration of network security functions such as firewalls and VPN gateways. In literature, formal methods were used to check if a security configuration satisfies the policies describing the security properties to be enforced in the network. However, most existing proposals use a-posteriori formal verification, which still requires multiple tasks to be carried out by human administrators and may be time-consuming. In order to overcome these limitations, we have carried out research toward applying correctness-by-construction approaches for network security configuration. In this paper, we survey our most relevant contributions to this area, describing techniques based on constraint programming, like MaxSMT formulations, for a formal representation and resolution of the automatic security configuration problem, in such a way that the computed result is already proved to be correct and compliant with the requested policies.