From 4ba9d501275836745b5f97f32786e8b9f0fb19e9 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Wed, 22 Feb 2023 18:03:35 +0100
Subject: [PATCH] Adding draw avatar model from proverif window
---
.../avatartranslator/AvatarSpecification.java | 4 +-
.../proverifspec/ProVerifOutputAnalyzer.java | 9 +-
src/main/java/tmltranslator/TMLChannel.java | 9 +
src/main/java/tmltranslator/TMLModeling.java | 23 +-
.../tmltranslator/toavatarsec/TML2Avatar.java | 1232 ++++++++---------
src/main/java/ui/GTURTLEModeling.java | 71 +-
src/main/java/ui/MainGUI.java | 20 +-
.../java/ui/tmlcompd/TMLCPrimitivePort.java | 6 +
.../window/JDialogProverifVerification.java | 33 +-
9 files changed, 732 insertions(+), 675 deletions(-)
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index b8e02fab88..a88de7ec0c 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -67,14 +67,14 @@ public class AvatarSpecification extends AvatarElement {
//private AvatarBroadcast broadcast;
private String applicationCode;
- private final List<AvatarPragma> pragmas;
+ private final List<AvatarPragma> pragmas; // Security pragmas
private final List<String> safetyPragmas;
private final HashMap<String, String> safetyPragmasRefs;
private final List<AvatarPragmaLatency> latencyPragmas;
private final List<AvatarConstant> constants;
private final boolean robustnessMade = false;
- private Object informationSource; // element from which the spec has been built
+ private Object informationSource; // Element from which the spec has been built
public AvatarSpecification(String _name, Object _referenceObject) {
diff --git a/src/main/java/proverifspec/ProVerifOutputAnalyzer.java b/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
index 8417823e68..e1df8cd88e 100644
--- a/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
+++ b/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
@@ -257,8 +257,7 @@ public class ProVerifOutputAnalyzer {
}
// This concerns a strong authenticity check
- else if (str.contains(isTyped ? typedStrongAuth : untypedStrongAuth))
- {
+ else if (str.contains(isTyped ? typedStrongAuth : untypedStrongAuth)) {
str = str.substring((isTyped ? typedStrongAuth : untypedStrongAuth).length());
String attributeStateName1 = null;
@@ -267,8 +266,7 @@ public class ProVerifOutputAnalyzer {
previousAuthPragma = new ProVerifQueryAuthResult(true, true);
result = previousAuthPragma;
- if (isTyped)
- {
+ if (isTyped) {
attributeStateName1 = str.split("\\(")[0];
attributeStateName2 = str.split(Pattern.quote(typedAuthSplit))[1].split("\\(")[0];
if (str.contains(typedFalse))
@@ -282,8 +280,7 @@ public class ProVerifOutputAnalyzer {
result.setProved(false);
}
}
- else
- {
+ else {
attributeStateName1 = str.split("\\(")[0];
attributeStateName2 = str.split(untypedAuthSplit)[1].split("\\(")[0];
if (str.contains(untypedFalse))
diff --git a/src/main/java/tmltranslator/TMLChannel.java b/src/main/java/tmltranslator/TMLChannel.java
index 9ba0eef1fc..66e91a6fbf 100755
--- a/src/main/java/tmltranslator/TMLChannel.java
+++ b/src/main/java/tmltranslator/TMLChannel.java
@@ -657,4 +657,13 @@ public class TMLChannel extends TMLCommunicationElement {
comp.isPortListEquals(destinationPorts, channel.getDestinationPorts());
}
+
+ public String getSecurityPorts() {
+ String ret = "";
+ for(TMLPortWithSecurityInformation port : ports) {
+ ret += port.toString() + " ";
+ }
+ return ret;
+ }
+
}
diff --git a/src/main/java/tmltranslator/TMLModeling.java b/src/main/java/tmltranslator/TMLModeling.java
index 981394732f..5c26650f9d 100755
--- a/src/main/java/tmltranslator/TMLModeling.java
+++ b/src/main/java/tmltranslator/TMLModeling.java
@@ -885,7 +885,7 @@ public class TMLModeling<E> {
public void backtraceAuthenticity(ProVerifOutputAnalyzer pvoa, String mappingName) {
- // TraceManager.addDev("Backtracing Authenticity");
+ //TraceManager.addDev("\n** Backtracing Authenticity ** ");
Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authenticityResults = pvoa.getAuthenticityResults();
for (AvatarPragmaAuthenticity pragma : authenticityResults.keySet()) {
ProVerifQueryAuthResult result = authenticityResults.get(pragma);
@@ -898,7 +898,9 @@ public class TMLModeling<E> {
+ "__" + pragma.getAttrA().getAttribute().getName()
+ "__" + pragma.getAttrA().getState().getName();
+ TraceManager.addDev("\n\n **Backtracing Authenticity s=" + s + " **");
if (result.isProved() && !result.isSatisfied()) {
+ TraceManager.addDev("Backtracing Authenticity proved but not satisfied");
String signalName = s.toString().split("_chData")[0];
signalName = signalName.split("__")[signalName.split("__").length - 1];
@@ -910,6 +912,7 @@ public class TMLModeling<E> {
if (channel != null) {
for (TMLPortWithSecurityInformation port : channel.ports) {
if (port.getCheckAuth()) {
+ TraceManager.addDev("Backtracing Authenticity proved but not satisfied / Found port with checkAuth");
port.setStrongAuthStatus(3);
port.setMappingName(mappingName);
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
@@ -919,6 +922,8 @@ public class TMLModeling<E> {
}
}
}
+ } else {
+ TraceManager.addDev("Backtracing Authenticity proved but not satisfied / NULL channel");
}
signalName = s.toString().split("_reqData")[0];
for (TMLTask t : getTasks()) {
@@ -959,10 +964,11 @@ public class TMLModeling<E> {
for (String channelName : channels) {
channel = getChannelByShortName(channelName);
if (channel != null) {
+ TraceManager.addDev("Security ports: " + channel.getSecurityPorts());
for (TMLPortWithSecurityInformation port : channel.ports) {
if (port.getCheckAuth() && port.getCheckStrongAuthStatus() == 1) {
port.setStrongAuthStatus(3);
- TraceManager.addDev("not verified " + signalName);
+ TraceManager.addDev("Backtracing Authenticity not verified " + signalName);
port.setSecName(signalName);
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
if (trace != null && !port.isOrigin()) {
@@ -1009,10 +1015,13 @@ public class TMLModeling<E> {
}
if (result.isWeakProved() && result.isWeakSatisfied()) {
+ TraceManager.addDev("Backtracing Authenticity weak proved and weak satisfied");
String signalName = s.split("_chData")[0];
signalName = signalName.split("__")[1];
TMLChannel channel = getChannelByShortName(signalName);
+
if (channel != null) {
+ TraceManager.addDev("Security ports (1): " + channel.getSecurityPorts());
for (TMLPortWithSecurityInformation port : channel.ports) {
if (port.getCheckAuth()) {
port.setWeakAuthStatus(2);
@@ -1024,7 +1033,10 @@ public class TMLModeling<E> {
}
}
}
+ } else {
+ TraceManager.addDev("Backtracing Authenticity weak proved and weak satisfied: NULL Channel");
}
+
signalName = s.split("_reqData")[0];
for (TMLTask t : getTasks()) {
if (signalName.contains(t.getName())) {
@@ -1064,12 +1076,16 @@ public class TMLModeling<E> {
signalName = signalName.replace(t.getName()+"__","");
}
}*/
+
signalName = signalName.split("__")[1];
+ TraceManager.addDev("Signal name (2): " + signalName);
List<String> channels = secChannelMap.get(signalName);
if (channels != null) {
for (String channelName : channels) {
channel = getChannelByShortName(channelName);
+
if (channel != null) {
+ TraceManager.addDev("Security ports (2): " + channel.getSecurityPorts());
for (TMLPortWithSecurityInformation port : channel.ports) {
if (port.getCheckAuth()) {
port.setWeakAuthStatus(2);
@@ -1081,6 +1097,8 @@ public class TMLModeling<E> {
}
}
}
+ } else {
+ TraceManager.addDev("Backtracing Authenticity weak proved and weak satisfied: NULL Channel");
}
}
}
@@ -1119,6 +1137,7 @@ public class TMLModeling<E> {
}
if (result.isProved() && result.isSatisfied()) {
+ TraceManager.addDev("Backtracing Authenticity proved and satisfied" );
String signalName = s.split("_chData")[0];
for (TMLTask t : getTasks()) {
if (signalName.contains(t.getName())) {
diff --git a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
index 86dc677a98..e2ac734d28 100644
--- a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
@@ -1,38 +1,38 @@
/* ludovic.apvrille AT enst.fr
-*
-* This software is a computer program whose purpose is to allow the
-* edition of TURTLE analysis, design and deployment diagrams, to
-* allow the generation of RT-LOTOS or Java code from this diagram,
-* and at last to allow the analysis of formal validation traces
-* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
-* from INRIA Rhone-Alpes.
-*
-* This software is governed by the CeCILL license under French law and
-* abiding by the rules of distribution of free software. You can use,
-* modify and/ or redistribute the software under the terms of the CeCILL
-* license as circulated by CEA, CNRS and INRIA at the following URL
-* "http://www.cecill.info".
-*
-* As a counterpart to the access to the source code and rights to copy,
-* modify and redistribute granted by the license, users are provided only
-* with a limited warranty and the software's author, the holder of the
-* economic rights, and the successive licensors have only limited
-* liability.
-*
-* In this respect, the user's attention is drawn to the risks associated
-* with loading, using, modifying and/or developing or reproducing the
-* software by the user in light of its specific status of free software,
-* that may mean that it is complicated to manipulate, and that also
-* therefore means that it is reserved for developers and experienced
-* professionals having in-depth computer knowledge. Users are therefore
-* encouraged to load and test the software's suitability as regards their
-* requirements in conditions enabling the security of their systems and/or
-* data to be ensured and, more generally, to use and operate it in the
-* same conditions as regards security.
-*
-* The fact that you are presently reading this means that you have had
-* knowledge of the CeCILL license and that you accept its terms.
-*/
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
package tmltranslator.toavatarsec;
@@ -43,7 +43,6 @@ import proverifspec.ProVerifQueryResult;
import tmltranslator.*;
import ui.TGComponent;
import ui.tmlad.*;
-import ui.tmlcompd.TMLCPrimitivePort;
import java.util.*;
import java.util.regex.Matcher;
@@ -57,38 +56,33 @@ import java.util.regex.Pattern;
* @version 1.1 29/02/2016
*/
public class TML2Avatar {
- private TMLMapping<?> tmlmap;
- private TMLModeling<?> tmlmodel;
-
- private Map<SecurityPattern, List<AvatarAttribute>> symKeys = new HashMap<SecurityPattern, List<AvatarAttribute>>();
- private Map<SecurityPattern, List<AvatarAttribute>> pubKeys = new HashMap<SecurityPattern, List<AvatarAttribute>>();
- private Map<String, String> nameMap = new HashMap<String, String>();
+ private final static Integer channelPublic = 0;
+ private final static Integer channelPrivate = 1;
+ private final static Integer channelUnreachable = 2;
//private AvatarAttribute pKey;
public Map<TMLChannel, Integer> channelMap = new HashMap<TMLChannel, Integer>();
public Map<TMLTask, AvatarBlock> taskBlockMap = new HashMap<TMLTask, AvatarBlock>();
public Map<String, Integer> originDestMap = new HashMap<String, Integer>();
- private Map<String, AvatarSignal> signalInMap = new HashMap<String, AvatarSignal>();
- private Map<String, AvatarSignal> signalOutMap = new HashMap<String, AvatarSignal>();
public Map<String, Object> stateObjectMap = new HashMap<String, Object>();
public Map<TMLTask, List<SecurityPattern>> accessKeys = new HashMap<TMLTask, List<SecurityPattern>>();
-
+ public ArrayList<SecurityPattern> secPatterns = new ArrayList<SecurityPattern>();
+ public int loopLimit = 1;
HashMap<String, List<String>> secChannelMap = new HashMap<String, List<String>>();
-
HashMap<String, AvatarAttributeState> signalAuthOriginMap = new HashMap<String, AvatarAttributeState>();
HashMap<String, AvatarAttributeState> signalAuthDestMap = new HashMap<String, AvatarAttributeState>();
-
- public ArrayList<SecurityPattern> secPatterns = new ArrayList<SecurityPattern>();
-
List<AvatarSignal> signals = new ArrayList<AvatarSignal>();
- private final static Integer channelPublic = 0;
- private final static Integer channelPrivate = 1;
- private final static Integer channelUnreachable = 2;
- public int loopLimit = 1;
AvatarSpecification avspec;
ArrayList<String> attrsToCheck;
List<String> allStates;
boolean mc = false;
boolean security = false;
+ private TMLMapping<?> tmlmap;
+ private TMLModeling<?> tmlmodel;
+ private Map<SecurityPattern, List<AvatarAttribute>> symKeys = new HashMap<SecurityPattern, List<AvatarAttribute>>();
+ private Map<SecurityPattern, List<AvatarAttribute>> pubKeys = new HashMap<SecurityPattern, List<AvatarAttribute>>();
+ private Map<String, String> nameMap = new HashMap<String, String>();
+ private Map<String, AvatarSignal> signalInMap = new HashMap<String, AvatarSignal>();
+ private Map<String, AvatarSignal> signalOutMap = new HashMap<String, AvatarSignal>();
public TML2Avatar(TMLMapping<?> tmlmap, boolean modelcheck, boolean sec) {
this.tmlmap = tmlmap;
@@ -146,7 +140,7 @@ public class TML2Avatar {
// Find path to secure memory from destination node
for (TMLTask t2 : tmlmodel.getTasks()) {
- HwExecutionNode node2 = tmlmap.getHwNodeOf(t2);
+ HwExecutionNode node2 = tmlmap.getHwNodeOf(t2);
if (!memory) {
// There is no path to a private memory
originDestMap.put(t1.getName() + "__" + t2.getName(), channelPublic);
@@ -673,7 +667,7 @@ public class TML2Avatar {
} else if (ae instanceof TMLActivityElementWithAction) {
//Might be encrypt or decrypt
- AvatarState as = new AvatarState(ae.getValue().replaceAll(" ", "").replaceAll("\\*","").replaceAll("\\+","").replaceAll("\\-","") + "_" + ae.getName().replaceAll(" ", "").replaceAll("\\*","").replaceAll("\\+","").replaceAll("\\-",""), ae.getReferenceObject());
+ AvatarState as = new AvatarState(ae.getValue().replaceAll(" ", "").replaceAll("\\*", "").replaceAll("\\+", "").replaceAll("\\-", "") + "_" + ae.getName().replaceAll(" ", "").replaceAll("\\*", "").replaceAll("\\+", "").replaceAll("\\-", ""), ae.getReferenceObject());
tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
as.addNext(tran);
elementList.add(as);
@@ -858,9 +852,11 @@ public class TML2Avatar {
ae.securityPattern.originTask = block.getName();
ae.securityPattern.state1 = as;
}
- //Set attributestate for authenticity
+
+ // Set attribute state for authenticity
if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
- AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName() + "." + as.getName() + "." + ae.securityPattern.name, ae.getReferenceObject(), block.getAvatarAttributeWithName(ae.securityPattern.name), as);
+ AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName() + "." + as.getName() + "." +
+ ae.securityPattern.name, ae.getReferenceObject(), block.getAvatarAttributeWithName(ae.securityPattern.name), as);
signalAuthOriginMap.put(ae.securityPattern.name, authOrigin);
}
@@ -907,7 +903,8 @@ public class TML2Avatar {
get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
get2.addParameter(block.getAvatarAttributeWithName("testnonce_" + ae.securityPattern.nonce));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName("testnonce_" + ae.securityPattern.nonce) != null) {
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null &&
+ block.getAvatarAttributeWithName("testnonce_" + ae.securityPattern.nonce) != null) {
block.addMethod(get2);
tran.addAction("get2(" + ae.securityPattern.name + "," + ae.securityPattern.name + ",testnonce_" + ae.securityPattern.nonce + ")");
}
@@ -923,7 +920,8 @@ public class TML2Avatar {
//Guard transition to determine if nonce matches
tran.setGuard("testnonce_" + ae.securityPattern.nonce + "==" + ae.securityPattern.nonce);
}
- //Add a dummy state afterwards for authenticity after decrypting the data
+
+ // Add a dummy state afterwards for authenticity after decrypting the data
AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ", "") + "_dummy", ae.getReferenceObject());
ae.securityPattern.state2 = dummy;
tran.addNext(dummy);
@@ -932,7 +930,8 @@ public class TML2Avatar {
elementList.add(dummy);
elementList.add(tran);
if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
- AvatarAttributeState authDest = new AvatarAttributeState(block.getName() + "." + dummy.getName() + "." + ae.securityPattern.name, ae.getReferenceObject(), block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
+ AvatarAttributeState authDest = new AvatarAttributeState(block.getName() + "." + dummy.getName() + "." +
+ ae.securityPattern.name, ae.getReferenceObject(), block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
signalAuthDestMap.put(ae.securityPattern.name, authDest);
}
} else if (ae.securityPattern.type.equals("Asymmetric Encryption")) {
@@ -940,8 +939,6 @@ public class TML2Avatar {
if (!ae.securityPattern.key.isEmpty()) {
//Decrypting key
-
-
//Add adecrypt method
block.addAttribute(new AvatarAttribute("encryptedKey_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
block.addAttribute(new AvatarAttribute("privKey_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
@@ -951,7 +948,9 @@ public class TML2Avatar {
adecrypt.addParameter(block.getAvatarAttributeWithName("privKey_" + ae.securityPattern.name));
adecrypt.addReturnParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.key));
- if (block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key) != null && block.getAvatarAttributeWithName("privKey_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.key) != null) {
+ if (block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key) != null &&
+ block.getAvatarAttributeWithName("privKey_" + ae.securityPattern.name) != null &&
+ block.getAvatarAttributeWithName("key_" + ae.securityPattern.key) != null) {
block.addMethod(adecrypt);
tran.addAction("key_" + ae.securityPattern.key + " = adecrypt(encryptedKey_" + ae.securityPattern.key + ", privKey_" + ae.securityPattern.name + ")");
}
@@ -1136,20 +1135,19 @@ public class TML2Avatar {
List<String> tmp = new ArrayList<String>();
secChannelMap.put(ae.securityPattern.name, tmp);
}
-
+
secChannelMap.get(ae.securityPattern.name).add(ch.getName());
- if (aec.getEncForm()){
- as.addValue(ae.securityPattern.name + "_encrypted");
- AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null);
- block.addAttribute(data);
- }
- else {
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) == null){
- AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null);
- block.addAttribute(data);
- }
- as.addValue(ae.securityPattern.name);
-
+ if (aec.getEncForm()) {
+ as.addValue(ae.securityPattern.name + "_encrypted");
+ AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null);
+ block.addAttribute(data);
+ } else {
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) == null) {
+ AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null);
+ block.addAttribute(data);
+ }
+ as.addValue(ae.securityPattern.name);
+
}
}
} else {
@@ -1199,38 +1197,41 @@ public class TML2Avatar {
}
//Add the confidentiality pragma for this channel data
if (ch.checkConf) {
- if (ch.originalOriginTasks.size()!=0 && ch.getOriginPort().getName().contains("PORTORIGIN")){
- // System.out.println("Channel " + ch.getOriginPort().getName() + " block " + block.getName());
- if (!attrsToCheck.contains(ch.getOriginPort().getName() + "_chData") ) {
- for (TMLTask origTask: ch.originalOriginTasks){
- AvatarBlock bl = avspec.getBlockWithName(origTask.getName().split("__")[origTask.getName().split("__").length - 1]);
- if (bl!=null){
- AvatarAttribute attr = bl.getAvatarAttributeWithName(block.getName() + "_chData");
- if (attr != null) {
- attrsToCheck.add(ch.getOriginPort().getName() + "_chData");
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality " + bl.getName() + "." + block.getName() + "_chData", ch.getReferenceObject(), attr));
- }
- }
- }
- }
- }
- else {
- if (!attrsToCheck.contains(ch.getOriginPort().getName() + "_chData") ) {
- AvatarAttribute attr = block.getAvatarAttributeWithName(ch.getOriginPort().getName() + "_chData");
- if (attr != null) {
- attrsToCheck.add(ch.getOriginPort().getName() + "_chData");
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality " + block.getName() + "." + ch.getName() + "_chData", ch.getReferenceObject(), attr));
- }
+ if (ch.originalOriginTasks.size() != 0 && ch.getOriginPort().getName().contains("PORTORIGIN")) {
+ // System.out.println("Channel " + ch.getOriginPort().getName() + " block " + block.getName());
+ if (!attrsToCheck.contains(ch.getOriginPort().getName() + "_chData")) {
+ for (TMLTask origTask : ch.originalOriginTasks) {
+ AvatarBlock bl = avspec.getBlockWithName(origTask.getName().split("__")[origTask.getName().split("__").length - 1]);
+ if (bl != null) {
+ AvatarAttribute attr = bl.getAvatarAttributeWithName(block.getName() + "_chData");
+ if (attr != null) {
+ attrsToCheck.add(ch.getOriginPort().getName() + "_chData");
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality " + bl.getName() + "." + block.getName() +
+ "_chData", ch.getReferenceObject(), attr));
+ }
+ }
+ }
+ }
+ } else {
+ if (!attrsToCheck.contains(ch.getOriginPort().getName() + "_chData")) {
+ AvatarAttribute attr = block.getAvatarAttributeWithName(ch.getOriginPort().getName() + "_chData");
+ if (attr != null) {
+ attrsToCheck.add(ch.getOriginPort().getName() + "_chData");
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality " + block.getName() + "." + ch.getName() +
+ "_chData", ch.getReferenceObject(), attr));
+ }
}
}
}
- //Add the authenticity pragma for this channel data
+
+ // Add the authenticity pragma for this channel data
if (ch.checkAuth) {
if (block.getAvatarAttributeWithName(getName(ch.getName()) + "_chData") == null) {
AvatarAttribute channelData = new AvatarAttribute(getName(ch.getName()) + "_chData", AvatarType.INTEGER, block, null);
block.addAttribute(channelData);
}
- AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName() + "." + signalState.getName() + "." + getName(ch.getName()) + "_chData", ae.getReferenceObject(), block.getAvatarAttributeWithName(getName(ch.getName()) + "_chData"), signalState);
+ AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName() + "." + signalState.getName() + "." +
+ getName(ch.getName()) + "_chData", ae.getReferenceObject(), block.getAvatarAttributeWithName(getName(ch.getName()) + "_chData"), signalState);
signalAuthOriginMap.put(ch.getName(), authOrigin);
}
AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
@@ -1249,20 +1250,19 @@ public class TML2Avatar {
} else {
//send encrypted data
//
- if (aec.getEncForm()){
- as.addValue(ae.securityPattern.name + "_encrypted");
- AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null);
- block.addAttribute(data);
- }
- else {
- //Send unecrypted form
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) == null){
- AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null);
- block.addAttribute(data);
- }
- as.addValue(ae.securityPattern.name);
+ if (aec.getEncForm()) {
+ as.addValue(ae.securityPattern.name + "_encrypted");
+ AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null);
+ block.addAttribute(data);
+ } else {
+ //Send unecrypted form
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) == null) {
+ AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null);
+ block.addAttribute(data);
+ }
+ as.addValue(ae.securityPattern.name);
}
-
+
if (!secChannelMap.containsKey(ae.securityPattern.name)) {
List<String> tmp = new ArrayList<String>();
secChannelMap.put(ae.securityPattern.name, tmp);
@@ -1272,7 +1272,7 @@ public class TML2Avatar {
} else {
//No security pattern
// TraceManager.addDev("no security pattern for " + ch.getName());
- as.addValue(ch.getOriginPort().getName()+ "_chData");
+ as.addValue(ch.getOriginPort().getName() + "_chData");
}
tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
@@ -1289,7 +1289,7 @@ public class TML2Avatar {
if (loop.isInfinite()) {
//Make initializaton, then choice state with transitions
List<AvatarStateMachineElement> elements = translateState(ae.getNextElement(0), block);
- /*List<AvatarStateMachineElement> afterloop =*/
+ /*List<AvatarStateMachineElement> afterloop =*/
translateState(ae.getNextElement(1), block);
AvatarState initState = new AvatarState(ae.getName().replaceAll(" ", "") + "__init", ae.getReferenceObject());
elementList.add(initState);
@@ -1357,7 +1357,7 @@ public class TML2Avatar {
tran = new AvatarTransition(block, "loop_increment__" + ae.getName(), ae.getReferenceObject());
//Set default loop limit guard
tran.setGuard(AvatarGuard.createFromString(block, "loop_index != " + loopLimit));
- /*AvatarGuard guard = */
+ /*AvatarGuard guard = */
AvatarGuard.createFromString(block, loop.getCondition().replaceAll("<", "!="));
int error = AvatarSyntaxChecker.isAValidGuard(avspec, block, loop.getCondition().replaceAll("<", "!="));
if (error != 0) {
@@ -1458,14 +1458,14 @@ public class TML2Avatar {
}*/
public String getName(String s) {
- // System.out.println("String " + s);
+ // System.out.println("String " + s);
if (nameMap.containsKey(s)) {
return nameMap.get(s);
} else {
if (!s.contains("__")) {
nameMap.put(s, s);
return s;
- } else if (s.split("__").length == 1 ) {
+ } else if (s.split("__").length == 1) {
nameMap.put(s, s.split("__")[s.split("__").length - 1]);
return s.split("__")[s.split("__").length - 1];
} else if (s.contains("JOIN") || s.contains("FORK")) {
@@ -1483,8 +1483,8 @@ public class TML2Avatar {
}*/
nameMap.put(s, s);
return s;
- // nameMap.put(s, s.split("__")[s.split("__").length - 1]);
- // return s.split("__")[s.split("__").length - 1];
+ // nameMap.put(s, s.split("__")[s.split("__").length - 1]);
+ // return s.split("__")[s.split("__").length - 1];
}
}
}
@@ -1505,30 +1505,30 @@ public class TML2Avatar {
}
attrsToCheck.clear();
tmlmodel.removeForksAndJoins();
-
+
// System.out.println("MODIFIED model " + tmlmodel);
-
- for (TMLChannel chan: tmlmodel.getChannels()){
- //System.out.println("chan " + chan);
- TMLTask task = chan.getOriginTask();
-
- TMLTask task2 = chan.getDestinationTask();
- HwExecutionNode node = tmlmap.getHwNodeOf(task);
- HwExecutionNode node2 = tmlmap.getHwNodeOf(task2);
- if (node==null){
- tmlmap.addTaskToHwExecutionNode(task, node2);
- }
-
- if (node2==null){
- tmlmap.addTaskToHwExecutionNode(task2, node);
- }
-
- if (chan.getName().contains("fork__") || chan.getName().contains("FORKCHANNEL")){
- chan.setName(chan.getName().replaceAll("__",""));
- }
-
+
+ for (TMLChannel chan : tmlmodel.getChannels()) {
+ //System.out.println("chan " + chan);
+ TMLTask task = chan.getOriginTask();
+
+ TMLTask task2 = chan.getDestinationTask();
+ HwExecutionNode node = tmlmap.getHwNodeOf(task);
+ HwExecutionNode node2 = tmlmap.getHwNodeOf(task2);
+ if (node == null) {
+ tmlmap.addTaskToHwExecutionNode(task, node2);
+ }
+
+ if (node2 == null) {
+ tmlmap.addTaskToHwExecutionNode(task2, node);
+ }
+
+ if (chan.getName().contains("fork__") || chan.getName().contains("FORKCHANNEL")) {
+ chan.setName(chan.getName().replaceAll("__", ""));
+ }
+
}
-
+
//Only set the loop limit if it's a number
String pattern = "^[0-9]{1,2}$";
Pattern r = Pattern.compile(pattern);
@@ -1679,9 +1679,9 @@ public class TML2Avatar {
}
//Create exit after # of loop iterations is maxed out
- /*AvatarStopState stop =*/
- new AvatarStopState("stop", task.getActivityDiagram().get(0).getReferenceObject());
- /*AvatarTransition exitTran = */
+ /*AvatarStopState stop =*/
+ new AvatarStopState("stop", task.getActivityDiagram().get(0).getReferenceObject());
+ /*AvatarTransition exitTran = */
new AvatarTransition(block, "to_stop", task.getActivityDiagram().get(0).getReferenceObject());
@@ -1736,65 +1736,64 @@ public class TML2Avatar {
tran.addNext(newStart);
}*/
- }
+ }
- asm.setStartState(ss);
+ asm.setStartState(ss);
- }
- else {
- //Not requested
- List<AvatarStateMachineElement> elementList= translateState(task.getActivityDiagram().get(0), block);
- for (AvatarStateMachineElement e: elementList){
- e.setName(processName(e.getName(), e.getID()));
- asm.addElement(e);
- stateObjectMap.put(task.getName().split("__")[1]+"__"+e.getName(), e.getReferenceObject());
- }
- asm.setStartState((AvatarStartState) elementList.get(0));
- }
- for (SecurityPattern secPattern: secPatterns){
- AvatarAttribute sec = block.getAvatarAttributeWithName(secPattern.name);
- if (sec!=null){
- //sec = new AvatarAttribute(secPattern.name, AvatarType.INTEGER, block, null);
- //AvatarAttribute enc = new AvatarAttribute(secPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
- // block.addAttribute(sec);
- // block.addAttribute(enc);
- //}
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ secPattern.name, null, sec));
- }
- }
+ } else {
+ //Not requested
+ List<AvatarStateMachineElement> elementList = translateState(task.getActivityDiagram().get(0), block);
+ for (AvatarStateMachineElement e : elementList) {
+ e.setName(processName(e.getName(), e.getID()));
+ asm.addElement(e);
+ stateObjectMap.put(task.getName().split("__")[1] + "__" + e.getName(), e.getReferenceObject());
+ }
+ asm.setStartState((AvatarStartState) elementList.get(0));
+ }
+ for (SecurityPattern secPattern : secPatterns) {
+ AvatarAttribute sec = block.getAvatarAttributeWithName(secPattern.name);
+ if (sec != null) {
+ //sec = new AvatarAttribute(secPattern.name, AvatarType.INTEGER, block, null);
+ //AvatarAttribute enc = new AvatarAttribute(secPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
+ // block.addAttribute(sec);
+ // block.addAttribute(enc);
+ //}
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality " + block.getName() + "." + secPattern.name, null, sec));
+ }
+ }
- }
+ }
- //Add authenticity pragmas
- for (String s: signalAuthOriginMap.keySet()){
- if (signalAuthDestMap.containsKey(s)){
- AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity("#Authenticity " + signalAuthOriginMap.get(s).getName() + " " + signalAuthDestMap.get(s).getName(), signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
- if (secChannelMap.containsKey(s)){
- for (String channel: secChannelMap.get(s)){
- TMLChannel ch = tmlmodel.getChannelByShortName(channel);
- if (ch!=null){
- if (ch.checkAuth){
- avspec.addPragma(pragma);
- break;
- }
- }
- }
-
- }
- else {
- avspec.addPragma(pragma);
- }
- }
- }
-
- //Create relations
- //Channels are ?? to ??
- //Requests are n to 1
- //Events are ?? to ??
- AvatarBlock fifo = new AvatarBlock("FIFO", avspec,null);
- for (TMLChannel channel:tmlmodel.getChannels()){
+ // Add authenticity pragmas
+ for (String s : signalAuthOriginMap.keySet()) {
+ if (signalAuthDestMap.containsKey(s)) {
+ AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity("#Authenticity " + signalAuthOriginMap.get(s).getName() + " "
+ + signalAuthDestMap.get(s).getName(), signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
+ if (secChannelMap.containsKey(s)) {
+ for (String channel : secChannelMap.get(s)) {
+ TMLChannel ch = tmlmodel.getChannelByShortName(channel);
+ if (ch != null) {
+ if (ch.checkAuth) {
+ avspec.addPragma(pragma);
+ break;
+ }
+ }
+ }
+
+ } else {
+ avspec.addPragma(pragma);
+ }
+ }
+ }
+
+ //Create relations
+ //Channels are ?? to ??
+ //Requests are n to 1
+ //Events are ?? to ??
+ AvatarBlock fifo = new AvatarBlock("FIFO", avspec, null);
+ for (TMLChannel channel : tmlmodel.getChannels()) {
/*if (channel.getName().contains("JOINCHANNEL")){
//System.out.println("JOINCHANNEL");
AvatarRelation ar= new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()), taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
@@ -1911,446 +1910,433 @@ public class TML2Avatar {
avspec.addRelation(ar);
}*/
- if (channel.isBasicChannel()){
- //TraceManager.addDev("CHAN checking basic channel " + channel.getName());
- AvatarRelation ar = new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()),
- taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
- LinkedList<HwCommunicationNode> path = tmlmap.findNodesForElement(channel);
- //TraceManager.addDev("CHAN checking basic channel " + channel.getName() + " path size: " + path.size());
- if (path.size() !=0 ){
- ar.setPrivate(true);
- for (HwCommunicationNode node: path){
- //TraceManager.addDev("CHAN\t Element of path: " + node.getName());
- if (node instanceof HwBus){
- if ( node.privacy == HwCommunicationNode.BUS_PUBLIC){
- ar.setPrivate(false);
- //TraceManager.addDev("CHAN\t Set as public: " + channel.getName() + "because of " + node.getName());
+ if (channel.isBasicChannel()) {
+ //TraceManager.addDev("CHAN checking basic channel " + channel.getName());
+ AvatarRelation ar = new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()),
+ taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
+ LinkedList<HwCommunicationNode> path = tmlmap.findNodesForElement(channel);
+ //TraceManager.addDev("CHAN checking basic channel " + channel.getName() + " path size: " + path.size());
+ if (path.size() != 0) {
+ ar.setPrivate(true);
+ for (HwCommunicationNode node : path) {
+ //TraceManager.addDev("CHAN\t Element of path: " + node.getName());
+ if (node instanceof HwBus) {
+ if (node.privacy == HwCommunicationNode.BUS_PUBLIC) {
+ ar.setPrivate(false);
+ //TraceManager.addDev("CHAN\t Set as public: " + channel.getName() + "because of " + node.getName());
+ break;
+ }
+ }
+ }
+ } else {
+ if (channel.originalOriginTasks.size() == 0) {
+ ar.setPrivate(originDestMap.get(channel.getOriginTask().getName() + "__" + channel.getDestinationTask().getName()) == 1);
+ } else {
+ //System.out.println("complex channel " + channel.getName());
+ //Find privacy of original tasks
+ boolean priv = true;
+ for (TMLTask task1 : channel.originalOriginTasks) {
+ for (TMLTask task2 : channel.originalDestinationTasks) {
+ if (originDestMap.get(task1.getName() + "__" + task2.getName()) != 1) {
+ priv = false;
break;
- }
- }
- }
- }
- else {
- if (channel.originalOriginTasks.size()==0){
- ar.setPrivate(originDestMap.get(channel.getOriginTask().getName()+"__"+channel.getDestinationTask().getName())==1);
- }
- else {
- //System.out.println("complex channel " + channel.getName());
- //Find privacy of original tasks
- boolean priv = true;
- for (TMLTask task1: channel.originalOriginTasks){
- for (TMLTask task2: channel.originalDestinationTasks){
- if (originDestMap.get(task1.getName()+"__"+task2.getName())!=1){
- priv=false;
- break;
- }
-
- }
-
- }
- ar.setPrivate(priv);
- }
- }
- if (channel.getType()==TMLChannel.BRBW){
- ar.setAsynchronous(true);
- ar.setSizeOfFIFO(channel.getSize());
- ar.setBlocking(true);
- }
- else if (channel.getType()==TMLChannel.BRNBW){
- ar.setAsynchronous(true);
- ar.setSizeOfFIFO(channel.getSize());
- ar.setBlocking(false);
- }
- else {
- //Create new block, hope for best
- if (mc){
- fifo = createFifo(channel.getName());
- ar.setAsynchronous(false);
- }
- }
- //Find in signal
-
- List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
- //Sig1 contains IN Signals, Sig2 contains OUT signals
- sig1.add(signalInMap.get(channel.getName()));
- List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
- sig2.add(signalOutMap.get(channel.getName()));
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.IN){
- String name = sig.getName();
- if (name.equals(getName(channel.getName()))){
- // sig1.add(sig);
- }
- }
- }
- //Find out signal
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.OUT){
- String name = sig.getName();
- if (name.equals(channel.getOriginPort().getName())){
- // sig2.add(sig);
- }
- }
- }
- //System.out.println("size " + sig1.size() + " " + sig2.size());
- if (sig1.size()==0){
- sig1.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.IN, null));
- }
- if (sig2.size()==0){
- sig2.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.OUT, null));
- }
- if (sig1.size()==1 && sig2.size()==1){
- if (channel.getType()==TMLChannel.NBRNBW && mc){
- AvatarSignal read = fifo.getSignalByName("readSignal");
+ }
- ar.block2= fifo;
- //Set IN signal with read
- ar.addSignals(sig1.get(0), read);
- AvatarRelation ar2= new AvatarRelation(channel.getName()+"2", fifo, taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
- AvatarSignal write = fifo.getSignalByName("writeSignal");
- //set OUT signal with write
- ar2.addSignals(write, sig2.get(0));
- // System.out.println("Set " + sig2.get(0) + " and write");
- ar2.setAsynchronous(false);
- avspec.addRelation(ar2);
- }
- else {
- ar.addSignals(sig2.get(0), sig1.get(0));
- }
- }
- else {
- //Create relation if it does not exist
- if (top.getSignalByName(getName(channel.getName())+"in")==null){
- AvatarRelation relation= new AvatarRelation(channel.getName(), top, top, channel.getReferenceObject());
- AvatarSignal s1 = new AvatarSignal(getName(channel.getName())+"in", AvatarSignal.IN, null);
- AvatarSignal s2 = new AvatarSignal(getName(channel.getName())+"out", AvatarSignal.OUT, null);
- top.addSignal(s1);
- top.addSignal(s2);
- relation.addSignals(s2,s1);
- avspec.addRelation(relation);
- // System.out.println("Failure to match signals for TMLChannel "+ channel.getName());
- }
- }
- avspec.addRelation(ar);
- }
- else {
- //System.out.println("WTF Found non-basic channel");
- //If not a basic channel, create a relation between TOP block and itself
- AvatarRelation relation= new AvatarRelation(channel.getName(), top, top, channel.getReferenceObject());
- AvatarSignal s1 = new AvatarSignal(getName(channel.getName())+"in", AvatarSignal.IN, null);
- AvatarSignal s2 = new AvatarSignal(getName(channel.getName())+"out", AvatarSignal.OUT, null);
- top.addSignal(s1);
- top.addSignal(s2);
- relation.addSignals(s2,s1);
- avspec.addRelation(relation);
- for (TMLTask t1: channel.getOriginTasks()){
- for (TMLTask t2: channel.getDestinationTasks()){
- AvatarRelation ar= new AvatarRelation(channel.getName(), taskBlockMap.get(t1), taskBlockMap.get(t2), channel.getReferenceObject());
- ar.setPrivate(originDestMap.get(t1.getName()+"__"+t2.getName())==1);
- //Find in signal
- List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
- List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.IN){
- String name = sig.getName();
- if (name.equals(getName(channel.getName()))){
- sig1.add(sig);
- }
- }
- }
- //Find out signal
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.OUT){
- String name = sig.getName();
- if (name.equals(getName(channel.getName()))){
- sig2.add(sig);
- }
- }
- }
- if (sig1.size()==0){
- sig1.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.IN, null));
- }
- if (sig2.size()==0){
- sig2.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.OUT, null));
- }
- if (sig1.size()==1 && sig2.size()==1){
- ar.addSignals(sig2.get(0), sig1.get(0));
- }
- else {
- System.out.println("Failure to match signals for TMLChannel "+ channel.getName() + " between " + t1.getName() + " and "+ t2.getName());
- }
- avspec.addRelation(ar);
- }
- }
- }
- }
- for (TMLRequest request: tmlmodel.getRequests()){
- for (TMLTask t1: request.getOriginTasks()){
- AvatarRelation ar = new AvatarRelation(request.getName(), taskBlockMap.get(t1), taskBlockMap.get(request.getDestinationTask()), request.getReferenceObject());
- ar.setPrivate(originDestMap.get(t1.getName()+"__"+request.getDestinationTask().getName())==1);
- List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
- List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.IN){
- String name = sig.getName();
+ }
- if (name.equals(getName(request.getName()))){
- sig1.add(sig);
- }
- }
- }
- //Find out signal
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.OUT){
- String name = sig.getName();
+ }
+ ar.setPrivate(priv);
+ }
+ }
+ if (channel.getType() == TMLChannel.BRBW) {
+ ar.setAsynchronous(true);
+ ar.setSizeOfFIFO(channel.getSize());
+ ar.setBlocking(true);
+ } else if (channel.getType() == TMLChannel.BRNBW) {
+ ar.setAsynchronous(true);
+ ar.setSizeOfFIFO(channel.getSize());
+ ar.setBlocking(false);
+ } else {
+ //Create new block, hope for best
+ if (mc) {
+ fifo = createFifo(channel.getName());
+ ar.setAsynchronous(false);
+ }
+ }
+ //Find in signal
+
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ //Sig1 contains IN Signals, Sig2 contains OUT signals
+ sig1.add(signalInMap.get(channel.getName()));
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ sig2.add(signalOutMap.get(channel.getName()));
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.IN) {
+ String name = sig.getName();
+ if (name.equals(getName(channel.getName()))) {
+ // sig1.add(sig);
+ }
+ }
+ }
+ //Find out signal
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.OUT) {
+ String name = sig.getName();
+ if (name.equals(channel.getOriginPort().getName())) {
+ // sig2.add(sig);
+ }
+ }
+ }
+ //System.out.println("size " + sig1.size() + " " + sig2.size());
+ if (sig1.size() == 0) {
+ sig1.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.IN, null));
+ }
+ if (sig2.size() == 0) {
+ sig2.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.OUT, null));
+ }
+ if (sig1.size() == 1 && sig2.size() == 1) {
+ if (channel.getType() == TMLChannel.NBRNBW && mc) {
+ AvatarSignal read = fifo.getSignalByName("readSignal");
+
+ ar.block2 = fifo;
+ //Set IN signal with read
+ ar.addSignals(sig1.get(0), read);
+ AvatarRelation ar2 = new AvatarRelation(channel.getName() + "2", fifo, taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
+ AvatarSignal write = fifo.getSignalByName("writeSignal");
+ //set OUT signal with write
+ ar2.addSignals(write, sig2.get(0));
+ // System.out.println("Set " + sig2.get(0) + " and write");
+ ar2.setAsynchronous(false);
+ avspec.addRelation(ar2);
+ } else {
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ }
+ } else {
+ //Create relation if it does not exist
+ if (top.getSignalByName(getName(channel.getName()) + "in") == null) {
+ AvatarRelation relation = new AvatarRelation(channel.getName(), top, top, channel.getReferenceObject());
+ AvatarSignal s1 = new AvatarSignal(getName(channel.getName()) + "in", AvatarSignal.IN, null);
+ AvatarSignal s2 = new AvatarSignal(getName(channel.getName()) + "out", AvatarSignal.OUT, null);
+ top.addSignal(s1);
+ top.addSignal(s2);
+ relation.addSignals(s2, s1);
+ avspec.addRelation(relation);
+ // System.out.println("Failure to match signals for TMLChannel "+ channel.getName());
+ }
+ }
+ avspec.addRelation(ar);
+ } else {
+ //System.out.println("WTF Found non-basic channel");
+ //If not a basic channel, create a relation between TOP block and itself
+ AvatarRelation relation = new AvatarRelation(channel.getName(), top, top, channel.getReferenceObject());
+ AvatarSignal s1 = new AvatarSignal(getName(channel.getName()) + "in", AvatarSignal.IN, null);
+ AvatarSignal s2 = new AvatarSignal(getName(channel.getName()) + "out", AvatarSignal.OUT, null);
+ top.addSignal(s1);
+ top.addSignal(s2);
+ relation.addSignals(s2, s1);
+ avspec.addRelation(relation);
+ for (TMLTask t1 : channel.getOriginTasks()) {
+ for (TMLTask t2 : channel.getDestinationTasks()) {
+ AvatarRelation ar = new AvatarRelation(channel.getName(), taskBlockMap.get(t1), taskBlockMap.get(t2), channel.getReferenceObject());
+ ar.setPrivate(originDestMap.get(t1.getName() + "__" + t2.getName()) == 1);
+ //Find in signal
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.IN) {
+ String name = sig.getName();
+ if (name.equals(getName(channel.getName()))) {
+ sig1.add(sig);
+ }
+ }
+ }
+ //Find out signal
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.OUT) {
+ String name = sig.getName();
+ if (name.equals(getName(channel.getName()))) {
+ sig2.add(sig);
+ }
+ }
+ }
+ if (sig1.size() == 0) {
+ sig1.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.IN, null));
+ }
+ if (sig2.size() == 0) {
+ sig2.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.OUT, null));
+ }
+ if (sig1.size() == 1 && sig2.size() == 1) {
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ } else {
+ System.out.println("Failure to match signals for TMLChannel " + channel.getName() + " between " + t1.getName() + " and " + t2.getName());
+ }
+ avspec.addRelation(ar);
+ }
+ }
+ }
+ }
+ for (TMLRequest request : tmlmodel.getRequests()) {
+ for (TMLTask t1 : request.getOriginTasks()) {
+ AvatarRelation ar = new AvatarRelation(request.getName(), taskBlockMap.get(t1), taskBlockMap.get(request.getDestinationTask()), request.getReferenceObject());
+ ar.setPrivate(originDestMap.get(t1.getName() + "__" + request.getDestinationTask().getName()) == 1);
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.IN) {
+ String name = sig.getName();
+
+ if (name.equals(getName(request.getName()))) {
+ sig1.add(sig);
+ }
+ }
+ }
+ //Find out signal
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.OUT) {
+ String name = sig.getName();
- if (name.equals(getName(request.getName()))){
- sig2.add(sig);
- }
- }
- }
- if (sig1.size()==0){
- sig1.add(new AvatarSignal(getName(request.getName()), AvatarSignal.IN, null));
- }
- if (sig2.size()==0){
- sig2.add(new AvatarSignal(getName(request.getName()), AvatarSignal.OUT, null));
- }
- if (sig1.size()==1 && sig2.size()==1){
- ar.addSignals(sig2.get(0), sig1.get(0));
- }
- else {
- //Throw error
- System.out.println("Could not match for " + request.getName());
- }
+ if (name.equals(getName(request.getName()))) {
+ sig2.add(sig);
+ }
+ }
+ }
+ if (sig1.size() == 0) {
+ sig1.add(new AvatarSignal(getName(request.getName()), AvatarSignal.IN, null));
+ }
+ if (sig2.size() == 0) {
+ sig2.add(new AvatarSignal(getName(request.getName()), AvatarSignal.OUT, null));
+ }
+ if (sig1.size() == 1 && sig2.size() == 1) {
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ } else {
+ //Throw error
+ System.out.println("Could not match for " + request.getName());
+ }
- ar.setAsynchronous(false);
- avspec.addRelation(ar);
- }
- }
- for (TMLEvent event: tmlmodel.getEvents()){
-
- AvatarRelation ar = new AvatarRelation(event.getName(), taskBlockMap.get(event.getOriginTask()), taskBlockMap.get(event.getDestinationTask()), event.getReferenceObject());
- ar.setPrivate(originDestMap.get(event.getOriginTask().getName()+"__"+event.getDestinationTask().getName())==1);
- List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
- List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.IN){
- String name = sig.getName();
- if (name.equals(getName(event.getName()))){
- sig1.add(sig);
- }
- }
- }
- //Find out signal
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.OUT){
- String name = sig.getName();
- if (name.equals(getName(event.getName()))){
- sig2.add(sig);
- }
- }
- }
- if (sig1.size()==0){
- sig1.add(new AvatarSignal(getName(event.getName()), AvatarSignal.IN, null));
- }
- if (sig2.size()==0){
- sig2.add(new AvatarSignal(getName(event.getName()), AvatarSignal.OUT, null));
- }
- if (sig1.size()==1 && sig2.size()==1){
- ar.addSignals(sig2.get(0), sig1.get(0));
- }
- else {
- //Throw error
- System.out.println("Could not match for " + event.getName());
- }
- if (event.isBlocking()){
- ar.setAsynchronous(true);
- ar.setBlocking(true);
- ar.setSizeOfFIFO(event.getMaxSize());
- }
- else {
- ar.setAsynchronous(true);
- ar.setBlocking(false);
- ar.setSizeOfFIFO(event.getMaxSize());
+ ar.setAsynchronous(false);
+ avspec.addRelation(ar);
+ }
+ }
+ for (TMLEvent event : tmlmodel.getEvents()) {
+
+ AvatarRelation ar = new AvatarRelation(event.getName(), taskBlockMap.get(event.getOriginTask()), taskBlockMap.get(event.getDestinationTask()), event.getReferenceObject());
+ ar.setPrivate(originDestMap.get(event.getOriginTask().getName() + "__" + event.getDestinationTask().getName()) == 1);
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.IN) {
+ String name = sig.getName();
+ if (name.equals(getName(event.getName()))) {
+ sig1.add(sig);
+ }
+ }
+ }
+ //Find out signal
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.OUT) {
+ String name = sig.getName();
+ if (name.equals(getName(event.getName()))) {
+ sig2.add(sig);
+ }
+ }
+ }
+ if (sig1.size() == 0) {
+ sig1.add(new AvatarSignal(getName(event.getName()), AvatarSignal.IN, null));
+ }
+ if (sig2.size() == 0) {
+ sig2.add(new AvatarSignal(getName(event.getName()), AvatarSignal.OUT, null));
+ }
+ if (sig1.size() == 1 && sig2.size() == 1) {
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ } else {
+ //Throw error
+ System.out.println("Could not match for " + event.getName());
+ }
+ if (event.isBlocking()) {
+ ar.setAsynchronous(true);
+ ar.setBlocking(true);
+ ar.setSizeOfFIFO(event.getMaxSize());
+ } else {
+ ar.setAsynchronous(true);
+ ar.setBlocking(false);
+ ar.setSizeOfFIFO(event.getMaxSize());
+
+ }
+ avspec.addRelation(ar);
+ }
+
+ // System.out.println("Avatar relations " + avspec.getRelations());
+
+ for (AvatarSignal sig : signals) {
+ // System.out.println("signal " + sig.getName());
+ //check that all signals are put in relations
+ AvatarRelation ar = avspec.getAvatarRelationWithSignal(sig);
+ if (ar == null) {
+ System.out.println("missing relation for " + sig.getName());
+ }
+ }
+ //Check if we matched up all signals
+ for (SecurityPattern sp : symKeys.keySet()) {
+ if (symKeys.get(sp).size() > 1) {
+ String keys = "";
+ for (AvatarAttribute key : symKeys.get(sp)) {
+ keys = keys + " " + key.getBlock().getName() + "." + key.getName();
+ }
+ avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge " + keys, null, symKeys.get(sp), true));
+ }
+ }
+ for (SecurityPattern sp : pubKeys.keySet()) {
+ if (pubKeys.get(sp).size() != 0) {
+ String keys = "";
+ List<String> pubKeyNames = new ArrayList<String>();
+ for (AvatarAttribute key : pubKeys.get(sp)) {
+ if (!pubKeyNames.contains(key.getBlock().getName() + "." + key.getName())) {
+ keys = keys + " " + key.getBlock().getName() + "." + key.getName();
+ pubKeyNames.add(key.getBlock().getName() + "." + key.getName());
+ }
+ }
+ // avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge "+keys, null, pubKeys.get(sp),true));
+ //System.out.println("pragma " + keys);
+ }
+ }
+
+ tmlmap.getTMLModeling().secChannelMap = secChannelMap;
- }
- avspec.addRelation(ar);
- }
-
- // System.out.println("Avatar relations " + avspec.getRelations());
-
- for (AvatarSignal sig: signals){
- // System.out.println("signal " + sig.getName());
- //check that all signals are put in relations
- AvatarRelation ar = avspec.getAvatarRelationWithSignal(sig);
- if (ar==null){
- System.out.println("missing relation for " + sig.getName());
- }
- }
- //Check if we matched up all signals
- for (SecurityPattern sp:symKeys.keySet()){
- if (symKeys.get(sp).size()>1){
- String keys = "";
- for (AvatarAttribute key: symKeys.get(sp)){
- keys= keys+" "+key.getBlock().getName() + "."+key.getName();
- }
- avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge "+ keys, null, symKeys.get(sp), true));
- }
- }
- for (SecurityPattern sp:pubKeys.keySet()){
- if (pubKeys.get(sp).size()!=0){
- String keys = "";
- List<String> pubKeyNames = new ArrayList<String>();
- for (AvatarAttribute key: pubKeys.get(sp)){
- if (!pubKeyNames.contains(key.getBlock().getName()+"."+key.getName())){
- keys= keys+" "+key.getBlock().getName() + "."+key.getName();
- pubKeyNames.add(key.getBlock().getName()+"."+key.getName());
- }
- }
- // avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge "+keys, null, pubKeys.get(sp),true));
- //System.out.println("pragma " + keys);
- }
- }
-
- tmlmap.getTMLModeling().secChannelMap = secChannelMap;
-
// System.out.println("avatar spec\n" +avspec);
- return avspec;
- }
+ return avspec;
+ }
- public void backtraceReachability( Map<AvatarPragmaReachability, ProVerifQueryResult> reachabilityResults) {
- for (AvatarPragmaReachability pragma: reachabilityResults.keySet())
- {
- ProVerifQueryResult result = reachabilityResults.get(pragma);
- if (!result.isProved())
- continue;
+ public void backtraceReachability(Map<AvatarPragmaReachability, ProVerifQueryResult> reachabilityResults) {
+ for (AvatarPragmaReachability pragma : reachabilityResults.keySet()) {
+ ProVerifQueryResult result = reachabilityResults.get(pragma);
+ if (!result.isProved())
+ continue;
- int r = result.isSatisfied() ? 1 : 2;
+ int r = result.isSatisfied() ? 1 : 2;
- String s = pragma.getBlock().getName() + "__" + pragma.getState().getName();
+ String s = pragma.getBlock().getName() + "__" + pragma.getState().getName();
- if (stateObjectMap.containsKey(s)) {
- Object obj = stateObjectMap.get(s);
- if (obj instanceof TMLADWriteChannel){
- TMLADWriteChannel wc =(TMLADWriteChannel) obj;
- wc.reachabilityInformation=r;
- }
- if (obj instanceof TMLADReadChannel){
- TMLADReadChannel wc =(TMLADReadChannel) obj;
- wc.reachabilityInformation=r;
- }
+ if (stateObjectMap.containsKey(s)) {
+ Object obj = stateObjectMap.get(s);
+ if (obj instanceof TMLADWriteChannel) {
+ TMLADWriteChannel wc = (TMLADWriteChannel) obj;
+ wc.reachabilityInformation = r;
+ }
+ if (obj instanceof TMLADReadChannel) {
+ TMLADReadChannel wc = (TMLADReadChannel) obj;
+ wc.reachabilityInformation = r;
+ }
- if (obj instanceof TMLADSendEvent){
- TMLADSendEvent wc =(TMLADSendEvent) obj;
- wc.reachabilityInformation=r;
- }
+ if (obj instanceof TMLADSendEvent) {
+ TMLADSendEvent wc = (TMLADSendEvent) obj;
+ wc.reachabilityInformation = r;
+ }
+
+ if (obj instanceof TMLADSendRequest) {
+ TMLADSendRequest wc = (TMLADSendRequest) obj;
+ wc.reachabilityInformation = r;
+ }
+ if (obj instanceof TMLADWaitEvent) {
+ TMLADWaitEvent wc = (TMLADWaitEvent) obj;
+ wc.reachabilityInformation = r;
+ }
+ }
+ }
+ }
+
+ public void distributeKeys() {
+ List<TMLTask> tasks = tmlmap.getTMLModeling().getTasks();
+ for (TMLTask t : accessKeys.keySet()) {
+ AvatarBlock b = taskBlockMap.get(t);
+ for (SecurityPattern sp : accessKeys.get(t)) {
+ if (sp.type.equals("Symmetric Encryption") || sp.type.equals("MAC")) {
+ AvatarAttribute key = new AvatarAttribute("key_" + sp.name, AvatarType.INTEGER, b, null);
+ if (symKeys.containsKey(sp)) {
+ symKeys.get(sp).add(key);
+ } else {
+ LinkedList<AvatarAttribute> tmp = new LinkedList<AvatarAttribute>();
+ tmp.add(key);
+ symKeys.put(sp, tmp);
+ }
+ b.addAttribute(key);
+ } else if (sp.type.equals("Asymmetric Encryption")) {
+ AvatarAttribute pubkey = new AvatarAttribute("pubKey_" + sp.name, AvatarType.INTEGER, b, null);
+ b.addAttribute(pubkey);
+
+ AvatarAttribute privkey = new AvatarAttribute("privKey_" + sp.name, AvatarType.INTEGER, b, null);
+ b.addAttribute(privkey);
+ avspec.addPragma(new AvatarPragmaPrivatePublicKey("#PrivatePublicKeys " + b.getName() + " " + privkey.getName() + " " +
+ pubkey.getName(), null, privkey, pubkey));
+ if (pubKeys.containsKey(sp)) {
+ pubKeys.get(sp).add(pubkey);
+ } else {
+ LinkedList<AvatarAttribute> tmp = new LinkedList<AvatarAttribute>();
+ tmp.add(pubkey);
+ pubKeys.put(sp, tmp);
+ }
+ //Distribute public key everywhere
+ for (TMLTask task2 : tasks) {
+ AvatarBlock b2 = taskBlockMap.get(task2);
+ pubkey = new AvatarAttribute("pubKey_" + sp.name, AvatarType.INTEGER, b2, null);
+ b2.addAttribute(pubkey);
+ if (pubKeys.containsKey(sp)) {
+ pubKeys.get(sp).add(pubkey);
+ }
+ }
+ }
+ }
+ }
+
+ }
+
+ public AvatarBlock createFifo(String name) {
+ AvatarBlock fifo = new AvatarBlock("FIFO__FIFO" + name, avspec, null);
+ AvatarState root = new AvatarState("root", null, false, false);
+ AvatarSignal read = new AvatarSignal("readSignal", AvatarSignal.IN, null);
+ AvatarAttribute data = new AvatarAttribute("data", AvatarType.INTEGER, fifo, null);
+ fifo.addAttribute(data);
+ read.addParameter(data);
+ AvatarSignal write = new AvatarSignal("writeSignal", AvatarSignal.OUT, null);
+ write.addParameter(data);
+ AvatarStartState start = new AvatarStartState("start", null);
+ AvatarTransition afterStart = new AvatarTransition(fifo, "afterStart", null);
+ fifo.addSignal(read);
+ fifo.addSignal(write);
+ AvatarTransition toRead = new AvatarTransition(fifo, "toReadSignal", null);
+ AvatarTransition toWrite = new AvatarTransition(fifo, "toWriteSignal", null);
+ AvatarTransition afterRead = new AvatarTransition(fifo, "afterReadSignal", null);
+ AvatarTransition afterWrite = new AvatarTransition(fifo, "afterWriteSignal", null);
+ AvatarActionOnSignal readAction = new AvatarActionOnSignal("read", read, null);
+ AvatarActionOnSignal writeAction = new AvatarActionOnSignal("write", write, null);
+
+ AvatarStateMachine asm = fifo.getStateMachine();
+ asm.addElement(start);
+ asm.setStartState(start);
+ asm.addElement(afterStart);
+ asm.addElement(root);
+ asm.addElement(toRead);
+ asm.addElement(toWrite);
+ asm.addElement(afterRead);
+ asm.addElement(afterWrite);
+ asm.addElement(readAction);
+ asm.addElement(writeAction);
+
+ start.addNext(afterStart);
+ afterStart.addNext(root);
+ root.addNext(toRead);
+ root.addNext(toWrite);
+ toRead.addNext(readAction);
+ toWrite.addNext(writeAction);
+ readAction.addNext(afterRead);
+ writeAction.addNext(afterWrite);
+ afterRead.addNext(root);
+ afterWrite.addNext(root);
+
+ avspec.addBlock(fifo);
+ return fifo;
+ }
- if (obj instanceof TMLADSendRequest){
- TMLADSendRequest wc =(TMLADSendRequest) obj;
- wc.reachabilityInformation=r;
- }
- if (obj instanceof TMLADWaitEvent){
- TMLADWaitEvent wc =(TMLADWaitEvent) obj;
- wc.reachabilityInformation=r;
- }
- }
- }
- }
- public void distributeKeys(){
- List<TMLTask> tasks = tmlmap.getTMLModeling().getTasks();
- for (TMLTask t:accessKeys.keySet()){
- AvatarBlock b = taskBlockMap.get(t);
- for (SecurityPattern sp: accessKeys.get(t)){
- if (sp.type.equals("Symmetric Encryption") || sp.type.equals("MAC")){
- AvatarAttribute key = new AvatarAttribute("key_"+sp.name, AvatarType.INTEGER, b, null);
- if (symKeys.containsKey(sp)){
- symKeys.get(sp).add(key);
- }
- else {
- LinkedList<AvatarAttribute> tmp = new LinkedList<AvatarAttribute>();
- tmp.add(key);
- symKeys.put(sp, tmp);
- }
- b.addAttribute(key);
- }
- else if (sp.type.equals("Asymmetric Encryption")){
- AvatarAttribute pubkey = new AvatarAttribute("pubKey_"+sp.name, AvatarType.INTEGER, b, null);
- b.addAttribute(pubkey);
-
- AvatarAttribute privkey = new AvatarAttribute("privKey_"+sp.name, AvatarType.INTEGER, b, null);
- b.addAttribute(privkey);
- avspec.addPragma(new AvatarPragmaPrivatePublicKey("#PrivatePublicKeys " + b.getName() + " " + privkey.getName() + " " + pubkey.getName(), null, privkey, pubkey));
- if (pubKeys.containsKey(sp)){
- pubKeys.get(sp).add(pubkey);
- }
- else {
- LinkedList<AvatarAttribute> tmp = new LinkedList<AvatarAttribute>();
- tmp.add(pubkey);
- pubKeys.put(sp, tmp);
- }
- //Distribute public key everywhere
- for (TMLTask task2 : tasks){
- AvatarBlock b2 = taskBlockMap.get(task2);
- pubkey = new AvatarAttribute("pubKey_"+sp.name, AvatarType.INTEGER, b2, null);
- b2.addAttribute(pubkey);
- if (pubKeys.containsKey(sp)){
- pubKeys.get(sp).add(pubkey);
- }
- }
- }
- }
- }
-
- }
- public AvatarBlock createFifo(String name){
- AvatarBlock fifo = new AvatarBlock("FIFO__FIFO"+name, avspec, null);
- AvatarState root = new AvatarState("root",null, false, false);
- AvatarSignal read = new AvatarSignal("readSignal", AvatarSignal.IN, null);
- AvatarAttribute data = new AvatarAttribute("data", AvatarType.INTEGER, fifo, null);
- fifo.addAttribute(data);
- read.addParameter(data);
- AvatarSignal write = new AvatarSignal("writeSignal", AvatarSignal.OUT, null);
- write.addParameter(data);
- AvatarStartState start = new AvatarStartState("start", null);
- AvatarTransition afterStart = new AvatarTransition(fifo, "afterStart", null);
- fifo.addSignal(read);
- fifo.addSignal(write);
- AvatarTransition toRead = new AvatarTransition(fifo, "toReadSignal", null);
- AvatarTransition toWrite = new AvatarTransition(fifo, "toWriteSignal", null);
- AvatarTransition afterRead = new AvatarTransition(fifo, "afterReadSignal", null);
- AvatarTransition afterWrite = new AvatarTransition(fifo, "afterWriteSignal", null);
- AvatarActionOnSignal readAction= new AvatarActionOnSignal("read", read, null);
- AvatarActionOnSignal writeAction= new AvatarActionOnSignal("write", write, null);
-
- AvatarStateMachine asm = fifo.getStateMachine();
- asm.addElement(start);
- asm.setStartState(start);
- asm.addElement(afterStart);
- asm.addElement(root);
- asm.addElement(toRead);
- asm.addElement(toWrite);
- asm.addElement(afterRead);
- asm.addElement(afterWrite);
- asm.addElement(readAction);
- asm.addElement(writeAction);
-
- start.addNext(afterStart);
- afterStart.addNext(root);
- root.addNext(toRead);
- root.addNext(toWrite);
- toRead.addNext(readAction);
- toWrite.addNext(writeAction);
- readAction.addNext(afterRead);
- writeAction.addNext(afterWrite);
- afterRead.addNext(root);
- afterWrite.addNext(root);
-
- avspec.addBlock(fifo);
- return fifo;
- }
-
-
public AvatarSpecification convertToSecurityType(AvatarSpecification spec) {
return spec;
}
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index a2ac47c1bd..c7b20fc9af 100644
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -9172,7 +9172,8 @@ public class GTURTLEModeling {
if (blockLevelMap.get(ab) == level) {
if (level == 0) {
TraceManager.addDev("New block at level 0");
- AvatarBDBlock bl = new AvatarBDBlock(xpos, ypos, abd.getMinX(), abd.getMaxX(), abd.getMinY(), abd.getMaxY(), false, null, abd);
+ AvatarBDBlock bl = new AvatarBDBlock(xpos, ypos, abd.getMinX(), abd.getMaxX(), abd.getMinY(), abd.getMaxY(), false,
+ null, abd);
if ((ab.getReferenceObject() != null) && (ab.getReferenceObject() instanceof CDElement)) {
CDElement cd = (CDElement) ab.getReferenceObject();
bl.setUserResize(cd.getX(), cd.getY(), cd.getWidth(), cd.getHeight());
@@ -9189,7 +9190,8 @@ public class GTURTLEModeling {
xpos += 100 * blockSizeMap.get(ab) + 200;
} else {
TraceManager.addDev("New block at level " + level);
- AvatarBDBlock father = blockMap.get(ab.getFather().getName().split("__")[ab.getFather().getName().split("__").length - 1]);
+ AvatarBDBlock father =
+ blockMap.get(ab.getFather().getName().split("__")[ab.getFather().getName().split("__").length - 1]);
TraceManager.addDev("Father name: " + father.getBlockName());
if (father == null) {
//
@@ -9289,43 +9291,50 @@ public class GTURTLEModeling {
//Add Pragmas
- /*AvatarBDPragma pragma = new AvatarBDPragma(xpos, ypos, xpos, xpos * 2, ypos, ypos * 2, false, null, abd);
- // String[] arr = new String[avspec.getPragmas().size()];
- String s = "";
- // int i=0;
- for (
- AvatarPragma p : avspec.getPragmas()) {
- // arr[i] = p.getName();
- String t = "";
- String[] split = p.getName().split(" ");
- if (p.getName().contains("#Confidentiality")) {
- for (String str : split) {
- if (str.contains(".")) {
- String tmp = str.split("\\.")[0];
- String tmp2 = str.split("\\.")[1];
- t = t.concat(tmp.split("__")[tmp.split("__").length - 1] + "." + tmp2.split("__")[tmp2.split("__").length - 1] + " ");
- } else {
- t = t.concat(str + " ");
+
+ if (avspec.getPragmas().size() > 0) {
+ AvatarBDPragma pragma = new AvatarBDPragma(xpos, ypos, xpos, xpos * 2, ypos, ypos * 2, false, null, abd);
+ // String[] arr = new String[avspec.getPragmas().size()];
+ String s = "";
+ // int i=0;
+ for (AvatarPragma p : avspec.getPragmas()) {
+
+ // arr[i] = p.getName();
+ String t = "";
+ String[] split = p.getName().split(" ");
+ if (p.getName().contains("#Confidentiality")) {
+ for (String str : split) {
+ if (str.contains(".")) {
+ String tmp = str.split("\\.")[0];
+ String tmp2 = str.split("\\.")[1];
+ t = t.concat(tmp.split("__")[tmp.split("__").length - 1] +
+ "." + tmp2.split("__")[tmp2.split("__").length - 1] + " ");
+ } else {
+ t = t.concat(str + " ");
+ }
}
+ } else if (p.getName().contains("Authenticity")) {
+ t = p.getName();
+ } else if (p.getName().contains("Initial")) {
+ t = p.getName();
+ } else {
+ t = p.getName();
}
- } else if (p.getName().contains("Authenticity")) {
- t = p.getName();
- } else if (p.getName().contains("Initial")) {
- t = p.getName();
- } else {
- t = p.getName();
+ s = s.concat(t + "\n");
+ // i++;
}
- s = s.concat(t + "\n");
- // i++;
+ pragma.setValue(s);
+ pragma.makeValue();
+ abd.addComponent(pragma, xpos, ypos, false, true);
}
- pragma.setValue(s);
- pragma.makeValue();
- abd.addComponent(pragma, xpos, ypos, false, true);
+
+
+
//Add message and key datatype if there is a cryptoblock
xpos = 50;
- ypos += 200;*/
+ ypos += 200;
if (hasCrypto) {
AvatarBDDataType message = new AvatarBDDataType(xpos, ypos, xpos, xpos * 2, ypos, ypos * 2, false, null, abd);
message.setValue("Message");
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index a463f50682..d687209e03 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -4787,17 +4787,21 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
* (tp instanceof TMLComponentDesignPanel) {
* ((TMLComponentDesignPanel)tp).modelBacktracingProVerif(pvoa); } }
*/
- gtm.getTMLMapping().getTMLModeling().clearBacktracing();
- gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, getTabName(tp));
- gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
- gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa, getTabName(tp));
+ if (gtm.getTMLMapping() != null) {
+ gtm.getTMLMapping().getTMLModeling().clearBacktracing();
+ gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, getTabName(tp));
+ gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
+ gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa, getTabName(tp));
+ }
} else if (tp instanceof TMLComponentDesignPanel) {
TraceManager.addDev("Backtracing to TMLComponentDesignPanel");
- gtm.getTMLMapping().getTMLModeling().clearBacktracing();
- gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, "Default Mapping");
- gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
- gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa, "Default Mapping");
+ if (gtm.getTMLMapping() != null) {
+ gtm.getTMLMapping().getTMLModeling().clearBacktracing();
+ gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, "Default Mapping");
+ gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
+ gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa, "Default Mapping");
+ }
}
return;
}
diff --git a/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java b/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
index af00092c29..d6b6d81bf9 100755
--- a/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
+++ b/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
@@ -374,6 +374,10 @@
Color c = g.getColor();
Color c1;
Color c2;
+
+ //TraceManager.addDev("Drawing port " + getPortName() + ": checkStrongAuthStatus=" + checkStrongAuthStatus);
+ //TraceManager.addDev("Drawing port " + getPortName() + ": checkWeakAuthStatus=" + checkWeakAuthStatus);
+
switch (checkStrongAuthStatus) {
case 2:
c1 = Color.green;
@@ -1268,10 +1272,12 @@
public void setStrongAuthStatus(int _status) {
+ TraceManager.addDev("Port " + getPortName() + ": Strong Auth status set to " + _status );
checkStrongAuthStatus = _status;
}
public void setWeakAuthStatus(int _status) {
+ TraceManager.addDev("Port " + getPortName() + ": Weak Auth status set to " + _status );
checkWeakAuthStatus = _status;
}
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 4391c4f358..9a172e77e9 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -138,6 +138,8 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
private static boolean PI_CALCULUS = true;
private static int LOOP_ITERATION = 1;
+ private static boolean DRAW_AVATAR = false;
+
protected MainGUI mgui;
private AvatarDesignPanel adp;
@@ -181,7 +183,7 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
// Security generation buttons
ButtonGroup secGroup;
- protected JCheckBox autoConf, autoWeakAuth, autoStrongAuth, custom, addHSM;
+ protected JCheckBox drawAvatarDesign, autoConf, autoWeakAuth, autoStrongAuth, custom, addHSM;
protected JRadioButton autoSec, autoMapKeys;
protected JTextField encTime, decTime, secOverhead;
protected JComboBox<String> addtoCPU;
@@ -496,6 +498,8 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
GridBagConstraints.BOTH, insets, 0, 0));
curY++;
+
+
JLabel gen = new JLabel("Generate ProVerif code in: ");
addComponent(jp01, gen, 0, curY, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
@@ -554,6 +558,13 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
curY++;
}
+ if (mgui.isExperimentalOn()) {
+ drawAvatarDesign = new JCheckBox("Draw Avatar model");
+ drawAvatarDesign.setSelected(DRAW_AVATAR);
+ drawAvatarDesign.addActionListener(this);
+ addComponent(jp01, drawAvatarDesign, 2, curY, 2, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
+ }
+
JLabel empty = new JLabel("");
jp01.add(empty, new GridBagConstraints(0, curY, 3, 1, 1.0, 1.0, GridBagConstraints.CENTER,
GridBagConstraints.BOTH, insets, 0, 0));
@@ -663,6 +674,11 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
public void actionPerformed(ActionEvent evt) {
String command = evt.getActionCommand();
+ if (evt.getSource() == drawAvatarDesign) {
+ DRAW_AVATAR = drawAvatarDesign.isSelected();
+ return;
+ }
+
switch (command) {
case "Start":
startProcess();
@@ -902,16 +918,21 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
TraceManager.addDev("FILE EXISTS!!!");
}
+
+
if (!mgui.gtm.generateProVerifFromAVATAR(
pathCode,
- stateReachabilityAll.isSelected() ? REACHABILITY_ALL : stateReachabilitySelected.isSelected() ? REACHABILITY_SELECTED : REACHABILITY_NONE,
+ stateReachabilityAll.isSelected() ? REACHABILITY_ALL :
+ stateReachabilitySelected.isSelected() ? REACHABILITY_SELECTED : REACHABILITY_NONE,
typedLanguage.isSelected(),
privateChannelDup.isSelected(),
loopLimit.getText())
) {
throw new ProVerifVerificationException("Could not generate proverif code");
}
-
+
+
+
String cmd = exe2.getText().trim();
@@ -943,6 +964,12 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
mgui.modelBacktracingProVerif(pvoa);
+ if (drawAvatarDesign != null) {
+ if (drawAvatarDesign.isSelected()) {
+ mgui.drawAvatarSpecification(mgui.gtm.getAvatarSpecification());
+ }
+ }
+
mode = NOT_STARTED;
}
--
GitLab