From 1d9ca211a9268fd9f695a32d933e3e9e93acf1a8 Mon Sep 17 00:00:00 2001 From: DanieleBringhenti Date: Fri, 24 Mar 2023 07:57:43 +0100 Subject: [PATCH 01/11] Update README.md --- README.md | 104 +++++++++++++++++++++++++++++++++++------------------- 1 file changed, 67 insertions(+), 37 deletions(-) diff --git a/README.md b/README.md index 8a6ddce9..61a7b4af 100644 --- a/README.md +++ b/README.md @@ -1,77 +1,97 @@ -![](/resources/verefoo_icon.png) +![](./resources/verefoo_icon.png) -##### VEREFOO (VErified REFinement and Optimized Orchestrator) is a framework designed to provide an automatic way to allocate packet filters - the most common and traditional firewall technology - in a Service Graph defined by the service designer and an auto-configuration technique to create firewall rules with respect to the specified security requirements. +##### VEREFOO (VErified REFinement and Optimized Orchestrator) is a framework designed to automatically allocate and configure packet filtering firewalls in a service graph defined by the network administrator, so as to fulfill the user-specified security connectivity requirements. VEREFOO combines automation, formal verification and optimization by formulating the firewall configuration problem with constraint programming, as a Maximum Satisfiability Modulo Theories (MaxSMT) problem. -## Z3 library support +## VEREFOO Dependencies -[Download](https://github.com/Z3Prover/z3/releases) the correct version of Z3 according to your OS and your JVM endianness. The recommended Z3 version number is 4.8.8. For the correct functioning of the application, you must have the Z3 native library and include it to Java Library Path. The most convenient way to do this is add the path that the library to the dynamic linking library path. +The VEREFOO framework requires the following dependencies to correctly work: +* Java SE Development Kit 8 (https://www.oracle.com/it/java/technologies/javase/javase8-archive-downloads.html) +* Apache Tomcat 8 (https://tomcat.apache.org/download-80.cgi) +* Apache Ant 1.10 (https://ant.apache.org/bindownload.cgi) +* Apache Maven 3.6 (https://maven.apache.org/download.cgi) +* Neo4j Community 3.5.25 (https://neo4j.com/download-center/) +* Z3 4.8.8 (https://github.com/Z3Prover/z3/releases) -* In Linux is `LD_LIBRARY_PATH` -* In MacOS is `DYLD_LIBRARY_PATH` -* In Windows is `PATH` +### Z3 library support -> e.g., +Z3 is an automated solver of the MaxSMT problem defined in VEREFOO. + +[Download](https://github.com/Z3Prover/z3/releases) the correct version of Z3 according to your OS and your JVM endianness. For the correct functioning of the application, you must have the Z3 native library and include it in the Java Library Path. The most convenient way to do this is to add the library path to the dynamic linking library path, which +* in Linux is `LD_LIBRARY_PATH` +* in MacOS is `DYLD_LIBRARY_PATH` +* in Windows is `PATH` +> e.g., on Linux, > * `sudo nano /etc/environment` -> * `LD_LIBRARY_PATH = $LD_LIBRARY_PATH:/home/verefoo/z3/bin/` -> * `Z3 = /home/verefoo/z3/bin/` (also required) +> * `LD_LIBRARY_PATH = $LD_LIBRARY_PATH:/home/VEREFOO/z3/bin/` + +A new environment variable, named Z3, must be also created: +> * `Z3 = /home/VEREFOO/z3/bin/` + +## VEREFOO Installation -## Installing Verefoo via Maven (Spring Boot application with Embedded Tomcat) [Solution 1] +The VEREFOO framework can be installed in two alternative ways: +* via Maven (recommended); +* via Ant. + +### Installing VEREFOO via Maven (Spring Boot application with Embedded Tomcat) [Solution 1] * install [jdk1.8.X YY](http://www.oracle.comntechnetwork/java/javase/downloads/jdk8-downloads-2133151.html); * install [maven](https://maven.apache.org/install.html) * `mvn clean package` * `java -jar target/verifoo-0.0.1-SNAPSHOT.jar` -Swagger documentation can be accessed at [localhost:8085/verefoo](localhost:8085/verefoo). +The Swagger documentation can be accessed at [localhost:8085/VEREFOO](localhost:8085/VEREFOO). -## Installing Verefoo via Ant (Apache Tomcat required) [Solution 2] +### Installing VEREFOO via Ant (Apache Tomcat required) [Solution 2] * install [jdk1.8.X YY](http://www.oracle.comntechnetwork/java/javase/downloads/jdk8-downloads-2133151.html); * install [Apache Tomcat 8](https://tomcat.apache.org/download-80.cgi); - * set CATALINA HOME ambient variable to the directory where you installed Apache; + * set CATALINA HOME environment variable to the directory where you installed Apache Tomcat; * (optional) configure Tomcat Manager: * open the file ``%CATALINA_HOME%\conf\tomcat-users.xml`` - * under the ``tomcat-users`` tag place, initialize an user with roles "tomcat, manager-gui, manager-script". An example is the following content: + * under the ``tomcat-users`` tag place, initialize a user with roles "tomcat, manager-gui, manager-script". An example is the following content: ``xml ``; - * edit the "to\_be\_defined" fields in tomcat-build.xml with the before defined credentials; -* execute the `generate` ant task in order to generate the .war; + * edit the "to\_be\_defined" fields in tomcat-build.xml with the previously defined credentials; +* execute the `generate` ant task in order to generate the .war file; * launch Tomcat 8 with the startup script ``%CATALINA_HOME%\bin\startup.bat`` or by the start-tomcat task ant; * (optional) if you previously configured Tomcat Manager you can open a browser and navigate to `this link ` and login using the proper username and password (e.g., ``admin/admin`` in the previous example); * (optional) you can `deploy/undeploy/redeploy` the downloaded WARs through the web interface. ## REST APIs +In order to access the VEREFOO framework, some REST APIs are available when VEREFOO is deployed. + ### Connecting to the REST APIs -In order to access the core of Verefoo, some REST APIs are available. Follow these steps to boot the environment: + Follow these steps to boot the environment, deploy VEREFOO and use the APIs (these instructions refer to the version with embedded Tomcat): * Run the Neo4j server: open a shell in the folder */neo4j-server/neo4j-community-3.5.25/bin* and type ```./neo4j console```; * Run Tomcat: open another shell in the project root folder and type the following two commands: ```mvn clean package``` and ```java -jar target/verifoo-0.0.1-SNAPSHOT.jar```; -* Interact with the REST APIs: start doing requests to Verefoo by means of a RESTful client; for any doubt about the REST APIs, their documentation can be found at [localhost:8085/verefoo](localhost:8085/verefoo). +* Interact with the REST APIs: any RESTful client can be used to interact with the VEREFOO APIs; the APIs home URI is [localhost:8085/VEREFOO](localhost:8085/VEREFOO). For any doubt about the REST APIs, their documentation can be found at [localhost:8085/VEREFOO](localhost:8085/VEREFOO). -### Verefoo Interaction -In order to interact with Verefoo, it is necessary to specify the algorithm used. Currently, this version of Verefoo is equipped with two algorithms: Maximal Flows (MF) and Atomic Predicates (AP), each of which is suitable for distinct use cases. To select the algorithm utilized, the query parameter that specifies the algorithm should be included in the REST API request, subsequent to the framework's launch. +### VEREFOO Interaction -> Example: -> * `http://localhost:8085/verefoo/adp/simulations?Algorithm=AP` -> * `http://localhost:8085/verefoo/adp/simulations?Algorithm=MF` - -The primary API is `/adp/simulations` as it serves as the API where the algorithm is executed. The Service Graph written in XML must be incorporated in the body of a POST API. Furthermore, it is obligatory to indicate the Algorithm to be employed by the framework, for instance, `?Algorithm=AP` is specified to execute the Atomic Predicate Algorithm, or `?Algorithm=MF` to select the Maximal Flows Algorithm. It should be noted that the specification of the algorithm is mandatory, otherwise, the framework will return an error. +In order to interact with VEREFOO, it is necessary to specify the algorithm used. This version of VEREFOO is equipped with two algorithms: Maximal Flows (MF) and Atomic Predicates (AP), each of which is suitable for distinct use cases. -### Launching the integration tests +The algorithm for the computation of Atomic Flows express each complex network predicate (e.g., a predicate +representing a firewall rule, a NAT input packet class, or a +security policy) as a subset of atomic predicates, which are disjoint to each other. Th Atomic flows are thus computed so that each tansmitted packet class is represented by an atomic predicate, and it can be represented by an integer number. This algorithm is suitable for scenarios where the automatic firewall configuration must be very fast, even at the expense of a larger number of rules that are created with this algoritm. -Some integration tests are available for the REST APIs. +The algorithm for the computation of Maximal Flows maximizing their aggregation. It groups all traffic flows that behave in the same way when crossing the network into a single Maximal Flow, so that +it is sufficient to consider the Maximal Flow for solving the +security configuration problem instead of all separate flows. This algorithm is suitable for scenarios where the minimum possible number of firewall rules must be computed, even if the MaxSMT problem resolution may take longer as each packet class cannot be associated with an integer value. It is also suitables for formally verifying the compliance of an already existing configuration with a set of user-specified secuirity requirements. -In order to launch them, it is enough to: +To select the algorithm utilized, the query parameter that specifies the algorithm should be included in the REST API request, subsequent to the framework's launch. -* Run the Neo4j server: open a shell in the folder */neo4j-server/neo4j-community-3.5.25/bin* and type ```./neo4j console```; -* Launch the tests: open another shell in the project root folder and type ```mvn clean verify```. +> Example: +> * `http://localhost:8085/VEREFOO/adp/simulations?Algorithm=AP` +> * `http://localhost:8085/VEREFOO/adp/simulations?Algorithm=MF` -In case of failure, the detailed report can be found at */target/failsafe-report/failsafe-summary.xml*. +The primary API is `/adp/simulations` as it serves as the API where the algorithm is executed. The Service Graph written in XML must be incorporated in the body of a POST request. It should be noted that the specification of the algorithm, as shown above, is mandatory, otherwise, the framework will return an error. ### Neo4j compatibility recommendations -The current version of the Neo4j server is 3.5.25 (Community Edition): it is compatible with the Neo4j Spring Data dependency in use. It is advisable to not employ at all newer versions of the server or Spring Data, despite available, for three main reasons: +The framework was tested with the the Neo4j server version 3.5.25 (Community Edition): it is compatible with the Neo4j Spring Data dependency in use. It is advisable to avoid employing newer versions of the server or Spring Data, despite available, for three main reasons: * The required JDK for more recent releases may be the JDK 11 at least, while the current compiler for Verifoo is Java 8; the migration to a newer JDK **must** be first agreed with all the developers of the project; * The configuration of Spring in the file SpringBootConfiguration should be changed because some classes are not available anymore; @@ -79,14 +99,24 @@ The current version of the Neo4j server is 3.5.25 (Community Edition): it is com ## Regression Tests -Kindly note that the regression tests performed on the framework have been executed using the Z3 library versions 4.8.8. +Regression tests can be used to test the framework after any applied change. Two classes of regression tests are availables: tests to check the correctness of the MaxSMT problem resolution, and tests to check the correctness of the REST APIs. + +The regression tests to check the correctness of the MaxSMT problem resolution can be launched manually, and they are available in src/it/polito/verefoo/test. + +The regression tests to check the correctness of the REST APIs can be launched as follows: +* Run the Neo4j server: open a shell in the folder */neo4j-server/neo4j-community-3.5.25/bin* and type ```./neo4j console```; +* Launch the tests: open another shell in the project root folder and type ```mvn clean verify```. + +In case of failure, the detailed report can be found at */target/failsafe-report/failsafe-summary.xml*. + +All the regression tests performed on the framework have been executed using the Z3 library version 4.8.8. -## DEMO +## Demo You can find a full demonstration of the VEREFOO framework at the following link: https://youtu.be/QCFNLE2gHgE -In this demo, VEREFOO has been used to automatically computed the firewall allocation scheme and configuration in a virtual network that is devoid of firewalling functionalities. +In this demo, VEREFOO has been used to automatically compute the firewall allocation scheme and configuration in a virtual network that is devoid of firewalling functionalities. The input Service Graph represents a ramified network, where multiple different function types are included, e.g., a load balancer, a web cache, a traffic monitor, a network address translators. Some end points are single hosts, whereas other ones are subnetworks representing the office networks of some companies. @@ -102,4 +132,4 @@ After running the framework, VEREFOO produces two outputs. On the one hand, it e ![Firewall Allocation Scheme](./resources/images-demo/FAS.png) -![Firewall Configuration](./resources/images-demo/FwRules.png) \ No newline at end of file +![Firewall Configuration](./resources/images-demo/FwRules.png) From db9c4cc71569dc9459d94094ca25c4dfca1431ac Mon Sep 17 00:00:00 2001 From: Francesco Pizzato Date: Tue, 23 Apr 2024 19:25:13 +0200 Subject: [PATCH 02/11] Updated NFV schema with InitialProperties --- xsd/nfvSchema.xsd | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/xsd/nfvSchema.xsd b/xsd/nfvSchema.xsd index 91ea1999..0e6085b8 100644 --- a/xsd/nfvSchema.xsd +++ b/xsd/nfvSchema.xsd @@ -16,6 +16,7 @@ + @@ -73,6 +74,13 @@ + + + + + + + From 2c89f3bc0fefc9bb97c6a944e53d4e119e93fa21 Mon Sep 17 00:00:00 2001 From: Francesco Pizzato Date: Wed, 24 Apr 2024 14:57:10 +0200 Subject: [PATCH 03/11] Logic for calling REACT Verefoo and extracting updated security requirements --- src/it/polito/verefoo/VerefooProxy.java | 146 ++++++++++++++++++- src/it/polito/verefoo/VerefooSerializer.java | 73 ++++++++++ 2 files changed, 218 insertions(+), 1 deletion(-) diff --git a/src/it/polito/verefoo/VerefooProxy.java b/src/it/polito/verefoo/VerefooProxy.java index 9a482df8..af05197c 100644 --- a/src/it/polito/verefoo/VerefooProxy.java +++ b/src/it/polito/verefoo/VerefooProxy.java @@ -53,13 +53,15 @@ public class VerefooProxy { private NetContextAP nctxAP; private NetContextMF nctxMF; private List properties; + private List initialProperties; + private List toAddProperties,toKeptProperties; private List paths; private WildcardManager wildcardManager; private HashMap allocationNodesAP; private HashMap allocationNodesMF; private HashMap trafficFlowsMapAP; private HashMap trafficFlowsMapMF; - private HashMap securityRequirements; + private HashMap securityRequirements, toAddSecurityRequirements; public Checker check; private List nodes; private List nodeMetrics; @@ -226,8 +228,120 @@ public VerefooProxy(Graph graph, Hosts hosts, Connections conns, Constraints con } } + + /** + * Alternative version for REACT-VEREFOO + * + */ + public VerefooProxy(Graph graph, Hosts hosts, Connections conns, Constraints constraints, List initialProp, + List targetProp, List paths,String algo) throws BadGraphError { + + // Determine what algorithm to be executed + this.AlgoUsed = algo; + + if(AlgoUsed.equals("AP")){ // Atomic Predicate algo execution + + // Initialization of the variables related to the nodes + allocationNodesAP = new HashMap<>(); + nodes = graph.getNode(); + nodes.forEach(n -> allocationNodesAP.put(n.getName(), new AllocationNodeAP(n))); // class for AP + wildcardManager = new WildcardManager(allocationNodesAP); + + // Initialization of the variables related to the requirements + properties = targetProp; + initialProperties = initialProp; + toAddProperties = new ArrayList<>(targetProp); + + securityRequirements = new HashMap<>(); + int idRequirement = 0; + //Create map for requirements + if(initialProperties != null) { + + //Compute intersection between initialProp and targetProp, then remove it from "targetProp" to find out "toAddProperties" + toKeptProperties = computeKeptList(initialProperties, properties); + toKeptProperties.forEach(e -> { + for(Property p: toAddProperties) { + if(propertyCompare(p,e)) { + toAddProperties.remove(p); + break; + } + } + }); + + //Create a map about the updated security requirements + toAddSecurityRequirements = new HashMap<>(); + for(Property p : toAddProperties) { + toAddSecurityRequirements.put(idRequirement, new SecurityRequirement(p,idRequirement)); + idRequirement++; + } + + //Fill the map with target set of security requirements + securityRequirements.putAll(toAddSecurityRequirements); + for(Property p: toKeptProperties) { + securityRequirements.put(idRequirement, new SecurityRequirement(p,idRequirement)); + idRequirement++; + } + } else { + for(Property p : properties) { + securityRequirements.put(idRequirement, new SecurityRequirement(p, idRequirement)); + idRequirement++; + } + } + + this.paths = paths; + this.nodeMetrics = constraints.getNodeConstraints().getNodeMetrics(); + //Creation of the z3 context + HashMap cfg = new HashMap(); + cfg.put("model", "true"); + ctx = new Context(cfg); + + //Creation of the NetContext (z3 variables) + nctxAP = nctxGenerateAP(ctx, nodes, targetProp, allocationNodesAP); + nctxAP.setWildcardManager(wildcardManager); + aputilsAP = new APUtilsAP(); + + + /* + * Main sequence of methods in VerefooProxy for Atomic Predicates: + * 1) given every requirement, all the possible paths of the related flows are computed; + * 2) then starting from requirements and transformers, all relative atomic predicates for the network are computed + * 3) the transformation map for each transformer is filled (e.g. NAT1 input ap 5 -> output ap 8) + * 4) then all atomic flows are computed + */ + + allocationManager = new AllocationManager(ctx, nctxAP, allocationNodesAP, nodeMetrics, targetProp, wildcardManager); + allocationManager.instantiateFunctions("AP"); + + /* Atomic predicates */ + aputilsAP = new APUtilsAP(); + long t1 = System.currentTimeMillis(); + trafficFlowsMapAP = generateFlowPathsAP(); + networkAtomicPredicates = generateAtomicPredicateNew(); + long t2 = System.currentTimeMillis(); + testResults.setAtomicPredCompTime(t2-t1); + fillTransformationMap(); + //printTransformations(); //DEBUG + computeAtomicFlows(); + t1 = System.currentTimeMillis(); + testResults.setAtomicFlowsCompTime(t1-t2); + testResults.setBeginMaxSMTTime(t1); + //distributeTrafficFlows(); + allocateFunctionsAP(); + // Change Execution depending on chosen algorithm + allocationManager.configureFunctionsAP(); // atomic predicate method + + check = new Checker(ctx, nctxAP, allocationNodesAP); + formalizeRequirementsAP(); + + } + + if(AlgoUsed.equals("MF")){ // Maximal flows algorithm execution + //Not yet implemented. + } + } /**************************************************Atomic Predicate Methods **************************************************************/ + /** * This function receives in input a set of already computed Atomic Predicates * (atomicPredicates) and a set of Predicates (predicates), not yet atomic, to convert @@ -871,6 +985,36 @@ else if(node.getFunctionalType() == FunctionalTypes.FIREWALL) { return networkAtomicPredicates; } + private List computeKeptList(List set1, List set2){ + List kept = new ArrayList(); + for(Property p1: set1) { + for(Property p2: set2) { + if(propertyCompare(p1,p2)) { + kept.add(p1); + break; + } + } + } + return kept; + } + + private boolean propertyCompare(Property p1, Property p2) { + if(!p1.getName().value().equals(p2.getName().value())) + return false; + if(!p1.getSrc().equals(p2.getSrc())) + return false; + if(!p1.getDst().equals(p2.getDst())) + return false; + if(p1.getSrcPort()== null ? !(p2.getSrcPort() == null) : !p1.getSrcPort().equals(p2.getSrcPort())) + return false; + if(p1.getDstPort()== null ? !(p2.getDstPort() == null) : !p1.getDstPort().equals(p2.getDstPort())) + return false; + if(p1.getLv4Proto()== null ? !(p2.getLv4Proto() == null) : !p1.getLv4Proto().equals(p2.getLv4Proto())) + return false; + return true; + } + + /*****************************************************AP duplicated methods**************************************************************************/ /** * This method allocates the functions on allocation nodes that are empty. diff --git a/src/it/polito/verefoo/VerefooSerializer.java b/src/it/polito/verefoo/VerefooSerializer.java index 2f012f97..bc1856bf 100644 --- a/src/it/polito/verefoo/VerefooSerializer.java +++ b/src/it/polito/verefoo/VerefooSerializer.java @@ -26,6 +26,7 @@ public class VerefooSerializer { private String z3Model; private TestResults testResults; private String AlgoUsed = "AP"; + private Boolean REACT = false; int time = 0; VerificationResult res; @@ -110,6 +111,78 @@ public VerefooSerializer(NFV root,String algo) { throw e; } } + + + public VerefooSerializer(NFV root,String algo, Boolean react) { + this.nfv = root; + this.AlgoUsed = algo; + this.REACT = react; + AllocationGraphGenerator agg = new AllocationGraphGenerator(root); + root = agg.getAllocationGraph(); + VerefooNormalizer norm = new VerefooNormalizer(root); + root = norm.getRoot(); + //VerificationResult res; + Translator t; + + try { + List paths = null; + if (root.getNetworkForwardingPaths() != null) + paths = root.getNetworkForwardingPaths().getPath(); + for (Graph g : root.getGraphs().getGraph()) { + List prop = root.getPropertyDefinition().getProperty().stream() + .filter(p -> p.getGraph() == g.getId()).collect(Collectors.toList()); + List initialProp = (root.getInitialProperty() == null)? null : root.getInitialProperty().getProperty().stream() + .filter(p -> p.getGraph() == g.getId()).collect(Collectors.toList()); + if (prop.size() == 0) + throw new BadGraphError("No property defined for the Graph " + g.getId(), + EType.INVALID_PROPERTY_DEFINITION); + VerefooProxy test = new VerefooProxy(g, root.getHosts(), root.getConnections(), root.getConstraints(), initialProp, + prop, paths, AlgoUsed); + testResults = test.getTestTimeResults(); + long beginAll = System.currentTimeMillis(); + + if(AlgoUsed.equals("AP")) + res = test.checkNFFGPropertyAP(); + else + res = test.checkNFFGPropertyMF(); + + long endAll = System.currentTimeMillis(); + //loggerResult.debug("Only checker: " + (endAll - beginAll) + "ms"); + //System.out.println("Only checker: " + (endAll - beginAll) + "ms"); + time = (int) res.getTime(); + + if (res.result != Status.UNSATISFIABLE && res.result != Status.UNKNOWN) { + // Execute Translator according to algorithm chosen + if(AlgoUsed.equals("AP")) + t = new Translator(res.model.toString(), root, g, test.getAllocationNodesAP(), test.getTrafficFlowsMapAP(), test.getNetworkAtomicPredicates()); + else + t = new Translator(res.model.toString(), root, g, test.getAllocationNodesMF(), test.getTrafficFlowsMapMF()); + + z3Model = res.model.toString(); + t.setNormalizer(norm); + result = t.convert(AlgoUsed); + root = result; + sat = true; + System.out.println("SAT\n"); + testResults.setZ3Result("SAT"); + + } else { + System.out.println("UNSAT\n"); + testResults.setZ3Result("UNSAT"); + sat = false; + result = root; + } + + root.getPropertyDefinition().getProperty().stream().filter(p -> p.getGraph() == g.getId()) + .forEach(p -> p.setIsSat(res.result != Status.UNSATISFIABLE)); + + } + } catch (BadGraphError e) { + throw e; + } + } + + /** From f582fea9559b9add497778e0229a260d06842b9e Mon Sep 17 00:00:00 2001 From: Francesco Pizzato Date: Wed, 24 Apr 2024 17:13:57 +0200 Subject: [PATCH 04/11] Implemented algorithm for detection of Reconfigured nodes --- src/it/polito/verefoo/VerefooProxy.java | 155 +++++++++++++++++++++++- 1 file changed, 153 insertions(+), 2 deletions(-) diff --git a/src/it/polito/verefoo/VerefooProxy.java b/src/it/polito/verefoo/VerefooProxy.java index af05197c..7f0a13d0 100644 --- a/src/it/polito/verefoo/VerefooProxy.java +++ b/src/it/polito/verefoo/VerefooProxy.java @@ -17,6 +17,7 @@ import com.microsoft.z3.Context; import it.polito.verefoo.allocation.AllocationManager; +import it.polito.verefoo.allocation.AllocationNode; import it.polito.verefoo.allocation.AllocationNodeAP; import it.polito.verefoo.allocation.AllocationNodeMF; import it.polito.verefoo.extra.BadGraphError; @@ -256,7 +257,7 @@ public VerefooProxy(Graph graph, Hosts hosts, Connections conns, Constraints con int idRequirement = 0; //Create map for requirements if(initialProperties != null) { - + //Compute intersection between initialProp and targetProp, then remove it from "targetProp" to find out "toAddProperties" toKeptProperties = computeKeptList(initialProperties, properties); toKeptProperties.forEach(e -> { @@ -307,6 +308,7 @@ public VerefooProxy(Graph graph, Hosts hosts, Connections conns, Constraints con * 2) then starting from requirements and transformers, all relative atomic predicates for the network are computed * 3) the transformation map for each transformer is filled (e.g. NAT1 input ap 5 -> output ap 8) * 4) then all atomic flows are computed + * 5) using atomic flows, network's components that must be reconfigured are detected */ allocationManager = new AllocationManager(ctx, nctxAP, allocationNodesAP, nodeMetrics, targetProp, wildcardManager); @@ -324,7 +326,36 @@ public VerefooProxy(Graph graph, Hosts hosts, Connections conns, Constraints con computeAtomicFlows(); t1 = System.currentTimeMillis(); testResults.setAtomicFlowsCompTime(t1-t2); - testResults.setBeginMaxSMTTime(t1); + + /* REACT Algorithm */ + List nodesToBeReconfigured = computeReconfiguredNetwork(); + for(AllocationNodeAP n: nodesToBeReconfigured) { + if(n.getTypeNF().value().equals("FIREWALL")) { +// PacketFilterAP fw = (PacketFilterAP) n.getPlacedNF(); +// fw.reConfigure(); + n.setTypeNF(null); + n.setPlacedNF(null); + n.getNode().setFunctionalType(null); + n.getNode().setConfiguration(null); + } else if(n.getTypeNF().value().equals("FORWARDER")) { + n.setTypeNF(null); + n.setPlacedNF(null); + n.getNode().setFunctionalType(null); + n.getNode().setConfiguration(null); + } + } + t2 = System.currentTimeMillis(); + //testResults.setReconfiguredNetworkCompTime(t2-t1); + + if(nodesToBeReconfigured.isEmpty()) { + System.out.println("There are no nodes which needs to be reconfigured."); + } else { + System.out.println("The nodes to be reconfigured are ["+nodesToBeReconfigured.size()+"]:"); + for(AllocationNode an : nodesToBeReconfigured) + System.out.println(an.getIpAddress()); + } + + testResults.setBeginMaxSMTTime(t2); //distributeTrafficFlows(); allocateFunctionsAP(); // Change Execution depending on chosen algorithm @@ -1013,6 +1044,126 @@ private boolean propertyCompare(Property p1, Property p2) { return false; return true; } + + private List computeReconfiguredNetwork() { + List nodes; + List toBeReconfigured = new ArrayList<>(); + Set tmpToBeReconfigured; + List tmpFlowNodes; + Boolean found,foundTmp,NAT; + Integer index; + + for(SecurityRequirement sr : toAddSecurityRequirements.values()) { + if(sr.getOriginalProperty().getName().toString().equals("ISOLATION_PROPERTY")) { + //Iterate over all of the correlated Atomic Flows + for(FlowPathAP p : sr.getFlowsMapAP().values()) { + nodes = p.getPath(); + for(AtomicFlow af : p.getAtomicFlowsMap().values()) { + found = false; + index = 0; + for(AllocationNodeAP n : nodes.subList(1, nodes.size()-1)) { + //check if the node blocks the traffic + if(n.getNode().getFunctionalType() != null) { + if(n.getNode().getFunctionalType().value().equals("FIREWALL") + && n.getDroppedList().contains(af.getAtomicPredicateList().get(index))) { + found = true; + break; + } + } + index++; + } + //if the traffic is not blocked the nodes should be reconfigured + if(!found) { + //We reconfigure both FWs and FORWARDERS + toBeReconfigured.addAll(nodes.stream() + .filter(n -> !toBeReconfigured.contains(n)) //not already inserted + .filter(n -> transformersNode.containsKey(n.getIpAddress())) //is an already configured transformed node + .filter(n -> transformersNode.get(n.getIpAddress()).getFunctionalType().value().equals("FIREWALL")) //is a FW (it handles only FW reconfiguration at the moment) + .collect(Collectors.toList())); + toBeReconfigured.addAll(nodes.stream() + .filter(n-> !toBeReconfigured.contains(n)) + .filter(n-> n.getTypeNF()!=null && n.getTypeNF().value().equals("FORWARDER")) + .collect(Collectors.toList())); + } + } + } + } else if(sr.getOriginalProperty().getName().toString().equals("REACHABILITY_PROPERTY")) { + tmpToBeReconfigured = new HashSet<>(); + found = false; + for(FlowPathAP p : sr.getFlowsMapAP().values()) { + nodes = p.getPath(); + for(AtomicFlow af : p.getAtomicFlowsMap().values()) { + index = 0; + tmpFlowNodes = new ArrayList<>(); + NAT = false; + for(AllocationNodeAP n : nodes.subList(1, nodes.size()-1)) { + //check if there is a NAT on the path + if(!NAT && n.getNode().getFunctionalType() != null + && n.getNode().getFunctionalType().value().equals("NAT")) { + NAT = true; + //check if the node blocks the traffic + } else if (n.getNode().getFunctionalType() != null + && n.getNode().getFunctionalType().value().equals("FIREWALL") + && n.getDroppedList().contains(af.getAtomicPredicateList().get(index))) { + + tmpFlowNodes.add(n); + /* + * Check for special case: with NAT, extra nodes need to be selected + */ + if(NAT) { + //scan all the FlowPaths crossing the current node n + for(FlowPathAP fp : n.getCrossingFlows().values()) { + //consider only FlowPaths associated with opposite requirements, otherwise there could be no conflict + if(fp.getRequirement().getOriginalProperty().getName().toString().equals("ISOLATION_PROPERTY")) { + //scan all the AP in input for current node and current FlowPath + for(int ap : n.getAtomicPredicatesInInputForFlow(fp.getIdFlow()).values()) { + if(ap == af.getAtomicPredicateList().get(index)) { + //Reconfigure also all FORWARDERS on the Isolation's FlowPath before each NAT and before reaching current node n + AllocationNodeAP an; + for(int i=0; i !toBeReconfigured.contains(n)) + .collect(Collectors.toList())); + } + } + } + return toBeReconfigured; + } /*****************************************************AP duplicated methods**************************************************************************/ From 1e18babeec8d72ccfeefeb6208365ee8bf17d59e Mon Sep 17 00:00:00 2001 From: Francesco Pizzato Date: Wed, 24 Apr 2024 18:14:21 +0200 Subject: [PATCH 05/11] Modified version of hard and soft constraint management for Reconfigured nodes --- src/it/polito/verefoo/VerefooProxy.java | 9 +++--- .../verefoo/functions/PacketFilterAP.java | 30 +++++++++++++++++-- src/it/polito/verefoo/solver/NetContext.java | 2 ++ .../polito/verefoo/solver/NetContextAP.java | 9 +++++- 4 files changed, 42 insertions(+), 8 deletions(-) diff --git a/src/it/polito/verefoo/VerefooProxy.java b/src/it/polito/verefoo/VerefooProxy.java index 7f0a13d0..68d64edc 100644 --- a/src/it/polito/verefoo/VerefooProxy.java +++ b/src/it/polito/verefoo/VerefooProxy.java @@ -41,6 +41,7 @@ import it.polito.verefoo.utils.TestResults; import it.polito.verefoo.utils.VerificationResult; import it.polito.verefoo.functions.Forwarder; +import it.polito.verefoo.functions.PacketFilterAP; import it.polito.verefoo.graph.MaximalFlow; import it.polito.verefoo.graph.Traffic; @@ -331,10 +332,10 @@ public VerefooProxy(Graph graph, Hosts hosts, Connections conns, Constraints con List nodesToBeReconfigured = computeReconfiguredNetwork(); for(AllocationNodeAP n: nodesToBeReconfigured) { if(n.getTypeNF().value().equals("FIREWALL")) { -// PacketFilterAP fw = (PacketFilterAP) n.getPlacedNF(); -// fw.reConfigure(); - n.setTypeNF(null); - n.setPlacedNF(null); + PacketFilterAP fw = (PacketFilterAP) n.getPlacedNF(); + fw.reConfigure(); +// n.setTypeNF(null); +// n.setPlacedNF(null); n.getNode().setFunctionalType(null); n.getNode().setConfiguration(null); } else if(n.getTypeNF().value().equals("FORWARDER")) { diff --git a/src/it/polito/verefoo/functions/PacketFilterAP.java b/src/it/polito/verefoo/functions/PacketFilterAP.java index d6529a3b..e9d62d3c 100644 --- a/src/it/polito/verefoo/functions/PacketFilterAP.java +++ b/src/it/polito/verefoo/functions/PacketFilterAP.java @@ -38,6 +38,7 @@ public class PacketFilterAP extends GenericFunction{ FuncDecl filtering_function; boolean autoConfigured; + boolean reconfigured; BoolExpr behaviour; FuncDecl rule_func; // blacklisting and defaultAction must match @@ -62,6 +63,7 @@ public PacketFilterAP(AllocationNodeAP source, Context ctx, NetContextAP nctx, W pf = source.getZ3Name(); constraints = new ArrayList(); isEndHost = false; + reconfigured = false; // true for blacklisting, false for whitelisting // this is the default, but it can be changed @@ -110,8 +112,13 @@ public void automaticConfiguration() { //allocation if(autoplace) { - // packet filter should not be used if possible - nctxAP.softConstrAutoPlace.add(new Tuple(ctx.mkNot(used), "fw_auto_conf")); + if(reconfigured) { + //Prefer a previously configured FW with respect to a new allocation point + nctxAP.softConstrMaintainStatePlacement.add(new Tuple(ctx.mkNot(used), "fw_auto_conf")); + } else { + // packet filter should not be used if possible + nctxAP.softConstrAutoPlace.add(new Tuple(ctx.mkNot(used), "fw_auto_conf")); + } }else { used = ctx.mkTrue(); constraints.add(ctx.mkEq(used, ctx.mkTrue())); @@ -140,7 +147,16 @@ public void automaticConfiguration() { ) ) ); - nctxAP.softConstrAutoConf.add(new Tuple(ctx.mkEq(rule, ctx.mkFalse()), "fw_auto_conf")); + //For reconfigured FWs, maintaining its configuration should be preferred + if(!reconfigured) { + nctxAP.softConstrAutoConf.add(new Tuple(ctx.mkEq(rule, ctx.mkFalse()), "fw_auto_conf")); + } else { + if(this.sourceAP.getDroppedList().contains(traffic) || this.sourceAP.getForwardBehaviourList().contains(traffic)) + nctxAP.softConstrMaintainStateConfiguration.add(new Tuple(ctx.mkEq(rule, ctx.mkFalse()), "fw_auto_conf")); + else { + nctxAP.softConstrAutoConf.add(new Tuple(ctx.mkEq(rule, ctx.mkFalse()), "fw_auto_conf")); + } + } } } @@ -218,4 +234,12 @@ public void addContraints(Optimize solver) { solver.Add(constraints.toArray(constr)); //additionalConstraints(solver); } + + public void reConfigure() { + //Set automatic placement and configuration + autoplace = true; + autoConfigured = true; + defaultActionSet = false; + reconfigured = true; + } } diff --git a/src/it/polito/verefoo/solver/NetContext.java b/src/it/polito/verefoo/solver/NetContext.java index f1dde0a6..06277f2c 100644 --- a/src/it/polito/verefoo/solver/NetContext.java +++ b/src/it/polito/verefoo/solver/NetContext.java @@ -42,6 +42,8 @@ abstract public class NetContext { public List constraints; public List> softConstrAutoConf; public List> softConstrAutoPlace; + public List> softConstrMaintainStatePlacement; + public List> softConstrMaintainStateConfiguration; public List> softConstrWildcard; public List> softConstrProtoWildcard; public List> softConstrPorts; diff --git a/src/it/polito/verefoo/solver/NetContextAP.java b/src/it/polito/verefoo/solver/NetContextAP.java index 7a869436..e01788d3 100644 --- a/src/it/polito/verefoo/solver/NetContextAP.java +++ b/src/it/polito/verefoo/solver/NetContextAP.java @@ -39,6 +39,9 @@ public class NetContextAP extends NetContext { // weights public final int WAUTOCONF = 1; + //REACT_VEREFOO + public final int WMAINTAINSTATECONF = WAUTOCONF / 2; + public final int WMAINTAINSTATEPLACEMENT = WAUTOPLACEMENT/10; /** @@ -56,9 +59,11 @@ public NetContextAP(Context ctx, HashMap allocationNod constraints = new ArrayList(); softConstrAutoConf = new ArrayList<>(); softConstrAutoPlace = new ArrayList<>(); + softConstrMaintainStatePlacement = new ArrayList<>(); + softConstrMaintainStateConfiguration = new ArrayList<>(); softConstrWildcard = new ArrayList<>(); softConstrProtoWildcard = new ArrayList<>(); - softConstrPorts = new ArrayList<>(); + softConstrPorts = new ArrayList<>(); this.ctx = ctx; this.allocationNodes = allocationNodes; @@ -81,6 +86,8 @@ protected void addConstraints(Optimize solver) { solver.Add(constraints.toArray(constr)); softConstrAutoConf.forEach(t->solver.AssertSoft(t._1, WAUTOCONF, t._2)); softConstrAutoPlace.forEach(t->solver.AssertSoft(t._1, WAUTOPLACEMENT, t._2)); + softConstrMaintainStatePlacement.forEach(t->solver.AssertSoft(t._1, WMAINTAINSTATEPLACEMENT, t._2)); + softConstrMaintainStateConfiguration.forEach(t->solver.AssertSoft(t._1, WMAINTAINSTATECONF, t._2)); } /** From 63b43e76daf46bbb7c0082d20d64d202cb551681 Mon Sep 17 00:00:00 2001 From: Francesco Pizzato Date: Wed, 24 Apr 2024 18:29:35 +0200 Subject: [PATCH 06/11] Custom version of AllocationGraphGenerator for REACT VEREFOO --- src/it/polito/verefoo/VerefooSerializer.java | 2 +- .../allocation/AllocationGraphGenerator.java | 136 ++++++++++++++++++ 2 files changed, 137 insertions(+), 1 deletion(-) diff --git a/src/it/polito/verefoo/VerefooSerializer.java b/src/it/polito/verefoo/VerefooSerializer.java index bc1856bf..d9391841 100644 --- a/src/it/polito/verefoo/VerefooSerializer.java +++ b/src/it/polito/verefoo/VerefooSerializer.java @@ -117,7 +117,7 @@ public VerefooSerializer(NFV root,String algo, Boolean react) { this.nfv = root; this.AlgoUsed = algo; this.REACT = react; - AllocationGraphGenerator agg = new AllocationGraphGenerator(root); + AllocationGraphGenerator agg = new AllocationGraphGenerator(root, react); root = agg.getAllocationGraph(); VerefooNormalizer norm = new VerefooNormalizer(root); root = norm.getRoot(); diff --git a/src/it/polito/verefoo/allocation/AllocationGraphGenerator.java b/src/it/polito/verefoo/allocation/AllocationGraphGenerator.java index bc54170f..c3b652a0 100644 --- a/src/it/polito/verefoo/allocation/AllocationGraphGenerator.java +++ b/src/it/polito/verefoo/allocation/AllocationGraphGenerator.java @@ -2,6 +2,7 @@ import java.util.ArrayList; import java.util.List; +import java.util.stream.Collectors; import it.polito.verefoo.jaxb.ActionTypes; import it.polito.verefoo.jaxb.AllocationConstraintType; @@ -50,6 +51,141 @@ public AllocationGraphGenerator(NFV nfv) { } + /** + * Special constructor for REACT-VEREFOO implementation + * + */ + public AllocationGraphGenerator(NFV nfv, Boolean react) { + this.nfv = nfv; + for(Graph graph : nfv.getGraphs().getGraph()) { + if(graph.isServiceGraph()) { + List list = new ArrayList(); + AllocationConstraints ac = nfv.getConstraints().getAllocationConstraints(); + if(ac != null) { + list.addAll(ac.getAllocationConstraint()); + } + + generateAllocationGraph_REACT(graph, list); + } + } + + } + + + private void generateAllocationGraph_REACT(Graph graph, List list) { + int counter = 1; + List newNodes = new ArrayList(); + + //List of IPAddresses of configured FWs + List firewalls = graph.getNode().stream().filter(n -> n.getFunctionalType()!=null) + .filter(n -> n.getFunctionalType().value().equals("FIREWALL")) + .map(n -> n.getName()).collect(Collectors.toList()); + //List of IPAddresses of configured FORWARDERs + List forwarders = graph.getNode().stream().filter(n -> n.getFunctionalType()!=null) + .filter(n -> n.getFunctionalType().value().equals("FORWARDER")) + .map(n -> n.getName()).collect(Collectors.toList()); + //List of IPAddresses of APs + List allocationPoints = graph.getNode().stream().filter(n -> n.getFunctionalType()==null) + .map(n -> n.getName()).collect(Collectors.toList()); + for(Node node : graph.getNode()) { + //We avoid generating new AP near a FW, another AP, or a FORWARDER + if(!firewalls.contains(node.getName()) + && !forwarders.contains(node.getName()) + && !allocationPoints.contains(node.getName())) { + + List toRemove = new ArrayList(); + List toAdd = new ArrayList(); + + for(Neighbour neighbour : node.getNeighbour()) { + // Ignore the neighbour if it is a newly created AP,a FW, a FORWARDER, or an AP already present in the initial graph + if(!neighbour.getName().startsWith(initialAPIp) + && !firewalls.contains(neighbour.getName()) + && !allocationPoints.contains(neighbour.getName()) + && !forwarders.contains(neighbour.getName())) { + boolean notForbidden = true; + boolean fwForced = false; + for(AllocationConstraint ac : list) { + if(ac.getType().equals(AllocationConstraintType.FORBIDDEN) && + ( + (ac.getNodeA().equals(node.getName()) && ac.getNodeB().equals(neighbour.getName()) ) || + (ac.getNodeB().equals(node.getName()) && ac.getNodeA().equals(neighbour.getName()) ) + ) + ) { + notForbidden = false; + } + + if(ac.getType().equals(AllocationConstraintType.FORCED) && + ( + (ac.getNodeA().equals(node.getName()) && ac.getNodeB().equals(neighbour.getName()) ) || + (ac.getNodeB().equals(node.getName()) && ac.getNodeA().equals(neighbour.getName()) ) + ) + ) { + fwForced = true; + } + } + + if(notForbidden) { + Node other = graph.getNode().stream().filter(n -> n.getName().equals(neighbour.getName())).findFirst().orElse(null); + boolean bidirectional = other.getNeighbour().stream().anyMatch(n -> n.getName().equals(node.getName())); + + Node allocationPlace = new Node(); + //This is needed to avoid duplicate IP addresses (with respect to previous runs) + boolean found = false; + while(!found) { + String IP= initialAPIp + counter; + if(!allocationPoints.contains(IP)) { + allocationPlace.setName(IP); + found = true; + } else { + counter++; + } + } + Neighbour apNeigh = new Neighbour(); + apNeigh.setName(allocationPlace.getName()); + counter++; + + //node.getNeighbour().removeIf(n -> n.getName().equals(neighbour.getName())); + //node.getNeighbour().add(apNeigh); + toRemove.add(neighbour.getName()); + toAdd.add(apNeigh); + + Neighbour nextNeigh = new Neighbour(); + nextNeigh.setName(neighbour.getName()); + allocationPlace.getNeighbour().add(nextNeigh); + + if(bidirectional) { + other.getNeighbour().removeIf(n -> n.getName().equals(node.getName())); + other.getNeighbour().add(apNeigh); + Neighbour prevNeigh = new Neighbour(); + prevNeigh.setName(node.getName()); + allocationPlace.getNeighbour().add(prevNeigh); + } + + if(fwForced) { + allocationPlace.setFunctionalType(FunctionalTypes.FIREWALL); + Configuration confFW = new Configuration(); + confFW.setDescription("FWDescription"); + confFW.setName("FWConfiguration"); + Firewall fw = new Firewall(); + fw.setDefaultAction(ActionTypes.DENY); + confFW.setFirewall(fw); + allocationPlace.setConfiguration(confFW); + } + + newNodes.add(allocationPlace); + } + + } + } + + node.getNeighbour().removeIf( n -> toRemove.stream().anyMatch(s -> s.equals(n.getName()))); + node.getNeighbour().addAll(toAdd); + } + } + + graph.getNode().addAll(newNodes); + + } /** * This method automatically generates an Allocation Graph with placeholders where Network Security Functions can be allocated. From a003ce1766509459900464e26f987f49611d683d Mon Sep 17 00:00:00 2001 From: Francesco Pizzato Date: Wed, 24 Apr 2024 18:45:00 +0200 Subject: [PATCH 07/11] Minor fixes and modified main with selection of REACT version --- src/it/polito/verefoo/Main.java | 18 +++++++++++++++--- src/it/polito/verefoo/VerefooProxy.java | 9 +++++++-- 2 files changed, 22 insertions(+), 5 deletions(-) diff --git a/src/it/polito/verefoo/Main.java b/src/it/polito/verefoo/Main.java index 594a9be7..6b07fcce 100644 --- a/src/it/polito/verefoo/Main.java +++ b/src/it/polito/verefoo/Main.java @@ -32,8 +32,14 @@ public class Main { public static void main(String[] args) throws MalformedURLException { System.setProperty("log4j.configuration", new File("resources", "log4j2.xml").toURI().toURL().toString()); - // Let user input the choice of algorithm to execute + // Let user input the choice of algorithm to execute and version of VEREFOO Scanner myObj = new Scanner(System.in); // Create a Scanner object + System.out.println("Enable REACT version (Y/N)?"); + String reactChoice = myObj.nextLine().toUpperCase(); + while (!reactChoice.equals("Y") && !reactChoice.equals("N")) { // input validation + System.out.println("Enter a correct input (Y/N)"); + reactChoice = myObj.nextLine(); + } System.out.println("Enter AP for atomic predicates algorithm Or MF for maximal flows algorithm"); String algo = myObj.nextLine(); while (!algo.equals("AP") && !algo.equals("MF")) { // input validation @@ -52,8 +58,14 @@ public static void main(String[] args) throws MalformedURLException { Marshaller m = jc.createMarshaller(); m.setProperty(Marshaller.JAXB_FORMATTED_OUTPUT, Boolean.TRUE); m.setProperty(Marshaller.JAXB_NO_NAMESPACE_SCHEMA_LOCATION, "./xsd/nfvSchema.xsd"); - // VerefooSerializer takes as parameter the type of algorithm to be used - VerefooSerializer test = new VerefooSerializer((NFV) u.unmarshal(new FileInputStream("./testfile/RegressioneTestCases/Test2_2.xml")),algo); + VerefooSerializer test; + if(reactChoice.equals("Y")) { + test = new VerefooSerializer((NFV) u.unmarshal(new FileInputStream("./testfile/NetworkTopology/Internet2.xml")),algo, true); + } else { + // VerefooSerializer takes as parameter the type of algorithm to be used + test = new VerefooSerializer((NFV) u.unmarshal(new FileInputStream("./testfile/NetworkTopology/Internet2.xml")),algo); + } + if (test.isSat()) { loggerResult.info("SAT"); loggerResult.info("----------------------OUTPUT----------------------"); diff --git a/src/it/polito/verefoo/VerefooProxy.java b/src/it/polito/verefoo/VerefooProxy.java index 68d64edc..a0bd2356 100644 --- a/src/it/polito/verefoo/VerefooProxy.java +++ b/src/it/polito/verefoo/VerefooProxy.java @@ -284,10 +284,15 @@ public VerefooProxy(Graph graph, Hosts hosts, Connections conns, Constraints con idRequirement++; } } else { - for(Property p : properties) { - securityRequirements.put(idRequirement, new SecurityRequirement(p, idRequirement)); + //Create a map about the updated security requirements + toAddSecurityRequirements = new HashMap<>(); + for(Property p : toAddProperties) { + toAddSecurityRequirements.put(idRequirement, new SecurityRequirement(p,idRequirement)); idRequirement++; } + + //Fill the map with target set of security requirements + securityRequirements.putAll(toAddSecurityRequirements); } this.paths = paths; From 0b40aa6bd61b1499497df6642c342a8a4f97fd3e Mon Sep 17 00:00:00 2001 From: Francesco Pizzato Date: Tue, 30 Apr 2024 10:50:51 +0200 Subject: [PATCH 08/11] Simple tests for REACT Verefoo --- .../verefoo/test/TestREACTCorrectness.java | 257 ++++++++++++++++++ testfile/REACT/Test1.xml | 84 ++++++ testfile/REACT/Test2.xml | 160 +++++++++++ testfile/REACT/Test3.xml | 194 +++++++++++++ 4 files changed, 695 insertions(+) create mode 100644 src/it/polito/verefoo/test/TestREACTCorrectness.java create mode 100644 testfile/REACT/Test1.xml create mode 100644 testfile/REACT/Test2.xml create mode 100644 testfile/REACT/Test3.xml diff --git a/src/it/polito/verefoo/test/TestREACTCorrectness.java b/src/it/polito/verefoo/test/TestREACTCorrectness.java new file mode 100644 index 00000000..e084b254 --- /dev/null +++ b/src/it/polito/verefoo/test/TestREACTCorrectness.java @@ -0,0 +1,257 @@ +/** + * + */ +package it.polito.verefoo.test; + +import static org.junit.Assert.*; + +import java.io.File; +import java.io.FileInputStream; +import java.util.ArrayList; +import java.util.List; +import java.util.Scanner; +import java.util.stream.Collectors; + +import javax.xml.XMLConstants; +import javax.xml.bind.JAXBContext; +import javax.xml.bind.Unmarshaller; +import javax.xml.validation.Schema; +import javax.xml.validation.SchemaFactory; + +import org.junit.After; +import org.junit.AfterClass; +import org.junit.Before; +import org.junit.BeforeClass; +import org.junit.Test; +import com.microsoft.z3.Status; + +import it.polito.verefoo.VerefooProxy; +import it.polito.verefoo.VerefooSerializer; +import it.polito.verefoo.extra.BadGraphError; +import it.polito.verefoo.jaxb.*; +import it.polito.verefoo.translator.Translator; +import it.polito.verefoo.utils.VerificationResult; +/** + * + * This class runs some tests in order to check the correctness of the auto-configuration module of Algorithm Atomic Predicates with the REACT version enabled. + * + */ +public class TestREACTCorrectness { + + /** + * @throws java.lang.Exception + */ + @BeforeClass + public static void setUpBeforeClass() throws Exception { // run once before all tests to compute results then check them + } + + /** + * @throws java.lang.Exception + */ + @AfterClass + public static void tearDownAfterClass() throws Exception { + } + + /** + * @throws java.lang.Exception + */ + @Before + public void setUp() throws Exception { + } + + /** + * @throws java.lang.Exception + */ + @After + public void tearDown() throws Exception { + } + + private VerefooSerializer test(String file) throws Exception{ + List tmp = new ArrayList<>(); + // create a JAXBContext capable of handling the generated classes + System.out.println("===========FILE " + file + "==========="); + long beginAll=System.currentTimeMillis(); + JAXBContext jc = JAXBContext.newInstance( "it.polito.verefoo.jaxb" ); + // create an Unmarshaller + Unmarshaller u = jc.createUnmarshaller(); + SchemaFactory sf = SchemaFactory.newInstance(XMLConstants.W3C_XML_SCHEMA_NS_URI); + Schema schema = sf.newSchema( new File( "./xsd/nfvSchema.xsd" )); + u.setSchema(schema); + NFV root = (NFV) u.unmarshal( new FileInputStream( file ) ); + + VerefooSerializer test = new VerefooSerializer(root,"AP",true); + + + if(test.isSat()){ + System.out.println("SAT"); + } + else{ + System.out.println("UNSAT"); + } + long endAll=System.currentTimeMillis(); + System.out.println("Total time -> " + (endAll-beginAll)+"ms" ); + + return test; + } +/********************************************************************** Tests **********************************************************************/ +// The Test files are found in /testfile/REACT. +/** + * Note: In each file there is at least one previous NSF that has to be modified. The tests performed for each file are considering 3 aspects + * a) SAT - UNSAT + * b) Correct number of firewalls allocated + * c) Correct number of firewall rules allocated + * + * Test1 = simple solution with 3 endpoints connected by a FORWARDER. Reach/Isol are swapped and: current FW has to be removed, a new one has to be instantiated (zero rules). + * + * Test2 = 5 endpoints connected by multiple FORWARDER. An Isol is swapped into Reach: current FW has to be reconfigured, with additional rules to support the situation. + * + * Test3 = more complex scenario with NATs and different rules. + * / + + /** + * This test checks if Test1 result have the expected SAT status + */ + @Test + public void test1_a(){ + try { + VerefooSerializer result = test( "./testfile/REACT/Test1.xml"); + assertTrue(result.isSat()); + } catch (Exception e) { + fail(e.toString()); + } + } + + /** + * This test checks if Test1 result have the expected number of firewalls + */ + @Test + public void test1_b(){ + try { + VerefooSerializer result = test("./testfile/REACT/Test1.xml"); + assertTrue(result.isSat()); + List listFW = result.getNfv().getGraphs().getGraph().get(0).getNode().stream().filter(n -> n.getFunctionalType().equals(FunctionalTypes.FIREWALL)).collect(Collectors.toList()); + assertTrue(listFW.size() == 1); + } catch (Exception e) { + fail(e.toString()); + } + } + + /** + * This test checks if Test1 result have the expected number of firewalls + */ + @Test + public void test1_c(){ + try { + VerefooSerializer result = test("./testfile/REACT/Test1.xml"); + assertTrue(result.isSat()); + List listFW = result.getNfv().getGraphs().getGraph().get(0).getNode().stream().filter(n -> n.getFunctionalType().equals(FunctionalTypes.FIREWALL)).collect(Collectors.toList()); + assertTrue(listFW.size() == 1); + + Node node = listFW.get(0); + assertTrue(node.getConfiguration().getFirewall().getElements().size() == 0); // firewall should have 0 rules and default deny + } catch (Exception e) { + fail(e.toString()); + } + } + + /** + * This test checks if Test2 result have the expected SAT status + */ + @Test + public void test2_a(){ + try { + VerefooSerializer result = test( "./testfile/REACT/Test2.xml"); + assertTrue(result.isSat()); + } catch (Exception e) { + fail(e.toString()); + } + } + + /** + * This test checks if Test2 result have the expected number of firewalls + */ + @Test + public void test2_b(){ + try { + VerefooSerializer result = test("./testfile/REACT/Test2.xml"); + assertTrue(result.isSat()); + List listFW = result.getNfv().getGraphs().getGraph().get(0).getNode().stream().filter(n -> n.getFunctionalType().equals(FunctionalTypes.FIREWALL)).collect(Collectors.toList()); + assertTrue(listFW.size() == 1); + } catch (Exception e) { + fail(e.toString()); + } + } + + /** + * This test checks if Test2 result have the expected number of firewalls + */ + @Test + public void test2_c(){ + try { + VerefooSerializer result = test("./testfile/REACT/Test2.xml"); + assertTrue(result.isSat()); + List listFW = result.getNfv().getGraphs().getGraph().get(0).getNode().stream().filter(n -> n.getFunctionalType().equals(FunctionalTypes.FIREWALL)).collect(Collectors.toList()); + assertTrue(listFW.size() == 1); + + Node node = listFW.get(0); + assertTrue(node.getConfiguration().getFirewall().getElements().size() == 4); // firewall should have 4 rules + } catch (Exception e) { + fail(e.toString()); + } + } + + /** + * This test checks if Test3 result have the expected SAT status + */ + @Test + public void test3_a(){ + try { + VerefooSerializer result = test( "./testfile/REACT/Test3.xml"); + assertTrue(result.isSat()); + } catch (Exception e) { + fail(e.toString()); + } + } + + /** + * This test checks if Test3 result have the expected number of firewalls + */ + @Test + public void test3_b(){ + try { + VerefooSerializer result = test("./testfile/REACT/Test3.xml"); + assertTrue(result.isSat()); + List listFW = result.getNfv().getGraphs().getGraph().get(0).getNode().stream().filter(n -> n.getFunctionalType().equals(FunctionalTypes.FIREWALL)).collect(Collectors.toList()); + assertTrue(listFW.size() == 3); + } catch (Exception e) { + fail(e.toString()); + } + } + + /** + * This test checks if Test3 result have the expected number of firewalls + */ + @Test + public void test3_c(){ + try { + VerefooSerializer result = test("./testfile/REACT/Test3.xml"); + assertTrue(result.isSat()); + List listFW = result.getNfv().getGraphs().getGraph().get(0).getNode().stream().filter(n -> n.getFunctionalType().equals(FunctionalTypes.FIREWALL)).collect(Collectors.toList()); + assertTrue(listFW.size() == 3); + + int acc = 0; + Node node = listFW.get(0); + acc += node.getConfiguration().getFirewall().getElements().size(); + node = listFW.get(1); + acc += node.getConfiguration().getFirewall().getElements().size(); + node = listFW.get(2); + acc += node.getConfiguration().getFirewall().getElements().size(); + + assertTrue(acc == 4); // 3 firewalls; one with zero rules and others with 2 rules each + + + } catch (Exception e) { + fail(e.toString()); + } + } +} \ No newline at end of file diff --git a/testfile/REACT/Test1.xml b/testfile/REACT/Test1.xml new file mode 100644 index 00000000..0f54ef45 --- /dev/null +++ b/testfile/REACT/Test1.xml @@ -0,0 +1,84 @@ + + + + + + + + + + + + + + + + + + + + + + + + + 130.10.0.1 + + + + + + + + + + + Forwarder + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/testfile/REACT/Test2.xml b/testfile/REACT/Test2.xml new file mode 100644 index 00000000..8b590ca1 --- /dev/null +++ b/testfile/REACT/Test2.xml @@ -0,0 +1,160 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 130.10.0.1 + + + + + + + + + 130.10.0.2 + + + + + + + + + + + Forwarder + + + + + + + + + + + Forwarder + + + + + + + + + + + Forwarder + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/testfile/REACT/Test3.xml b/testfile/REACT/Test3.xml new file mode 100644 index 00000000..a1e774e6 --- /dev/null +++ b/testfile/REACT/Test3.xml @@ -0,0 +1,194 @@ + + + + + + + + + + + + + + + + + + + + + 10.0.0.3 + + + + + + + + + + + + + + + + + + + + + + + + + + + + 10.0.0.1 + 10.0.0.2 + + + + + + + + + + 10.0.0.5 + 10.0.0.6 + + + + + + + + + + + Traffic Monitor + + + + + + + + + Forwarder + + + + + + + + + Forwarder + + + + + + + + + + DENY + 40.0.0.1 + 10.0.0.3 + ANY + * + * + + + + + + + + + + Forwarder + + + + + + + + + + DENY + 10.0.0.5 + 10.0.0.4 + ANY + * + * + + + + + + + + + + + + + + + + + Forwarder + + + + + + + + + Forwarder + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file From c55759446f2e6e4b31fb544d265462fdf26ed90c Mon Sep 17 00:00:00 2001 From: Francesco Pizzato Date: Tue, 30 Apr 2024 18:04:17 +0200 Subject: [PATCH 09/11] Extension to REST API for REACT VEREFOO --- .../controller/SimulationsController.java | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/src/it/polito/verefoo/rest/spring/controller/SimulationsController.java b/src/it/polito/verefoo/rest/spring/controller/SimulationsController.java index d75be399..eeb26546 100644 --- a/src/it/polito/verefoo/rest/spring/controller/SimulationsController.java +++ b/src/it/polito/verefoo/rest/spring/controller/SimulationsController.java @@ -45,7 +45,7 @@ public class SimulationsController { }) @RequestMapping(value = "", consumes = { "application/xml", "application/json" }, method = RequestMethod.POST) - public ResponseEntity> runSimulationByNFV(@RequestBody NFV nfv, @RequestParam(value = "fid", required = false) List usableFunctionalTypes,@RequestParam(name = "Algorithm") String alg) { + public ResponseEntity> runSimulationByNFV(@RequestBody NFV nfv, @RequestParam(value = "fid", required = false) List usableFunctionalTypes,@RequestParam(name = "Algorithm") String alg, @RequestParam(value = "REACT", required = false) boolean REACT) { try { // the nfv is modified in place by VerefooSerializer @@ -59,8 +59,13 @@ public ResponseEntity> runSimulationByNFV(@RequestBody NFV nfv, @ index2++; } } - - new VerefooSerializer(nfv,alg); + + // being a primitive data type, not possible to be null. If not specified is false + if(REACT) { + new VerefooSerializer(nfv,alg,true); + } else { + new VerefooSerializer(nfv,alg); + } } catch (BadGraphError e) { throw verefooCoreExceptionBuilder(e); } catch (Exception e) { @@ -91,13 +96,18 @@ public ResponseEntity> runSimulationByParams(@RequestParam(value @RequestParam(value = "rid", required = false) Long rid, @RequestParam(value = "sid", required = false) Long sid, @RequestParam(value = "fid", required = false) List usableFunctionalTypes, + @RequestParam(value = "REACT", required = false) boolean REACT, @RequestParam(name = "Algorithm") String alg) { NFV nfv = service.buildNFVFromParams(gid, rid, sid); try { // the nfv is modified in place by VerefooSerializer - new VerefooSerializer(nfv,alg); + if(REACT) { + new VerefooSerializer(nfv,alg,true); + } else { + new VerefooSerializer(nfv,alg); + } } catch (BadGraphError e) { throw verefooCoreExceptionBuilder(e); } catch (Exception e) { From df79180adf5f70da4f5eb7e6442efae41bb90214 Mon Sep 17 00:00:00 2001 From: Francesco Pizzato Date: Tue, 30 Apr 2024 18:05:27 +0200 Subject: [PATCH 10/11] Modified README --- README.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/README.md b/README.md index 61a7b4af..e8847898 100644 --- a/README.md +++ b/README.md @@ -111,6 +111,16 @@ In case of failure, the detailed report can be found at */target/failsafe-report All the regression tests performed on the framework have been executed using the Z3 library version 4.8.8. +## REACT VEREFOO + +REACT VEREFOO is a custom version of VEREFOO with additional support for the reconfiguration of packet filtering firewalls, so as to fulfill the user-specified security connectivity requirements. REACT VEREFOO maintains the core principles of VEREFOO (i.e., automation, formal correctness assurance, optimization) and adds the capability of reusing any previously computed configuration instead of forcing the reconfiguration of the whole network from scratch. + +To interact with REACT VEREFOO, it is necessary to express this with an additional query parameter. For the moment the implementation supports only the AP algorithm. + +> Example: +> * `http://localhost:8085/VEREFOO/adp/simulations?Algorithm=AP&REACT=true` + +It should be noted that this parameter is optional, to maintain full compatibility with the previous version and APIs. ## Demo From c07ab26d39d1b2057ec69390347ffced93318c8a Mon Sep 17 00:00:00 2001 From: DanieleBringhenti Date: Thu, 2 May 2024 08:08:05 +0200 Subject: [PATCH 11/11] Dublin version finalized