From 18bbe6ba6c99ae6444249447e63384bd57dc2aea Mon Sep 17 00:00:00 2001
From: jerray <jawher.jerray@eurecom.fr>
Date: Wed, 3 Jul 2024 20:19:38 +0200
Subject: [PATCH] Add timeout for Proverif processes in tests + rename cli
PatternHandling class
---
...ng.java => DiplodocusPatternHandling.java} | 4 +-
src/main/java/cli/Interpreter.java | 2 +-
.../SecurityGenerationForTMAP.java | 58 +++++++++++++---
... => CLIDiplodocusPatternHandlingTest.java} | 6 +-
ttool/src/test/java/test/AbstractTest.java | 66 +++++++++++--------
.../AutoSecurityGenerationDiplodocusTest.java | 2 +-
.../tmltranslator/DiplodocusSecurityTest.java | 2 +-
7 files changed, 95 insertions(+), 45 deletions(-)
rename src/main/java/cli/{PatternHandling.java => DiplodocusPatternHandling.java} (99%)
rename ttool/src/test/java/cli/{CLIPatternHandlingTest.java => CLIDiplodocusPatternHandlingTest.java} (96%)
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 406fcd48e5..a455b572dc 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 52e9afed35..f3b233edbd 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 796d9b6ea6..f7a924dbc5 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 ac339612ec..4b48dd9368 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 8e9f030485..7a29150c39 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 4a14b97fa0..53b0107f56 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 bdc902064f..4420489e55 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"))}
});
}
--
GitLab