diff --git a/src/main/java/cli/PatternHandling.java b/src/main/java/cli/DiplodocusPatternHandling.java similarity index 99% rename from src/main/java/cli/PatternHandling.java rename to src/main/java/cli/DiplodocusPatternHandling.java index 406fcd48e5c936fb5fe67469ef92c6aaf15a366f..a455b572dc0289cf94778bec23a9f0ad7edcfe26 100644 --- a/src/main/java/cli/PatternHandling.java +++ b/src/main/java/cli/DiplodocusPatternHandling.java @@ -83,7 +83,7 @@ import ui.TURTLEPanel; * @author Jawher JERRAY */ -public class PatternHandling extends Command { +public class DiplodocusPatternHandling extends Command { private final static String SYNTAX_ERROR = "Syntax Error"; private final static String NO_NAME_NO_TASK_FOR_PATTERN = "No name or no tasks is giving for the pattern"; @@ -134,7 +134,7 @@ public class PatternHandling extends Command { private String selectedPatternToIntergrate, selectedPatternPathToIntergrate, selectedJsonFilePath; - public PatternHandling() { + public DiplodocusPatternHandling() { } diff --git a/src/main/java/cli/Interpreter.java b/src/main/java/cli/Interpreter.java index 52e9afed35952ff6b9d8c9be2ef03ae53ad32598..f3b233edbd25680dd7c3024a998e9d5805df29c9 100644 --- a/src/main/java/cli/Interpreter.java +++ b/src/main/java/cli/Interpreter.java @@ -60,7 +60,7 @@ import java.util.Vector; public class Interpreter implements Runnable, TerminalProviderInterface { public final static Command[] commands = {new Action(), new Chat(), new Help(), new HelpTTool(), new History(), new Print(), - new Plan(), new PluginAction(), new PatternHandling(), new Quit(), + new Plan(), new PluginAction(), new DiplodocusPatternHandling(), new Quit(), new TestSpecific(), new TML(), new Set(), new Wait(), new Robot(), new BF(), new SimulatorScript()}; // Errors diff --git a/src/main/java/tmltranslator/patternhandling/SecurityGenerationForTMAP.java b/src/main/java/tmltranslator/patternhandling/SecurityGenerationForTMAP.java index 796d9b6ea6eb0660826043b92eafea4383a24e64..f7a924dbc5825d54e11e6eb22d2e6394badceaad 100644 --- a/src/main/java/tmltranslator/patternhandling/SecurityGenerationForTMAP.java +++ b/src/main/java/tmltranslator/patternhandling/SecurityGenerationForTMAP.java @@ -65,6 +65,7 @@ import java.io.BufferedReader; import java.io.InputStreamReader; import java.io.Reader; import java.util.*; +import java.util.concurrent.*; public class SecurityGenerationForTMAP implements Runnable { @@ -77,6 +78,7 @@ public class SecurityGenerationForTMAP implements Runnable { private final String decComp; private final List<String> selectedTasks; private final boolean linkedHSMs; + private int timeOutInSeconds = 0; private final Map<TMLTask, List<TMLTask>> taskAndItsHSMMap = new HashMap<>(); private final Map<TMLTask, List<HwCommunicationNode>> taskHSMCommunicationNodesMap = new HashMap<>(); @@ -100,6 +102,18 @@ public class SecurityGenerationForTMAP implements Runnable { this.selectedTasks = selectedTasks; this.linkedHSMs = isLinkedHSMs; } + + public SecurityGenerationForTMAP(String appName, TMLMapping<?> tmap, String encComp, String overhead, String decComp, + List<String> selectedTasks, boolean isLinkedHSMs, int timeOutInSeconds) { + this.appName = appName; + this.tmap = tmap; + this.overhead = overhead; + this.decComp = decComp; + this.encComp = encComp; + this.selectedTasks = selectedTasks; + this.linkedHSMs = isLinkedHSMs; + this.timeOutInSeconds = timeOutInSeconds; + } private void proverifAnalysis(TMLMapping<?> tmap, List<TMLChannel> nonConfChans, List<TMLChannel> nonWeakAuthChans, List<TMLChannel> nonStrongAuthChans) { @@ -127,18 +141,38 @@ public class SecurityGenerationForTMAP implements Runnable { FileUtils.saveFile(ConfigurationTTool.ProVerifCodeDirectory + "pvspec", proverifSpec.getStringSpec()); String cmd = ConfigurationTTool.ProVerifVerifierPath + " -in pitype " + ConfigurationTTool.ProVerifCodeDirectory + "pvspec"; - Process process; - Reader data; - try { - process = Runtime.getRuntime().exec(cmd); - data = new BufferedReader(new InputStreamReader(process.getInputStream())); - } catch (Exception e) { - TraceManager.addDev("FAILED: executing: " + cmd + ": " + e.getMessage()); - throw new RuntimeException(e); + final Process[] process = new Process[1]; + final Reader[] data = new Reader[1]; + final ExecutorService executor = Executors.newSingleThreadExecutor(); + if (timeOutInSeconds > 0) { + try { + process[0] = Runtime.getRuntime().exec(cmd); + data[0] = new BufferedReader(new InputStreamReader(process[0].getInputStream())); + } catch (Exception e) { + TraceManager.addDev("FAILED: executing: " + cmd + ": " + e.getMessage()); + throw new RuntimeException(e); + } + } else { + final Future<?> future = executor.submit(() -> { + try { + process[0] = Runtime.getRuntime().exec(cmd); + data[0] = new BufferedReader(new InputStreamReader(process[0].getInputStream())); + } catch (Exception e) { + TraceManager.addDev("FAILED: executing: " + cmd + ": " + e.getMessage()); + throw new RuntimeException(e); + } + }); + try { + future.get(timeOutInSeconds, TimeUnit.SECONDS); + } catch (TimeoutException | InterruptedException | ExecutionException e) { + future.cancel(true); + throw new RuntimeException(e); + } finally { + executor.shutdown(); + } } - ProVerifOutputAnalyzer pvoa = avatar2proverif.getOutputAnalyzer(); - pvoa.analyzeOutput(data, true); + pvoa.analyzeOutput(data[0], true); if (pvoa.getResults().isEmpty()) { TraceManager.addDev("SECGEN ERROR: No security results"); @@ -1541,4 +1575,8 @@ public class SecurityGenerationForTMAP implements Runnable { return tmap; } + public void setTimeOutInSeconds(int timeOutInSeconds) { + this.timeOutInSeconds = timeOutInSeconds; + } + } diff --git a/ttool/src/test/java/cli/CLIPatternHandlingTest.java b/ttool/src/test/java/cli/CLIDiplodocusPatternHandlingTest.java similarity index 96% rename from ttool/src/test/java/cli/CLIPatternHandlingTest.java rename to ttool/src/test/java/cli/CLIDiplodocusPatternHandlingTest.java index ac339612ecbbed3a6deacc908e5e53d61d53b7ac..4b48dd9368514e199b630592b04a3f9dbf7142ce 100644 --- a/ttool/src/test/java/cli/CLIPatternHandlingTest.java +++ b/ttool/src/test/java/cli/CLIDiplodocusPatternHandlingTest.java @@ -62,7 +62,7 @@ import tmltranslator.TMLSyntaxChecking; import tmltranslator.TMLError; -public class CLIPatternHandlingTest extends AbstractTest implements InterpreterOutputInterface { +public class CLIDiplodocusPatternHandlingTest extends AbstractTest implements InterpreterOutputInterface { private final static String PATH_TO_TEST_FILE = "cli/testPatternHandling/"; private static final String PATH_PATTERNS [] = {PATH_TO_TEST_FILE + "tmr/"}; @@ -84,7 +84,7 @@ public class CLIPatternHandlingTest extends AbstractTest implements InterpreterO private StringBuilder outputResult; private List<String> errorOutputs = new ArrayList<String>(); - public CLIPatternHandlingTest() { + public CLIDiplodocusPatternHandlingTest() { // } @@ -223,7 +223,7 @@ public class CLIPatternHandlingTest extends AbstractTest implements InterpreterO assertTrue(scriptConfig.length() > 0); Interpreter interpretConfigModel = new Interpreter(scriptConfig, (InterpreterOutputInterface)this, false); String interp = interpretConfigModel.interpretUntilError(); - assertTrue("expected error: ", interp.equals(PatternHandling.PATTERN_NOT_CONNECTED)); + assertTrue("expected error: ", interp.equals(DiplodocusPatternHandling.PATTERN_NOT_CONNECTED)); //TraceManager.addDev("\noutputResult:>" + outputResult); //assertTrue("comparing between 2 TML files", outputResult.equals(PatternHandling.PATTERN_NOT_CONNECTED)); diff --git a/ttool/src/test/java/test/AbstractTest.java b/ttool/src/test/java/test/AbstractTest.java index 8e9f030485abec527520927fb8c5c4de3b14ecea..7a29150c39b2c93c166ae7e57ea64387706ebb61 100644 --- a/ttool/src/test/java/test/AbstractTest.java +++ b/ttool/src/test/java/test/AbstractTest.java @@ -17,6 +17,7 @@ import java.nio.file.Paths; import java.util.ArrayList; import java.util.HashMap; import java.util.List; +import java.util.concurrent.*; import java.util.regex.Matcher; import java.util.regex.Pattern; import java.util.stream.Stream; @@ -225,41 +226,52 @@ public abstract class AbstractTest { alreadyMapComm.clear(); } String cmd = "proverif -in pitype " + pvspecPath; - Process process; - BufferedReader cmdOutput; - try { - process = Runtime.getRuntime().exec(cmd); - cmdOutput = new BufferedReader(new InputStreamReader(process.getInputStream())); - String outputLine; - int checked = 0; - - while ((outputLine = cmdOutput.readLine()) != null) { - if (outputLine.startsWith(PROVERIF_RESULT_PREFIX)) { - if (!idIssue) { - TraceManager.addDev("ProVerif Output : " + outputLine); - if (golden.contains(outputLine)) { - checked += 1; + final Process[] process = new Process[1]; + final BufferedReader[] cmdOutput = new BufferedReader[1]; + int timeOutInSeconds = 10; + final ExecutorService executor = Executors.newSingleThreadExecutor(); + final Future<?> future = executor.submit(() -> { + try { + process[0] = Runtime.getRuntime().exec(cmd); + cmdOutput[0] = new BufferedReader(new InputStreamReader(process[0].getInputStream())); + String outputLine; + int checked = 0; + while ((outputLine = cmdOutput[0].readLine()) != null) { + if (outputLine.startsWith(PROVERIF_RESULT_PREFIX)) { + if (!idIssue) { + TraceManager.addDev("ProVerif Output : " + outputLine); + if (golden.contains(outputLine)) { + checked += 1; + } else { + return false; + } } else { - return false; + TraceManager.addDev("ProVerif Output : " + outputLine); + assertTrue(golden.size() > checked); + assertTrue(equalsWithIdIssues(golden.get(checked), outputLine)); + checked++; } - } else { - TraceManager.addDev("ProVerif Output : " + outputLine); - assertTrue(golden.size() > checked); - assertTrue(equalsWithIdIssues(golden.get(checked), outputLine)); - checked++; } } - } - if (golden.size() != 1 || !golden.get(0).isEmpty()) { - return golden.size() == checked; + if (golden.size() != 1 || !golden.get(0).isEmpty()) { + return golden.size() == checked; + } + return false; + } catch (Exception e) { + TraceManager.addDev("FAILED: executing: " + cmd + ": " + e.getMessage()); + throw new RuntimeException(e); } - return false; - - } catch (Exception e) { - TraceManager.addDev("FAILED: executing: " + cmd + ": " + e.getMessage()); + }); + try { + future.get(timeOutInSeconds, TimeUnit.SECONDS); + } catch (TimeoutException | InterruptedException | ExecutionException e) { + future.cancel(true); throw new RuntimeException(e); + } finally { + executor.shutdown(); } + return true; } public static List<String> generateGoldenList(String goldenPath) throws IOException { diff --git a/ttool/src/test/java/tmltranslator/AutoSecurityGenerationDiplodocusTest.java b/ttool/src/test/java/tmltranslator/AutoSecurityGenerationDiplodocusTest.java index 4a14b97fa026325e29eacf1f3cca65c4a12f6bb5..53b0107f569541c0dd3bf55e948c6abfaa91e65d 100644 --- a/ttool/src/test/java/tmltranslator/AutoSecurityGenerationDiplodocusTest.java +++ b/ttool/src/test/java/tmltranslator/AutoSecurityGenerationDiplodocusTest.java @@ -152,7 +152,7 @@ public class AutoSecurityGenerationDiplodocusTest extends AbstractTest { ConfigurationTTool.ProVerifCodeDirectory = pathDirJsonFile; SecurityGenerationForTMAP secgen = new SecurityGenerationForTMAP(tabName, tmap, Integer.toString(ENCRYPTION_COMPUTATION), - Integer.toString(OVERHEAD), Integer.toString(DECRYPTION_COMPUTATION), selectedTasksHSM, isDirectConnectHSM); + Integer.toString(OVERHEAD), Integer.toString(DECRYPTION_COMPUTATION), selectedTasksHSM, isDirectConnectHSM, 600); tmap = secgen.startThread(); if (tmap != null) { diff --git a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java index bdc902064fe08c2271408e38222cf4c4941f27f4..4420489e555e9a8bd6a36dc222a78feda559a60a 100644 --- a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java +++ b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java @@ -59,7 +59,7 @@ public class DiplodocusSecurityTest extends AbstractTest { {"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac", "SampleAutoSec"))}, {"ITA01_v6", new ArrayList<>(Arrays.asList("mapAtt", "mapNoProtection"))}, {"Rovers_SPARTA_DIPLO", new ArrayList<>(Arrays.asList("NoCountermeasureMapping", "MACMapping", "SymmetricEncryptionNonceMapping"))}, - {"ITSDemo", new ArrayList<>(Arrays.asList("Architecture", "Architecture_enc_or"))} + {"ITSDemo", new ArrayList<>(Arrays.asList("Architecture", "Architecture_hsm", "Architecture_enc_or"))} }); }