@article{2022ACC,
  author    = {Daniele Bringhenti and Guido Marchetto and Riccardo Sisto and
               Fulvio Valenza and Jalolliddin Yusupov},
  title     = {Automated firewall configuration in virtual networks},
  journal   = {{IEEE} Transactions on Dependable and Secure Computing},
  year      = {2022},
  url       = {https://iris.polito.it/retrieve/handle/11583/2958744/571845/TDSC2022.pdf},
  doi       = {10.1109/TDSC.2022.3160293},
  abstract = {The configuration of security functions in computer
networks is still typically performed manually, which likely
leads to security breaches and long re-configuration times.
This problem is exacerbated for modern networks based on
network virtualization, because their complexity and dynamics
make a correct manual configuration practically unfeasible. This
article focuses on packet filters, i.e., the most common firewall
technology used in computer networks, and it proposes a new
methodology to automatically define the allocation scheme and
configuration of packet filters in the logical topology of a virtual
network. The proposed method is based on solving a carefully
designed partial weighted Maximum Satisfiability Modulo Theories problem 
by means of a state of the art solver. This approach
formally guarantees the correctness of the solution, i.e., that
all security requirements are satisfied, and it minimizes the
number of needed firewalls and firewall rules. This methodology
is extensively evaluated using different metrics and tests on both
synthetic and real use cases, and compared to the state-of-the-art
solutions, showing its superiority. © 2022 IEEE.},   
  note      = {in press}}

The configuration of security functions in computer networks is still typically performed manually, which likely leads to security breaches and long re-configuration times. This problem is exacerbated for modern networks based on network virtualization, because their complexity and dynamics make a correct manual configuration practically unfeasible. This article focuses on packet filters, i.e., the most common firewall technology used in computer networks, and it proposes a new methodology to automatically define the allocation scheme and configuration of packet filters in the logical topology of a virtual network. The proposed method is based on solving a carefully designed partial weighted Maximum Satisfiability Modulo Theories problem by means of a state of the art solver. This approach formally guarantees the correctness of the solution, i.e., that all security requirements are satisfied, and it minimizes the number of needed firewalls and firewall rules. This methodology is extensively evaluated using different metrics and tests on both synthetic and real use cases, and compared to the state-of-the-art solutions, showing its superiority. © 2022 IEEE.

@article{2022CN,
  author    = {Daniele Bringhenti and Jalolliddin Yusupov and Alejandro Molina Zarca and Fulvio Valenza and Riccardo Sisto and Jorge Bernal Bernabe and Antonio Skarmeta},
  title     = {Automatic, verifiable and optimized policy-based security enforcement for SDN-aware IoT networks},
  journal   = {Elsevier Computer Networks},
  volume    = {213},
  pages     = {109--123},
  year      = {2022},
  url       = {https://iris.polito.it/retrieve/handle/11583/2968670/593984/AuthorManuscript.pdf},
  doi       = {10.1016/j.comnet.2022.109123},
  abstract={The pervasiveness of Internet of Things (IoT) has made the management of computer networks more troublesome. The
softwarized control provided by Software-Defined Networking (SDN) is not sufficient to overcome the problems raising in
this context. An increasing number of attacks can, in fact, occur in SDN-aware IoT networks if the security configuration
enforced on the SDN switches is manually computed and not formally verified. To mitigate this problem, this paper
proposes a novel methodology which leverages Maximum Satisfiability Modulo Theories (MaxSMT) to automatically
compute a formally correct and optimized allocation scheme and configuration of SDN switches by refining security
policies, user-defined or derived from detected attacks. This mechanism is compliant with the main characteristics of
virtualized IoT-based networks, such as the simultaneous presence of numerous interconnected devices and strict latency
requirements. The feasibility and the performance of the framework developed to implement this methodology have
been validated in a realistic use case.},
  keywords={Policy Refinement,Security Automation}, 	
}

The pervasiveness of Internet of Things (IoT) has made the management of computer networks more troublesome. The softwarized control provided by Software-Defined Networking (SDN) is not sufficient to overcome the problems raising in this context. An increasing number of attacks can, in fact, occur in SDN-aware IoT networks if the security configuration enforced on the SDN switches is manually computed and not formally verified. To mitigate this problem, this paper proposes a novel methodology which leverages Maximum Satisfiability Modulo Theories (MaxSMT) to automatically compute a formally correct and optimized allocation scheme and configuration of SDN switches by refining security policies, user-defined or derived from detected attacks. This mechanism is compliant with the main characteristics of virtualized IoT-based networks, such as the simultaneous presence of numerous interconnected devices and strict latency requirements. The feasibility and the performance of the framework developed to implement this methodology have been validated in a realistic use case.

@article{2022ACC,
  author    = {Daniele Bringhenti and
               Fulvio Valenza},
  title     = {A Twofold Model for {VNF} Embedding and Time-Sensitive Network Flow
               Scheduling},
  journal   = {{IEEE} Access},
  volume    = {10},
  pages     = {44384--44399},
  year      = {2022},
  url       = {https://iris.polito.it/retrieve/handle/11583/2962049/579649/OnlineVersion.pdf},
  doi       = {10.1109/ACCESS.2022.3169863},
  abstract={The revolution that Industrial Control Systems are undergoing is reshaping the traditional
network management and it is introducing new challenges. After the advent of network virtualization,
an enhanced level of automation has been required to cope with the safety-critical mission of industrial
systems and strict requirements for end-to-end latency. In the literature, there have been attempts to
automatically solve two strictly interconnected problems for the management of virtual industrial networks:
the Virtual Network Function embedding and the time-sensitive flow scheduling problems. However, dealing
with these problems separately can lead to unoptimized results, or in the worst case to situations where the
latency requirements cannot be satisfied because of a poorly chosen function embedding. In light of these
motivations, this paper proposes a formal approach to jointly solve the two problems through an Optimization
Satisfiability Modulo Theories formulation. This choice also allows combining two vital features: a formal
guarantee of the solution correctness and optimization targeting the minimization of the end-to-end delay for
flow scheduling. The feasibility of the proposed approach has been validated by implementing a prototype
framework and experimentally testing it on realistic use cases.},
  keywords={Security Function Modeling,Policy Verification}, 	
}

The revolution that Industrial Control Systems are undergoing is reshaping the traditional network management and it is introducing new challenges. After the advent of network virtualization, an enhanced level of automation has been required to cope with the safety-critical mission of industrial systems and strict requirements for end-to-end latency. In the literature, there have been attempts to automatically solve two strictly interconnected problems for the management of virtual industrial networks: the Virtual Network Function embedding and the time-sensitive flow scheduling problems. However, dealing with these problems separately can lead to unoptimized results, or in the worst case to situations where the latency requirements cannot be satisfied because of a poorly chosen function embedding. In light of these motivations, this paper proposes a formal approach to jointly solve the two problems through an Optimization Satisfiability Modulo Theories formulation. This choice also allows combining two vital features: a formal guarantee of the solution correctness and optimization targeting the minimization of the end-to-end delay for flow scheduling. The feasibility of the proposed approach has been validated by implementing a prototype framework and experimentally testing it on realistic use cases.

@article{2022SEP,
  author    = {Daniele Bringhenti and
               Fulvio Valenza and
               Cataldo Basile},
  title     = {Toward Cybersecurity Personalization in Smart Homes},
  journal   = {{IEEE} Secur. Priv.},
  volume    = {20},
  number    = {1},
  pages     = {45--53},
  year      = {2022},
  url       = {https://iris.polito.it/retrieve/handle/11583/2927212/573382/IEEESP.pdf},
  doi       = {10.1109/MSEC.2021.3117471},
  abstract={Security personalization has become a critical need for smart homes in recent years. The current
approaches cannot fully satisfy this requirement of user-centered security. We propose a user-friendly
approach for the automatic configuration of home security solutions through policy-based management,
minimizing human interventions, and improving security usability},
  keywords={Policy Refinement,Security Automation}, 	
}

Security personalization has become a critical need for smart homes in recent years. The current approaches cannot fully satisfy this requirement of user-centered security. We propose a user-friendly approach for the automatic configuration of home security solutions through policy-based management, minimizing human interventions, and improving security usability

@Article{2021TNSM,
  author   = {D. {Bringhenti} and G. {Marchetto} and R. {Sisto} and S. {Spinoso} and F. {Valenza} and J. {Yusupov}},
  journal  = {IEEE Transactions on Network and Service Management},
  title    = {Improving the Formal Verification of Reachability Policies in Virtualized Networks},
  year     = {2021},
  number   = {1},
  pages    = {713-728},
  volume   = {18},
  abstract = {Network Function Virtualization (NFV) and Software Defined Networking (SDN) are new emerging paradigms that changed the rules of networking, shifting the focus on dynamicity and programmability. In this new scenario, a very important and challenging task is to detect anomalies in the data plane, especially with the aid of suitable automated software tools. In particular, this operation must be performed within quite strict times, due to the high dynamism introduced by virtualization. In this article, we propose a new network modeling approach that enhances the performance of formal verification of reachability policies, checked by solving a Satisfiability Modulo Theories (SMT) problem. This performance improvement is motivated by the definition of function models that do not work on single packets, but on packet classes. Nonetheless, the modeling approach is comprehensive not only of stateless functions, but also stateful functions such as NATs and firewalls. The implementation of the proposed approach achieves high scalability in complex networked systems consisting of several heterogeneous functions.},
  doi      = {10.1109/TNSM.2020.3045781},
  keywords = {Reachability Verification, Policy Verification, Security Function Modeling},
  url      = {https://iris.polito.it/retrieve/handle/11583/2859052/435762/TNSM2021.pdf},
}

Network Function Virtualization (NFV) and Software Defined Networking (SDN) are new emerging paradigms that changed the rules of networking, shifting the focus on dynamicity and programmability. In this new scenario, a very important and challenging task is to detect anomalies in the data plane, especially with the aid of suitable automated software tools. In particular, this operation must be performed within quite strict times, due to the high dynamism introduced by virtualization. In this article, we propose a new network modeling approach that enhances the performance of formal verification of reachability policies, checked by solving a Satisfiability Modulo Theories (SMT) problem. This performance improvement is motivated by the definition of function models that do not work on single packets, but on packet classes. Nonetheless, the modeling approach is comprehensive not only of stateless functions, but also stateful functions such as NATs and firewalls. The implementation of the proposed approach achieves high scalability in complex networked systems consisting of several heterogeneous functions.

@article{ValenzaRS21,
  author    = {Fulvio Valenza and
               Matteo Repetto and
               Stavros Shiaeles},
  title     = {Guest editorial: Special issue on novel cyber-security paradigms for
               software-defined and virtualized systems},
  journal   = {Comput. Networks},
  volume    = {193},
  pages     = {108126},
  year      = {2021},
  url       = {https://iris.polito.it/retrieve/handle/11583/2897950/480116/1-s2.0-S1389128621001997-main.pdf},
  doi       = {10.1016/j.comnet.2021.108126},
 abstract={The massive shift to ‘‘virtualization’’ paradigms has largely transformed the traditional computing models, by progressively eroding the typical strong link between applications and devices, hence requiring to rethink and reshape the structure and composition of services and infrastructures. On the one hand, the continuous disaggregation between the software and the hardware facilitates the migration of applications and services to different infrastructures. On the other hand, the growing ‘‘softwarization’’ trend allows the creation and disposal of even complex execution environments in a matter of minutes or seconds instead of days or weeks; this includes the provisioning of (virtual) computing and networking resources, the retrieval of software images, the processing of large data sets and the connection to an ever-growing Internet of Things. The undergoing evolution has also fostered a ground-breaking transition in design and development patterns, from monolithic applications and closed silos to open and interconnected service meshes, which leverage cloud models, common interfaces, and orchestration paradigms. Pragmatic examples of such architectures in the networking domains are Network Functions Virtualization (NFV) and Software Defined Networking (SDN), which has not only brought more flexibility in network management, but has also opened new perspectives and opportunities in the realization of large, distributed, and pervasive cyber–physical systems. However, this has also determined an increase in the networks’ size and complexity, not to mention the security dependency on external software, services, data and infrastructures. The management of network devices has become more difficult than in the past, and the number of vulnerabilities that could be exploited in a cyberattack is nowadays bigger as well. Unfortunately, cyber-security paradigms have not evolved at the same pace. As a matter of fact, the ‘‘security perimeter’’ model is still the predominant paradigm, but it cannot effectively address the many issues related to multi-tenancy, increased complexity, automated lifecycle management. Although cloud management and orchestration software is already mature for the market, many enterprises are reluctant to adopt such technologies due to security concerns, which still imply more traditional (and longer) processes. For instance, network services can today be designed as the composition of Virtual Network Functions (VNFs), including resource constraints, and then automatically deployed over self-provisioning virtualized infrastructures. VNFs can be rapidly turned on and set up, with respect to what a hardware device was used to require in the past. However, there are not as much fast security processes for checking software images, hardening an ever evolving topology, give visibility over functions running in external infrastructures. A new breed of cyber-security paradigms and models are therefore necessary that could address the increased complexity and size of modern systems, not to mention the rapid escalation of advanced persistent threats and multi-vector attacks. Beyond more advanced techniques based on Machine Learning and other forms of Artificial Intelligence that could effectively cope the ever evolving threat landscape and attack patterns, it is also important to address the growing dynamicity of modern computing paradigms, self-provisioning models, service-oriented architectures, shared resources and software-defined infrastructures. This special issue of Elsevier Computer Networks fostered new research work that took into consideration security challenges brought by the usage of public cloud, heterogeneous infrastructures and providers, and dynamic software deployment and orchestration mechanisms. The scope is not limited to a single topic, but covers several aspects that fall under the aforementioned evolutionary perspective. To this end, after the two successful SecSoft workshops1 that deal with these fields, we selected the best papers from these editions to invite the authors for submission of an extended paper for peer review and potential publication in this special issue.},
   keywords  = {Security Orchestration, Security Automation}
}

The massive shift to ‘‘virtualization’’ paradigms has largely transformed the traditional computing models, by progressively eroding the typical strong link between applications and devices, hence requiring to rethink and reshape the structure and composition of services and infrastructures. On the one hand, the continuous disaggregation between the software and the hardware facilitates the migration of applications and services to different infrastructures. On the other hand, the growing ‘‘softwarization’’ trend allows the creation and disposal of even complex execution environments in a matter of minutes or seconds instead of days or weeks; this includes the provisioning of (virtual) computing and networking resources, the retrieval of software images, the processing of large data sets and the connection to an ever-growing Internet of Things. The undergoing evolution has also fostered a ground-breaking transition in design and development patterns, from monolithic applications and closed silos to open and interconnected service meshes, which leverage cloud models, common interfaces, and orchestration paradigms. Pragmatic examples of such architectures in the networking domains are Network Functions Virtualization (NFV) and Software Defined Networking (SDN), which has not only brought more flexibility in network management, but has also opened new perspectives and opportunities in the realization of large, distributed, and pervasive cyber–physical systems. However, this has also determined an increase in the networks’ size and complexity, not to mention the security dependency on external software, services, data and infrastructures. The management of network devices has become more difficult than in the past, and the number of vulnerabilities that could be exploited in a cyberattack is nowadays bigger as well. Unfortunately, cyber-security paradigms have not evolved at the same pace. As a matter of fact, the ‘‘security perimeter’’ model is still the predominant paradigm, but it cannot effectively address the many issues related to multi-tenancy, increased complexity, automated lifecycle management. Although cloud management and orchestration software is already mature for the market, many enterprises are reluctant to adopt such technologies due to security concerns, which still imply more traditional (and longer) processes. For instance, network services can today be designed as the composition of Virtual Network Functions (VNFs), including resource constraints, and then automatically deployed over self-provisioning virtualized infrastructures. VNFs can be rapidly turned on and set up, with respect to what a hardware device was used to require in the past. However, there are not as much fast security processes for checking software images, hardening an ever evolving topology, give visibility over functions running in external infrastructures. A new breed of cyber-security paradigms and models are therefore necessary that could address the increased complexity and size of modern systems, not to mention the rapid escalation of advanced persistent threats and multi-vector attacks. Beyond more advanced techniques based on Machine Learning and other forms of Artificial Intelligence that could effectively cope the ever evolving threat landscape and attack patterns, it is also important to address the growing dynamicity of modern computing paradigms, self-provisioning models, service-oriented architectures, shared resources and software-defined infrastructures. This special issue of Elsevier Computer Networks fostered new research work that took into consideration security challenges brought by the usage of public cloud, heterogeneous infrastructures and providers, and dynamic software deployment and orchestration mechanisms. The scope is not limited to a single topic, but covers several aspects that fall under the aforementioned evolutionary perspective. To this end, after the two successful SecSoft workshops1 that deal with these fields, we selected the best papers from these editions to invite the authors for submission of an extended paper for peer review and potential publication in this special issue.

@InProceedings{2021Netsoft,
  author    = {Daniele Bringhenti and
               Guido Marchetto and
               Riccardo Sisto and
               Fulvio Valenza},
  title     = {A novel approach for security function graph configuration and deployment},
  booktitle = {7th {IEEE} International Conference on Network Softwarization, NetSoft
               2021, Tokyo, Japan, June 28 - July 2, 2021},
  pages     = {457--463},
  publisher = {{IEEE}},
  year      = {2021},
  url       = {https://iris.polito.it/retrieve/handle/11583/2921763/513222/main.pdf},
  doi       = {10.1109/NetSoft51509.2021.9492654},
    abstract={Network virtualization increased the versatility in
enforcing security protection, by easing the development of
new security function implementations. However, the drawback
of this opportunity is that a security provider, in charge of
configuring and deploying a security function graph, has to
choose the best virtual security functions among a pool so large
that makes manual decisions unfeasible. In light of this problem,
the paper proposes a novel approach for synthesizing virtual
security services by introducing the functionality abstraction.
This new level of abstraction allows to work in the virtual level
without considering the different function implementations, with
the objective to postpone the function selection jointly with the
deployment, after the configuration of the virtual graph. This
novelty enables to optimize the function selection when the pool
of available functions is very large. A framework supporting
this approach has been implemented and it showed adequate
scalability for the requirements of modern virtual networks},
  keywords={Security Function Modeling,Policy Refinement,Security Automation}, 
}

Network virtualization increased the versatility in enforcing security protection, by easing the development of new security function implementations. However, the drawback of this opportunity is that a security provider, in charge of configuring and deploying a security function graph, has to choose the best virtual security functions among a pool so large that makes manual decisions unfeasible. In light of this problem, the paper proposes a novel approach for synthesizing virtual security services by introducing the functionality abstraction. This new level of abstraction allows to work in the virtual level without considering the different function implementations, with the objective to postpone the function selection jointly with the deployment, after the configuration of the virtual graph. This novelty enables to optimize the function selection when the pool of available functions is very large. A framework supporting this approach has been implemented and it showed adequate scalability for the requirements of modern virtual networks

@Article{2021TII,
  author   = {Guido Marchetto and Riccardo Sisto and Fulvio Valenza and Jalolliddin Yusupov and Adlen Ksentini},
  journal  = {{IEEE} Transactions on Industrial Informatics},
  title    = {A Formal Approach to Verify Connectivity and Optimize {VNF} Placement in Industrial Networks},
  year     = {2021},
  number   = {2},
  pages    = {1515--1525},
  volume   = {17},
  abstract = {The increased flexibility and interconnectivity of modern industrial communication networks, obtained through the use of innovative technologies like network function virtualization and software-defined networking, require a secure and manageable framework to support the new communication and computing needs. To focus on these requirements, this article proposes a framework for reliable placement of services across physically separated locations, which offers both system optimization, in terms of latency and resource utilization, and connectivity policy enforcement to guarantee service reliability, safety, and security. This is achieved by exploiting a new approach to solve the virtual network embedding problem, using optimization modulo theories (MaxSMT), which allows the use of very expressive constraints. © 2020 IEEE.},
  doi      = {10.1109/TII.2020.3002816},
  keywords = {Industrial Network Systems, VNF Placement, Reachability Verification},
  url      = {https://iris.polito.it/retrieve/handle/11583/2853938/410825/09119174.pdf},
}

The increased flexibility and interconnectivity of modern industrial communication networks, obtained through the use of innovative technologies like network function virtualization and software-defined networking, require a secure and manageable framework to support the new communication and computing needs. To focus on these requirements, this article proposes a framework for reliable placement of services across physically separated locations, which offers both system optimization, in terms of latency and resource utilization, and connectivity policy enforcement to guarantee service reliability, safety, and security. This is achieved by exploiting a new approach to solve the virtual network embedding problem, using optimization modulo theories (MaxSMT), which allows the use of very expressive constraints. © 2020 IEEE.

@InProceedings{2020WFCS,
  author    = {Alessio Sacco and Guido Marchetto and Riccardo Sisto and Fulvio Valenza},
  booktitle = {Proceedings of the 16th {IEEE} International Conference on Factory Communication Systems ({WFCS} 2020)},
  doi       = {10.1109/WFCS47810.2020.9114432},
  pages     = {1--4},
  publisher = {{IEEE}},
  title     = {Work-in-Progress: {A} Formal Approach to Verify Fault Tolerance in Industrial Network Systems},
  year      = {2020},
abstract={Distributed systems are extremely difficult to design and implement correctly because they must handle both system correctness and device failures. Most of the work focuses on the first aspect, and in particular, on the correctness of security and network configuration. The large demand for availability and reliability for critical services is actually pushing new architectures that tolerate faults, but a-priori analysis of redundancy and recovery features is still limited. To this end, we present a framework to design and formally verify the persistence of network properties, even in case of failures. The solution considers both nodes and links failure, and it is based on a formal model that takes both network topology and network device configurations into account. In contrast, most of the existing approaches only consider network topology. By analyzing the formal model, the framework can check whether the specified network services are still available after failures, and in case of success, it outputs a possible configuration of the devices to be used for automatic recovery. © 2020 IEEE.},
keywords={Industrial Network Systems,  Reachability Verification},
  url       = {https://iris.polito.it/retrieve/handle/11583/2842984/390133/WFCS_2020_WiP_submitted.pdf},
}

Distributed systems are extremely difficult to design and implement correctly because they must handle both system correctness and device failures. Most of the work focuses on the first aspect, and in particular, on the correctness of security and network configuration. The large demand for availability and reliability for critical services is actually pushing new architectures that tolerate faults, but a-priori analysis of redundancy and recovery features is still limited. To this end, we present a framework to design and formally verify the persistence of network properties, even in case of failures. The solution considers both nodes and links failure, and it is based on a formal model that takes both network topology and network device configurations into account. In contrast, most of the existing approaches only consider network topology. By analyzing the formal model, the framework can check whether the specified network services are still available after failures, and in case of success, it outputs a possible configuration of the devices to be used for automatic recovery. © 2020 IEEE.

@InProceedings{2020NOMS_ArgoFiCo,
  author    = {Erisa Karafili and Fulvio Valenza and Yichen Chen and Emil C. Lupu},
  booktitle = {Proceedings of the {IEEE/IFIP} Network Operations and Management Symposium ({NOMS} 2020)},
  doi       = {10.1109/NOMS47738.2020.9110399},
  pages     = {1--4},
  publisher = {{IEEE}},
  title     = {Towards a Framework for Automatic Firewalls Configuration via Argumentation Reasoning},
  year      = {2020},
  url       = {https://iris.polito.it/retrieve/handle/11583/2837544/426696/2020NOMS_ArgoFiCo_author.pdf},
  abstract={Firewalls have been widely used to protect not only small and local networks but also large enterprise networks. The configuration of firewalls is mainly done by network administrators, thus, it suffers from human errors. This paper aims to solve the network administrators' problem by introducing a formal approach that helps to configure centralized and distributed firewalls and automatically generate conflict-free firewall rules. We propose a novel framework, called ArgoFiCo, which is based on argumentation reasoning. Our framework automatically populates the firewalls of a network, given the network topology and the high-level requirements that represent how the network should behave. ArgoFiCo provides two strategies for firewall rules distribution. © 2020 IEEE.},
   keywords={Argumentation reasoning,  Firewall, Anomaly Resolution},
}

Firewalls have been widely used to protect not only small and local networks but also large enterprise networks. The configuration of firewalls is mainly done by network administrators, thus, it suffers from human errors. This paper aims to solve the network administrators' problem by introducing a formal approach that helps to configure centralized and distributed firewalls and automatically generate conflict-free firewall rules. We propose a novel framework, called ArgoFiCo, which is based on argumentation reasoning. Our framework automatically populates the firewalls of a network, given the network topology and the high-level requirements that represent how the network should behave. ArgoFiCo provides two strategies for firewall rules distribution. © 2020 IEEE.

@InProceedings{2020NOMS_VEREFOO,
  author    = {Daniele Bringhenti and Guido Marchetto and Riccardo Sisto and Fulvio Valenza and Jalolliddin Yusupov},
  booktitle = {Proceedings of the {IEEE/IFIP} Network Operations and Management Symposium ({NOMS} 2020)},
  title     = {Automated optimal firewall orchestration and configuration in virtualized networks},
  year      = {2020},
  pages     = {1--7},
  publisher = {{IEEE}},
  abstract  = {Emerging technologies such as Software-Defined Networking and Network Functions Virtualization are making the definition and configuration of network services more dynamic, thus making automatic approaches that can replace manual and error-prone tasks more feasible. In view of these considerations, this paper proposes a novel methodology to automatically compute the optimal allocation scheme and configuration of virtual firewalls within a user-defined network service graph subject to a corresponding set of security requirements. The presented framework adopts a formal approach based on the solution of a weighted partial MaxSMT problem, which also provides good confidence about the solution correctness. A prototype implementation of the proposed approach based on the z3 solver has been used for validation, showing the feasibility of the approach for problem instances requiring tens of virtual firewalls and similar numbers of security requirements. © 2020 IEEE.},
  doi       = {10.1109/NOMS47738.2020.9110402},
  keywords  = {Firewall, Policy Refinement, Security Automation},
  url       = {https://iris.polito.it/retrieve/handle/11583/2837546/426876/2020NOMS_VEREFOO_author.pdf},
}

Emerging technologies such as Software-Defined Networking and Network Functions Virtualization are making the definition and configuration of network services more dynamic, thus making automatic approaches that can replace manual and error-prone tasks more feasible. In view of these considerations, this paper proposes a novel methodology to automatically compute the optimal allocation scheme and configuration of virtual firewalls within a user-defined network service graph subject to a corresponding set of security requirements. The presented framework adopts a formal approach based on the solution of a weighted partial MaxSMT problem, which also provides good confidence about the solution correctness. A prototype implementation of the proposed approach based on the z3 solver has been used for validation, showing the feasibility of the approach for problem instances requiring tens of virtual firewalls and similar numbers of security requirements. © 2020 IEEE.

@Article{2020JISIS,
  author    = {Fulvio Valenza and Manuel Cheminod},
  doi       = {10.22667/JISIS.2020.02.29.022},
  journal   = {Journal of Internet Services and Information Security},
  number    = {1},
  pages     = {22--37},
  title     = {An Optimized Firewall Anomaly Resolution},
  volume    = {10},
  year      = {2020},
  abstract={Firewalls are the key mechanism in cybersecurity, that has been widely used to ensure network security. In literature, several works have been proposed in the area of firewall rules managing, however, the correct firewall configuration still remains a complex and error-prone task. Anomalies among firewall rules can cause severe network breaches, such as allowing harmful packets to slip into a subnetwork or dropping legitimate traffic which in turn could hinder the correct availability of web services. This paper aims to help the network security administrators by introducing a formal approach that reduces the number of anomalies in firewalls’ configurations that the administrators are usually obligated to manually solve. © 2020, Innovative Information Science and Technology Research Group.},
  url       = {https://iris.polito.it/retrieve/handle/11583/2819872/356860/jisis-2020-vol10-no1-02.pdf},
    keywords={Firewall, Anomaly Resolution},

}

Firewalls are the key mechanism in cybersecurity, that has been widely used to ensure network security. In literature, several works have been proposed in the area of firewall rules managing, however, the correct firewall configuration still remains a complex and error-prone task. Anomalies among firewall rules can cause severe network breaches, such as allowing harmful packets to slip into a subnetwork or dropping legitimate traffic which in turn could hinder the correct availability of web services. This paper aims to help the network security administrators by introducing a formal approach that reduces the number of anomalies in firewalls’ configurations that the administrators are usually obligated to manually solve. © 2020, Innovative Information Science and Technology Research Group.

@Article{2020TVT,
  author    = {Marco Iorio and Massimo Reineri and Fulvio Risso and Riccardo Sisto and Fulvio Valenza},
  doi       = {10.1109/TVT.2020.3028880},
  journal   = {{IEEE} Transactions on Vehicular Technology},
  number    = {11},
  pages     = {13450--13466},
  title     = {Securing {SOME/IP} for In-Vehicle Service Protection},
  volume    = {69},
  year      = {2020},
  url       = {https://iris.polito.it/retrieve/handle/11583/2847755/399772/09215036.pdf},
  abstract={Although high-speed in-vehicle networks are being increasingly adopted by the industry to support emerging use cases, previous research already demonstrated that car hacking is a real threat. This paper formalizes a novel framework proposed to provide improved security to the emerging SOME/IP middleware, without introducing at the same time limitations in the communication patterns available. Most notably, the entire traffic matrix is designed to be configured using simple high-level rules, clearly stating who can talk to whom according to the service abstraction adopted by SOME/IP. Three incremental security levels are made available, accounting for different services being associated with different requirements. The core security protocol, encompassing a session establishment phase followed by the transmission of secured SOME/IP messages, has been formally verified, to prove its correctness in terms of authentication and secrecy properties. Performance-wise, in-depth experimental evaluations conducted with an extended version of vsomeip confirmed the introduction of quite limited penalties compared to the bare unsecured implementation. © 1967-2012 IEEE.},
  keywords={In-vehicle Security},
}

Although high-speed in-vehicle networks are being increasingly adopted by the industry to support emerging use cases, previous research already demonstrated that car hacking is a real threat. This paper formalizes a novel framework proposed to provide improved security to the emerging SOME/IP middleware, without introducing at the same time limitations in the communication patterns available. Most notably, the entire traffic matrix is designed to be configured using simple high-level rules, clearly stating who can talk to whom according to the service abstraction adopted by SOME/IP. Three incremental security levels are made available, accounting for different services being associated with different requirements. The core security protocol, encompassing a session establishment phase followed by the transmission of secured SOME/IP messages, has been formally verified, to prove its correctness in terms of authentication and secrecy properties. Performance-wise, in-depth experimental evaluations conducted with an extended version of vsomeip confirmed the introduction of quite limited penalties compared to the bare unsecured implementation. © 1967-2012 IEEE.

@InProceedings{2020CYSARM,
  author    = {Bringhenti, D. and Marchetto, G. and Sisto, R. and Valenza, F.},
  booktitle = {Proceedings of the 2nd {AMC CCS} Workshop on Cyber-Security Arms Race (CYSARM 2020)},
  doi       = {10.1145/3411505.3418439},
  pages     = {25-30},
  title     = {Short Paper: Automatic Configuration for an Optimal Channel Protection in Virtualized Networks},
  year      = {2020},
  abstract  = {Data confidentiality, integrity and authentication are security properties which are often enforced with the generation of secure channels, such as Virtual Private Networks, over unreliable network infrastructures. Traditionally, the configuration of the systems responsible of encryption operations is performed manually. However, the advent of software-based paradigms, such as Software-Defined Networking and Network Functions Virtualization, has introduced new arms races. In particular, even though network management has become more flexible, the increased complexity of virtual networks is making manual operations unfeasible and leading to errors which open the path to a large number of cyber attacks. A possible solution consists in reaching a trade-off between flexibility and complexity, by automatizing the configuration of the channel protection systems through policy refinement. In view of these considerations, this paper proposes a preliminary study for an innovative methodology to automatically allocate and configure channel protection systems in virtualized networks. The proposed approach would be based on the formulation of a MaxSMT problem and it would be the first to combine automation, formal verification and optimality in a single technique. © 2020 ACM.},
  keywords  = {VPN, Policy Refinement},
  url       = {https://iris.polito.it/retrieve/handle/11583/2844334/426885/2020_CYSARM_author.pdf},
}

Data confidentiality, integrity and authentication are security properties which are often enforced with the generation of secure channels, such as Virtual Private Networks, over unreliable network infrastructures. Traditionally, the configuration of the systems responsible of encryption operations is performed manually. However, the advent of software-based paradigms, such as Software-Defined Networking and Network Functions Virtualization, has introduced new arms races. In particular, even though network management has become more flexible, the increased complexity of virtual networks is making manual operations unfeasible and leading to errors which open the path to a large number of cyber attacks. A possible solution consists in reaching a trade-off between flexibility and complexity, by automatizing the configuration of the channel protection systems through policy refinement. In view of these considerations, this paper proposes a preliminary study for an innovative methodology to automatically allocate and configure channel protection systems in virtualized networks. The proposed approach would be based on the formulation of a MaxSMT problem and it would be the first to combine automation, formal verification and optimality in a single technique. © 2020 ACM.

@ARTICLE{VTM2020,
author={Iorio, M. and Buttiglieri, A. and Reineri, M. and Risso, F. and Sisto, R. and Valenza, F.},
title={Protecting In-Vehicle Services: Security-Enabled SOME/IP Middleware},
journal={IEEE Vehicular Technology Magazine},
year={2020},
volume={15},
number={3},
pages={77-85},
doi={10.1109/MVT.2020.2980444},
url={https://iris.polito.it/retrieve/handle/11583/2833292/372396/09085373.pdf},
abstract={With every generation, vehicles are becoming smarter and more oriented toward information and communications technology (ICT). However, computerization is posing unforeseen challenges in a sector for which the first goal must be safety: Car hacking has been shown to be a real threat. This article presents a novel mechanism to provide improved security for applications executed in the vehicle based on the principle of defining exactly who can talk to whom. The proposed security framework targets Ethernet-based com-munications and is tightly integrated within the emerging Scalable service-Oriented MiddlewarE over IP (SOME/IP) middleware. No complex configurations are needed: Simple high-level rules, clearly stating the communications allowed, are the only element required to enable the security features. The designed solution has been implemented as a proof of concept (PoC) inside the vsomeip stack to evaluate the validity of the approach proposed: Experimental measurements confirm that the additional overhead introduced in end-to-end communication is negligible. © 2020 IEEE.},
keywords={In-vehicle Security},
}

With every generation, vehicles are becoming smarter and more oriented toward information and communications technology (ICT). However, computerization is posing unforeseen challenges in a sector for which the first goal must be safety: Car hacking has been shown to be a real threat. This article presents a novel mechanism to provide improved security for applications executed in the vehicle based on the principle of defining exactly who can talk to whom. The proposed security framework targets Ethernet-based com-munications and is tightly integrated within the emerging Scalable service-Oriented MiddlewarE over IP (SOME/IP) middleware. No complex configurations are needed: Simple high-level rules, clearly stating the communications allowed, are the only element required to enable the security features. The designed solution has been implemented as a proof of concept (PoC) inside the vsomeip stack to evaluate the validity of the approach proposed: Experimental measurements confirm that the additional overhead introduced in end-to-end communication is negligible. © 2020 IEEE.

@ARTICLE{2020IJEST,
author={Makartetskiy, D. and Marchetto, G. and Sisto, R. and Valenza, F. and Virgilio, M. and Leri, D. and Denti, P. and Finizio, R.},
title={(User-friendly) formal requirements verification in the context of ISO26262},
journal={Engineering Science and Technology, an International Journal},
year={2020},
volume={23},
number={3},
pages={494-506},
doi={10.1016/j.jestch.2019.09.005},
url={https://iris.polito.it/retrieve/handle/11583/2785894/367840/1-s2.0-S2215098619306147-main.pdf},
abstract={In order to achieve the highest safety integrity levels, ISO26262 recommends the use of formal methods for various verification activities, throughout the lifecycle of safety-related embedded systems for road vehicles. Since formal methods are known to be difficult to use, one of the main challenges raised by these ISO26262 requirements is to find cost-effective approaches for being compliant with them. This paper proposes an approach for requirements formal verification where formal methods, languages, and tools are only minimally exposed to the user, and are integrated into one of the commonly used system modeling environments based on SysML. This approach does not require particular expertise in formal methods still allowing to apply them. Hence, personnel training costs and development costs should be kept limited. The proposed approach has been implemented as a plugin of the Topcased environment. Although it is limited to discrete system models, it has been successfully experimented on an industrial use case. © 2019 Karabuk University},
keywords={In-vehicle Security},
}

In order to achieve the highest safety integrity levels, ISO26262 recommends the use of formal methods for various verification activities, throughout the lifecycle of safety-related embedded systems for road vehicles. Since formal methods are known to be difficult to use, one of the main challenges raised by these ISO26262 requirements is to find cost-effective approaches for being compliant with them. This paper proposes an approach for requirements formal verification where formal methods, languages, and tools are only minimally exposed to the user, and are integrated into one of the commonly used system modeling environments based on SysML. This approach does not require particular expertise in formal methods still allowing to apply them. Hence, personnel training costs and development costs should be kept limited. The proposed approach has been implemented as a plugin of the Topcased environment. Although it is limited to discrete system models, it has been successfully experimented on an industrial use case. © 2019 Karabuk University

@InProceedings{2020NetSoft,
  author    = {Bringhenti, D. and Marchetto, G. and Sisto, R. and Valenza, F. and Yusupov, J.},
  booktitle = {Proceedings of the 6th {IEEE} Conference on Network Softwarization (NetSoft 2020)},
  title     = {Introducing programmability and automation in the synthesis of virtual firewall rules},
  year      = {2020},
  pages     = {473-478},
  abstract  = {The rise of new forms of cyber-threats is mostly due to the extensive use of virtualization paradigms and the increasing adoption of automation in the software life-cycle. To address these challenges we propose an innovative framework that leverages the intrinsic programmability of the cloud and software-defined infrastructures to improve the effectiveness and efficiency of reaction mechanisms. In this paper, we present our contributions with a demonstrative use case in the context of Kubernetes. By means of this framework, developers of cybersecurity appliances will not have any more to care about how to react to events or to struggle to define any possible security tasks at design time. In addition, automatic firewall ruleset generation provided by our framework will mostly avoid human intervention, hence decreasing the time to carry out them and the likelihood of errors. We focus our discussions on technical challenges: definition of common actions at the policy level and their translation into configurations for the heterogeneous set of security functions by means of a use case. © 2020 IEEE.},
  doi       = {10.1109/NetSoft48620.2020.9165434},
  keywords  = {Firewall, Security Orchestration},
  url       = {https://iris.polito.it/retrieve/handle/11583/2844332/391324/main.pdf},
}

The rise of new forms of cyber-threats is mostly due to the extensive use of virtualization paradigms and the increasing adoption of automation in the software life-cycle. To address these challenges we propose an innovative framework that leverages the intrinsic programmability of the cloud and software-defined infrastructures to improve the effectiveness and efficiency of reaction mechanisms. In this paper, we present our contributions with a demonstrative use case in the context of Kubernetes. By means of this framework, developers of cybersecurity appliances will not have any more to care about how to react to events or to struggle to define any possible security tasks at design time. In addition, automatic firewall ruleset generation provided by our framework will mostly avoid human intervention, hence decreasing the time to carry out them and the likelihood of errors. We focus our discussions on technical challenges: definition of common actions at the policy level and their translation into configurations for the heterogeneous set of security functions by means of a use case. © 2020 IEEE.

@Article{2019,
  author    = {Fulvio Valenza and Serena Spinoso and Riccardo Sisto},
  doi       = {10.1016/j.jnca.2019.102419},
  journal   = {Journal of Network and Computer Applications},
  title     = {Formally specifying and checking policies and anomalies in service function chaining},
  volume    = {146},
  year      = {2019},
abstract={One of the proposed management strategies for SDN networks is to specify traffic forwarding through policies, where each policy rule identifies a traffic flow and its traversed service chains. While network operators need to check network configurations as soon as possible, the SDN verification literature focuses on checking policy correctness during or after their deployment. This paper, instead, proposes early verification of forwarding policies before their deployment, by looking for the presence of anomalies that can potentially lead to erroneous and unexpected network behaviour. The proposed verification relies on a formal model that enables high flexibility in specifying both a forwarding policy and the set of anomalies to verify. The presented approach is efficient and highly scalable, as confirmed by tests with large networks. © 2019 Elsevier Ltd},
  keywords={Policy Verification},
  url       = {},
}

One of the proposed management strategies for SDN networks is to specify traffic forwarding through policies, where each policy rule identifies a traffic flow and its traversed service chains. While network operators need to check network configurations as soon as possible, the SDN verification literature focuses on checking policy correctness during or after their deployment. This paper, instead, proposes early verification of forwarding policies before their deployment, by looking for the presence of anomalies that can potentially lead to erroneous and unexpected network behaviour. The proposed verification relies on a formal model that enables high flexibility in specifying both a forwarding policy and the set of anomalies to verify. The presented approach is efficient and highly scalable, as confirmed by tests with large networks. © 2019 Elsevier Ltd

@Article{2019SCN,
  author    = {Ignazio Pedone and Antonio Lioy and Fulvio Valenza},
  doi       = {10.1155/2019/2425983},
  journal   = {Secur. Commun. Networks},
  pages     = {2425983:1--2425983:11},
  title     = {Towards an Efficient Management and Orchestration Framework for Virtual Network Security Functions},
  volume    = {2019},
  year      = {2019},
abstract={The recent years have witnessed a growth in the number of users connected to computer networks, due mainly to megatrends such as Internet of Things (IoT), Industry 4.0, and Smart Grids. Simultaneously, service providers started offering vertical services related to a specific business case (e.g., automotive, banking, and e-health) requiring more and more scalability and flexibility for the infrastructures and their management. NFV and SDN technologies are a clear way forward to address these challenges even though they are still in their early stages. Security plays a central role in this scenario, mainly because it must follow the rapid evolution of computer networks and the growing number of devices. The main issue is to protect the end-user from the increasing threats, and for this reason, we propose in this paper a security framework compliant to the Security-as-a-Service paradigm. In order to implement this framework, we leverage NFV and SDN technologies, using a user-centered approach. This allows to customize the security service starting from user preferences. Another goal of our work is to highlight the main relevant challenges encountered in the design and implementation of our solution. In particular, we demonstrate how significant is to choose an efficient way to configure the Virtual Network Security Functions in terms of performance. Furthermore, we also address the nontrivial problem of Service Function Chaining in an NFV MANO platform and we show what are the main challenges with respect to this problem. © 2019 Ignazio Pedone et al.},
      keywords={Security Orchestration},
  url = {https://iris.polito.it/retrieve/handle/11583/2766668/287206/2425983.pdf}
}

The recent years have witnessed a growth in the number of users connected to computer networks, due mainly to megatrends such as Internet of Things (IoT), Industry 4.0, and Smart Grids. Simultaneously, service providers started offering vertical services related to a specific business case (e.g., automotive, banking, and e-health) requiring more and more scalability and flexibility for the infrastructures and their management. NFV and SDN technologies are a clear way forward to address these challenges even though they are still in their early stages. Security plays a central role in this scenario, mainly because it must follow the rapid evolution of computer networks and the growing number of devices. The main issue is to protect the end-user from the increasing threats, and for this reason, we propose in this paper a security framework compliant to the Security-as-a-Service paradigm. In order to implement this framework, we leverage NFV and SDN technologies, using a user-centered approach. This allows to customize the security service starting from user preferences. Another goal of our work is to highlight the main relevant challenges encountered in the design and implementation of our solution. In particular, we demonstrate how significant is to choose an efficient way to configure the Virtual Network Security Functions in terms of performance. Furthermore, we also address the nontrivial problem of Service Function Chaining in an NFV MANO platform and we show what are the main challenges with respect to this problem. © 2019 Ignazio Pedone et al.

@Article{2019ACCESS,
  author    = {Guido Marchetto and Riccardo Sisto and Fulvio Valenza and Jalolliddin Yusupov},
  doi       = {10.1109/ACCESS.2019.2929325},
  journal   = {{IEEE} Access},
  pages     = {99349--99359},
  title     = {A Framework for Verification-Oriented User-Friendly Network Function Modeling},
  volume    = {7},
  year      = {2019},
  abstract={Network virtualization and softwarization will serve as a new way to implement new services, increases network functionality and flexibility. However, the increasing complexity of the services and the management of very large scale environments drastically complicate detecting alerts and configuration errors of the network components. Nowadays, misconfigurations can be identified using formal analysis of network components for compliance with network requirements. Unfortunately, formal specification of network services requires familiarity with discrete mathematical modeling languages of verification tools, which requires extensive training for network engineers to have the essential knowledge. This paper addresses the above-mentioned problem by presenting a framework designed for automatically extracting verification models starting from an abstract representation of a given network function. Using guidelines provided in this paper, vendors can describe the forwarding behavior of their network function in developer-friendly, high-level languages, which can be then translated into formal verification models of different verification tools. © 2019 IEEE.},
  keywords={Security Function Modeling},
  url = {https://iris.polito.it/retrieve/handle/11583/2749814/271080/08765301.pdf}
}

Network virtualization and softwarization will serve as a new way to implement new services, increases network functionality and flexibility. However, the increasing complexity of the services and the management of very large scale environments drastically complicate detecting alerts and configuration errors of the network components. Nowadays, misconfigurations can be identified using formal analysis of network components for compliance with network requirements. Unfortunately, formal specification of network services requires familiarity with discrete mathematical modeling languages of verification tools, which requires extensive training for network engineers to have the essential knowledge. This paper addresses the above-mentioned problem by presenting a framework designed for automatically extracting verification models starting from an abstract representation of a given network function. Using guidelines provided in this paper, vendors can describe the forwarding behavior of their network function in developer-friendly, high-level languages, which can be then translated into formal verification models of different verification tools. © 2019 IEEE.

@Article{2019COSE,
  author    = {Manuel Cheminod and Luca Durante and Lucia Seno and Fulvio Valenza and Adriano Valenzano},
  doi       = {10.1016/j.cose.2018.09.013},
  journal   = {Computers and Security},
  pages     = {186--199},
  title     = {A comprehensive approach to the automatic refinement and verification of access control policies},
  volume    = {80},
  year      = {2019},
  abstract={Access control is one of the building blocks of network security and is often managed by network administrators through the definition of sets of high-level policies meant to regulate network behavior (policy-based management). In this scenario, policy refinement and verification are important processes that have to be dealt with carefully, possibly relaying on computer-aided automated software tools. This paper presents a comprehensive approach for access control policy refinement, verification and, in case errors are detected in the policy implementation, their fixing. The proposed methodology is based on a twofold model able to describe both policies and system configurations and allows, by suitably processing the model, to either propose a system configuration that correctly enforces the policies, or determine whether a specific implementation matches the policy specification also providing hints on how possible anomalies can be fixed. Results on the average complexity of the solution confirm its feasibility in terms of computation time, even for complex networked systems consisting of several hundred nodes. © 2018 Elsevier Ltd},
  keywords={Access Control Policy, Industrial Networked Systems},
   url = {https://iris.polito.it/retrieve/handle/11583/2724584/356856/main.pdf}
}

Access control is one of the building blocks of network security and is often managed by network administrators through the definition of sets of high-level policies meant to regulate network behavior (policy-based management). In this scenario, policy refinement and verification are important processes that have to be dealt with carefully, possibly relaying on computer-aided automated software tools. This paper presents a comprehensive approach for access control policy refinement, verification and, in case errors are detected in the policy implementation, their fixing. The proposed methodology is based on a twofold model able to describe both policies and system configurations and allows, by suitably processing the model, to either propose a system configuration that correctly enforces the policies, or determine whether a specific implementation matches the policy specification also providing hints on how possible anomalies can be fixed. Results on the average complexity of the solution confirm its feasibility in terms of computation time, even for complex networked systems consisting of several hundred nodes. © 2018 Elsevier Ltd

@InProceedings{2019NFVSDN,
  author    = {Matteo Repetto and Alessandro Carrega and Jalolliddin Yusupov and Fulvio Valenza and Fulvio Risso and G. Lamanna},
  booktitle = {Proceedings of the {IEEE} Conference on Network Function Virtualization and Software Defined Networks ({NFV-SDN} 2019)},
  doi       = {10.1109/NFV-SDN47374.2019.9040069},
  pages     = {1--2},
  publisher = {{IEEE}},
  title     = {Automated Security Management for Virtual Services},
  year      = {2019},
  abstract={The virtualization of applications and network functions facilitates the dynamic creation of compound services, automating both the provisioning of computing/networking/storage resources and their life-cycle management. Virtualization of security appliances is a common approach to protect such services, but can neither offer broad visibility across the whole deployed service nor implement coordinated and fine-grained enforcement actions. This paper proposes a novel security framework based on the integration of lightweight and programmable monitoring and enforcement hooks in each virtual function, which are collectively controlled by a common logic for prevention, detection, reaction, and mitigation of security threats. Our framework keeps direct control over the functionalities of the security hooks, and leverages standard orchestration tools for management actions on the service graph. It can be automatically instantiated by common orchestration operations, hence seamlessly integrating with the deployment process of service graphs. © 2019 IEEE.},
  keywords={Security Orchestration},
  url={https://iris.polito.it/retrieve/handle/11583/2753693/302241/nfv%20sdn.pdf}
}

The virtualization of applications and network functions facilitates the dynamic creation of compound services, automating both the provisioning of computing/networking/storage resources and their life-cycle management. Virtualization of security appliances is a common approach to protect such services, but can neither offer broad visibility across the whole deployed service nor implement coordinated and fine-grained enforcement actions. This paper proposes a novel security framework based on the integration of lightweight and programmable monitoring and enforcement hooks in each virtual function, which are collectively controlled by a common logic for prevention, detection, reaction, and mitigation of security threats. Our framework keeps direct control over the functionalities of the security hooks, and leverages standard orchestration tools for management actions on the service graph. It can be automatically instantiated by common orchestration operations, hence seamlessly integrating with the deployment process of service graphs. © 2019 IEEE.

@InProceedings{2019ICCCS,
  author    = {Daniele Bringhenti and Guido Marchetto and Riccardo Sisto and Fulvio Valenza and Jalolliddin Yusupov},
  booktitle = {Proceedings of the 4th International Conference on Computing, Communications and Security ({ICCCS} 2019)},
  doi       = {10.1109/CCCS.2019.8888130},
  pages     = {1--7},
  publisher = {{IEEE}},
  title     = {Towards a fully automated and optimized network security functions orchestration},
  year      = {2019},
abstract={Automated policy-based network security management tools represent a new research frontier to be fully explored, so as to reduce the number of human errors due to a manual and suboptimal configuration of security services. Moreover, the agility that an automated tool would require can be provided by the most recent networking technologies, Network Functions Virtualization and Software-Defined Networking, which move the network management from the hardware level to the software. However, even though a Security Automation approach is nowadays feasible and would bring several benefits in facing cybersecurity attacks, pending problems are that currently only a limited number of automatic management tools have been developed and that they do not have a direct integration with cloud orchestrators, consequently requiring human interaction. Given these considerations, in this paper we propose a novel framework, whose goal is to automatically and optimally allocate and conFigure security functions in a virtualized network service in a formal and verified way, directly integrated in cloud orchestrators. We validated this contribution through an implementation that is able to cooperate with two well-known orchestrators, that are Open Baton and Kubernetes. © 2019 IEEE.},
keywords={Security Orchestration},
url       = {https://iris.polito.it/retrieve/handle/11583/2753692/313520/main-2.pdf},
}

Automated policy-based network security management tools represent a new research frontier to be fully explored, so as to reduce the number of human errors due to a manual and suboptimal configuration of security services. Moreover, the agility that an automated tool would require can be provided by the most recent networking technologies, Network Functions Virtualization and Software-Defined Networking, which move the network management from the hardware level to the software. However, even though a Security Automation approach is nowadays feasible and would bring several benefits in facing cybersecurity attacks, pending problems are that currently only a limited number of automatic management tools have been developed and that they do not have a direct integration with cloud orchestrators, consequently requiring human interaction. Given these considerations, in this paper we propose a novel framework, whose goal is to automatically and optimally allocate and conFigure security functions in a virtualized network service in a formal and verified way, directly integrated in cloud orchestrators. We validated this contribution through an implementation that is able to cooperate with two well-known orchestrators, that are Open Baton and Kubernetes. © 2019 IEEE.

@Article{2019TNEN,
  author    = {Cataldo Basile and Fulvio Valenza and Antonio Lioy and Diego R. L{\'{o}}pez and Antonio Pastor Perales},
  doi       = {10.1109/TNET.2019.2895278},
  journal   = {{IEEE/ACM} Transactions on Networking},
  number    = {2},
  pages     = {707--720},
  title     = {Adding Support for Automatic Enforcement of Security Policies in {NFV} Networks},
  volume    = {27},
  year      = {2019},
abstract={This paper introduces an approach toward the automatic enforcement of security policies in network functions virtualization (NFV) networks and dynamic adaptation to network changes. The approach relies on a refinement model that allows the dynamic transformation of high-level security requirements into configuration settings for the network security functions (NSFs), and optimization models that allow the optimal selection of the NSFs to use. These models are built on a formalization of the NSF capabilities, which serves to unequivocally describe what NSFs are able to do for security policy enforcement purposes. The approach proposed is the first step toward a security policy aware NFV management, orchestration, and resource allocation system - a paradigm shift for the management of virtualized networks - and it requires minor changes to the current NFV architecture. We prove that our approach is feasible, as it has been implemented by extending the OpenMANO framework and validated on several network scenarios. Furthermore, we prove with performance tests that policy refinement scales well enough to support current and future virtualized networks. © 1993-2012 IEEE.},
keywords={Policy Refinement, Security Automation},
  url       = {https://iris.polito.it/retrieve/handle/11583/2724445/231759/IEEE_ACM_10.1109_TNET.2019.2895278_preprint.pdf},
}

This paper introduces an approach toward the automatic enforcement of security policies in network functions virtualization (NFV) networks and dynamic adaptation to network changes. The approach relies on a refinement model that allows the dynamic transformation of high-level security requirements into configuration settings for the network security functions (NSFs), and optimization models that allow the optimal selection of the NSFs to use. These models are built on a formalization of the NSF capabilities, which serves to unequivocally describe what NSFs are able to do for security policy enforcement purposes. The approach proposed is the first step toward a security policy aware NFV management, orchestration, and resource allocation system - a paradigm shift for the management of virtualized networks - and it requires minor changes to the current NFV architecture. We prove that our approach is feasible, as it has been implemented by extending the OpenMANO framework and validated on several network scenarios. Furthermore, we prove with performance tests that policy refinement scales well enough to support current and future virtualized networks. © 1993-2012 IEEE.

@Article{2018JISIS,
  author    = {Fulvio Valenza and Antonio Lioy},
  doi       = {10.22667/JISIS.2018.05.31.033},
  journal   = {J. of Internet Services and Information Security (JISIS)},
  number    = {2},
  pages     = {33--47},
  title     = {User-oriented Network Security Policy Specification},
  volume    = {8},
  year      = {2018},
  abstract={The configuration and management of security controls and applications is complex and not well
understood by the majority of end-users (i.e. it typically requires specific skills). The security policy
language simplifies this task and reduces the number of errors and anomalies. This paper proposes the
specification of the two mechanisms for defining user’s security policies, namely High-level Security
Policy Language (HSPL) and Medium-level Security Policy Language (MSPL). HSPL is suitable for
expressing the protection requirements of typical non-technical users, while MSPL is a lower-level
abstraction useful for expressing specific configurations of security controls in a generic format (as
such it is more appealing for technical users).© 2018, Innovative Information Science and Technology Research Group.},
    keywords={Policy Refinement, Security Automation},
  url = {https://iris.polito.it/retrieve/e384c430-ba6d-d4b2-e053-9f05fe0a1d67/jisis-2018-vol8-no2-03.pdf}
}

The configuration and management of security controls and applications is complex and not well understood by the majority of end-users (i.e. it typically requires specific skills). The security policy language simplifies this task and reduces the number of errors and anomalies. This paper proposes the specification of the two mechanisms for defining user’s security policies, namely High-level Security Policy Language (HSPL) and Medium-level Security Policy Language (MSPL). HSPL is suitable for expressing the protection requirements of typical non-technical users, while MSPL is a lower-level abstraction useful for expressing specific configurations of security controls in a generic format (as such it is more appealing for technical users).© 2018, Innovative Information Science and Technology Research Group.

@Article{2018JOWUA,
  author    = {Alessio Viticchi{\'{e}} and Cataldo Basile and Fulvio Valenza and Antonio Lioy},
  doi       = {10.22667/JOWUA.2018.06.30.001},
  journal   = {J. Wirel. Mob. Networks Ubiquitous Comput. Dependable Appl.},
  number    = {2},
  pages     = {1--25},
  title     = {On the impossibility of effectively using likely-invariants for software attestation purposes},
  volume    = {9},
  year      = {2018},
  abstract={Invariants monitoring is a software attestation technique that aims at proving the integrity of a run-ning application by checking likely-invariants, which are statistically significant predicates inferred on variables’ values. Being very promising, according to the software protection literature, we de-veloped a technique to remotely monitor invariants. This paper presents the analysis we performed to assess the effectiveness of our technique and the effectiveness of likely-invariants for software attestation purposes. Moreover, it illustrates the identified limitations and our attempts to improve the detection abilities of this technique. Our results suggest that, although further studies and future results might increase its effectiveness and reduce the side effects, software attestation based on likely-invariants is not yet ready for the real world. Software developers should be warned of these limitations, if they would be tempted by adopting this technique, and companies developing software protections should not invest in development without investing in further research too. © 2018, Innovative Information Science and Technology Research Group.},
    keywords={Remote Attestation},
  url = {https://iris.polito.it/retrieve/handle/11583/2711778/206061/2018BasileInvariants.pdf}
}

Invariants monitoring is a software attestation technique that aims at proving the integrity of a run-ning application by checking likely-invariants, which are statistically significant predicates inferred on variables’ values. Being very promising, according to the software protection literature, we de-veloped a technique to remotely monitor invariants. This paper presents the analysis we performed to assess the effectiveness of our technique and the effectiveness of likely-invariants for software attestation purposes. Moreover, it illustrates the identified limitations and our attempts to improve the detection abilities of this technique. Our results suggest that, although further studies and future results might increase its effectiveness and reduce the side effects, software attestation based on likely-invariants is not yet ready for the real world. Software developers should be warned of these limitations, if they would be tempted by adopting this technique, and companies developing software protections should not invest in development without investing in further research too. © 2018, Innovative Information Science and Technology Research Group.

@InProceedings{2018WFCS,
  author    = {Manuel Cheminod and Luca Durante and Fulvio Valenza and Adriano Valenzano},
  booktitle = {14th {IEEE} International Workshop on Factory Communication Systems, {WFCS} 2018, Imperia, Italy, June 13-15, 2018},
  doi       = {10.1109/WFCS.2018.8402339},
  pages     = {1--9},
  publisher = {{IEEE}},
  title     = {Toward attribute-based access control policy in industrial networked systems},
  year      = {2018},
  abstract={The definition of a correct Access Control Policy is a fundamental step in the design of a secure information system. However, the complexity of modern systems makes critical the choice upon which model to use for such definition. This is becoming particularly true for Industrial Networked Systems, where a correct access control policy must cover all the different and ever evolving interactions between all of its heterogeneous sub-systems at different levels of the production process. In this paper, with the support of an example of a typical industrial system, we highlight the limitations of the well known and widely used Role Based Access Control policy model and we propose an alternative model, built on the ideas of the Attribute Based Access Control model, showing how it can be leveraged to easily define complex access control policies in Industrial Networked Systems. We provide also a preliminary analysis on the kind of conflicts or anomalies that such expressive model can introduce. © 2018 IEEE.},
      keywords={Access Control Policy},
  url = {https://iris.polito.it/retrieve/handle/11583/2724583/356835/2018WFCS_author.pdf}
}

The definition of a correct Access Control Policy is a fundamental step in the design of a secure information system. However, the complexity of modern systems makes critical the choice upon which model to use for such definition. This is becoming particularly true for Industrial Networked Systems, where a correct access control policy must cover all the different and ever evolving interactions between all of its heterogeneous sub-systems at different levels of the production process. In this paper, with the support of an example of a typical industrial system, we highlight the limitations of the well known and widely used Role Based Access Control policy model and we propose an alternative model, built on the ideas of the Attribute Based Access Control model, showing how it can be leveraged to easily define complex access control policies in Industrial Networked Systems. We provide also a preliminary analysis on the kind of conflicts or anomalies that such expressive model can introduce. © 2018 IEEE.

@Article{2017JOUWA,
  author    = {Fulvio Valenza and Tao Su and Serena Spinoso and Antonio Lioy and Riccardo Sisto and Marco Vallini},
  doi       = {10.22667/JOWUA.2017.03.31.079},
  journal   = {J. Wirel. Mob. Networks Ubiquitous Comput. Dependable Appl.},
  number    = {1},
  pages     = {79--100},
  title     = {A formal approach for network security policy validation},
  volume    = {8},
  year      = {2017},
  doi={10.22667/JOWUA.2017.03.31.079},
  abstract={Network security is a crucial aspect for administrators due to increasing network size and number of functions and controls (e.g. firewall, DPI, parental control). Errors in configuring security controls may result in serious security breaches and vulnerabilities (e.g. blocking legitimate traffic or permitting unwanted traffic) that must be absolutely detected and addressed. This work proposes a novel approach for validating network policy enforcement, by checking the network status and configuration, and detection of the possible causes in case of misconfiguration or software attacks. Our contribution exploits formal methods to model and validate the packet processing and forwarding behaviour of security controls, and to validate the trustworthiness of the controls by using remote attestation. A prototype implementation of this approach is proposed to validate different scenarios. © 2017, Innovative Information Science and Technology Research Group},
  keywords={Policy Analysis, Policy Verification, Remote Attestation},
  url       = {https://iris.polito.it/retrieve/handle/11583/2659302/284666/2017JOWUA.pdf},
}

Network security is a crucial aspect for administrators due to increasing network size and number of functions and controls (e.g. firewall, DPI, parental control). Errors in configuring security controls may result in serious security breaches and vulnerabilities (e.g. blocking legitimate traffic or permitting unwanted traffic) that must be absolutely detected and addressed. This work proposes a novel approach for validating network policy enforcement, by checking the network status and configuration, and detection of the possible causes in case of misconfiguration or software attacks. Our contribution exploits formal methods to model and validate the packet processing and forwarding behaviour of security controls, and to validate the trustworthiness of the controls by using remote attestation. A prototype implementation of this approach is proposed to validate different scenarios. © 2017, Innovative Information Science and Technology Research Group

@InProceedings{2017WFCS_ACP,
  author    = {Manuel Cheminod and Luca Durante and Lucia Seno and Fulvio Valenza and Adriano Valenzano},
  booktitle = {Proceedings of the 13th {IEEE} International Workshop on Factory Communication Systems ({WFCS} 2017)},
  doi       = {10.1109/WFCS.2017.7991947},
  pages     = {1--9},
  publisher = {{IEEE}},
  title     = {Automated fixing of access policy implementation in Industrial Networked Systems},
  year      = {2017},
  doi={10.1109/WFCS.2017.7991947},
abstract={Access control (AC) is the core of every architectural solution for information security. Indeed, no effective protection scheme can abstract from the careful design of access control policies, and infrastructures underlying modern Industrial Networked Systems (INSs) are not exceptions from this point of view. This paper presents a comprehensive framework for INS access control. The proposed approach enables the description of both positive and negative AC policies, by applying the Role Based Access Control (RBAC) paradigm to typical INS implementations, while taking into account different levels of abstraction. Suitable techniques are adopted to check whether or not policies are correctly implemented in the system (verification). When conflicts are detected, possible (re)assignments of credentials to the system users are automatically computed, that can be adopted to correct anomalies (conflict resolution). © 2017 IEEE.},
 keywords={Access Control Policy, Industrial Networked Systems},
 url       = {https://iris.polito.it/retrieve/handle/11583/2672412/426664/2017WFCS_ACP_author.pdf},
}

Access control (AC) is the core of every architectural solution for information security. Indeed, no effective protection scheme can abstract from the careful design of access control policies, and infrastructures underlying modern Industrial Networked Systems (INSs) are not exceptions from this point of view. This paper presents a comprehensive framework for INS access control. The proposed approach enables the description of both positive and negative AC policies, by applying the Role Based Access Control (RBAC) paradigm to typical INS implementations, while taking into account different levels of abstraction. Suitable techniques are adopted to check whether or not policies are correctly implemented in the system (verification). When conflicts are detected, possible (re)assignments of credentials to the system users are automatically computed, that can be adopted to correct anomalies (conflict resolution). © 2017 IEEE.

@InProceedings{2017WFCS_SDN,
  author    = {Manuel Cheminod and Luca Durante and Lucia Seno and Fulvio Valenza and Adriano Valenzano and Claudio Zunino},
  booktitle = {Proceedings of the 13th {IEEE} International Workshop on Factory Communication Systems ({WFCS} 2017)},
  doi       = {10.1109/WFCS.2017.7991960},
  pages     = {1--7},
  publisher = {{IEEE}},
  title     = {Leveraging {SDN} to improve security in industrial networks},
  year      = {2017},
  abstract={In recent years, several important initiatives have appeared worldwide, aimed at bringing significant innovation in industrial networked systems (INSs). As an example, the Industry 4.0 and Factory of the Future frameworks are paving the way to modern intelligent factories, where issues such as the communication complexity between smart devices and system on-the-fly reconfiguration are dealt with in efficient and cost-effective manner. However, global connectivity also implies constant increase of cyber threats targeting industrial systems, so security must be considered since the very beginning when new appealing solutions need to be conceived. In this paper, we exploit the innovative Software Defined Networking (SDN) paradigm to introduce improvements in managing the network infrastructure of INSs, as this can help in reducing the management costs and complexity. In particular, enhanced SDN functionalities are adopted, which are able to provide security support in additions to their native switching/routing functionalities. The paper also shows how this approach can overcome some limitations of many current INS security architectures. The feasibility of the proposed solution is confirmed by the development of a simple laboratory prototype based on commodity hardware, and used to obtain some preliminary evaluation of the achievable functionality and performance benefits. © 2017 IEEE.},
   keywords={Industrial Networked Systems},
 url       = {https://iris.polito.it/retrieve/handle/11583/2673926/426677/2017WFCS_SDN_author.pdf},

}

In recent years, several important initiatives have appeared worldwide, aimed at bringing significant innovation in industrial networked systems (INSs). As an example, the Industry 4.0 and Factory of the Future frameworks are paving the way to modern intelligent factories, where issues such as the communication complexity between smart devices and system on-the-fly reconfiguration are dealt with in efficient and cost-effective manner. However, global connectivity also implies constant increase of cyber threats targeting industrial systems, so security must be considered since the very beginning when new appealing solutions need to be conceived. In this paper, we exploit the innovative Software Defined Networking (SDN) paradigm to introduce improvements in managing the network infrastructure of INSs, as this can help in reducing the management costs and complexity. In particular, enhanced SDN functionalities are adopted, which are able to provide security support in additions to their native switching/routing functionalities. The paper also shows how this approach can overcome some limitations of many current INS security architectures. The feasibility of the proposed solution is confirmed by the development of a simple laboratory prototype based on commodity hardware, and used to obtain some preliminary evaluation of the achievable functionality and performance benefits. © 2017 IEEE.

@InProceedings{2017NetSoft,
  author    = {Luca Durante and Lucia Seno and Fulvio Valenza and Adriano Valenzano},
  booktitle = {Proceedings of the {IEEE} Conference on Network Softwarization (NetSoft 2017)},
  doi       = {10.1109/NETSOFT.2017.8004230},
  pages     = {1--6},
  publisher = {{IEEE}},
  title     = {A model for the analysis of security policies in service function chains},
  year      = {2017},
abstract={Two emerging architectural paradigms, i.e., Software Defined Networking (SDN) and Network Function Virtualization (NFV), enable the deployment and management of Service Function Chains (SFCs). A SFC is an ordered sequence of abstract Service Functions (SFs), e.g., firewalls, VPN-gateways, traffic monitors, that packets have to traverse in the route from source to destination. While this appealing solution offers significant advantages in terms of flexibility, it also introduces new challenges such as the correct configuration and ordering of SFs in the chain to satisfy overall security requirements. This paper presents a formal model conceived to enable the verification of correct policy enforcements in SFCs. Software tools based on the model can then be designed to cope with unwanted network behaviors (e.g., security flaws) deriving from incorrect interactions of SFs in the same SFC. © 2017 IEEE.},
   keywords={Policy Verification, Security Function Modeling},
 url       = {https://iris.polito.it/retrieve/handle/11583/2677064/426685/2017SNS_author.pdf},
}

Two emerging architectural paradigms, i.e., Software Defined Networking (SDN) and Network Function Virtualization (NFV), enable the deployment and management of Service Function Chains (SFCs). A SFC is an ordered sequence of abstract Service Functions (SFs), e.g., firewalls, VPN-gateways, traffic monitors, that packets have to traverse in the route from source to destination. While this appealing solution offers significant advantages in terms of flexibility, it also introduces new challenges such as the correct configuration and ordering of SFs in the chain to satisfy overall security requirements. This paper presents a formal model conceived to enable the verification of correct policy enforcements in SFCs. Software tools based on the model can then be designed to cope with unwanted network behaviors (e.g., security flaws) deriving from incorrect interactions of SFs in the same SFC. © 2017 IEEE.

@Article{2017TNET,
  author    = {Fulvio Valenza and Cataldo Basile and Daniele Canavese and Antonio Lioy},
  doi       = {10.1109/TNET.2017.2708096},
  journal   = {{IEEE/ACM} Transactions on Networking},
  number    = {5},
  pages     = {2601--2614},
  title     = {Classification and Analysis of Communication Protection Policy Anomalies},
  volume    = {25},
  year      = {2017},
  abstract={This paper presents a classification of the anomalies that can appear when designing or implementing communication protection policies. Together with the already known intra- and inter-policy anomaly types, we introduce a novel category, the inter-technology anomalies, related to security controls implementing different technologies, both within the same network node and among different network nodes. Through an empirical assessment, we prove the practical significance of detecting this new anomaly class. Furthermore, this paper introduces a formal model, based on first-order logic rules that analyses the network topology and the security controls at each node to identify the detected anomalies and suggest the strategies to resolve them. This formal model has manageable computational complexity and its implementation has shown excellent performance and good scalability. © 2017 IEEE.},
  keywords={VPN,  Policy Analysis},
  url       = {https://iris.polito.it/retrieve/handle/11583/2673838/426540/2017TNET_author.pdf},
 }

 
 

This paper presents a classification of the anomalies that can appear when designing or implementing communication protection policies. Together with the already known intra- and inter-policy anomaly types, we introduce a novel category, the inter-technology anomalies, related to security controls implementing different technologies, both within the same network node and among different network nodes. Through an empirical assessment, we prove the practical significance of detecting this new anomaly class. Furthermore, this paper introduces a formal model, based on first-order logic rules that analyses the network topology and the security controls at each node to identify the detected anomalies and suggest the strategies to resolve them. This formal model has manageable computational complexity and its implementation has shown excellent performance and good scalability. © 2017 IEEE.

@Article{2017CAEE,
  author    = {Cataldo Basile and Daniele Canavese and Christian Pitscheider and Antonio Lioy and Fulvio Valenza},
  doi       = {10.1016/j.compeleceng.2017.02.019},
  journal   = {Computers and Electrical Engineering},
  pages     = {110--131},
  title     = {Assessing network authorization policies via reachability analysis},
  volume    = {64},
  year      = {2017},
  abstract={Evaluating if a computer network only permits allowed business operations without transmitting unwanted or malicious traffic is a crucial security task. Reachability analysis – the process that evaluates allowed communications – is a tool useful not only to discover security issues but also to identify network misconfigurations. This paper presents a novel approach to quantify network reachability based on the concept of equivalent firewall – a fictitious device, ideally connected directly to the communicating peers and whose policy summarizes the network behaviour between them – that can be queried to derive reachability information. We build equivalent firewalls by using a mathematical model that supports a large variety of network security controls (like NAT, NAPT, tunnels and filters up to the application layer) and allows an accurate analysis. The presented approach is efficient and highly scalable, as confirmed by tests with a large corporate network as well as synthetic networks. © 2017 Elsevier Ltd},
  keywords={Policy Verification, Reachability Verification},
  url = {https://iris.polito.it/retrieve/handle/11583/2671778/426546/2017CAEE_author.pdf}
}

Evaluating if a computer network only permits allowed business operations without transmitting unwanted or malicious traffic is a crucial security task. Reachability analysis – the process that evaluates allowed communications – is a tool useful not only to discover security issues but also to identify network misconfigurations. This paper presents a novel approach to quantify network reachability based on the concept of equivalent firewall – a fictitious device, ideally connected directly to the communicating peers and whose policy summarizes the network behaviour between them – that can be queried to derive reachability information. We build equivalent firewalls by using a mathematical model that supports a large variety of network security controls (like NAT, NAPT, tunnels and filters up to the application layer) and allows an accurate analysis. The presented approach is efficient and highly scalable, as confirmed by tests with a large corporate network as well as synthetic networks. © 2017 Elsevier Ltd

@Article{2016IJNM,
  author    = {Cataldo Basile and Daniele Canavese and Antonio Lioy and Christian Pitscheider and Fulvio Valenza},
  doi       = {10.1002/nem.1917},
  journal   = {International Journal of Network Management},
  number    = {1},
  pages     = {25--43},
  title     = {Inter-function anomaly analysis for correct {SDN/NFV} deployment},
  volume    = {26},
  year      = {2016},
  abstract={Implementing the security of a network consists in individually configuring several network functions. Network functions are configured by means of a policy composed of a set of rules, but their actual behaviour is influenced by the other policies implemented by all the other network functions around them. This paper proposes a formal model that can be used to detect inter-function anomalies, which are defined as the interferences between two or more functions deployed in the same network. We have proved with experiments that the proposed model is fast and scalable. Copyright © 2015 John Wiley & Sons, Ltd.},
  keywords={Policy Analysis},
  url       = {https://iris.polito.it/retrieve/handle/11583/2623293/426336/2016IJNM_author.pdf},
}

Implementing the security of a network consists in individually configuring several network functions. Network functions are configured by means of a policy composed of a set of rules, but their actual behaviour is influenced by the other policies implemented by all the other network functions around them. This paper proposes a formal model that can be used to detect inter-function anomalies, which are defined as the interferences between two or more functions deployed in the same network. We have proved with experiments that the proposed model is fast and scalable. Copyright © 2015 John Wiley & Sons, Ltd.

@InProceedings{2016MIST@CCS,
  author    = {Fulvio Valenza and Marco Vallini and Antonio Lioy},
  booktitle = {Proceedings of the 8th {ACM} {CCS} International Workshop on Managing Insider Security Threats (MIST@CCS 2016)},
  pages     = {101--104},
  publisher = {{ACM}},
  doi={10.1145/2995959.2995970},
  title     = {Online and Offline Security Policy Assessment},
  year      = {2016},
  abstract={Network architectures and applications are becoming increasingly complex. Several approaches to automatically enforce configurations on devices, applications and services have been proposed, such as Policy-Based Network Management (PBNM). However, the management of enforced configurations in production environments (e.g. data center) is a crucial and complex task. For example, updates on firewall configuration to change a set of rules. Although this task is fundamental for complex systems, few effective solutions have been proposed for monitoring and managing enforced configurations. This work proposes a novel approach to monitor and manage enforced configurations in production environments. The main contributions of this paper are a formal model to identify/generate traffic flows and to verify the enforced configurations; and a slim and transparent framework to perform the policy assessment. We have implemented and validated our approach in a virtual environment in order to evaluate different scenarios. The results demonstrate that the prototype is effective and has good performance, therefore our model can be effectively used to analyse several types of IT infrastructures. A further interesting result is that our approach is complementary to PBNM.  © 2016 ACM.},
  keywords={Policy Verification},
  url       = {https://iris.polito.it/retrieve/handle/11583/2650400/426703/2016MIST_author.pdf},

}

Network architectures and applications are becoming increasingly complex. Several approaches to automatically enforce configurations on devices, applications and services have been proposed, such as Policy-Based Network Management (PBNM). However, the management of enforced configurations in production environments (e.g. data center) is a crucial and complex task. For example, updates on firewall configuration to change a set of rules. Although this task is fundamental for complex systems, few effective solutions have been proposed for monitoring and managing enforced configurations. This work proposes a novel approach to monitor and manage enforced configurations in production environments. The main contributions of this paper are a formal model to identify/generate traffic flows and to verify the enforced configurations; and a slim and transparent framework to perform the policy assessment. We have implemented and validated our approach in a virtual environment in order to evaluate different scenarios. The results demonstrate that the prototype is effective and has good performance, therefore our model can be effectively used to analyse several types of IT infrastructures. A further interesting result is that our approach is complementary to PBNM. © 2016 ACM.

@InProceedings{2015CSP,
  author    = {Cataldo Basile and Christian Pitscheider and Fulvio Risso and Fulvio Valenza and Marco Vallini},
  editor    = {Frances Cleary and Massimo Felici},
  pages     = {65--76},
  publisher = {Springer},
  title     = {Towards the Dynamic Provision of Virtualized Security Services},
  year      = {2015},
  series    = {Communications in Computer and Information Science},
  volume    = {530},
  abstract  = {Network operators face several limitations in terms of infrastructure management and costs when trying to offer security services to a large number of customers with current technologies. Network Functions Virtualization and Software-Defined Networks paradigms try to overcome these limitations by allowing more flexibility, configurability and agility. Unfortunately, the problem of deciding which security services to use, where to place and how to configure them is a multidimensional problem that has no easy solution. This paper provides a model that can be used to determine the best allocation for the security applications needed to satisfy the user requirements while minimizing the cost for the network operator, subject to the different constraints expressed by the involved actors. This model can be exploited to pursue an initial dimensioning and set-up of the system infrastructure or to dynamically adapt it to support the user security policies. Initial validation shows that allocations generated with our model have considerable advantages in terms of costs and performance compared to traditional approaches. © Springer International Publishing Switzerland 2015.},
  booktitle = {Cyber Security and Privacy - 4th Cyber Security and Privacy Innovation Forum, {CSP} Innovation Forum 2015, Brussels, Belgium, April 28-29, 2015, Revised Selected Papers},
  doi       = {10.1007/978-3-319-25360-2\_6},
  keywords  = {VNF Placement},
  url       = {https://iris.polito.it/retrieve/handle/11583/2621480/426198/2015CSP_author.pdf},
}

Network operators face several limitations in terms of infrastructure management and costs when trying to offer security services to a large number of customers with current technologies. Network Functions Virtualization and Software-Defined Networks paradigms try to overcome these limitations by allowing more flexibility, configurability and agility. Unfortunately, the problem of deciding which security services to use, where to place and how to configure them is a multidimensional problem that has no easy solution. This paper provides a model that can be used to determine the best allocation for the security applications needed to satisfy the user requirements while minimizing the cost for the network operator, subject to the different constraints expressed by the involved actors. This model can be exploited to pursue an initial dimensioning and set-up of the system infrastructure or to dynamically adapt it to support the user security policies. Initial validation shows that allocations generated with our model have considerable advantages in terms of costs and performance compared to traditional approaches. © Springer International Publishing Switzerland 2015.

@InProceedings{2015NetSoft,
  author    = {Cataldo Basile and Antonio Lioy and Christian Pitscheider and Fulvio Valenza and Marco Vallini},
  booktitle = {Proceedings of the 1st {IEEE} Conference on Network Softwarization (NetSoft 2015)},
  doi       = {10.1109/NETSOFT.2015.7116152},
  pages     = {1--5},
  publisher = {{IEEE}},
  title     = {A novel approach for integrating security policy enforcement with dynamic network virtualization},
  year      = {2015},
  abstract={Network function virtualization (NFV) is a new networking paradigm that virtualizes single network functions. NFV introduces several advantages compared to classical approaches, such as the dynamic provisioning of functionality or the implementation of scalable and reliable services (e.g., adding a new instance to support demands). NFV also allows the deployment of security controls, like firewalls or VPN gateways, as virtualized network functions. However, currently there is not an automatic way to select the security functions to enable and to configure the selected ones according to a set of user's security requirements. This paper presents a first approach towards the integration of network and security policy management into the NFV framework. By adding to the NFV architecture a new software component, the Policy Manager, we provide NFV with an easy and effective way for users to specify their security requirements and a process that hides all the details of the correct deployment and configuration of security functions. To perform its tasks, the Policy Manager uses policy refinement techniques. © 2015 IEEE.},
   keywords  = {Policy Refinement, Security Automation},
   url       = {https://iris.polito.it/retrieve/handle/11583/2592157/426647/2015Netsoft_author.pdf},
}

Network function virtualization (NFV) is a new networking paradigm that virtualizes single network functions. NFV introduces several advantages compared to classical approaches, such as the dynamic provisioning of functionality or the implementation of scalable and reliable services (e.g., adding a new instance to support demands). NFV also allows the deployment of security controls, like firewalls or VPN gateways, as virtualized network functions. However, currently there is not an automatic way to select the security functions to enable and to configure the selected ones according to a set of user's security requirements. This paper presents a first approach towards the integration of network and security policy management into the NFV framework. By adding to the NFV architecture a new software component, the Policy Manager, we provide NFV with an easy and effective way for users to specify their security requirements and a process that hides all the details of the correct deployment and configuration of security functions. To perform its tasks, the Policy Manager uses policy refinement techniques. © 2015 IEEE.

@InProceedings{2015SPRO,
  author    = {Cataldo Basile and Daniele Canavese and J{\'{e}}r{\^{o}}me d'Annoville and Bjorn De Sutter and Fulvio Valenza},
  booktitle = {Proceedings of the 1st {IEEE/ACM} International Workshop on Software Protection ({SPRO} 2015)},
  doi       = {10.1109/SPRO.2015.17},
  pages     = {52--58},
  publisher = {{IEEE}},
  title     = {Automatic Discovery of Software Attacks via Backward Reasoning},
  year      = {2015},
 abstract={Security risk management and mitigation are two of the most important items on several companies' agendas. In this scenario, software attacks pose a major threat to the reliable execution of services, thus bringing negative effects on businesses. This paper presents a formal model that allows the identification of all the attacks against the assets embedded in a software application. Our approach can be used to perform the identification of the threats that loom over the assets and help to determine the potential countermeasures, that is the protections to deploy for mitigating the risks. The proposed model uses a Knowledge Base to represent the software assets, the steps that can be executed to mount an attack and their relationships. Inference rules permit the automatic discovery of attack step combinations towards the compromised assets that are discovered using a backward programming methodology. This approach is very usable as the attack discovery is fully automatic, once the Knowledge Base is populated with the information regarding the application to protect. In addition, it has been proven highly efficient and exhaustive. © 2015 IEEE.},
 keywords={Threat Analysis},
   url       = {https://iris.polito.it/retrieve/handle/11583/2615485/426236/2015SPRO_author.pdf},
}

Security risk management and mitigation are two of the most important items on several companies' agendas. In this scenario, software attacks pose a major threat to the reliable execution of services, thus bringing negative effects on businesses. This paper presents a formal model that allows the identification of all the attacks against the assets embedded in a software application. Our approach can be used to perform the identification of the threats that loom over the assets and help to determine the potential countermeasures, that is the protections to deploy for mitigating the risks. The proposed model uses a Knowledge Base to represent the software assets, the steps that can be executed to mount an attack and their relationships. Inference rules permit the automatic discovery of attack step combinations towards the compromised assets that are discovered using a backward programming methodology. This approach is very usable as the attack discovery is fully automatic, once the Knowledge Base is populated with the information regarding the application to protect. In addition, it has been proven highly efficient and exhaustive. © 2015 IEEE.

@InProceedings{2015RTSI,
  author    = {Valenza, F. and Spinoso, S. and Basile, C. and Sisto, R. and Lioy, A.},
  booktitle = {Proceedings of the 1st {IEEE} International Forum on Research and Technologies for Society and Industry (RTSI 2015)},
  doi       = {10.1109/RTSI.2015.7325150},
  pages     = {516-522},
  title     = {A formal model of network policy analysis},
  year      = {2015},
  abstract  = {The complexity of network topology together with heterogeneity of network services make the network configuration a hard task, even for skilled and experienced administrators. In order to reduce the complexity of the network configuration, administrators have leveraged network policies, introducing hence new possibility of error. Indeed, erroneous and unexpected network behaviour (e.g., security flaws) can derive from the wrong network policy definition, but also from the possible anomalies among policies of different domains. This paper presents a formal model for detecting inter-and intra-domain policy anomalies. Policy anomalies allow administrators to identify all the network behaviours they consider erroneous or to be monitored. To validate the generality of the proposed solution, the model has been applied to three policy domains (packet filtering, communication protection and service function chaining) and the impact of an anomaly detection analysis was tested in different sized networks. © 2015 IEEE.},
  keywords  = {Policy Analysis},
  url       = {https://iris.polito.it/retrieve/handle/11583/2621143/426656/2015RTSI_author.pdf},
}

The complexity of network topology together with heterogeneity of network services make the network configuration a hard task, even for skilled and experienced administrators. In order to reduce the complexity of the network configuration, administrators have leveraged network policies, introducing hence new possibility of error. Indeed, erroneous and unexpected network behaviour (e.g., security flaws) can derive from the wrong network policy definition, but also from the possible anomalies among policies of different domains. This paper presents a formal model for detecting inter-and intra-domain policy anomalies. Policy anomalies allow administrators to identify all the network behaviours they consider erroneous or to be monitored. To validate the generality of the proposed solution, the model has been applied to three policy domains (packet filtering, communication protection and service function chaining) and the impact of an anomaly detection analysis was tested in different sized networks. © 2015 IEEE.

@InProceedings{2015Crisis,
  author    = {Cataldo Basile and Daniele Canavese and Antonio Lioy and Fulvio Valenza},
  booktitle = {Proceedings of the 9th International Conference of Risks and Security of Internet and Systems (CRiSIS 2014)},
  doi       = {10.1007/978-3-319-17127-2\_10},
  pages     = {148--163},
  publisher = {Springer,},
  title     = {Inter-technology Conflict Analysis for Communication Protection Policies},
  year      = {2014},
  abstract  = {Usually network administrators implement a protection policy by refining a set of (abstract) communication security requirements into configuration settings for the security controls that will provide the required protection. The refinement consists in evaluating the available technologies that can enforce the policy at node and network level, selecting the most suitable ones, and possibly making fine adjustments, like aggregating several individual channels into a single tunnel. The refinement process is a sensitive task which can lead to incorrect or suboptimal implementations, that in turn affect the overall security, decrease the network throughput and increase the maintenance costs. In literature, several techniques exist that can be used to identify anomalies (i.e. potential incompatibilities and redundancies among policy implementations. However, these techniques usually focus only on a single security technology (e.g. IPsec) and overlook the effects of multiple overlapping protection techniques. This paper presents a novel classification of communication protection policy anomalies and a formal model which is able to detect anomalies among policy implementations relying on technologies that work at different network layers. The result of our analysis allows administrators to have a precise insight on the various alternative implementations, their relations and the possibility of resolving anomalies, thus increasing the overall security and performance of a network. © Springer International Publishing Switzerland 2015.},
  keywords  = {VPN, Policy Analysis},
  url       = {https://iris.polito.it/retrieve/handle/11583/2573139/426176/2015CRISIS_author.pdf},
}

Usually network administrators implement a protection policy by refining a set of (abstract) communication security requirements into configuration settings for the security controls that will provide the required protection. The refinement consists in evaluating the available technologies that can enforce the policy at node and network level, selecting the most suitable ones, and possibly making fine adjustments, like aggregating several individual channels into a single tunnel. The refinement process is a sensitive task which can lead to incorrect or suboptimal implementations, that in turn affect the overall security, decrease the network throughput and increase the maintenance costs. In literature, several techniques exist that can be used to identify anomalies (i.e. potential incompatibilities and redundancies among policy implementations. However, these techniques usually focus only on a single security technology (e.g. IPsec) and overlook the effects of multiple overlapping protection techniques. This paper presents a novel classification of communication protection policy anomalies and a formal model which is able to detect anomalies among policy implementations relying on technologies that work at different network layers. The result of our analysis allows administrators to have a precise insight on the various alternative implementations, their relations and the possibility of resolving anomalies, thus increasing the overall security and performance of a network. © Springer International Publishing Switzerland 2015.