Biblio

Network covert channels enable stealthy communications for malware and data exfiltration. For this reason, the development of effective countermeasures for covert channels is important for the protection of individuals and organizations. However, due to the number of available covert channel techniques, it can be considered impractical to develop countermeasures for all existing covert channels. In recent years, researchers started to develop countermeasures that (instead of only countering one particular hiding technique) can be applied to a whole family of similar hiding techniques. These families are referred to as hiding patterns. The main contribution of this paper is that we extend the idea of hiding patterns by introducing the concept of countermeasure variation. Countermeasure variation is the slight modification of a given countermeasure that was designed to detect covert channels of one specific hiding pattern so that the countermeasure can also detect covert channels that are representing other hiding patterns. We exemplify countermeasure variation using the compressibility score originally presented by Cabuk et al. The compressibility score is used to detect covert channels of the 'inter-packet times' pattern and we show that countermeasure variation allows the application of the compressibility score to detect covert channels of the 'size modulation' pattern, too.

Software-defined networks provide new facilities for deploying security mechanisms dynamically. In particular, it is possible to build and adjust security chains to protect the infrastructures, by combining different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. It is important to ensure that these security chains, in view of their complexity and dynamics, are consistent and do not include security violations. We propose in this paper an automated strategy for supporting the verification of security chains in software-defined networks. It relies on an architecture integrating formal verification methods for checking both the control and data planes of these chains, before their deployment. We describe algorithms for translating specifications of security chains into formal models that can then be verified by SMT1 solving or model checking. Our solution is prototyped as a package, named Synaptic, built as an extension of the Frenetic family of SDN programming languages. The performances of our approach are evaluated through extensive experimentations based on the CVC4, veriT, and nuXmv checkers.

Software-defined networks provide new facilities for deploying security mechanisms dynamically. In particular, it is possible to build and adjust security chains to protect the infrastructures, by combining different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. It is important to ensure that these security chains, in view of their complexity and dynamics, are consistent and do not include security violations. We propose in this paper an automated strategy for supporting the verification of security chains in software-defined networks. It relies on an architecture integrating formal verification methods for checking both the control and data planes of these chains, before their deployment. We describe algorithms for translating specifications of security chains into formal models that can then be verified by SMT1 solving or model checking. Our solution is prototyped as a package, named Synaptic, built as an extension of the Frenetic family of SDN programming languages. The performances of our approach are evaluated through extensive experimentations based on the CVC4, veriT, and nuXmv checkers.