Automating Security Configuration �in Virtualized Computer Networks

1

Daniele Bringhenti

XXXV PhD Cycle – 3^rd Year Student

​

​

Advisors: Prof. Riccardo Sisto, Dott. Fulvio Valenza

​

August 29, 2022 – FOSAD PhD Forum

Security Management in Virtualized Networks�

​

In virtualized networks, security management has become a daunting task because of:

• Dimension of the networks;
• Parallelism of the software processes;
• Complexity (e.g., stateful middleboxes).

​

​

​

​

​

​

​

2

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

Achieving a correct configuration for

virtual Network Security Functions (NSFs) is complex.

Security Misconfiguration

3

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

82% of breaches involved the human errors for

security configuration in 2021.

:

Introducing Automation

Automation can help avoid security misconfiguration:

• exploit the agility of network virtualization
• avoid manual trial-and-error configuration
• produce better results

​

​

​

​

4

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

Manual configuration is error-prone, unoptimized, time consuming.

Main problem:

Security Automation Proposal

My proposal is to pursue a Security Automation approach for the orchestration and configuration of NSFs in virtualized networks:

• automatic definition of the optimal allocation scheme for NSFs;
• automatic generation of the optimal configuration of the allocated NSFs.

​

​

5

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

Automation

Formal Verification

Optimization

Network Security

Related Work

In the literature, other works do not guarantee all these three features at the same time:

• most of the methodologies automatically compute NSFs configurations without considering optimization and formal verification [1][2];

​

• some methodologies formally verify NSFs configurations, but they cannot automatically generate those configurations [3][4];

​

• other methodologies define the NSFs allocation scheme, without generating the rule set for their configuration [5][6].

6

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

VEREFOO

7

VErified REFinement and Optimized Orchestration

Automation

Formal Verification

Optimization

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

VEREFOO Approach

8

Input

Output

Virtual Network Topology

NSFs allocation scheme

Network Security Policies

NSFs configurations

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

Formal Verification in VEREFOO

9

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

VErified REFinement and Optimized Orchestration

MaxSMT Problem Formulation�

Partial weighted MaxSMT: an optimization-enhanced version of the Satisfiability Modulo Theories (SMT) problem.

• Partial: there are hard constraints that must be always satisfied and soft constraints that should be satisfied as far as possible.
• Weighted: find an assignment of the Boolean variables that maximizes the total weight of the satisfied soft clauses.

​

10

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

Network Formal Models

• The virtual topology is modeled as an Allocation Graph (AG), containing Allocation Places (APs).

​

• The APs represent the possible positions where an NSF could be allocated in the logical topology.

​

• The forwarding behavior of each network function (i.e., the possibility that a received packet is forwarded) is formally modeled [7]:

​

​

​

11

11

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

Optimization in VEREFOO

12

Trade-off with performance

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

VErified REFinement and Optimized Orchestration

Optimization Objectives (I)

VEREFOO has two optimization objectives.

​

1. Minimization of the NSF allocation scheme:
• to consume less resources of the physical servers
• to save time when deploying the virtual NSFs

​

13

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

​

For each Allocation Place, a class of soft constraints is introduced:

​

The optimal allocation scheme does not have any allocated NSF – but, if a NSF is needed to enforce the NSPs, then it is allocated to satisfy the hard constraints.

• The value of the 𝑎𝑙𝑙𝑜𝑐𝑎𝑡𝑒𝑑 predicate is left open and decided by the MaxSMT solver.

​

​

​

​

Optimization Objectives (II)

2. Minimization of the NSF configuration rule set:
• to reduce the memory for storing the rules
• to speed up the decisional operations of the NSFs

​

14

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

VEREFOO Framework

Integration:

• Interfaces to virtualization and cloud orchestrators
• European projects (ASTRID, CyberSec4Europe)

​

​

15

Implementation:

• Java-based framework, with REST APIs
• z3 as MaxSMT solver

​

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

EU projects:

​

​

VEREFOO GUI

16

Virtual Network Topology

Network Security Policies

Network Configuration

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

VEREFOO GitHub Repository and Demo

Demo:

• Complete experience of VEREFOO
• Virtual environment with containers
• Refinement from NSPs to low-level configuration

(e.g., iptables, eBPF firewall, Open vSwitch)

​

​

17

GitHub Repository:

• Open-source software
• https://github.com/netgroup-polito/verefoo/tree/Budapest

​

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

VEREFOO Validation [8]

18

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

Conclusions and Future Work

Future Work:

• analyze alternative heuristic algorithms
• extend the methodology to support other NSFs (e.g., anti-spam filter, IDS)

​

​

​

19

Conclusions:

• novel methodology for a fully automated configuration of NSFs in virtualized networks
• formal verification with a correctness-by-construction approach
• optimization based on a MaxSMT formulation
• feasible until hundreds of APs and security policies

​

August 29, 2022 – FOSAD PhD Forum D. Bringhenti

Daniele Bringhenti

daniele.bringhenti@polito.it

​

VEREFOO GitHub Repository:

https://github.com/netgroup-polito/verefoo

​

VEREFOO Demo:

​

​

Thanks for your attention!

References

[1] Y. Bartal, A. Mayer, K. Nissim, and A. Wool, “Firmato: A novel firewall management toolkit,” ACM Trans. Comput. Syst., vol. 22, no. 4, pp. 381–420, Nov. 2004.

[2] P. Verma and A. Prakash, “FACE: A firewall analysis and configuration engine,” in 2005 IEEE/IPSJ International Symposium on Applications and the Internet, Trento, Italy, Feb. 2005.

[3] K. Adi, L. Hamza, and L. Pene, “Automatic security policy enforcement in computer systems,” Computers & Security, vol. 73, pp. 156–171, 2018.

[4] A. Gember-Jacobson, A. Akella, R. Mahajan, and H. H. Liu, “Automatically repairing network control planes using an abstract representation,” in Proceedings of the 26th Symposium on Operating Systems Principles, Shanghai, China, Oct. 2017.

[5] M. Yoon, S. Chen, and Z. Zhang, “Minimizing the maximum firewall rule set in a network with multiple firewalls,” IEEE Trans. Computers, vol. 59, no. 2, pp. 218–230, 2010.

[6] M. A. Rahman and E. Al-Shaer, “Automated synthesis of distributed network access controls: A formal framework with refinement,” IEEE Trans. Parallel Distrib. Syst., vol. 28, no. 2, pp. 416–430, 2017.

[7] D. Bringhenti, G. Marchetto, R. Sisto, S. Spinoso, F. Valenza and J. Yusupov, "Improving the Formal Verification of Reachability Policies in Virtualized Networks," in IEEE Transactions on Network and Service Management, vol. 18, no. 1, pp. 713-728, 2021.

[8] D. Bringhenti, G. Marchetto, R. Sisto, F. Valenza and J. Yusupov, "Automated firewall configuration in virtual networks," in IEEE Transactions on Dependable and Secure Computing, in press, 2022.

21

August 29, 2022 – FOSAD PhD Forum D. Bringhenti