A formal model of the capabilities for channel protection security controls

In today's rapidly evolving cybersecurity landscape, professionals are tasked with managing numerous tools to safeguard systems against a growing array of threats. With diverse implementations of open-source and vendor-specific security controls, each utilizing its own configuration languages and ecosystems, selecting and disposing of the right solutions becomes a complex and time-consuming challenge for network administrators. This results, more often than desired, in human-based faults when security policies are enforced. This thesis presents a formal model of security controls that abstracts security capabilities from a theoretical standpoint. By leveraging software engineering design patterns and best practices, this model enables the specification of security properties for information systems without requiring prior knowledge of the underlying enforcement technologies. A key feature of this approach has been the involvement of a software translator that seamlessly converts these high-level security requirements into low-level configurations specific to different technologies. The research further explores the usage of this model to describe channel protection security policies from a high-level perspective, offering a new viewpoint on how abstract descriptions can drive practical security configurations. A significant part of this investigation is grounded in strongSwan, an IPsec solution widely used to secure remote network communication, which has served as a practical validation of the model. This thesis demonstrates the model's capacity to produce reliable and robust security configurations by testing the framework in real-world cybersecurity scenarios. Moreover, its flexible architecture allows for future extensions, enabling support for a wide range of security software beyond the initial scope and expanding the possibilities for more adaptable cybersecurity solutions.