summaryrefslogtreecommitdiffstats
path: root/verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java
diff options
context:
space:
mode:
Diffstat (limited to 'verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java')
-rw-r--r--verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java1185
1 files changed, 1185 insertions, 0 deletions
diff --git a/verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java b/verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java
new file mode 100644
index 0000000..1d31ae9
--- /dev/null
+++ b/verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java
@@ -0,0 +1,1185 @@
+/*******************************************************************************
+ * Copyright (c) 2017 Politecnico di Torino and others.
+ *
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Apache License, Version 2.0
+ * which accompanies this distribution, and is available at
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *******************************************************************************/
+
+package it.polito.escape.verify.service;
+
+import java.io.BufferedReader;
+import java.io.File;
+import java.io.FileWriter;
+import java.io.FilenameFilter;
+import java.io.IOException;
+import java.io.InputStreamReader;
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.Iterator;
+import java.util.List;
+import java.util.Locale;
+import java.util.Map;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+import java.util.stream.Collectors;
+
+import javax.tools.Diagnostic;
+import javax.tools.DiagnosticCollector;
+import javax.tools.JavaCompiler;
+import javax.tools.JavaFileObject;
+import javax.tools.StandardJavaFileManager;
+import javax.tools.ToolProvider;
+import javax.ws.rs.ProcessingException;
+import javax.xml.bind.JAXBException;
+
+import org.json.simple.JSONArray;
+import org.json.simple.JSONObject;
+
+import com.fasterxml.jackson.databind.JsonNode;
+
+import it.polito.escape.verify.client.Neo4jManagerClient;
+import it.polito.escape.verify.exception.BadRequestException;
+import it.polito.escape.verify.exception.DataNotFoundException;
+import it.polito.escape.verify.exception.ForbiddenException;
+import it.polito.escape.verify.exception.InternalServerErrorException;
+import it.polito.escape.verify.model.Configuration;
+import it.polito.escape.verify.model.Entry;
+import it.polito.escape.verify.model.Graph;
+import it.polito.escape.verify.model.Neighbour;
+import it.polito.escape.verify.model.Node;
+import it.polito.escape.verify.model.Test;
+import it.polito.escape.verify.model.Verification;
+import it.polito.escape.verify.resources.beans.VerificationBean;
+import it.polito.nffg.neo4j.jaxb.Paths;
+import qj.util.ReflectUtil;
+import qj.util.lang.DynamicClassLoader;
+
+public class VerificationService {
+
+ private static final String generatorFolder = System.getProperty("catalina.base")
+ + "/webapps/verify/WEB-INF/classes/tests/j-verigraph-generator";
+
+ private static final String generatorFolderForGrpc = "service/src/tests/j-verigraph-generator";
+
+ private String testClassGenerator = generatorFolder + "/test_class_generator.py";
+
+ private String testGenerator = generatorFolder + "/test_generator.py";
+
+ public VerificationService() {
+
+ }
+
+ private Paths getPaths(Graph graph, Node sourceNode, Node destinationNode) {
+
+ String source = sourceNode.getName() + "_" + sourceNode.getId();
+ String destination = destinationNode.getName() + "_" + destinationNode.getId();
+
+ List<String> endpoints = new ArrayList<>();
+ List<String> firewalls = new ArrayList<>();
+ Map<String, List<Entry>> routingTable = new HashMap<>();
+
+ for (Node node : graph.getNodes().values()) {
+ // if firewall
+ if (node.getFunctional_type().equals("NF")) {
+ // add 2 connection points to RT
+ routingTable.put(node.getName() + "_" + node.getId() + "_in", new ArrayList<Entry>());
+ routingTable.put(node.getName() + "_" + node.getId() + "_out", new ArrayList<Entry>());
+ // add node to firewalls
+ firewalls.add(node.getName() + "_" + node.getId());
+ // scan neighbours
+ for (Neighbour neighbour : node.getNeighbours().values()) {
+ // check if neighbour is a firewall
+ Node hop = graph.searchNodeByName(neighbour.getName());
+ // if neighbour is a firewall connect to its input port
+ if (hop.getFunctional_type().equals("NF"))
+ routingTable.get(node.getName() + "_" + node.getId() + "_out")
+ .add(new Entry("output", neighbour.getName() + "_" + hop.getId() + "_in"));
+ else
+ // connect
+ // normally to
+ // node
+ routingTable.get(node.getName() + "_" + node.getId()
+ + "_out")
+ .add(new Entry( "output",
+ neighbour.getName() + "_"
+ + hop.getId()));
+ }
+ }
+ // if endpoint
+ else {
+ // add endpoint to RT
+ routingTable.put(node.getName() + "_" + node.getId(), new ArrayList<Entry>());
+ // add to endpoints
+ endpoints.add(node.getName() + "_" + node.getId());
+ // scan neighbours
+ for (Neighbour neighbour : node.getNeighbours().values()) {
+ // check if neighbour is a firewall
+ Node hop = graph.searchNodeByName(neighbour.getName());
+ // if neighbour is a firewall connect to its input port
+ if (hop.getFunctional_type().equals("NF"))
+ routingTable.get(node.getName() + "_" + node.getId())
+ .add(new Entry("output", neighbour.getName() + "_" + hop.getId() + "_in"));
+ else {
+ // connect
+ // normally to
+ // node
+ routingTable.get(node.getName() + "_" + node.getId())
+ .add(new Entry("output", neighbour.getName() + "_" + hop.getId()));
+ }
+ }
+ }
+
+ // end node scan
+ }
+ // debug print
+ System.out.println("Endpoints:");
+ for (String endpoint : endpoints) {
+ System.out.println(endpoint);
+ }
+ System.out.println("Firewalls:");
+ for (String firewall : firewalls) {
+ System.out.println(firewall);
+ }
+ System.out.println("Source: " + source);
+ System.out.println("Destination: " + destination);
+ for (String key : routingTable.keySet()) {
+ System.out.println("RT for node " + key);
+ for (Entry entry : routingTable.get(key)) {
+ System.out.println("\t" + entry.getDirection() + "->" + entry.getDestination());
+ }
+ }
+ // end debug print
+
+ Neo4jManagerClient client = new Neo4jManagerClient( "http://localhost:8080/neo4jmanager/rest/",
+ source,
+ destination,
+ endpoints,
+ firewalls,
+ routingTable);
+
+ Paths paths = null;
+ try {
+ paths = client.getPaths();
+ }
+ catch (JAXBException e) {
+ throw new InternalServerErrorException("Error generating input for neo4jmanager: " + e.getMessage());
+ }
+ catch (ProcessingException e) {
+ throw new InternalServerErrorException("Response of neo4jmanager doesn't contain any path: "
+ + e.getMessage());
+ }
+ catch (IllegalStateException e) {
+ throw new InternalServerErrorException("Error getting a response from neo4jmanager, no input stream for paths or input stream already consumed: "
+ + e.getMessage());
+ }
+ catch (Exception e) {
+ throw new InternalServerErrorException("Unable to continue due to a neo4jmanager error: " + e.getMessage());
+ }
+
+ return paths;
+
+ }
+
+ private List<String> sanitizePath(String path) {
+ List<String> newPath = new ArrayList<String>();
+ // find all nodes, i.e. all names between parentheses
+ Matcher m = Pattern.compile("\\(([^)]+)\\)").matcher(path);
+ while (m.find()) {
+ String node = m.group(1);
+
+ int spaceIndex = node.lastIndexOf("_");
+ if (spaceIndex != -1) {
+ node = node.substring(0, spaceIndex);
+ newPath.add(node);
+ }
+ }
+ return newPath;
+
+ }
+
+ private List<List<String>> sanitizePaths(Paths paths) {
+ List<List<String>> sanitizedPaths = new ArrayList<List<String>>();
+ for (String path : paths.getPath()) {
+ System.out.println("Original path: " + path);
+ List<String> newPath = sanitizePath(path);
+ sanitizedPaths.add(newPath);
+ }
+ return sanitizedPaths;
+ }
+
+ static private Map<String, Long> toMap(List<String> lst) {
+ return lst.stream().collect(Collectors.groupingBy(s -> s, Collectors.counting()));
+ }
+
+ private void eliminateLoopsInPaths(List<List<String>> sanitizedPaths) {
+ List<List<String>> pathsToBeRemoved = new ArrayList<List<String>>();
+
+ for (List<String> path : sanitizedPaths) {
+ Map<String, Long> occurrencesMap = toMap(path);
+ for (long occurrences : occurrencesMap.values()) {
+ if (occurrences > 1) {
+ pathsToBeRemoved.add(path);
+ break;
+ }
+ }
+ }
+ for (List<String> path : pathsToBeRemoved) {
+ sanitizedPaths.remove(path);
+ }
+ }
+
+ private void printListsOfStrings(String message, List<List<String>> lists) {
+ System.out.println(message);
+ for (List<String> element : lists) {
+ System.out.println(element);
+ }
+ }
+
+ private static File createTempDir(String prefix) throws IOException {
+ String tmpDirStr = System.getProperty("java.io.tmpdir");
+ if (tmpDirStr == null) {
+ throw new IOException("System property 'java.io.tmpdir' does not specify a tmp dir");
+ }
+
+ File tmpDir = new File(tmpDirStr);
+ if (!tmpDir.exists()) {
+ boolean created = tmpDir.mkdirs();
+ if (!created) {
+ throw new IOException("Unable to create tmp dir " + tmpDir);
+ }
+ }
+
+ File resultDir = null;
+ int suffix = (int) System.currentTimeMillis();
+ int failureCount = 0;
+ do {
+ resultDir = new File(tmpDir, prefix + suffix % 10000);
+ suffix++;
+ failureCount++;
+ } while (resultDir.exists() && failureCount < 50);
+
+ if (resultDir.exists()) {
+ throw new IOException(failureCount
+ + " attempts to generate a non-existent directory name failed, giving up");
+ }
+ boolean created = resultDir.mkdir();
+ if (!created) {
+ throw new IOException("Failed to create tmp directory");
+ }
+
+ return resultDir;
+ }
+
+ @SuppressWarnings("unchecked")
+ private void generateChainsFile(Graph graph, List<List<String>> sanitizedPaths, String chainsFile) {
+ JSONObject root = new JSONObject();
+ JSONArray chains = new JSONArray();
+
+ int chainCounter = 0;
+
+ for (List<String> path : sanitizedPaths) {
+ Iterator<String> pathsIterator = path.iterator();
+ JSONObject chain = new JSONObject();
+ chain.put("id", ++chainCounter);
+ chain.put("flowspace", "tcp=80");
+ JSONArray nodes = new JSONArray();
+ while (pathsIterator.hasNext()) {
+ String nodeName = (String) pathsIterator.next();
+ Node currentNode = graph.searchNodeByName(nodeName);
+ if (currentNode == null) {
+ throw new InternalServerErrorException("Unable to generate 'chains.json' for neo4jmanager: node "
+ + nodeName + " not found");
+ }
+ JSONObject node = new JSONObject();
+ node.put("name", currentNode.getName());
+ // if(currentNode.getFunctional_type().equals("firewall"))
+ // node.put("address", "ip_nat");
+ // else
+ node.put("address", "ip_" + currentNode.getName());
+ node.put("functional_type", currentNode.getFunctional_type());
+ nodes.add(node);
+ chain.put("nodes", nodes);
+ }
+ chains.add(chain);
+ }
+ root.put("chains", chains);
+
+ try (FileWriter file = new FileWriter(chainsFile)) {
+ file.write(root.toJSONString());
+ System.out.println("Successfully created 'chains.json' with the following content:");
+ System.out.println(root);
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Error saving 'chains.json' for neo4jmanager");
+ }
+
+ }
+
+ @SuppressWarnings("unchecked")
+ private void generateConfigFile(Graph graph, String configFile) {
+ JSONObject root = new JSONObject();
+ JSONArray nodes = new JSONArray();
+
+ for (Node n : graph.getNodes().values()) {
+ JSONObject node = new JSONObject();
+ // JSONArray configuration = new JSONArray();
+ Configuration nodeConfig = n.getConfiguration();
+ JsonNode configuration = nodeConfig.getConfiguration();
+
+ node.put("configuration", configuration);
+ node.put("id", nodeConfig.getId());
+ node.put("description", nodeConfig.getDescription());
+
+ nodes.add(node);
+
+ }
+ root.put("nodes", nodes);
+
+ try (FileWriter file = new FileWriter(configFile)) {
+ file.write(root.toJSONString());
+ System.out.println("Successfully created 'config.json' with the following content:");
+ System.out.println(root);
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Error saving 'config.json' for neo4jmanager");
+ }
+
+ }
+
+ private void printCommand(String[] cmd) {
+ for (String c : cmd) {
+ System.out.printf(c + " ");
+ }
+ System.out.println("");
+ }
+
+ private String platfromIndependentPath(String path) {
+ path = path.replaceAll("/", Matcher.quoteReplacement(Character.toString(File.separatorChar)));
+ return path;
+ }
+
+ private void generateTestScenarios(String chainsFile, String configFile, String scenarioFile) {
+
+ String[] cmd = { "python", platfromIndependentPath(testClassGenerator), "-c",
+ platfromIndependentPath(chainsFile), "-f", platfromIndependentPath(configFile), "-o",
+ platfromIndependentPath(scenarioFile) };
+ printCommand(cmd);
+
+ ProcessBuilder pb = new ProcessBuilder(cmd);
+ pb.redirectErrorStream(true);
+ Process process;
+ try {
+ process = pb.start();
+
+ BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream()));
+ String line;
+ while ((line = reader.readLine()) != null)
+ System.out.println("test_class_generator.py: " + line);
+ process.waitFor();
+ if (process.exitValue() != 0) {
+ throw new InternalServerErrorException("Unable to generate test scenario file for the verification request: test_class_generator returned "
+ + process.exitValue());
+ }
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Error generating tests for Z3: unable to execute generator");
+ }
+ catch (InterruptedException e) {
+ throw new InternalServerErrorException("Error generating tests for Z3: generator got interrupted during execution");
+ }
+
+ }
+
+ private void generateTests( int scenariosCounter, String scenariosBasename, String source, String destination,
+ String testsBasename) {
+
+ List<String> scenarios = new ArrayList<String>();
+ List<String> tests = new ArrayList<String>();
+ for (int i = 0; i < scenariosCounter; i++) {
+ scenarios.add(scenariosBasename + "_" + (i + 1) + ".java");
+ tests.add(testsBasename + "_" + (i + 1) + ".java");
+ }
+
+ for (int i = 0; i < scenariosCounter; i++) {
+ String[] cmd = { "python", platfromIndependentPath(testGenerator), "-i",
+ platfromIndependentPath(scenarios.get(i)), "-o", platfromIndependentPath(tests.get(i)),
+ "-s", source, "-d", destination };
+ printCommand(cmd);
+
+ ProcessBuilder pb = new ProcessBuilder(cmd);
+ pb.redirectErrorStream(true);
+ Process process;
+ try {
+ process = pb.start();
+
+ BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream()));
+ String line;
+ while ((line = reader.readLine()) != null)
+ System.out.println("test_generator.py: " + line);
+ process.waitFor();
+ if (process.exitValue() != 0) {
+ throw new InternalServerErrorException("Unable to generate test file for the verification request: test_generator returned "
+ + process.exitValue());
+ }
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Error generating tests for Z3: unable to execute generator");
+ }
+ catch (InterruptedException e) {
+ throw new InternalServerErrorException("Error generating tests for Z3: generator got interrupted during execution");
+ }
+
+ }
+
+ }
+
+ private void prepareForCompilationAndExecution( int scenariosCounter, String scenarioBasename, String testBasename,
+ List<File> sourceFiles, List<File> classFiles) {
+ for (int i = 0; i < scenariosCounter; i++) {
+ String scenario = scenarioBasename + "_" + (i + 1) + ".java";
+ sourceFiles.add(new File(scenario));
+ System.out.println("Scenario file " + scenario + " added to compilation");
+
+ String testSource = testBasename + "_" + (i + 1) + ".java";
+ String testClass = testBasename + "_" + (i + 1);
+
+ sourceFiles.add(new File(testSource));
+ System.out.println("Test file " + testSource + " added to copilation");
+ classFiles.add(new File(testClass));
+ System.out.println("Test file " + testClass + " added to execution");
+ }
+ }
+
+ private void compileFiles(List<File> files, String folder) {
+
+ JavaCompiler compiler = ToolProvider.getSystemJavaCompiler();
+ if (compiler == null) {
+ throw new InternalServerErrorException("Error getting the Java compiler: JDK >= 1.8 required");
+ }
+ StandardJavaFileManager fileManager = compiler.getStandardFileManager(null, null, null);
+
+ try {
+ // fileManager.setLocation(StandardLocation.CLASS_OUTPUT,
+ // Arrays.asList(new File(projectFolder)));
+
+ // String z3 = "/usr/lib/com.microsoft.z3.jar";
+ // List<String> optionList = new ArrayList<String>();
+ // optionList.add("-classpath");
+ // optionList.add(System.getProperty("java.class.path") + ":" + z3);
+ List<String> optionList = new ArrayList<String>();
+ optionList.add("-d");
+ optionList.add(folder);
+ DiagnosticCollector<JavaFileObject> diagnostics = new DiagnosticCollector<>();
+
+ boolean success = compiler
+ .getTask( null,
+ fileManager,
+ diagnostics,
+ optionList,
+ null,
+ fileManager.getJavaFileObjectsFromFiles(files))
+ .call();
+ if (!success) {
+ Locale myLocale = Locale.getDefault();
+ StringBuilder msg = new StringBuilder();
+ msg.append("Error compiling Z3 test files: ");
+ for (Diagnostic<? extends JavaFileObject> err : diagnostics.getDiagnostics()) {
+ msg.append('\n');
+ msg.append(err.getKind());
+ msg.append(": ");
+ if (err.getSource() != null) {
+ msg.append(err.getSource().getName());
+ }
+ msg.append(':');
+ msg.append(err.getLineNumber());
+ msg.append(": ");
+ msg.append(err.getMessage(myLocale));
+ }
+ throw new InternalServerErrorException(msg.toString());
+ }
+ fileManager.close();
+
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Unable to set the location of the Z3 test files to be compiled");
+ }
+
+ }
+
+ private int runIt(File filename, String folder) {
+ int endIndex = filename.getName().lastIndexOf(".");
+ String filenameNoExtension;
+ if (endIndex == -1) {
+ filenameNoExtension = filename.getName();
+ }
+ else {
+ filenameNoExtension = filename.getName().substring(0, endIndex);
+ if (!filenameNoExtension.matches("\\w+")) {
+ filenameNoExtension = filename.getName();
+ }
+ }
+
+ System.out.println("Filename is: " + filenameNoExtension);
+ try {
+ Class<?> userClass = new DynamicClassLoader(folder).load("tests." + filenameNoExtension);
+ Object context = ReflectUtil.newInstance(userClass);
+ Object result = ReflectUtil.invoke("run", context);
+ return (int) result;
+ }
+ catch (Exception e) {
+ StringWriter errors = new StringWriter();
+ e.printStackTrace(new PrintWriter(errors));
+ throw new InternalServerErrorException("Error executing Z3 tests: " + e.getMessage()
+ + ". There are errors in the Z3 model.");
+ }
+ }
+
+ private List<Test> runFiles(String folder, List<List<String>> paths, Graph graph, List<File> files) {
+ List<Test> tests = new ArrayList<Test>();
+ for (int i = 0; i < files.size(); i++) {
+ System.out.println("Running test file \"" + files.get(i).getAbsolutePath() + "\"");
+ int result = runIt(files.get(i), folder);
+ System.out.println("Execution returned: " + result);
+
+ List<Node> path = new ArrayList<Node>();
+ for (String nodeString : paths.get(i)) {
+ Node node = graph.searchNodeByName(nodeString);
+ path.add(node);
+ }
+ Test t = new Test(path, result);
+ tests.add(t);
+ }
+
+ return tests;
+ }
+
+ @SuppressWarnings("unused")
+ private static boolean deleteDir(File dir) {
+ if (dir.isDirectory()) {
+ String[] children = dir.list();
+ for (int i = 0; i < children.length; i++) {
+ boolean success = deleteDir(new File(dir, children[i]));
+ if (!success) {
+ return false;
+ }
+ }
+ }
+
+ return dir.delete();
+
+ }
+
+ @SuppressWarnings("unused")
+ private void deleteFilesWithPrefix(String directory, String prefix, String extension) {
+ final File scenarioFolder = new File(directory);
+ final File[] scenarioFiles = scenarioFolder.listFiles(new FilenameFilter() {
+
+ @Override
+ public boolean accept(final File dir, final String name) {
+ return name.matches(prefix + ".*\\." + extension);
+ }
+ });
+ for (final File file : scenarioFiles) {
+ if (!file.delete()) {
+ System.err.println("Can't remove " + file.getAbsolutePath());
+ }
+ else {
+ System.out.println("Removed file " + file.getAbsolutePath());
+ }
+ }
+ }
+
+ public Verification verify(long graphId, VerificationBean verificationBean) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ GraphService graphService = new GraphService();
+ Graph graph = graphService.getGraph(graphId);
+ if (graph == null) {
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ }
+ String source = verificationBean.getSource();
+ String destination = verificationBean.getDestination();
+ String type = verificationBean.getType();
+ if (source == null || source.equals("")) {
+ throw new BadRequestException("Please specify the 'source' parameter in your request");
+ }
+ if (destination == null || destination.equals("")) {
+ throw new BadRequestException("Please specify the 'destination' parameter in your request");
+ }
+ if (type == null || type.equals("")) {
+ throw new BadRequestException("Please specify the 'type' parameter in your request");
+ }
+
+ Node sourceNode = graph.searchNodeByName(verificationBean.getSource());
+ Node destinationNode = graph.searchNodeByName(verificationBean.getDestination());
+
+ if (sourceNode == null) {
+ throw new BadRequestException("The 'source' parameter '" + source + "' is not valid, please insert the name of an existing node");
+ }
+ if (destinationNode == null) {
+ throw new BadRequestException("The 'destination' parameter '" + destination + "' is not valid, please insert the name of an existing node");
+ }
+ if ((!type.equals("reachability")) && (!type.equals("isolation")) && (!type.equals("traversal"))) {
+ throw new BadRequestException("The 'type' parameter '" + type
+ + "' is not valid: valid types are: 'reachability', 'isolation' and 'traversal'");
+ }
+
+ Verification v = null;
+ String middlebox;
+ Node middleboxNode;
+ switch (type) {
+ case "reachability":
+ v = reachabilityVerification(graph, sourceNode, destinationNode);
+ break;
+ case "isolation":
+ middlebox = verificationBean.getMiddlebox();
+ if (middlebox == null || middlebox.equals("")) {
+ throw new BadRequestException("Please specify the 'middlebox' parameter in your request");
+ }
+
+ middleboxNode = graph.searchNodeByName(middlebox);
+ if (middleboxNode == null) {
+ throw new BadRequestException("The 'middlebox' parameter '" + middlebox + "' is not valid, please insert the name of an existing node");
+ }
+ if (middleboxNode.getFunctional_type().equals("endpoint")) {
+ throw new BadRequestException("'" + middlebox
+ + "' is of type 'endpoint', please choose a valid middlebox");
+ }
+ v = isolationVerification(graph, sourceNode, destinationNode, middleboxNode);
+ break;
+ case "traversal":
+ middlebox = verificationBean.getMiddlebox();
+ if (middlebox == null || middlebox.equals("")) {
+ throw new BadRequestException("Please specify the 'middlebox' parameter in your request");
+ }
+
+ middleboxNode = graph.searchNodeByName(middlebox);
+ if (middleboxNode == null) {
+ throw new BadRequestException("The 'middlebox' parameter '" + middlebox + "' is not valid, please insert the name of an existing node");
+ }
+ if (middleboxNode.getFunctional_type().equals("endpoint")) {
+ throw new BadRequestException("'" + middlebox
+ + "' is of type 'endpoint', please choose a valid middlebox");
+ }
+ v = traversalVerification(graph, sourceNode, destinationNode, middleboxNode);
+ break;
+ default:
+ break;
+ }
+
+ return v;
+ }
+
+ private Verification isolationVerification(Graph graph, Node sourceNode, Node destinationNode, Node middleboxNode) {
+
+ Paths paths = getPaths(graph, sourceNode, destinationNode);
+ if (paths.getPath().size() == 0) {
+ return new Verification("UNSAT",
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "'");
+ }
+
+ List<List<String>> sanitizedPaths = sanitizePaths(paths);
+
+ printListsOfStrings("Before loops removal", sanitizedPaths);
+
+ eliminateLoopsInPaths(sanitizedPaths);
+
+ printListsOfStrings("After loops removal", sanitizedPaths);
+
+ if (sanitizedPaths.isEmpty()) {
+ return new Verification("UNSAT",
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "'");
+ }
+
+ List<Test> tests = extractTestsFromPaths(graph, sanitizedPaths, "UNKNWON");
+
+ extractPathsWithMiddlebox(sanitizedPaths, middleboxNode.getName());
+
+ if (sanitizedPaths.isEmpty()) {
+ return new Verification("UNSAT",
+ tests,
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "' which traverse middlebox '"
+ + middleboxNode.getName() + "'. See below all the available paths.");
+ }
+
+ printListsOfStrings("Paths with middlebox '" + middleboxNode.getName() + "'", sanitizedPaths);
+
+ File tempDir = null;
+
+ try {
+ tempDir = createTempDir("isolation");
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Unable to perform verification: " + e.getMessage());
+ }
+
+ String chainsFile = tempDir.getAbsolutePath() + "/chains.json";
+ generateChainsFile(graph, sanitizedPaths, chainsFile);
+
+ String configFile = tempDir.getAbsolutePath() + "/config.json";
+ generateConfigFile(graph, configFile);
+
+ String isolationScenariosBasename = tempDir.getAbsolutePath() + "/IsolationScenario";
+ try{
+ generateTestScenarios(chainsFile, configFile, isolationScenariosBasename);
+ }catch(Exception ex){
+ testClassGenerator = generatorFolderForGrpc + "/test_class_generator.py";
+ generateTestScenarios(chainsFile, configFile, isolationScenariosBasename);
+ }
+
+ String isolationTestsBasename = tempDir.getAbsolutePath() + "/IsolationTest";
+ try{
+ generateTests( sanitizedPaths.size(),
+ isolationScenariosBasename,
+ sourceNode.getName(),
+ middleboxNode.getName(),
+ isolationTestsBasename);
+ }catch(InternalServerErrorException ex){
+ testGenerator = generatorFolderForGrpc + "/test_generator.py";
+ generateTests( sanitizedPaths.size(),
+ isolationScenariosBasename,
+ sourceNode.getName(),
+ middleboxNode.getName(),
+ isolationTestsBasename);
+ }
+
+ List<File> sourceFiles = new ArrayList<File>();
+ List<File> classFiles = new ArrayList<File>();
+ prepareForCompilationAndExecution( sanitizedPaths.size(),
+ isolationScenariosBasename,
+ isolationTestsBasename,
+ sourceFiles,
+ classFiles);
+
+ compileFiles(sourceFiles, tempDir.getAbsolutePath());
+
+ tests = runFiles(tempDir.getAbsolutePath(), sanitizedPaths, graph, classFiles);
+
+ return evaluateIsolationResults(tests,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ middleboxNode.getName());
+
+ }
+
+ private List<Test> extractTestsFromPaths(Graph graph, List<List<String>> paths, String result) {
+ List<Test> tests = new ArrayList<Test>();
+ for (List<String> path : paths) {
+ List<Node> nodes = new ArrayList<Node>();
+ for (String nodeName : path) {
+ nodes.add(graph.searchNodeByName(nodeName));
+ }
+ tests.add(new Test(nodes, result));
+ }
+ return tests;
+ }
+
+ private Verification evaluateIsolationResults( List<Test> tests, String source, String destination,
+ String middlebox) {
+ Verification v = new Verification();
+ boolean isSat = false;
+ int unsatCounter = 0;
+ for (Test t : tests) {
+ v.getTests().add(t);
+
+ if (t.getResult().equals("SAT")) {
+ isSat = true;
+ }
+ else if (t.getResult().equals("UNKNOWN")) {
+ v.setResult("UNKNWON");
+ v.setComment("Isolation property with source '" + source + "', destination '" + destination
+ + "' and middlebox '" + middlebox + "' is UNKNOWN because although '" + source
+ + "' cannot reach '" + middlebox + "' in any path from '" + source + "' to '"
+ + destination + "' which traverses middlebox '" + middlebox
+ + "' at least one reachability test between '" + source + "' and '" + middlebox
+ + "' returned UNKNOWN (see below all the paths that have been checked)");
+ }
+ else if (t.getResult().equals("UNSAT")) {
+ unsatCounter++;
+ }
+ }
+ if (isSat) {
+ v.setResult("UNSAT");
+ v.setComment("Isolation property with source '" + source + "', destination '" + destination
+ + "' and middlebox '" + middlebox + "' is UNSATISFIED because reachability between '"
+ + source + "' and '" + middlebox + "' is SATISFIED in at least one path between '" + source
+ + "' and '" + destination + "' which traverses middlebox '" + middlebox
+ + "' (see below all the paths that have been checked)");
+ }
+ else if (unsatCounter == tests.size()) {
+ v.setResult("SAT");
+ v.setComment("Isolation property with source '" + source + "', destination '" + destination
+ + "' and middlebox '" + middlebox + "' is SATISFIED because reachability between '" + source
+ + "' and '" + middlebox + "' is UNSATISFIED in all paths between '" + source + "' and '"
+ + destination + "' which traverse middlebox '" + middlebox
+ + "' (see below all the paths that have been checked)");
+ }
+ return v;
+
+ }
+
+ private void extractPathsWithMiddlebox(List<List<String>> sanitizedPaths, String middleboxName) {
+ List<List<String>> pathsToBeRemoved = new ArrayList<List<String>>();
+ for (List<String> path : sanitizedPaths) {
+ boolean middleboxFound = false;
+ for (String node : path) {
+ if (node.equals(middleboxName)) {
+ middleboxFound = true;
+ break;
+ }
+ }
+ if (!middleboxFound) {
+ pathsToBeRemoved.add(path);
+ }
+ }
+
+ for (List<String> path : pathsToBeRemoved) {
+ sanitizedPaths.remove(path);
+ }
+
+ }
+
+ private void extractPathsWithoutMiddlebox(List<List<String>> sanitizedPaths, String middleboxName) {
+ List<List<String>> pathsToBeRemoved = new ArrayList<List<String>>();
+ for (List<String> path : sanitizedPaths) {
+ boolean middleboxFound = false;
+ for (String node : path) {
+ if (node.equals(middleboxName)) {
+ middleboxFound = true;
+ break;
+ }
+ }
+ if (middleboxFound) {
+ pathsToBeRemoved.add(path);
+ }
+ }
+
+ for (List<String> path : pathsToBeRemoved) {
+ sanitizedPaths.remove(path);
+ }
+
+ }
+
+ private Verification traversalVerification(Graph graph, Node sourceNode, Node destinationNode, Node middleboxNode) {
+
+ Paths paths = getPaths(graph, sourceNode, destinationNode);
+ if (paths.getPath().size() == 0) {
+ return new Verification("UNSAT",
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "'");
+ }
+
+ List<List<String>> pathsBetweenSourceAndDestination = sanitizePaths(paths);
+
+ printListsOfStrings("Before loops removal", pathsBetweenSourceAndDestination);
+
+ eliminateLoopsInPaths(pathsBetweenSourceAndDestination);
+
+ printListsOfStrings("After loops removal", pathsBetweenSourceAndDestination);
+
+ if (pathsBetweenSourceAndDestination.isEmpty()) {
+ return new Verification("UNSAT",
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "'");
+ }
+
+ List<Test> tests = extractTestsFromPaths(graph, pathsBetweenSourceAndDestination, "UNKNOWN");
+
+ List<List<String>> pathsWithMiddlebox = new ArrayList<List<String>>();
+ for (List<String> path : pathsBetweenSourceAndDestination) {
+ pathsWithMiddlebox.add(path);
+ }
+
+ extractPathsWithMiddlebox(pathsWithMiddlebox, middleboxNode.getName());
+
+ if (pathsWithMiddlebox.isEmpty()) {
+ return new Verification("UNSAT",
+ tests,
+ "There are no paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "' which traverse middlebox '"
+ + middleboxNode.getName() + "'. See below all the available paths");
+ }
+
+ printListsOfStrings("Paths with middlebox '" + middleboxNode.getName() + "'", pathsWithMiddlebox);
+
+ File tempDir = null;
+
+ try {
+ tempDir = createTempDir("traversal");
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Unable to perform verification: " + e.getMessage());
+ }
+
+ String chainsFile = tempDir.getAbsolutePath() + "/chains.json";
+ generateChainsFile(graph, pathsWithMiddlebox, chainsFile);
+
+ String configFile = tempDir.getAbsolutePath() + "/config.json";
+ generateConfigFile(graph, configFile);
+
+ String traversalScenariosBasename = tempDir.getAbsolutePath() + "/TraversalScenario";
+ try{
+ generateTestScenarios(chainsFile, configFile, traversalScenariosBasename);
+ }catch(Exception ex){
+ testClassGenerator = generatorFolderForGrpc + "/test_class_generator.py";
+ generateTestScenarios(chainsFile, configFile, traversalScenariosBasename);
+ }
+
+ String traversalTestsBasename = tempDir.getAbsolutePath() + "/TraversalTest";
+ try{
+ generateTests( pathsWithMiddlebox.size(),
+ traversalScenariosBasename,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ traversalTestsBasename);
+ }catch(InternalServerErrorException ex){
+ testGenerator = generatorFolderForGrpc + "/test_generator.py";
+ generateTests( pathsWithMiddlebox.size(),
+ traversalScenariosBasename,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ traversalTestsBasename);
+ }
+ List<File> sourceFiles = new ArrayList<File>();
+ List<File> classFiles = new ArrayList<File>();
+ prepareForCompilationAndExecution( pathsWithMiddlebox.size(),
+ traversalScenariosBasename,
+ traversalTestsBasename,
+ sourceFiles,
+ classFiles);
+
+ compileFiles(sourceFiles, tempDir.getAbsolutePath());
+
+ tests = runFiles(tempDir.getAbsolutePath(), pathsWithMiddlebox, graph, classFiles);
+
+ for (Test t : tests) {
+ if (t.getResult().equals("UNSAT")) {
+ return new Verification("UNSAT",
+ tests,
+ "There is at least a path between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "' traversing middlebox '"
+ + middleboxNode.getName() + "' where '" + sourceNode.getName()
+ + "' cannot reach '" + destinationNode.getName()
+ + "'. See below the paths that have been checked");
+ }
+ if (t.getResult().equals("UNKNOWN")) {
+ return new Verification("UNKNOWN",
+ tests,
+ "There is at least a path between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "' traversing middlebox '"
+ + middleboxNode.getName() + "' where it is not guaranteed that '"
+ + sourceNode.getName() + "' can effectively reach '"
+ + destinationNode.getName()
+ + "'. See below the paths that have been checked");
+ }
+ }
+
+ extractPathsWithoutMiddlebox(pathsBetweenSourceAndDestination, middleboxNode.getName());
+ printListsOfStrings("Paths without middlebox '" + middleboxNode.getName() + "'", pathsBetweenSourceAndDestination);
+
+ if (pathsBetweenSourceAndDestination.isEmpty()) {
+ return new Verification("SAT",
+ tests,
+ "All the paths between node '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "' traverse middlebox '"
+ + middleboxNode.getName() + "'");
+ }
+
+ tempDir = null;
+
+ try {
+ tempDir = createTempDir("traversal");
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Unable to perform verification: " + e.getMessage());
+ }
+
+ chainsFile = tempDir.getAbsolutePath() + "/chains.json";
+ generateChainsFile(graph, pathsBetweenSourceAndDestination, chainsFile);
+
+ configFile = tempDir.getAbsolutePath() + "/config.json";
+ generateConfigFile(graph, configFile);
+
+ traversalScenariosBasename = tempDir.getAbsolutePath() + "/TraversalScenario";
+ generateTestScenarios(chainsFile, configFile, traversalScenariosBasename);
+
+ traversalTestsBasename = tempDir.getAbsolutePath() + "/TraversalTest";
+ generateTests( pathsBetweenSourceAndDestination.size(),
+ traversalScenariosBasename,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ traversalTestsBasename);
+
+ sourceFiles = new ArrayList<File>();
+ classFiles = new ArrayList<File>();
+ prepareForCompilationAndExecution( pathsBetweenSourceAndDestination.size(),
+ traversalScenariosBasename,
+ traversalTestsBasename,
+ sourceFiles,
+ classFiles);
+
+ compileFiles(sourceFiles, tempDir.getAbsolutePath());
+
+ tests = runFiles(tempDir.getAbsolutePath(), pathsBetweenSourceAndDestination, graph, classFiles);
+
+ return evaluateTraversalResults(tests,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ middleboxNode.getName());
+
+ }
+
+ private Verification evaluateTraversalResults( List<Test> tests, String source, String destination,
+ String middlebox) {
+ Verification v = new Verification();
+ boolean isSat = false;
+ int unsatCounter = 0;
+ for (Test t : tests) {
+ v.getTests().add(t);
+
+ if (t.getResult().equals("SAT")) {
+ isSat = true;
+ }
+ else if (t.getResult().equals("UNKNOWN")) {
+ v.setResult("UNKNWON");
+ v.setComment("There is at least one path from '" + source + "' to '" + destination
+ + "' that doesn't traverse middlebox '" + middlebox
+ + "' (see below all the paths that have been checked)");
+ }
+ else if (t.getResult().equals("UNSAT")) {
+ unsatCounter++;
+ }
+ }
+ if (isSat) {
+ v.setResult("UNSAT");
+ v.setComment("There is at least one path from '" + source + "' to '" + destination
+ + "' that doesn't traverse middlebox '" + middlebox
+ + "' (see below all the paths that have been checked)");
+ }
+ else if (unsatCounter == tests.size()) {
+ v.setResult("SAT");
+ v.setComment("The only available paths from '" + source + "' to '" + destination
+ + "' are those that traverse middlebox '" + middlebox
+ + "' (see below the alternative paths that have been checked and are unusable)");
+ }
+ return v;
+ }
+
+ private Verification reachabilityVerification(Graph graph, Node sourceNode, Node destinationNode) {
+ Paths paths = getPaths(graph, sourceNode, destinationNode);
+
+ if (paths.getPath().size() == 0) {
+ return new Verification("UNSAT",
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "'");
+ }
+
+ List<List<String>> sanitizedPaths = sanitizePaths(paths);
+
+ printListsOfStrings("Before loops removal", sanitizedPaths);
+
+ eliminateLoopsInPaths(sanitizedPaths);
+
+ printListsOfStrings("After loops removal", sanitizedPaths);
+
+ if (sanitizedPaths.isEmpty()) {
+ return new Verification("UNSAT",
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "'");
+ }
+
+ File tempDir = null;
+
+ try {
+ tempDir = createTempDir("reachability");
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Unable to perform verification: " + e.getMessage());
+ }
+
+ String chainsFile = tempDir.getAbsolutePath() + "/chains.json";
+ generateChainsFile(graph, sanitizedPaths, chainsFile);
+
+ String configFile = tempDir.getAbsolutePath() + "/config.json";
+ generateConfigFile(graph, configFile);
+
+ String reachabilityScenariosBasename = tempDir.getAbsolutePath() + "/ReachabilityScenario";
+ try{
+ generateTestScenarios(chainsFile, configFile, reachabilityScenariosBasename);
+ }catch(InternalServerErrorException ex){
+ testClassGenerator = generatorFolderForGrpc + "/test_class_generator.py";
+ generateTestScenarios(chainsFile, configFile, reachabilityScenariosBasename);
+ }
+
+
+ String reachabilityTestsBasename = tempDir.getAbsolutePath() + "/ReachabilityTest";
+ try{
+ generateTests( sanitizedPaths.size(),
+ reachabilityScenariosBasename,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ reachabilityTestsBasename);
+ }catch(InternalServerErrorException ex){
+ testGenerator = generatorFolderForGrpc + "/test_generator.py";
+ generateTests( sanitizedPaths.size(),
+ reachabilityScenariosBasename,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ reachabilityTestsBasename);
+ }
+ List<File> sourceFiles = new ArrayList<File>();
+ List<File> classFiles = new ArrayList<File>();
+ prepareForCompilationAndExecution( sanitizedPaths.size(),
+ reachabilityScenariosBasename,
+ reachabilityTestsBasename,
+ sourceFiles,
+ classFiles);
+
+ compileFiles(sourceFiles, tempDir.getAbsolutePath());
+
+ List<Test> tests = runFiles(tempDir.getAbsolutePath(), sanitizedPaths, graph, classFiles);
+
+ return evaluateReachabilityResult(tests, sourceNode.getName(), destinationNode.getName());
+ }
+
+ private Verification evaluateReachabilityResult(List<Test> tests, String source, String destination) {
+ Verification v = new Verification();
+ boolean sat = false;
+ int unsat = 0;
+ for (Test t : tests) {
+ v.getTests().add(t);
+
+ if (t.getResult().equals("SAT")) {
+ sat = true;
+ }
+ else if (t.getResult().equals("UNKNOWN")) {
+ v.setResult("UNKNWON");
+ v.setComment("Reachability from '" + source + "' to '" + destination
+ + "' is unknown. See all the checked paths below");
+ }
+ else if (t.getResult().equals("UNSAT")) {
+ unsat++;
+ }
+ }
+ if (sat) {
+ v.setResult("SAT");
+ v.setComment("There is at least one path '" + source + "' can use to reach '" + destination
+ + "'. See all the available paths below");
+ }
+ else if (unsat == tests.size()) {
+ v.setResult("UNSAT");
+ v.setComment("There isn't any path '" + source + "' can use to reach '" + destination
+ + "'. See all the checked paths below");
+ }
+ return v;
+ }
+
+}