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 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 9a482df8..a0bd2356 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; @@ -40,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; @@ -53,13 +55,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 +230,155 @@ 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 { + //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; + 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 + * 5) using atomic flows, network's components that must be reconfigured are detected + */ + + 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); + + /* 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 + 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 +1022,156 @@ 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; + } + + 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**************************************************************************/ /** * 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..d9391841 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, react); + 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; + } + } + + /** 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. 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/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) { 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)); } /** 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 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 @@ + + + + + + +