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, 0 insertions, 1185 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
deleted file mode 100644
index 1d31ae9..0000000
--- a/verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java
+++ /dev/null
@@ -1,1185 +0,0 @@
-/*******************************************************************************
- * 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;
- }
-
-}