Merge remote-tracking branch 'origin/Dublin'

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
 

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----------------------");

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<Property> properties;
+	private List<Property> initialProperties;
+	private List<Property> toAddProperties,toKeptProperties;
 	private List<Path> paths;
 	private WildcardManager wildcardManager;
 	private HashMap<String, AllocationNodeAP> allocationNodesAP;
 	private HashMap<String, AllocationNodeMF> allocationNodesMF;
 	private HashMap<Integer, FlowPathAP> trafficFlowsMapAP;
 	private HashMap<Integer, FlowPathMF> trafficFlowsMapMF;
-	private HashMap<Integer, SecurityRequirement> securityRequirements;
+	private HashMap<Integer, SecurityRequirement> securityRequirements, toAddSecurityRequirements;
 	public Checker check;
 	private List<Node> nodes;
 	private List<NodeMetrics> 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<Property> initialProp, 
+			List<Property> targetProp, List<Path> 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<String, String> cfg = new HashMap<String, String>();
+		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<AllocationNodeAP> 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<Property> computeKeptList(List<Property> set1, List<Property> set2){
+		List<Property> kept = new ArrayList<Property>();
+		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<AllocationNodeAP> computeReconfiguredNetwork() {
+		List<AllocationNodeAP> nodes;
+		List<AllocationNodeAP> toBeReconfigured = new ArrayList<>();
+		Set<AllocationNodeAP> tmpToBeReconfigured;
+		List<AllocationNodeAP> 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<fp.getPath().size(); i++) {
+														an = fp.getPath().get(i);
+														//Search for the node when ap1 != ap2
+														if(an.getNode().getFunctionalType() != null 
+																&& an.getNode().getFunctionalType().value().equals("NAT")) {
+															//reconfigure previous node (if it is a FORWARDER)
+															if(fp.getPath().get(i-1).getNode().getFunctionalType() != null && fp.getPath().get(i-1).getNode().getFunctionalType().value().equals("FORWARDER"))
+																tmpFlowNodes.add(fp.getPath().get(i-1));
+
+														}
+														if(an.getIpAddress().equals(n.getIpAddress()))
+																break;
+													}
+												}
+											}
+										}
+									}
+								}
+							}
+							index++;
+						}
+						//if it found a flow which can pass from source to destination there is no need of reconfiguration
+						if(tmpFlowNodes.isEmpty()) {
+							found = true;
+							break;
+						} else {
+							tmpToBeReconfigured.addAll(tmpFlowNodes);
+						}
+					}
+					//found a flow which satisfy the requirement, could stop here
+					if(found) {
+						break;
+					}
+				}
+				if(!found) {
+					//add all blocking nodes to the list of reconfigured nodes
+					toBeReconfigured.addAll(tmpToBeReconfigured.stream()
+							.filter(n -> !toBeReconfigured.contains(n))
+							.collect(Collectors.toList()));
+				}
+			}
+		}
+		return toBeReconfigured;
+	}
+
+
 /*****************************************************AP duplicated methods**************************************************************************/
 	/**
 	 * This method allocates the functions on allocation nodes that are empty.