diff --git a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
index 69eb54cfa615ccfd3114eafb5dcd9b91340f9cd9..932a74073f476b904837c299c1bcb87c231b266c 100755
--- a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -557,6 +557,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
String varName = AVATAR2ProVerif.translateTerm (trueAttr, null);
this.spec.addDeclaration (new ProVerifQueryAtt (varName, true));
+
TraceManager.addDev("| attacker (" + varName + ")");
this.secrecyChecked.add (trueAttr);
@@ -1255,7 +1256,9 @@ public class AVATAR2ProVerif implements AvatarTranslator {
if (this.secrecyChecked.contains (attr)) {
UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "'" + attr.getName () + "' is re-assigned while its secrecy is being checked. Note that the proof will only guarantee the secrecy of the initial value of " + attr.getName () + ".");
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ if (this.avspec.getReferenceObject() instanceof AvatarDesignPanel){
+ ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ }
ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
this.warnings.add(ce);
}
diff --git a/src/main/java/dseengine/DSEConfiguration.java b/src/main/java/dseengine/DSEConfiguration.java
index d8cf3eb5f2712bb6735890c39f0333f438471529..7e61f1c9783ebc185febd9e5760e7adee73a4278 100755
--- a/src/main/java/dseengine/DSEConfiguration.java
+++ b/src/main/java/dseengine/DSEConfiguration.java
@@ -1501,7 +1501,7 @@ public class DSEConfiguration implements Runnable {
// TraceManager.addDev("tmlcdp " + tmlcdp);
//
//Repeat for secured mapping
- TMLMapping<TGComponent> secMapping = mainGUI.gtm.autoSecure(mainGUI, "mapping" +(cpt-1),tmla, newArch, encComp, overhead, decComp,true,false,false);
+ TMLMapping<TGComponent> secMapping = mainGUI.gtm.autoSecure(mainGUI, "mapping" +(cpt-1),tmla, newArch, encComp, overhead, decComp,true,false,false, new HashMap<String, java.util.List<String>>());
//Run simulations on this mapping
if (generateAndCompileMappingCode(secMapping, _debug, _optimize) >= 0) {
diff --git a/src/main/java/proverifspec/ProVerifOutputAnalyzer.java b/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
index aa392822f91be29e2125df94a54457c0701e465d..cbdda1594ad0b1831fc3f34333b3ff9feef064b5 100644
--- a/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
+++ b/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
@@ -166,6 +166,8 @@ public class ProVerifOutputAnalyzer {
{
// Remove 'RESULT ' at the begining
str = str.substring(7);
+
+
ProVerifQueryResult result = new ProVerifQueryResult(true, true);
// This concerns an enteringState event
@@ -246,7 +248,9 @@ public class ProVerifOutputAnalyzer {
{
if (pragma instanceof AvatarPragmaSecret)
{
+
String trueName = this.avatar2proverif.getTrueName(((AvatarPragmaSecret) pragma).getArg());
+
if (trueName != null && trueName.equals(attributeName))
{
this.results.put(pragma, result);
diff --git a/src/main/java/tmltranslator/TMLModeling.java b/src/main/java/tmltranslator/TMLModeling.java
index 89a1779d5d8200a704de478ae8ade221c37bb673..31b7ead148bda8a7ed2ee2405933d96172a3b3cd 100755
--- a/src/main/java/tmltranslator/TMLModeling.java
+++ b/src/main/java/tmltranslator/TMLModeling.java
@@ -44,6 +44,7 @@ package tmltranslator;
import avatartranslator.AvatarAttribute;
import avatartranslator.AvatarPragmaAuthenticity;
import avatartranslator.AvatarPragmaSecret;
+import avatartranslator.AvatarPragmaReachability;
import myutil.Conversion;
import myutil.TraceManager;
import proverifspec.ProVerifOutputAnalyzer;
@@ -760,6 +761,7 @@ public class TMLModeling<E> {
Map<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
for (AvatarPragmaSecret pragma: confResults.keySet()) {
+ // System.out.println("pragma " +pragma);
ProVerifQueryResult result = confResults.get(pragma);
if (!result.isProved())
continue;
@@ -768,9 +770,40 @@ public class TMLModeling<E> {
AvatarAttribute attr = pragma.getArg();
TMLChannel channel = getChannelByShortName(attr.getName().replaceAll("_chData",""));
+ boolean invalidate=false;
+ //If an attribute is confidential because it has never been sent on that channel, do not backtrace that result since it is misleading
if (channel!=null){
+ //Mark the result only if the writechannel operator is reachable
+ Map<AvatarPragmaReachability, ProVerifQueryResult> reachResults = pvoa.getReachabilityResults();
+ if (reachResults.size()>0){
+ for (AvatarPragmaReachability reachPragma: reachResults.keySet()){
+ if (reachPragma.getState().getName().equals("aftersignalstate_reachannel_"+channel.getName())){
+ if (!reachResults.get(reachPragma).isSatisfied()){
+ invalidate=true;
+ }
+ }
+ }
+ }
+ //Next check if there exists a writechannel operator that sends unencrypted data
+ boolean found=false;
+ for (TMLTask task: getTasks()){
+ TMLActivity act = task.getActivityDiagram();
+ for (TMLActivityElement elem: act.getElements()){
+ if (elem instanceof TMLWriteChannel){
+ TMLWriteChannel wr = (TMLWriteChannel) elem;
+ if(wr.getChannel(0).getName().equals(channel.getName())){
+ if (wr.securityPattern==null){
+ found=true;
+ }
+ }
+ }
+ }
+ }
+ if (!found){
+ invalidate=true;
+ }
for (TMLCPrimitivePort port:channel.ports){
- if (port.checkConf){
+ if (port.checkConf && !invalidate){
port.checkConfStatus = r;
port.mappingName= mappingName;
}
@@ -796,6 +829,7 @@ public class TMLModeling<E> {
ev.port2.mappingName=mappingName;
}
}
+
List<String> channels=secChannelMap.get(attr.getName());
if (channels != null) {
for (String channelName: channels) {
@@ -810,7 +844,7 @@ public class TMLModeling<E> {
}
}
}
- for (TMLTask t:getTasks()){
+ /*for (TMLTask t:getTasks()){
if (t.getReferenceObject()==null){
continue;
}
@@ -821,7 +855,7 @@ public class TMLModeling<E> {
if (a.getId().equals(attr.getName()))
a.setConfidentialityVerification(result.isSatisfied() ? TAttribute.CONFIDENTIALITY_OK : TAttribute.CONFIDENTIALITY_KO);
}
- }
+ }*/
}
}
public TGComponent getTGComponent(){
@@ -978,7 +1012,7 @@ public class TMLModeling<E> {
}
}
signalName = s.toString().split("__decrypt")[0];
- TraceManager.addDev("signalName " +signalName);
+
/*for (TMLTask t: getTasks()){
if (signalName.contains(t.getName())){
signalName = signalName.replace(t.getName()+"__","");
diff --git a/src/main/java/tmltranslator/TMLTextSpecification.java b/src/main/java/tmltranslator/TMLTextSpecification.java
index 61d13dea36d765567c8c9a609a2b566dd1c26973..b3fcddaba73fd4e0277b54d1e2770ffcade42e58 100755
--- a/src/main/java/tmltranslator/TMLTextSpecification.java
+++ b/src/main/java/tmltranslator/TMLTextSpecification.java
@@ -47,11 +47,17 @@ import myutil.FileException;
import myutil.FileUtils;
import myutil.TraceManager;
+import tmltranslator.SecurityPattern;
+
import java.io.BufferedReader;
import java.io.File;
import java.io.StringReader;
import java.util.ArrayList;
import java.util.Date;
+import java.util.Map;
+import java.util.HashMap;
+
+
import common.SpecConfigTTool;
@@ -68,6 +74,15 @@ public class TMLTextSpecification<E> {
public final static String CR2 = "\n\n";
public final static String SC = ";";
public final static String C = ",";
+
+
+ public final static String AENCRYPT="AE";
+ public final static String SENCRYPT="SE";
+ public final static String MAC="MAC";
+ public final static String NONCE="NONCE";
+ public final static String HASH="HASH";
+ public final static String ADV="ADV";
+
private String spec;
private String title;
@@ -85,6 +100,8 @@ public class TMLTextSpecification<E> {
private TMLActivityElement tmlae;
private ArrayList<TMLParserSaveElt> parses;
+ private Map<String, SecurityPattern> securityPatternMap = new HashMap<String, SecurityPattern>();
+
private static String keywords[] = {"BOOL", "INT", "NAT", "CHANNEL", "EVENT", "REQUEST", "LOSSYCHANNEL", "LOSSYEVENT", "LOSSYREQUEST", "BRBW", "NBRNBW",
"BRNBW", "INF", "NIB", "NINB", "TASK", "ENDTASK", "IF", "ELSE", "ORIF", "ENDIF", "FOR", "ENDFOR",
"SELECTEVT", "CASE", "ENDSELECTEVT", "ENDCASE", "WRITE", "READ", "WAIT", "NOTIFY", "NOTIFIED", "RAND", "CASERAND", "ENDRAND", "ENDCASERAND", "EXECI", "EXECC", "DELAY", "RANDOM",
@@ -96,6 +113,10 @@ public class TMLTextSpecification<E> {
private String beginArray[] = {"TASK", "FOR", "IF", "ELSE", "ORIF", "SELECTEVT", "CASE", "RAND", "CASERAND", "RANDOMSEQ", "SEQ"};
private String endArray[] = {"ENDTASK", "ENDFOR", "ENDIF", "ELSE", "ORIF", "ENDSELECTEVT", "ENDCASE", "ENDRAND", "ENDCASERAND", "ENDRANDOMSEQ", "ENDSEQ"};
+// New argument to be added on EXECC for security: CC_name Type Encrypt_complexity Decrypt_Complexity Overhead Size Nonce Key
+// New argument on Read/Write Channels: CC_name
+
+
public TMLTextSpecification(String _title) {
title = _title;
}
@@ -185,16 +206,23 @@ public class TMLTextSpecification<E> {
public String toString() {
return spec;
}
+
+
public String toTextFormat(TMLModeling<E> tmlm) {
tmlm.removeForksAndJoins();
tmlm.sortByName();
spec = makeDeclarations(tmlm);
+ //Set up Cryptographic Configurations
+
spec += makeTasks(tmlm);
indent();
return spec;
}
+
+
+
public String makeDeclarations(TMLModeling<E> tmlm) {
int i;
String sb = "";
@@ -344,7 +372,31 @@ public class TMLTextSpecification<E> {
return code + makeBehavior(task, elt.getNextElement(0));
} else if (elt instanceof TMLExecC) {
- code = "EXECC" + SP + modifyString(((TMLExecC)elt).getAction()) + CR;
+ if (elt.securityPattern==null){
+ code = "EXECC" + SP + modifyString(((TMLExecC)elt).getAction()) + CR;
+ }
+ else {
+ String type="";
+ if (elt.securityPattern.type.equals("Asymmetric Encryption")){
+ type = AENCRYPT;
+ }
+ else if (elt.securityPattern.type.equals("Symmetric Encryption")){
+ type = SENCRYPT;
+ }
+ else if (elt.securityPattern.type.equals("MAC")){
+ type = MAC;
+ }
+ else if (elt.securityPattern.type.equals("Nonce")){
+ type = NONCE;
+ }
+ else if (elt.securityPattern.type.equals("Hash")){
+ type = HASH;
+ }
+ else {
+ type = ADV;
+ }
+ code = "EXECC" + SP + modifyString(((TMLExecC)elt).getAction()) + SP + elt.securityPattern.name + SP + type + SP + elt.securityPattern.encTime + SP + elt.securityPattern.decTime + SP + elt.securityPattern.overhead + SP + elt.securityPattern.size + SP + elt.securityPattern.nonce + SP + elt.securityPattern.key+ CR;
+ }
return code + makeBehavior(task, elt.getNextElement(0));
} else if (elt instanceof TMLExecCInterval) {
@@ -387,12 +439,23 @@ public class TMLTextSpecification<E> {
for(int k=0; k<tmlch.getNbOfChannels(); k++) {
code = code + tmlch.getChannel(k).getName() + SP;
}
- code = code + modifyString(tmlch.getNbOfSamples()) + CR;
+ code = code + modifyString(tmlch.getNbOfSamples());
+ if (elt.securityPattern!=null){
+ code = code + SP + elt.securityPattern.name + CR;
+ }
+ else {
+ code = code + CR;
+ }
return code + makeBehavior(task, elt.getNextElement(0));
} else if (elt instanceof TMLReadChannel) {
tmlch = (TMLActivityElementChannel)elt;
- code = "READ " + tmlch.getChannel(0).getName() + SP + modifyString(tmlch.getNbOfSamples()) + CR;
+ if (elt.securityPattern==null){
+ code = "READ " + tmlch.getChannel(0).getName() + SP + modifyString(tmlch.getNbOfSamples()) + CR;
+ }
+ else {
+ code = "READ " + tmlch.getChannel(0).getName() + SP + modifyString(tmlch.getNbOfSamples()) + SP + elt.securityPattern.name + CR;
+ }
return code + makeBehavior(task, elt.getNextElement(0));
} else if (elt instanceof TMLSendEvent) {
@@ -595,6 +658,35 @@ public class TMLTextSpecification<E> {
parses = new ArrayList<TMLParserSaveElt>();
+ //Start by reading once and creating all Cryptographic Configuration
+ try {
+ while((s = br.readLine()) != null) {
+ if (s != null) {
+ s = s.trim();
+ //TraceManager.addDev("s=" + s);
+ s = removeUndesiredWhiteSpaces(s, lineNb);
+ s1 = Conversion.replaceAllString(s, "\t", " ");
+ s1 = Conversion.replaceRecursiveAllString(s1, " ", " ");
+ //TraceManager.addDev("s1=" + s1);
+ if (s1 != null) {
+ split = s1.split("\\s");
+ if (split.length > 0) {
+ findSec(split);
+
+ }
+ }
+
+ lineNb++;
+ }
+ }
+
+ } catch (Exception e){
+ TraceManager.addError("Exception when reading specification: " + e.getMessage());
+ addError(0, lineNb, 0, "Exception when reading specification");
+ }
+
+ lineNb=0;
+ br = new BufferedReader(new StringReader(spec));
try {
while((s = br.readLine()) != null) {
if (s != null) {
@@ -622,6 +714,38 @@ public class TMLTextSpecification<E> {
}
}
+ public void findSec(String[] _split){
+ if (isInstruction(_split[0],"EXECC")){
+ if (_split.length>4){
+ String ccName = _split[3];
+ String type = _split[4];
+ String stringType="";
+ if (type.equals(AENCRYPT)){
+ stringType="Symmetric Encryption";
+ }
+ else if (type.equals(SENCRYPT)){
+ stringType="Symmetric Encryption";
+ }
+ else if (type.equals(HASH)){
+ stringType = "Hash";
+ }
+ else if (type.equals(MAC)){
+ stringType = "MAC";
+ }
+ else if (type.equals(NONCE)){
+ stringType = "Nonce";
+ }
+ else if (type.equals(ADV)){
+ stringType = "Advanced";
+ }
+ if (!stringType.equals("")){
+ SecurityPattern sp = new SecurityPattern(ccName, stringType, _split[6], _split[7], _split[4], _split[5], _split[8], "", _split[9]);
+ securityPatternMap.put(ccName, sp);
+ }
+ }
+ }
+ }
+
public void addError(int _type, int _lineNb, int _charNb, String _msg) {
TMLTXTError error = new TMLTXTError(_type);
error.lineNb = _lineNb;
@@ -1213,8 +1337,8 @@ public class TMLTextSpecification<E> {
inTaskDec = false;
// inTaskBehavior = true;
- if (_split.length != 3) {
- error = "A READ operation must be declared with exactly 3 parameters, and not " + (_split.length - 1) ;
+ if (_split.length != 3 && _split.length!= 4) {
+ error = "A READ operation must be declared with exactly 3 or 4 parameters, and not " + (_split.length - 1) ;
addError(0, _lineNb, 0, error);
return -1;
}
@@ -1245,6 +1369,13 @@ public class TMLTextSpecification<E> {
tmlrch.setNbOfSamples(_split[2]);
task.getActivityDiagram().addElement(tmlrch);
tmlae.addNext(tmlrch);
+
+ if (_split.length==4){
+ if (securityPatternMap.containsKey(_split[3])){
+ tmlrch.securityPattern = securityPatternMap.get(_split[3]);
+ }
+ }
+
tmlae = tmlrch;
} // READ
@@ -1263,8 +1394,10 @@ public class TMLTextSpecification<E> {
inTaskDec = false;
// inTaskBehavior = true;
- if (_split.length < 3) {
- error = "A WRITE operation must be declared with at most 3 parameters, and not " + (_split.length - 1) ;
+
+
+ if (_split.length > 5 || _split.length <2) {
+ error = "A WRITE operation must be declared with at most 4 parameters, and not " + (_split.length - 1) ;
addError(0, _lineNb, 0, error);
return -1;
}
@@ -1275,29 +1408,56 @@ public class TMLTextSpecification<E> {
//TraceManager.addDev("Handling write channel 1");
TMLWriteChannel tmlwch = new TMLWriteChannel(_split[1], null);
- for(int k=0; k<_split.length-2; k++) {
- //TraceManager.addDev("Handling write channel 1.1");
- ch = tmlm.getChannelByName(_split[1+k]);
- if (ch == null ){
- error = "Undeclared channel: " + _split[1+k];
- addError(0, _lineNb, 0, error);
- return -1;
- }
- //TraceManager.addDev("Handling write channel 1.2 for task: " + task.getName());
- if (!(ch.hasOriginTask(task))){
- error = "WRITE operations must be done only in origin task(s). Should be in task(s): " + ch.getNameOfOriginTasks();
- addError(0, _lineNb, 0, error);
- return -1;
- }
- //TraceManager.addDev("Handling write channel 1.3");
-
- tmlwch.addChannel(ch);
- }
-
- //TraceManager.addDev("Handling write channel 2");
+ if (_split.length>3){
+ if (securityPatternMap.containsKey(_split[_split.length-1])){
+ tmlwch.securityPattern = securityPatternMap.get(_split[_split.length-1]);
+ }
+ for(int k=0; k<_split.length-3; k++) {
+ //TraceManager.addDev("Handling write channel 1.1");
+ ch = tmlm.getChannelByName(_split[1+k]);
+ if (ch == null ){
+ error = "Undeclared channel: " + _split[1+k];
+ addError(0, _lineNb, 0, error);
+ return -1;
+ }
+ //TraceManager.addDev("Handling write channel 1.2 for task: " + task.getName());
+ if (!(ch.hasOriginTask(task))){
+ error = "WRITE operations must be done only in origin task(s). Should be in task(s): " + ch.getNameOfOriginTasks();
+ addError(0, _lineNb, 0, error);
+ return -1;
+ }
+ //TraceManager.addDev("Handling write channel 1.3");
+
+ tmlwch.addChannel(ch);
+ }
+ }
+ else {
+
+ for(int k=0; k<_split.length-2; k++) {
+ //TraceManager.addDev("Handling write channel 1.1");
+ ch = tmlm.getChannelByName(_split[1+k]);
+ if (ch == null ){
+ error = "Undeclared channel: " + _split[1+k];
+ addError(0, _lineNb, 0, error);
+ return -1;
+ }
+ //TraceManager.addDev("Handling write channel 1.2 for task: " + task.getName());
+ if (!(ch.hasOriginTask(task))){
+ error = "WRITE operations must be done only in origin task(s). Should be in task(s): " + ch.getNameOfOriginTasks();
+ addError(0, _lineNb, 0, error);
+ return -1;
+ }
+ //TraceManager.addDev("Handling write channel 1.3");
+
+ tmlwch.addChannel(ch);
+ }
+ }
+ //TraceManager.addDev("Handling write channel 2");
tmlwch.setNbOfSamples(_split[2]);
task.getActivityDiagram().addElement(tmlwch);
tmlae.addNext(tmlwch);
+
+
tmlae = tmlwch;
} // WRITE
@@ -2301,26 +2461,37 @@ public class TMLTextSpecification<E> {
inTask = true;
inTaskDec = false;
// inTaskBehavior = true;
-
- if ((_split.length < 2) ||(_split.length > 4)) {
- error = "An EXECC operation must be declared with 1 or 2 parameters, and not " + (_split.length - 1) ;
- addError(0, _lineNb, 0, error);
- return -1;
- }
-
- if (_split.length == 2) {
- TMLExecC execc = new TMLExecC("execc", null);
- execc.setAction(_split[1]);
- tmlae.addNext(execc);
- task.getActivityDiagram().addElement(execc);
- tmlae = execc;
- } else {
- TMLExecCInterval execci = new TMLExecCInterval("execci", null);
- execci.setMinDelay(_split[1]);
- execci.setMaxDelay(_split[2]);
- tmlae.addNext(execci);
- task.getActivityDiagram().addElement(execci);
- tmlae = execci;
+ if (_split.length>4){
+ if (securityPatternMap.containsKey(_split[2])){
+ //Security operation
+ TMLExecC execc = new TMLExecC("execc", null);
+ execc.setAction(_split[1]);
+ execc.securityPattern = securityPatternMap.get(_split[2]);
+ tmlae.addNext(execc);
+ task.getActivityDiagram().addElement(execc);
+ tmlae = execc;
+ }
+ }
+ else {
+ if ((_split.length < 2) ||(_split.length > 4)) {
+ error = "An EXECC operation must be declared with 1, 2 parameters, and not " + (_split.length - 1) ;
+ addError(0, _lineNb, 0, error);
+ return -1;
+ }
+ if (_split.length == 2) {
+ TMLExecC execc = new TMLExecC("execc", null);
+ execc.setAction(_split[1]);
+ tmlae.addNext(execc);
+ task.getActivityDiagram().addElement(execc);
+ tmlae = execc;
+ } else {
+ TMLExecCInterval execci = new TMLExecCInterval("execci", null);
+ execci.setMinDelay(_split[1]);
+ execci.setMaxDelay(_split[2]);
+ tmlae.addNext(execci);
+ task.getActivityDiagram().addElement(execci);
+ tmlae = execci;
+ }
}
} // EXECC
diff --git a/src/main/java/tmltranslator/toavatar/TML2Avatar.java b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
index 5f07b740da043ca8dae91cb23f5027c1f4b020d9..8ef89d096b5ac82891979a58d7062d503ed7cf05 100644
--- a/src/main/java/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
@@ -1675,497 +1675,519 @@ public class TML2Avatar {
tran.addNext(newStart);
}*/
- }
-
-
- 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 = 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));
- //TraceManager.addDev("adding pragma " + s);
- 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")) {
- AvatarRelation ar = new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()), taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
- ar.setPrivate(false);
- 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);
- }
- }
- //TraceManager.addDev(channel.getName() + " " +channel.getOriginTask().getName() + " " + channel.getDestinationTask().getName());
- //Find in signal
- //Sig1 contains IN Signals, Sig2 contains OUT signals
- List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
- List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
- for (AvatarSignal sig : taskBlockMap.get(channel.getDestinationTask()).getSignals()) {
- if (sig.getInOut() == AvatarSignal.IN) {
- String name = sig.getName();
- String tmp = getName(channel.getName());
- if (name.equals(tmp.split("JOIN")[tmp.split("JOIN").length - 1]) || name.equals(tmp)) {
- sig1.add(sig);
- }
- }
- }
- for (AvatarSignal sig : taskBlockMap.get(channel.getOriginTask()).getSignals()) {
- if (sig.getInOut() == AvatarSignal.OUT) {
- String name = sig.getName();
- String tmp = getName(channel.getName());
- if (name.equals(tmp.split("JOIN")[tmp.split("JOIN").length - 1]) || name.equals(tmp)) {
- sig2.add(sig);
- }
- }
- }
- TraceManager.addDev("Signals " + sig1 + " " + sig2);
- 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));
- TraceManager.addDev("Set " + sig2.get(0) + " and write");
- ar2.setAsynchronous(false);
- avspec.addRelation(ar2);
- } else {
- ar.addSignals(sig2.get(0), sig1.get(0));
- }
- }
- avspec.addRelation(ar);
- } else if (channel.isBasicChannel()) {
- //TraceManager.addDev("checking 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);
- if (path.size() != 0) {
- ar.setPrivate(true);
- for (HwCommunicationNode node : path) {
- if (node instanceof HwBus) {
- if (((HwBus) node).privacy == 0) {
- ar.setPrivate(false);
- }
- }
- }
- } else {
- ar.setPrivate(originDestMap.get(channel.getOriginTask().getName() + "__" + channel.getDestinationTask().getName()) == 1);
- }
- 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
- 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) {
- 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));
- TraceManager.addDev("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);
- TraceManager.addDev("Failure to match signals for TMLChannel " + channel.getName());
- }
- }
- avspec.addRelation(ar);
- } else {
- TraceManager.addDev("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 {
- TraceManager.addDev("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
- TraceManager.addDev("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
- TraceManager.addDev("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());
+ asm.setStartState(ss);
- }
- avspec.addRelation(ar);
- }
- for (AvatarSignal sig : signals) {
- //check that all signals are put in relations
- AvatarRelation ar = avspec.getAvatarRelationWithSignal(sig);
- if (ar == null) {
- TraceManager.addDev("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 = "";
- for (AvatarAttribute key : pubKeys.get(sp)) {
- keys = keys + " " + key.getBlock().getName() + "." + key.getName();
- }
- avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge " + keys, null, pubKeys.get(sp), true));
- }
- }
- tmlmap.getTMLModeling().secChannelMap = secChannelMap;
+ }
+ 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));
+ }
- // TraceManager.addDev("avatar spec\n" +avspec);
- return avspec;
- }
+ }
- 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;
+ //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));
+ //System.out.println("adding pragma " + s);
+ 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")){
+ AvatarRelation ar= new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()), taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
+ ar.setPrivate(false);
+ 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);
+ }
+ }
+ //System.out.println(channel.getName() + " " +channel.getOriginTask().getName() + " " + channel.getDestinationTask().getName());
+ //Find in signal
+ //Sig1 contains IN Signals, Sig2 contains OUT signals
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ for (AvatarSignal sig: taskBlockMap.get(channel.getDestinationTask()).getSignals()){
+ if (sig.getInOut()==AvatarSignal.IN){
+ String name = sig.getName();
+ String tmp = getName(channel.getName());
+ if (name.equals(tmp.split("JOIN")[tmp.split("JOIN").length-1]) || name.equals(tmp)){
+ sig1.add(sig);
+ }
+ }
+ }
+ for (AvatarSignal sig: taskBlockMap.get(channel.getOriginTask()).getSignals()){
+ if (sig.getInOut()==AvatarSignal.OUT){
+ String name = sig.getName();
+ String tmp = getName(channel.getName());
+ if (name.equals(tmp.split("JOIN")[tmp.split("JOIN").length-1]) || name.equals(tmp)){
+ sig2.add(sig);
+ }
+ }
+ }
- String s = pragma.getBlock().getName() + "__" + pragma.getState().getName();
+ 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));
+ ar2.setAsynchronous(false);
+ avspec.addRelation(ar2);
+ }
+ else {
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ }
+ }
+ avspec.addRelation(ar);
+ }
- 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;
- }
+ else if (channel.isBasicChannel()){
+ //System.out.println("checking 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);
+ if (path.size()!=0){
+ ar.setPrivate(true);
+ for (HwCommunicationNode node:path){
+ if (node instanceof HwBus){
+ if (((HwBus) node).privacy ==0){
+ ar.setPrivate(false);
+ }
+ }
+ }
+ }
+ else {
+ ar.setPrivate(originDestMap.get(channel.getOriginTask().getName()+"__"+channel.getDestinationTask().getName())==1);
+ }
+ 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
+ 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){
+ 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("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 (obj instanceof TMLADSendEvent) {
- TMLADSendEvent wc = (TMLADSendEvent) obj;
- wc.reachabilityInformation = r;
- }
+ 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 (obj instanceof TMLADSendRequest) {
- TMLADSendRequest wc = (TMLADSendRequest) obj;
- wc.reachabilityInformation = r;
- }
- if (obj instanceof TMLADWaitEvent) {
- TMLADWaitEvent wc = (TMLADWaitEvent) obj;
- wc.reachabilityInformation = r;
- }
- }
- }
- }
+ 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());
- 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);
- }
- }
- }
- }
- }
+ }
+ avspec.addRelation(ar);
+ }
+ for (AvatarSignal sig: signals){
+ //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 = "";
+ for (AvatarAttribute key: pubKeys.get(sp)){
+ keys= keys+" "+key.getBlock().getName() + "."+key.getName();
+ }
+ avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge "+keys, null, pubKeys.get(sp),true));
+ }
+ }
+ tmlmap.getTMLModeling().secChannelMap = secChannelMap;
+
+ // System.out.println("avatar spec\n" +avspec);
+ return avspec;
+ }
+
+ 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;
+
+ 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 (obj instanceof TMLADSendEvent){
+ TMLADSendEvent wc =(TMLADSendEvent) obj;
+ wc.reachabilityInformation=r;
+ }
- 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;
}
@@ -2173,3 +2195,4 @@ public class TML2Avatar {
}
+
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index 31b75a24b5bf998742e9e1c6b256809ddd155f26..907017bb74dfc45656762f51e58eb92cdc90fb45 100644
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -1075,12 +1075,12 @@ public class GTURTLEModeling {
}
public TMLMapping<TGComponent> autoSecure(MainGUI gui, String name, TMLMapping<TGComponent> map, TMLArchiPanel newarch) {
- return autoSecure(gui, name, map, newarch, "100", "0", "100", true, false, false);
+ return autoSecure(gui, name, map, newarch, "100", "0", "100", true, false, false, new HashMap<String, java.util.List<String>>());
}
public TMLMapping<TGComponent> autoSecure(MainGUI gui, String name, TMLMapping<TGComponent> map, TMLArchiPanel newarch, boolean autoConf,
boolean autoWeakAuth, boolean autoStrongAuth) {
- return autoSecure(gui, name, map, newarch, "100", "0", "100", autoConf, autoWeakAuth, autoStrongAuth);
+ return autoSecure(gui, name, map, newarch, "100", "0", "100", autoConf, autoWeakAuth, autoStrongAuth,new HashMap<String, java.util.List<String>>());
}
public TMLMapping<TGComponent> autoSecure(MainGUI gui, String encComp, String overhead, String decComp) {
@@ -1091,11 +1091,11 @@ public class GTURTLEModeling {
int arch = gui.tabs.indexOf(tmlap);
gui.cloneRenameTab(arch, "enc");
TMLArchiPanel newarch = (TMLArchiPanel) gui.tabs.get(gui.tabs.size() - 1);
- return autoSecure(gui, "enc", tmap, newarch, encComp, overhead, decComp, true, false, false);
+ return autoSecure(gui, "enc", tmap, newarch, encComp, overhead, decComp, true, false, false,new HashMap<String, java.util.List<String>>());
}
public TMLMapping<TGComponent> autoSecure(MainGUI gui, String encComp, String overhead, String decComp, boolean autoConf, boolean autoWeakAuth,
- boolean autoStrongAuth) {
+ boolean autoStrongAuth,Map<String, List<String>> selectedCpuTasks ) {
if (tmap == null) {
return null;
}
@@ -1103,20 +1103,23 @@ public class GTURTLEModeling {
int arch = gui.tabs.indexOf(tmlap);
gui.cloneRenameTab(arch, "enc");
TMLArchiPanel newarch = (TMLArchiPanel) gui.tabs.get(gui.tabs.size() - 1);
- return autoSecure(gui, "enc", tmap, newarch, encComp, overhead, decComp, autoConf, autoWeakAuth, autoStrongAuth);
+ return autoSecure(gui, "enc", tmap, newarch, encComp, overhead, decComp, autoConf, autoWeakAuth, autoStrongAuth, selectedCpuTasks);
}
public TMLMapping<TGComponent> autoSecure(MainGUI gui, String name, TMLMapping<TGComponent> map, TMLArchiPanel newarch, String encComp, String
overhead, String decComp) {
- return autoSecure(gui, name, tmap, newarch, encComp, overhead, decComp, true, false, false);
+ return autoSecure(gui, name, tmap, newarch, encComp, overhead, decComp, true, false, false, new HashMap<String, java.util.List<String>>());
}
- public TMLMapping<TGComponent> autoSecure(MainGUI gui, String name, TMLMapping<TGComponent> map, TMLArchiPanel newarch, String encComp, String overhead, String decComp, boolean autoConf, boolean autoWeakAuth, boolean autoStrongAuth) {
+
+ public TMLMapping<TGComponent> autoSecure(MainGUI gui, String name, TMLMapping<TGComponent> map, TMLArchiPanel newarch, String encComp, String overhead, String decComp, boolean autoConf, boolean autoWeakAuth, boolean autoStrongAuth, Map<String, List<String>> selectedCpuTasks ) {
//move to another thread
- SecurityGeneration secgen = new SecurityGeneration(gui, name, map, newarch, encComp, overhead, decComp, autoConf, autoWeakAuth, autoStrongAuth);
- return secgen.startThread();
+ SecurityGeneration secgen = new SecurityGeneration(gui, name, map, newarch, encComp, overhead, decComp, autoConf, autoWeakAuth, autoStrongAuth, selectedCpuTasks);
+ tmap = secgen.startThread();
+ autoMapKeys();
+ return tmap;
}
@@ -1187,13 +1190,13 @@ public class GTURTLEModeling {
}
public void autoMapKeys() {
- TraceManager.addDev("auto map keys");
if (tmap == null) {
return;
}
List<HwLink> links = tmap.getArch().getHwLinks();
//Find all Security Patterns, if they don't have an associated memory at encrypt and decrypt, map them
TMLModeling<TGComponent> tmlm = tmap.getTMLModeling();
+
if (tmlm.securityTaskMap == null) {
return;
}
@@ -1377,6 +1380,9 @@ public class GTURTLEModeling {
//tml2uppaal.setChoiceDeterministic(choices);
//tml2uppaal.setSizeInfiniteFIFO(_size);
proverif = avatar2proverif.generateProVerif(true, true, _stateReachability, _typed, allowPrivateChannelDuplication);
+
+ // System.out.println(proverif.getStringSpec());
+
warnings = avatar2proverif.getWarnings();
languageID = PROVERIF;
mgui.setMode(MainGUI.EDIT_PROVERIF_OK);
diff --git a/src/main/java/ui/HSMGeneration.java b/src/main/java/ui/HSMGeneration.java
index 9164d5da9fe8def68586b035b91ee261a1b1f96a..61fa4cf33ae963e3267825c289ec8444c073c8a6 100644
--- a/src/main/java/ui/HSMGeneration.java
+++ b/src/main/java/ui/HSMGeneration.java
@@ -173,7 +173,7 @@ public class HSMGeneration implements Runnable {
TGConnector fromStart;
Map<String, HSMChannel> secChannels = new HashMap<String, HSMChannel>();
- //Add a HSM for each selected CPU on the component diagram
+ //Add a HSM Task for each selected CPU on the component diagram
for (String cpuName : selectedCpuTasks.keySet()) {
Map<String, HSMChannel> hsmChannels = new HashMap<String, HSMChannel>();
TMLCPrimitiveComponent hsm = new TMLCPrimitiveComponent(0, 500, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxY(), false, null, tcdp);
@@ -210,8 +210,6 @@ public class HSMGeneration implements Runnable {
//
continue;
}
- //
- //
for (TMLCPrimitiveComponent comp : comps) {
Map<String, HSMChannel> compChannels = new HashMap<String, HSMChannel>();
@@ -473,15 +471,9 @@ public class HSMGeneration implements Runnable {
}
TGConnectingPoint point = fromStart.getTGConnectingPointP2();
- //Set isEnc to false
- int yShift = 50;
- // TMLADActionState act = new TMLADActionState(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- // act.setValue("isEnc=false");
- // tad.addComponent(act, xpos, ypos + yShift, false, true);
- //fromStart.setP2(act.getTGConnectingPointAtIndex(0));
+ int yShift = 50;
- //Add send request operator
yShift += 50;
TMLADSendRequest req = new TMLADSendRequest(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
@@ -493,11 +485,8 @@ public class HSMGeneration implements Runnable {
tad.addComponent(req, xpos, ypos + yShift, false, true);
- //Add connection
- // fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
- // fromStart.setP1(act.getTGConnectingPointAtIndex(1));
fromStart.setP2(req.getTGConnectingPointAtIndex(0));
- // tad.addComponent(fromStart, xpos, ypos, false, true);
+
yShift += 50;
@@ -547,9 +536,6 @@ public class HSMGeneration implements Runnable {
tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
tad.repaint();
}
- //for (String chan: chanNames){
- // hsmChannels.put(chan, compName);
- //}
}
int xpos = 0;
diff --git a/src/main/java/ui/SecurityGeneration.java b/src/main/java/ui/SecurityGeneration.java
index c8a2e0b0eb76893b45a152dcadbbad3a8e7cb687..bab0866e1ac1567a1cade412d764f89c060914a4 100644
--- a/src/main/java/ui/SecurityGeneration.java
+++ b/src/main/java/ui/SecurityGeneration.java
@@ -46,17 +46,30 @@ public class SecurityGeneration implements Runnable {
String encComp;
String overhead;
String decComp;
+ Map<String, List<String>> selectedCPUTasks;
boolean autoConf;
boolean autoWeakAuth;
boolean autoStrongAuth;
+ int channelIndex=0;
+ TMLComponentDesignPanel tmlcdp;
AVATAR2ProVerif avatar2proverif;
AvatarSpecification avatarspec;
ProVerifSpec proverif;
+ Map<String, HSMChannel> hsmChannels = new HashMap<String, HSMChannel>();
+ Map<String, HSMChannel> secChannels = new HashMap<String, HSMChannel>();
+ Map<String, Integer> channelIndexMap = new HashMap<String, Integer>();
- public SecurityGeneration(MainGUI gui, String name, TMLMapping<TGComponent> map, TMLArchiPanel newarch, String encComp, String overhead, String decComp, boolean autoConf, boolean autoWeakAuth, boolean autoStrongAuth){
+ Map<String, List<HSMChannel>> hsmChannelMap = new HashMap<String, List<HSMChannel>>();
+
+ Map<String, String> taskHSMMap = new HashMap<String, String>();
+ List<String> hsmTasks = new ArrayList<String>();
+
+ Map<String, String> channelSecMap = new HashMap<String, String>();
+
+ public SecurityGeneration(MainGUI gui, String name, TMLMapping<TGComponent> map, TMLArchiPanel newarch, String encComp, String overhead, String decComp, boolean autoConf, boolean autoWeakAuth, boolean autoStrongAuth, Map<String, List<String>> selectedCPUTasks){
this.gui = gui;
this.name=name;
@@ -68,6 +81,7 @@ public class SecurityGeneration implements Runnable {
this.autoConf=autoConf;
this.autoWeakAuth = autoWeakAuth;
this.autoStrongAuth = autoStrongAuth;
+ this.selectedCPUTasks = selectedCPUTasks;
}
public void proverifAnalysis(TMLMapping<TGComponent> map, List<String> nonAuthChans, List<String> nonSecChans) {
if (map == null) {
@@ -145,6 +159,7 @@ public class SecurityGeneration implements Runnable {
}
catch (Exception e){
TraceManager.addDev("Error in Security Generation Thread");
+ System.out.println("Error in Security Generation Thread");
}
return map;
}
@@ -158,9 +173,27 @@ public class SecurityGeneration implements Runnable {
Map<TMLTask, List<String>> nonceInChannels = new HashMap<TMLTask, List<String>>();
Map<TMLTask, List<String>> macOutChannels = new HashMap<TMLTask, List<String>>();
Map<TMLTask, List<String>> macInChannels = new HashMap<TMLTask, List<String>>();
- Map<TMLTask, List<String>> macNonceOutChannels = new HashMap<TMLTask, List<String>>();
- Map<TMLTask, List<String>> macNonceInChannels = new HashMap<TMLTask, List<String>>();
- TraceManager.addDev("mapping " + map.getSummaryTaskMapping());
+
+ Map<TMLTask, List<String>> hsmSecInChannels = new HashMap<TMLTask, List<String>>();
+ Map<TMLTask, List<String>> hsmSecOutChannels = new HashMap<TMLTask, List<String>>();
+
+ //TraceManager.addDev("mapping " + map.getSummaryTaskMapping());
+
+ // Map<String, HSMChannel> secChannels = new HashMap<String, HSMChannel>();
+ Map<String, HSMChannel> hsmChannels = new HashMap<String, HSMChannel>();
+
+
+ for (String cpuName : selectedCPUTasks.keySet()) {
+ for (String task: selectedCPUTasks.get(cpuName)){
+ hsmTasks.add(task);
+ taskHSMMap.put(task, cpuName);
+ }
+ hsmChannelMap.put(cpuName, new ArrayList<HSMChannel>());
+
+ }
+
+
+ //Proverif Analysis channels
List<String> nonAuthChans = new ArrayList<String>();
List<String> nonSecChans = new ArrayList<String>();
@@ -177,7 +210,7 @@ public class SecurityGeneration implements Runnable {
//Create clone of Component Diagram + Activity diagrams to secure
TGComponent tgcomp = map.getTMLModeling().getTGComponent();
- TMLComponentDesignPanel tmlcdp = (TMLComponentDesignPanel) tgcomp.getTDiagramPanel().tp;
+ tmlcdp = (TMLComponentDesignPanel) tgcomp.getTDiagramPanel().tp;
// TMLComponentDesignPanel tmlcdp = map.getTMLCDesignPanel();
int ind = gui.tabs.indexOf(tmlcdp);
if (ind == -1) {
@@ -186,9 +219,9 @@ public class SecurityGeneration implements Runnable {
}
String tabName = gui.getTitleAt(tmlcdp);
gui.cloneRenameTab(ind, name);
- TMLComponentDesignPanel t = (TMLComponentDesignPanel) gui.tabs.get(gui.tabs.size() - 1);
+ tmlcdp = (TMLComponentDesignPanel) gui.tabs.get(gui.tabs.size() - 1);
- TMLComponentTaskDiagramPanel tcdp = t.tmlctdp;
+ TMLComponentTaskDiagramPanel tcdp = tmlcdp.tmlctdp;
//Create clone of architecture panel and map tasks to it
newarch.renameMapping(tabName, tabName + "_" + name);
@@ -203,6 +236,8 @@ public class SecurityGeneration implements Runnable {
List<String> tmp8 = new ArrayList<String>();
List<String> tmp9 = new ArrayList<String>();
List<String> tmp10 = new ArrayList<String>();
+
+
secInChannels.put(task, tmp);
secOutChannels.put(task, tmp2);
toSecure.put(task, tmp3);
@@ -211,13 +246,17 @@ public class SecurityGeneration implements Runnable {
nonceOutChannels.put(task, tmp6);
macInChannels.put(task, tmp7);
macOutChannels.put(task, tmp8);
- macNonceOutChannels.put(task, tmp9);
- macNonceInChannels.put(task, tmp10);
+
+ hsmSecInChannels.put(task, tmp9);
+ hsmSecOutChannels.put(task, tmp10);
+
}
+
+
//With the proverif results, check which channels need to be secured
for (TMLTask task : map.getTMLModeling().getTasks()) {
//Check if all channel operators are secured
- TMLActivityDiagramPanel tad = t.getTMLActivityDiagramPanel(task.getName());
+ TMLActivityDiagramPanel tad = tmlcdp.getTMLActivityDiagramPanel(task.getName());
for (TGComponent tg : tad.getComponentList()) {
if (tg instanceof TMLADWriteChannel) {
TMLADWriteChannel writeChannel = (TMLADWriteChannel) tg;
@@ -226,49 +265,287 @@ public class SecurityGeneration implements Runnable {
TMLChannel chan = tmlmodel.getChannelByName(tabName + "__" + writeChannel.getChannelName());
//
if (chan != null) {
- if (chan.checkConf && autoConf) {
- //
- if (nonSecChans.contains(chan.getOriginTask().getName().split("__")[1] + "__" + writeChannel.getChannelName() + "_chData") && !secInChannels.get(chan.getDestinationTask()).contains(writeChannel.getChannelName())) {
- // if (!securePath(map, chan.getOriginTask(), chan.getDestinationTask())){
- secOutChannels.get(chan.getOriginTask()).add(writeChannel.getChannelName());
- secInChannels.get(chan.getDestinationTask()).add(writeChannel.getChannelName());
- toSecure.get(chan.getOriginTask()).add(chan.getDestinationTask());
- if (chan.checkAuth && autoStrongAuth) {
- toSecureRev.get(chan.getDestinationTask()).add(chan.getOriginTask());
- nonceOutChannels.get(chan.getOriginTask()).add(writeChannel.getChannelName());
- nonceInChannels.get(chan.getDestinationTask()).add(writeChannel.getChannelName());
- }
+ if (chan.checkConf && autoConf && nonSecChans.contains(chan.getOriginTask().getName().split("__")[1] + "__" + writeChannel.getChannelName() + "_chData")) {
+ toSecure.get(chan.getOriginTask()).add(chan.getDestinationTask());
+ if (chan.checkAuth && autoStrongAuth) {
+ toSecureRev.get(chan.getDestinationTask()).add(chan.getOriginTask());
}
- } else if (chan.checkAuth && autoWeakAuth) {
- if (nonAuthChans.contains(chan.getDestinationTask().getName().split("__")[1] + "__" + writeChannel.getChannelName())) {
- toSecure.get(chan.getOriginTask()).add(chan.getDestinationTask());
- macOutChannels.get(chan.getOriginTask()).add(writeChannel.getChannelName());
- macInChannels.get(chan.getDestinationTask()).add(writeChannel.getChannelName());
- if (autoStrongAuth) {
- toSecureRev.get(chan.getDestinationTask()).add(chan.getOriginTask());
- macNonceInChannels.get(chan.getDestinationTask()).add(writeChannel.getChannelName());
- macNonceOutChannels.get(chan.getOriginTask()).add(writeChannel.getChannelName());
+ if (hsmTasks.contains(chan.getOriginTask().getName().split("__")[1])){
+ if (!hsmSecOutChannels.get(chan.getOriginTask()).contains(writeChannel.getChannelName())){
+ HSMChannel hsmchan = new HSMChannel(writeChannel.getChannelName(), chan.getOriginTask().getName().split("__")[1], HSMChannel.SENC);
+ hsmChannelMap.get(taskHSMMap.get(chan.getOriginTask().getName().split("__")[1])).add(hsmchan);
+ hsmSecOutChannels.get(chan.getOriginTask()).add(writeChannel.getChannelName());
+ channelSecMap.put(writeChannel.getChannelName(), "hsmSec_"+writeChannel.getChannelName());
+ if (chan.checkAuth && autoStrongAuth) {
+ nonceOutChannels.get(chan.getOriginTask()).add(writeChannel.getChannelName());
+ hsmchan.nonceName="nonce_" + chan.getDestinationTask().getName().split("__")[1] + "_" + chan.getOriginTask().getName().split("__")[1];
+ }
}
+ }
+ else {
+ if (!secInChannels.get(chan.getOriginTask()).contains(writeChannel.getChannelName())) {
+ secOutChannels.get(chan.getOriginTask()).add(writeChannel.getChannelName());
+ channelSecMap.put(writeChannel.getChannelName(), "autoEncrypt_"+writeChannel.getChannelName());
+ if (chan.checkAuth && autoStrongAuth) {
+ nonceOutChannels.get(chan.getOriginTask()).add(writeChannel.getChannelName());
+ }
+ }
+ }
+
+ if (hsmTasks.contains(chan.getDestinationTask().getName().split("__")[1])){
+ if (!hsmSecOutChannels.get(chan.getDestinationTask()).contains(writeChannel.getChannelName())) {
+ HSMChannel hsmchan = new HSMChannel(writeChannel.getChannelName(), chan.getDestinationTask().getName().split("__")[1], HSMChannel.DEC);
+ hsmChannelMap.get(taskHSMMap.get(chan.getDestinationTask().getName().split("__")[1])).add(hsmchan);
+ hsmSecInChannels.get(chan.getDestinationTask()).add(writeChannel.getChannelName());
+ if (chan.checkAuth && autoStrongAuth) {
+ nonceInChannels.get(chan.getDestinationTask()).add(writeChannel.getChannelName());
+ hsmchan.nonceName="nonce_" + chan.getDestinationTask().getName().split("__")[1] + "_" + chan.getOriginTask().getName().split("__")[1];
+ }
+ }
+ }
+ else {
+ if (!secInChannels.get(chan.getDestinationTask()).contains(writeChannel.getChannelName())) {
+ secInChannels.get(chan.getDestinationTask()).add(writeChannel.getChannelName());
+ if (chan.checkAuth && autoStrongAuth) {
+ nonceInChannels.get(chan.getDestinationTask()).add(writeChannel.getChannelName());
+ }
+ }
+ }
+
+ } else if (chan.checkAuth && autoWeakAuth && nonAuthChans.contains(chan.getDestinationTask().getName().split("__")[1] + "__" + writeChannel.getChannelName())) {
+ toSecure.get(chan.getOriginTask()).add(chan.getDestinationTask());
+ if (autoStrongAuth) {
+ toSecureRev.get(chan.getDestinationTask()).add(chan.getOriginTask());
}
-
+ if (hsmTasks.contains(chan.getOriginTask().getName().split("__")[1])){
+ if (!hsmSecOutChannels.get(chan.getOriginTask()).contains(writeChannel.getChannelName())){
+ HSMChannel hsmchan = new HSMChannel(writeChannel.getChannelName(), chan.getOriginTask().getName().split("__")[1], HSMChannel.MAC);
+ hsmChannelMap.get(taskHSMMap.get(chan.getOriginTask().getName().split("__")[1])).add(hsmchan);
+ hsmSecOutChannels.get(chan.getOriginTask()).add(writeChannel.getChannelName());
+ channelSecMap.put(writeChannel.getChannelName(), "hsmSec_"+writeChannel.getChannelName());
+ if (autoStrongAuth) {
+ nonceOutChannels.get(chan.getOriginTask()).add(writeChannel.getChannelName());
+ hsmchan.nonceName="nonce_" + chan.getDestinationTask().getName().split("__")[1] + "_" + chan.getOriginTask().getName().split("__")[1];
+ }
+ }
+ }
+ else {
+ if (!macInChannels.get(chan.getOriginTask()).contains(writeChannel.getChannelName())) {
+ macOutChannels.get(chan.getOriginTask()).add(writeChannel.getChannelName());
+ channelSecMap.put(writeChannel.getChannelName(), "autoEncrypt_"+writeChannel.getChannelName());
+ if (autoStrongAuth) {
+ nonceOutChannels.get(chan.getOriginTask()).add(writeChannel.getChannelName());
+ }
+ }
+ }
+
+ if (hsmTasks.contains(chan.getDestinationTask().getName().split("__")[1])){
+ if (!hsmSecOutChannels.get(chan.getDestinationTask()).contains(writeChannel.getChannelName())) {
+ HSMChannel hsmchan = new HSMChannel(writeChannel.getChannelName(), chan.getDestinationTask().getName().split("__")[1], HSMChannel.DEC);
+ hsmChannelMap.get(taskHSMMap.get(chan.getDestinationTask().getName().split("__")[1])).add(hsmchan);
+ hsmSecInChannels.get(chan.getDestinationTask()).add(writeChannel.getChannelName());
+ if (chan.checkAuth && autoStrongAuth) {
+ nonceInChannels.get(chan.getDestinationTask()).add(writeChannel.getChannelName());
+ hsmchan.nonceName="nonce_" + chan.getDestinationTask().getName().split("__")[1] + "_" + chan.getOriginTask().getName().split("__")[1];
+ }
+ }
+ }
+ else {
+ if (!secInChannels.get(chan.getDestinationTask()).contains(writeChannel.getChannelName())) {
+ secInChannels.get(chan.getDestinationTask()).add(writeChannel.getChannelName());
+ if (chan.checkAuth && autoStrongAuth) {
+ nonceInChannels.get(chan.getDestinationTask()).add(writeChannel.getChannelName());
+ }
+ }
+ }
}
}
}
}
}
}
+
+ // System.out.println("hsmchannelmap" + hsmChannelMap);
+
+
TraceManager.addDev("macoutchans " + macOutChannels);
TraceManager.addDev("macinchans " + macInChannels);
TraceManager.addDev("nonsecin " + secInChannels);
TraceManager.addDev("nonsecout " + secOutChannels);
TraceManager.addDev("noncein " + nonceInChannels);
TraceManager.addDev("nonceout " + nonceOutChannels);
+
+
+ //Add a HSM Task for each selected CPU on the component diagram, add associated channels, etc
+ for (String cpuName : selectedCPUTasks.keySet()) {
+ TMLCPrimitiveComponent hsm = new TMLCPrimitiveComponent(0, 500, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxY(), false, null, tcdp);
+ TAttribute index = new TAttribute(2, "channelIndex", "0", 0);
+ hsm.getAttributeList().add(index);
+ tcdp.addComponent(hsm, 0, 500, false, true);
+ hsm.setValueWithChange("HSM_" + cpuName);
+ //Find all associated components
+ List<TMLCPrimitiveComponent> comps = new ArrayList<TMLCPrimitiveComponent>();
+ //Find the component to add a HSM to
+
+ for (TGComponent tg : tcdp.getComponentList()) {
+ if (tg instanceof TMLCPrimitiveComponent) {
+ for (String compName : selectedCPUTasks.get(cpuName)) {
+ if (tg.getValue().equals(compName)) {
+ comps.add((TMLCPrimitiveComponent) tg);
+ break;
+ }
+ }
+ } else if (tg instanceof TMLCCompositeComponent) {
+ TMLCCompositeComponent cc = (TMLCCompositeComponent) tg;
+ List<TMLCPrimitiveComponent> pcomps = cc.getAllPrimitiveComponents();
+ for (TMLCPrimitiveComponent pc : pcomps) {
+ for (String compName : selectedCPUTasks.get(cpuName)) {
+ if (pc.getValue().equals(compName)) {
+ comps.add(pc);
+ break;
+ }
+ }
+ }
+ }
+ }
+ if (comps.size() == 0) {
+ //System.out.println("No Components found");
+ continue;
+ }
+
+ for (TMLCPrimitiveComponent comp : comps) {
+
+ Map<String, HSMChannel> compChannels = new HashMap<String, HSMChannel>();
+ String compName = comp.getValue();
+
+ List<ChannelData> hsmChans = new ArrayList<ChannelData>();
+ ChannelData chd = new ChannelData("startHSM_" + cpuName, false, false);
+ hsmChans.add(chd);
+ for (HSMChannel hsmChan : hsmChannelMap.get(cpuName)) {
+ if (!hsmChan.task.equals(comp.getValue())){
+ continue;
+ }
+ if (!channelIndexMap.containsKey(hsmChan.name)){
+ channelIndexMap.put(hsmChan.name,channelIndex);
+ channelIndex++;
+ }
+ chd = new ChannelData("data_" + hsmChan.name + "_" + hsmChan.task, false, true);
+ hsmChans.add(chd);
+ chd = new ChannelData("retData_" + hsmChan.name + "_" + hsmChan.task, true, true);
+ hsmChans.add(chd);
+ }
+ for (ChannelData hsmChan : hsmChans) {
+ TMLCChannelOutPort originPort = new TMLCChannelOutPort(comp.getX(), comp.getY(), tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, hsm, tcdp);
+ TMLCChannelOutPort destPort = new TMLCChannelOutPort(comp.getX(), comp.getY(), tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, comp, tcdp);
+ originPort.commName = hsmChan.name;
+ originPort.isOrigin = hsmChan.isOrigin;
+ tcdp.addComponent(originPort, hsm.getX(), hsm.getY(), true, true);
+ destPort.commName = hsmChan.name;
+ if (!hsmChan.isChan) {
+ originPort.typep = 2;
+ destPort.typep = 2;
+ originPort.setParam(0, new TType(1));
+ destPort.setParam(0, new TType(1));
+ }
+ destPort.isOrigin = !hsmChan.isOrigin;
+
+ tcdp.addComponent(destPort, comp.getX(), comp.getY(), true, true);
+
+ TMLCPortConnector conn = new TMLCPortConnector(0, 0, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, null, tcdp, originPort.getTGConnectingPointAtIndex(0), destPort.getTGConnectingPointAtIndex(0), new Vector<Point>());
+ tcdp.addComponent(conn, 0, 0, false, true);
+ }
+ }
+ }
+
+
+ for (String cpuName : selectedCPUTasks.keySet()) {
+ buildHSMActivityDiagram(cpuName);
+ //Add a private bus to Hardware Accelerator with the task for hsm
+
+ //Find the CPU the task is mapped to
+ TMLArchiDiagramPanel archPanel = newarch.tmlap;
+ TMLArchiCPUNode cpu = null;
+ String refTask = "";
+ for (TGComponent tg : archPanel.getComponentList()) {
+ if (tg instanceof TMLArchiCPUNode) {
+ if (tg.getName().equals(cpuName)) {
+ cpu = (TMLArchiCPUNode) tg;
+ TMLArchiArtifact art = cpu.getArtifactList().get(0);
+ refTask = art.getReferenceTaskName();
+ break;
+
+ }
+ }
+ }
+
+ if (cpu == null) {
+ return;
+ }
+
+ //Add new memory
+ TMLArchiMemoryNode mem = new TMLArchiMemoryNode(cpu.getX(), archPanel.getMaxY()-400, archPanel.getMinX(), archPanel.getMaxX(), archPanel.getMinY(), archPanel.getMaxY(), true, null, archPanel);
+ archPanel.addComponent(mem, cpu.getX(), archPanel.getMaxY()-400, false, true);
+ mem.setName("HSMMemory_" + cpuName);
+ //Add Hardware Accelerator
+
+ TMLArchiHWANode hwa = new TMLArchiHWANode(cpu.getX() + 100, cpu.getY() + 100, archPanel.getMinX(), archPanel.getMaxX(), archPanel.getMinY(), archPanel.getMaxY(), true, null, archPanel);
+ archPanel.addComponent(hwa, cpu.getX() + 100, cpu.getY() + 100, false, true);
+ hwa.setName("HSM_" + cpuName);
+ //Add hsm task to hwa
+
+
+ TMLArchiArtifact hsmArt = new TMLArchiArtifact(cpu.getX() + 100, cpu.getY() + 100, archPanel.getMinX(), archPanel.getMaxX(), archPanel.getMinY(), archPanel.getMaxY(), true, hwa, archPanel);
+ archPanel.addComponent(hsmArt, cpu.getX() + 100, cpu.getY() + 100, true, true);
+ hsmArt.setFullName("HSM_" + cpuName, refTask);
+ //Add bus connecting the cpu and HWA
+
+ TMLArchiBUSNode bus = new TMLArchiBUSNode(cpu.getX() + 100, cpu.getY() + 100, archPanel.getMinX(), archPanel.getMaxX(), archPanel.getMinY(), archPanel.getMaxY(), true, null, archPanel);
+ bus.setPrivacy(1);
+ bus.setName("HSMBus_" + cpuName);
+ archPanel.addComponent(bus, cpu.getX() + 200, cpu.getY() + 200, false, true);
+
+ //Connect Bus and CPU
+ TMLArchiConnectorNode connect = new TMLArchiConnectorNode(cpu.getX() + 100, cpu.getY() + 100, archPanel.getMinX(), archPanel.getMaxX(), archPanel.getMinY(), archPanel.getMaxY(), true, null, archPanel, null, null, new Vector<Point>());
+ TGConnectingPoint p1 = bus.findFirstFreeTGConnectingPoint(true, true);
+ p1.setFree(false);
+ connect.setP2(p1);
+
+
+ TGConnectingPoint p2 = cpu.findFirstFreeTGConnectingPoint(true, true);
+ p1.setFree(false);
+ connect.setP1(p2);
+ archPanel.addComponent(connect, cpu.getX() + 100, cpu.getY() + 100, false, true);
+ //Connect Bus and HWA
+
+ connect = new TMLArchiConnectorNode(cpu.getX() + 100, cpu.getY() + 100, archPanel.getMinX(), archPanel.getMaxX(), archPanel.getMinY(), archPanel.getMaxY(), true, null, archPanel, null, null, new Vector<Point>());
+ p1 = bus.findFirstFreeTGConnectingPoint(true, true);
+ p1.setFree(false);
+ connect.setP2(p1);
+
+ p2 = hwa.findFirstFreeTGConnectingPoint(true, true);
+ p1.setFree(false);
+ connect.setP1(p2);
+
+ archPanel.addComponent(connect, cpu.getX() + 100, cpu.getY() + 100, false, true);
+ //Connect Bus and Memory
+
+ connect = new TMLArchiConnectorNode(cpu.getX() + 100, cpu.getY() + 100, archPanel.getMinX(), archPanel.getMaxX(), archPanel.getMinY(), archPanel.getMaxY(), true, null, archPanel, null, null, new Vector<Point>());
+ p1 = bus.findFirstFreeTGConnectingPoint(true, true);
+ p1.setFree(false);
+ connect.setP2(p1);
+
+ p2 = mem.findFirstFreeTGConnectingPoint(true, true);
+ p1.setFree(false);
+ connect.setP1(p2);
+ archPanel.addComponent(connect, cpu.getX() + 100, cpu.getY() + 100, false, true);
+ }
//
// int num=0;
//int nonceNum=0;
//Create reverse channels on component diagram to send nonces if they don't already exist
+
for (TMLTask task : toSecureRev.keySet()) {
TraceManager.addDev("Adding nonces to " + task.getName());
List<TMLChannel> chans = tmlmodel.getChannelsFromMe(task);
@@ -321,12 +598,16 @@ public class SecurityGeneration implements Runnable {
}
}
}
+
+
+
+
// }
//Add encryption/nonces to activity diagram
for (TMLTask task : toSecure.keySet()) {
- String title = task.getName().split("__")[0];
+ String title = task.getName().split("__")[0];
TraceManager.addDev("Securing task " + task.getName());
- TMLActivityDiagramPanel tad = t.getTMLActivityDiagramPanel(task.getName());
+ TMLActivityDiagramPanel tad = tmlcdp.getTMLActivityDiagramPanel(task.getName());
//Get start state position, shift everything down
int xpos = 0;
int ypos = 0;
@@ -336,6 +617,7 @@ public class SecurityGeneration implements Runnable {
//For each occurence of a write channel operator, add encryption/nonces before it
+
for (String channel : secOutChannels.get(task)) {
Set<TGComponent> channelInstances = new HashSet<TGComponent>();
int yShift = 50;
@@ -385,7 +667,7 @@ public class SecurityGeneration implements Runnable {
}
}
- enc.securityContext = "autoEncrypt_" + channel;
+ enc.securityContext = channelSecMap.get(channel);
enc.type = "Symmetric Encryption";
enc.message_overhead = overhead;
enc.encTime = encComp;
@@ -407,7 +689,7 @@ public class SecurityGeneration implements Runnable {
TraceManager.addDev("Inspecting write channel " + wChannel.getChannelName());
if (channel.equals(wChannel.getChannelName()) && wChannel.getSecurityContext().equals("")) {
TraceManager.addDev("Securing write channel " + wChannel.getChannelName());
- wChannel.setSecurityContext("autoEncrypt_" + wChannel.getChannelName());
+ wChannel.setSecurityContext(channelSecMap.get(channel));
}
}
@@ -450,7 +732,7 @@ public class SecurityGeneration implements Runnable {
//If we need to receive a nonce
TMLADReadChannel rd = new TMLADReadChannel(0, 0, 0, 0, 0, 0, false, null, tad);
- if (macNonceOutChannels.get(task).contains(channel)) {
+ if (nonceOutChannels.get(task).contains(channel)) {
//Receive any nonces if ensuring authenticity
rd = new TMLADReadChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
List<TMLChannel> matches = tmlmodel.getChannels(tmlc.getDestinationTask(), tmlc.getOriginTask());
@@ -476,7 +758,7 @@ public class SecurityGeneration implements Runnable {
//Add encryption operator
- enc.securityContext = "autoEncrypt_" + channel;
+ enc.securityContext = channelSecMap.get(channel);
enc.type = "MAC";
enc.message_overhead = overhead;
enc.encTime = encComp;
@@ -499,7 +781,7 @@ public class SecurityGeneration implements Runnable {
TraceManager.addDev("Inspecting write channel " + wChannel.getChannelName());
if (channel.equals(wChannel.getChannelName()) && wChannel.getSecurityContext().equals("")) {
TraceManager.addDev("Securing write channel " + wChannel.getChannelName());
- wChannel.setSecurityContext("autoEncrypt_" + wChannel.getChannelName());
+ wChannel.setSecurityContext(channelSecMap.get(channel));
tad.repaint();
}
}
@@ -510,6 +792,324 @@ public class SecurityGeneration implements Runnable {
tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
}
}
+ for (String channel: hsmSecOutChannels.get(task)){
+ Set<TGComponent> channelInstances = new HashSet<TGComponent>();
+ TGConnector conn = new TGConnectorTMLAD(0, 0, 0, 0, 0, 0, false, null, tad, null, null, new Vector<Point>());
+ TGConnectingPoint next = new TGConnectingPoint(null, 0, 0, false, false);
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg instanceof TMLADWriteChannel) {
+ TMLADWriteChannel writeChannel = (TMLADWriteChannel) tg;
+ if (writeChannel.getChannelName().equals(channel) && writeChannel.getSecurityContext().equals("")) {
+ fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
+ if (fromStart != null) {
+ channelInstances.add(tg);
+ }
+ }
+ }
+ }
+ for (TGComponent chan : channelInstances) {
+
+ TMLADWriteChannel writeChannel = (TMLADWriteChannel) chan;
+ String chanName = writeChannel.getChannelName();
+ TMLChannel tmlc = tmlmodel.getChannelByName(title + "__" + chanName);
+ writeChannel.setSecurityContext(channelSecMap.get(chanName));
+ xpos = chan.getX();
+ ypos = chan.getY();
+ fromStart = tad.findTGConnectorEndingAt(chan.getTGConnectingPointAtIndex(0));
+ point = fromStart.getTGConnectingPointP2();
+
+ int yShift = 50;
+
+
+
+
+ TMLADSendRequest req = new TMLADSendRequest(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ req.setRequestName("startHSM_" + taskHSMMap.get(task.getName().split("__")[1]));
+
+
+ req.setParam(0, Integer.toString(channelIndexMap.get(chanName)));
+ req.makeValue();
+ tad.addComponent(req, xpos, ypos + yShift, false, true);
+
+ fromStart.setP2(req.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+
+ //Add connection
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(req.getTGConnectingPointAtIndex(1));
+
+
+
+
+
+ TMLADWriteChannel wr = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+
+
+
+ yShift += 50;
+ //Add write channel operator
+ wr = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ wr.setChannelName("data_" + chanName + "_" + task.getName().split("__")[1]);
+ wr.setSecurityContext(channelSecMap.get(chanName));
+ tad.addComponent(wr, xpos, ypos + yShift, false, true);
+
+
+ fromStart.setP2(wr.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+ fromStart.setP1(wr.getTGConnectingPointAtIndex(1));
+
+
+ TMLADReadChannel rd = new TMLADReadChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+
+ TMLADWriteChannel wr2 = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+
+ //Receive any nonces if ensuring authenticity
+ if (nonceOutChannels.get(task).contains(channel)) {
+ //Read nonce from rec task
+ yShift+=50;
+
+ List<TMLChannel> matches = tmlmodel.getChannels(tmlc.getDestinationTask(), tmlc.getOriginTask());
+ rd = new TMLADReadChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ if (matches.size() > 0) {
+ rd.setChannelName(matches.get(0).getName().replaceAll(title + "__", ""));
+ } else {
+ rd.setChannelName("nonceCh" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
+ }
+ rd.setSecurityContext("nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
+ tad.addComponent(rd, xpos, ypos + yShift, false, true);
+ fromStart.setP2(rd.getTGConnectingPointAtIndex(0));
+
+ fromStart = new TGConnectorTMLAD(rd.getX(), rd.getY(), tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+ fromStart.setP1(rd.getTGConnectingPointAtIndex(1));
+
+
+ //Also send nonce to hsm
+ yShift+=50;
+ wr2 = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ wr2.setChannelName("data_" + chanName + "_" + task.getName().split("__")[1]);
+ wr2.setSecurityContext(channelSecMap.get(chanName));
+ tad.addComponent(wr2, xpos, ypos + yShift, false, true);
+
+ TGConnectorTMLAD tmp = new TGConnectorTMLAD(wr2.getX(), wr2.getY() + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, rd.getTGConnectingPointAtIndex(1), wr2.getTGConnectingPointAtIndex(0), new Vector<Point>());
+ tad.addComponent(tmp, xpos, ypos, false, true);
+
+ fromStart.setP2(wr2.getTGConnectingPointAtIndex(0));
+
+ fromStart = new TGConnectorTMLAD(rd.getX(), rd.getY(), tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+ fromStart.setP1(wr2.getTGConnectingPointAtIndex(1));
+
+
+
+ yShift += 60;
+ }
+
+
+ //Read channel operator to receive hsm data
+
+ yShift += 60;
+ TMLADReadChannel rd2 = new TMLADReadChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ rd2.setChannelName("retData_" + chanName + "_" + task.getName().split("__")[1]);
+ rd2.setSecurityContext(channelSecMap.get(chanName));
+ tad.addComponent(rd2, xpos, ypos + yShift, false, true);
+
+ fromStart.setP2(rd2.getTGConnectingPointAtIndex(0));
+ yShift += 50;
+
+ //Add connector
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+ fromStart.setP1(rd2.getTGConnectingPointAtIndex(1));
+ yShift += 50;
+
+ //Direct the last TGConnector back to the start of the write channel operator
+
+
+ fromStart.setP2(point);
+ //Shift components down to make room for the added ones, and add security contexts to write channels
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg.getY() >= ypos && tg != wr && tg != req && tg != rd && tg!=wr2 && tg!=rd2) {
+ tg.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }
+ tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
+ tad.repaint();
+ }
+ }
+
+ for (String channel: hsmSecInChannels.get(task)){
+ Set<TGComponent> channelInstances = new HashSet<TGComponent>();
+ TGConnector conn = new TGConnectorTMLAD(0, 0, 0, 0, 0, 0, false, null, tad, null, null, new Vector<Point>());
+ TGConnectingPoint next = new TGConnectingPoint(null, 0, 0, false, false);
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg instanceof TMLADReadChannel) {
+ TMLADReadChannel readChannel = (TMLADReadChannel) tg;
+ if (readChannel.getChannelName().equals(channel) && readChannel.getSecurityContext().equals("")) {
+ fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
+ if (fromStart != null) {
+ channelInstances.add(tg);
+ }
+ }
+ }
+ }
+ for (TGComponent chan : channelInstances) {
+ TMLADReadChannel readChannel = (TMLADReadChannel) chan;
+ String chanName = readChannel.getChannelName();
+ TMLChannel tmlc = tmlmodel.getChannelByName(title + "__" + chanName);
+ readChannel.setSecurityContext(channelSecMap.get(chanName));
+ xpos = chan.getX();
+ ypos = chan.getY();
+ fromStart = tad.findTGConnectorEndingAt(chan.getTGConnectingPointAtIndex(0));
+ point = fromStart.getTGConnectingPointP2();
+
+ int yShift = 50;
+
+
+
+
+
+ TMLADSendRequest req = new TMLADSendRequest(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ req.setRequestName("startHSM_" + taskHSMMap.get(task.getName().split("__")[1]));
+
+
+
+
+ req.setParam(0, Integer.toString(channelIndexMap.get(chanName)));
+ req.makeValue();
+ tad.addComponent(req, xpos, ypos + yShift, false, true);
+
+ fromStart.setP2(req.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+
+ //Add connection
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(req.getTGConnectingPointAtIndex(1));
+ TMLADWriteChannel wr = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+
+ yShift += 50;
+ //Add write channel operator
+ wr = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ wr.setChannelName("data_" + chanName + "_" + task.getName().split("__")[1]);
+ wr.setSecurityContext(channelSecMap.get(chanName));
+ tad.addComponent(wr, xpos, ypos + yShift, false, true);
+
+
+ fromStart.setP2(wr.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+ fromStart.setP1(wr.getTGConnectingPointAtIndex(1));
+
+
+
+
+
+
+ //If needed, forge nonce, send it to receiving task
+ TMLADEncrypt nonce = new TMLADEncrypt(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ TMLADWriteChannel wr3 = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ TMLADWriteChannel wr2 = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+
+ if (nonceInChannels.get(task).contains(channel)) {
+ //Create a nonce operator and a write channel operator
+ yShift+=60;
+ nonce = new TMLADEncrypt(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ nonce.securityContext = "nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1];
+ nonce.type = "Nonce";
+ nonce.message_overhead = overhead;
+ nonce.encTime = encComp;
+ nonce.decTime = decComp;
+ tad.addComponent(nonce, xpos, ypos + yShift, false, true);
+ fromStart.setP2(nonce.getTGConnectingPointAtIndex(0));
+ yShift += 50;
+
+ wr3 = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ //Send nonce along channel, the newly created nonce channel or an existing channel with the matching sender and receiver
+ //Find matching channels
+ List<TMLChannel> matches = tmlmodel.getChannels(tmlc.getDestinationTask(), tmlc.getOriginTask());
+
+ if (matches.size() > 0) {
+ wr3.setChannelName(matches.get(0).getName().replaceAll(title + "__", ""));
+ } else {
+ wr3.setChannelName("nonceCh" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
+ }
+ //send the nonce along the channel
+ wr3.setSecurityContext("nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
+ tad.addComponent(wr3, xpos, ypos + yShift, false, true);
+
+ wr3.makeValue();
+ TGConnector tmp = new TGConnectorTMLAD(wr3.getX(), wr3.getY() + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, nonce.getTGConnectingPointAtIndex(1), wr3.getTGConnectingPointAtIndex(0), new Vector<Point>());
+ tad.addComponent(tmp, xpos, ypos, false, true);
+
+
+ //Also send nonce to hsm
+ yShift+=50;
+ wr2 = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ wr2.setChannelName("data_" + chanName + "_" + task.getName().split("__")[1]);
+ wr2.setSecurityContext("nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
+ tad.addComponent(wr2, xpos, ypos + yShift, false, true);
+
+ tmp = new TGConnectorTMLAD(wr2.getX(), wr2.getY() + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, wr3.getTGConnectingPointAtIndex(1), wr2.getTGConnectingPointAtIndex(0), new Vector<Point>());
+ tad.addComponent(tmp, xpos, ypos, false, true);
+
+ fromStart = new TGConnectorTMLAD(wr2.getX(), wr.getY(), tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, wr2.getTGConnectingPointAtIndex(1), null, new Vector<Point>());
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+ //Connect created write channel operator to start of read channel operator
+ fromStart.setP1(wr2.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(point);
+
+
+
+
+
+
+ /* //Shift everything from the read channel on down
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg.getY() >= ypos && tg != nonce && tg != wr2 && tg!=wr3) {
+ tg.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }*/
+ }
+
+
+
+
+ //Add read channel operator
+
+ yShift += 60;
+ TMLADReadChannel rd = new TMLADReadChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ rd.setChannelName("retData_" + chanName + "_" + task.getName().split("__")[1]);
+ rd.setSecurityContext(channelSecMap.get(chanName));
+ tad.addComponent(rd, xpos, ypos + yShift, false, true);
+
+ fromStart.setP2(rd.getTGConnectingPointAtIndex(0));
+ yShift += 50;
+
+ //Add connector
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+ fromStart.setP1(rd.getTGConnectingPointAtIndex(1));
+ yShift += 50;
+
+ //Direct the last TGConnector back to the start of the read channel operator
+
+
+ fromStart.setP2(point);
+ //Shift components down to make room for the added ones, and add security contexts to write channels
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg.getY() >= ypos && tg != wr && tg != req && tg != rd && tg!=wr2 && tg!=nonce && tg!=wr3) {
+ tg.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }
+ tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
+ tad.repaint();
+ }
+ }
for (String channel : macInChannels.get(task)) {
//Add decryptmac after readchannel
int yShift = 50;
@@ -543,13 +1143,13 @@ public class SecurityGeneration implements Runnable {
TMLADReadChannel readChannel = (TMLADReadChannel) comp;
TraceManager.addDev("Securing read channel " + readChannel.getChannelName());
- readChannel.setSecurityContext("autoEncrypt_" + readChannel.getChannelName());
+ readChannel.setSecurityContext(channelSecMap.get(readChannel.getChannelName()));
tad.repaint();
TMLADWriteChannel wr = new TMLADWriteChannel(0, 0, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
//Create nonce and send it
TMLChannel tmlc = tmlmodel.getChannelByName(title + "__" + channel);
- if (macNonceInChannels.get(task).contains(channel)) {
+ if (nonceInChannels.get(task).contains(channel)) {
//Create a nonce operator and a write channel operator
TMLADEncrypt nonce = new TMLADEncrypt(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
nonce.securityContext = "nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1];
@@ -594,7 +1194,7 @@ public class SecurityGeneration implements Runnable {
ypos = conn.getY();
TMLADDecrypt dec = new TMLADDecrypt(xpos + 10, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- dec.securityContext = "autoEncrypt_" + readChannel.getChannelName();
+ dec.securityContext = channelSecMap.get(readChannel.getChannelName());
tad.addComponent(dec, dec.getX(), dec.getY(), false, true);
conn.setP2(dec.getTGConnectingPointAtIndex(0));
yShift += 60;
@@ -609,7 +1209,7 @@ public class SecurityGeneration implements Runnable {
TraceManager.addDev("Inspecting read channel " + readChannel.getChannelName());
if (channel.equals(readChannel.getChannelName()) && readChannel.getSecurityContext().equals("")) {
TraceManager.addDev("Securing read channel " + readChannel.getChannelName());
- readChannel.setSecurityContext("autoEncrypt_" + readChannel.getChannelName());
+ readChannel.setSecurityContext(channelSecMap.get(readChannel.getChannelName()));
}
}
@@ -699,16 +1299,16 @@ public class SecurityGeneration implements Runnable {
//Now add the decrypt operator
yShift = 40;
TraceManager.addDev("Securing read channel " + readChannel.getChannelName());
- readChannel.setSecurityContext("autoEncrypt_" + readChannel.getChannelName());
+ readChannel.setSecurityContext(channelSecMap.get(readChannel.getChannelName()));
tad.repaint();
//Add decryption operator if it does not already exist
xpos = readChannel.getX();
ypos = readChannel.getY();
TMLADDecrypt dec = new TMLADDecrypt(xpos + 10, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- dec.securityContext = "autoEncrypt_" + readChannel.getChannelName();
+ dec.securityContext = channelSecMap.get(readChannel.getChannelName());
tad.addComponent(dec, dec.getX(), dec.getY(), false, true);
conn.setP2(dec.getTGConnectingPointAtIndex(0));
- yShift += 100;
+ yShift += 60;
conn = new TGConnectorTMLAD(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, dec.getTGConnectingPointAtIndex(1), next, new Vector<Point>());
conn.setP1(dec.getTGConnectingPointAtIndex(1));
@@ -721,7 +1321,7 @@ public class SecurityGeneration implements Runnable {
TraceManager.addDev("Inspecting read channel " + readChannel.getChannelName());
if (channel.equals(readChannel.getChannelName()) && readChannel.getSecurityContext().equals("")) {
TraceManager.addDev("Securing read channel " + readChannel.getChannelName());
- readChannel.setSecurityContext("autoEncrypt_" + readChannel.getChannelName());
+ readChannel.setSecurityContext( channelSecMap.get(readChannel.getChannelName()));
}
}
@@ -737,9 +1337,12 @@ public class SecurityGeneration implements Runnable {
}
}
}
- GTMLModeling gtm = new GTMLModeling(t, false);
- TMLModeling<TGComponent> newmodel = gtm.translateToTMLModeling(false, false);
- for (TMLTask task : newmodel.getTasks()) {
+
+
+
+ GTMLModeling gtm = new GTMLModeling(newarch, false);
+ map = gtm.translateToTMLMapping();
+ /*for (TMLTask task : newmodel.getTasks()) {
task.setName(tabName + "_" + name + "__" + task.getName());
}
for (TMLTask task : tmlmodel.getTasks()) {
@@ -750,11 +1353,318 @@ public class SecurityGeneration implements Runnable {
} else {
}
- }
+ }*/
//map.setTMLModeling(newmodel);
- //
- //TMLMapping newMap = gtm.translateToTMLMapping();
- map.setTMLModeling(newmodel);
+
+// map.setTMLModeling(newmodel);
+
return;
}
+ public void buildHSMActivityDiagram(String cpuName){
+ int xpos = 0;
+ int ypos = 0;
+ TGConnector fromStart;
+ //Build HSM Activity diagram
+
+ TMLActivityDiagramPanel tad = tmlcdp.getTMLActivityDiagramPanel("HSM_" + cpuName);
+ if (tad ==null){
+ System.out.println("Missing task ");
+ return;
+ }
+
+ TMLADStartState start = (TMLADStartState) tad.getComponentList().get(0);
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+
+
+ TMLADReadRequestArg req = new TMLADReadRequestArg(300, 100, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ tad.addComponent(req, 300, 100, false, true);
+ req.setParam(0, "channelIndex");
+ req.makeValue();
+
+ //Connect start and readrequest
+ fromStart.setP1(start.getTGConnectingPointAtIndex(0));
+ fromStart.setP2(req.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+
+ TMLADChoice choice = new TMLADChoice(300, 200, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ tad.addComponent(choice, 300, 200, false, true);
+
+
+ //Connect readrequest and choice
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(req.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(choice.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+
+ int xc = 150;
+ //Allows 9 channels max to simplify the diagram
+
+ //If more than 3 channels, build 2 levels of choices
+
+ if (hsmChannelMap.get(cpuName).size() > 3) {
+ TMLADChoice choice2 = new TMLADChoice(xc, 400, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ int i = 0;
+ for (HSMChannel ch : hsmChannelMap.get(cpuName)) {
+ if (i % 3 == 0) {
+ //Add a new choice every third channel
+ choice2 = new TMLADChoice(xc, 250, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ tad.addComponent(choice2, xc, 400, false, true);
+ //Connect new choice operator to top choice
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(choice.getTGConnectingPointAtIndex(i / 3 + 1));
+ fromStart.setP2(choice2.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+ }
+ TMLADReadChannel rd = new TMLADReadChannel(xc, 300, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ rd.setChannelName("data_" + ch.name + "_" + ch.task);
+ rd.setSecurityContext(channelSecMap.get(ch.name));
+ tad.addComponent(rd, xc, 300, false, true);
+ //Connect choice and readchannel
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(choice2.getTGConnectingPointAtIndex(i % 3 + 1));
+ fromStart.setP2(rd.getTGConnectingPointAtIndex(0));
+
+ tad.addComponent(fromStart, 300, 200, false, true);
+ TMLADWriteChannel wr = new TMLADWriteChannel(xc, 600, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ wr.setChannelName("retData_" + ch.name + "_" + ch.task);
+ tad.addComponent(wr, xc, 600, false, true);
+ wr.setSecurityContext(channelSecMap.get(ch.name));
+
+
+ if (ch.secType == HSMChannel.DEC) {
+ TMLADDecrypt dec = new TMLADDecrypt(xc, 500, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ dec.securityContext = channelSecMap.get(ch.name);
+ tad.addComponent(dec, xc, 500, false, true);
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(rd.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(dec.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(rd.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(dec.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+ //Connect encrypt and writechannel
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(dec.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(wr.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+ } else {
+ TMLADEncrypt enc = new TMLADEncrypt(xc, 500, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ enc.securityContext = channelSecMap.get(ch.name);
+ if (ch.secType == HSMChannel.SENC) {
+ enc.type = "Symmetric Encryption";
+ } else if (ch.secType == HSMChannel.AENC) {
+ enc.type = "Asymmetric Encryption";
+ } else if (ch.secType == HSMChannel.MAC) {
+ enc.type = "MAC";
+ } else if (ch.secType == HSMChannel.NONCE) {
+ enc.type = "Nonce";
+ }
+
+ enc.message_overhead = overhead;
+ enc.encTime = encComp;
+ enc.decTime = decComp;
+ enc.nonce = ch.nonceName;
+ tad.addComponent(enc, xc, 500, false, true);
+
+ //Connect encrypt and readchannel
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(rd.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(enc.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+ //Connect encrypt and writechannel
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(enc.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(wr.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+ //Add Stop
+ TMLADStopState stop = new TMLADStopState(xc, 600, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ tad.addComponent(stop, xc, 700, false, true);
+
+
+ //Connext stop and write channel
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(wr.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(stop.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+ }
+ xc += 300;
+ i++;
+ }
+ } else {
+
+ int i = 1;
+
+ for (HSMChannel ch : hsmChannelMap.get(cpuName)) {
+
+ //Add guard as channelindex
+ choice.setGuard("[channelIndex=="+channelIndexMap.get(ch.name)+"]",i-1);
+
+ TMLADReadChannel rd = new TMLADReadChannel(xc, 300, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ rd.setChannelName("data_" + ch.name + "_" + ch.task);
+ rd.setSecurityContext(channelSecMap.get(ch.name));
+ tad.addComponent(rd, xc, 300, false, true);
+ //Connect choice and readchannel
+
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(choice.getTGConnectingPointAtIndex(i));
+ fromStart.setP2(rd.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, xc, 300, false, true);
+
+
+ fromStart = new TGConnectorTMLAD(xc, 350, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(rd.getTGConnectingPointAtIndex(1));
+
+
+ //If needed, receive nonce from task
+ if (!ch.nonceName.equals("")){
+
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+ rd = new TMLADReadChannel(xc, 350, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ rd.setChannelName("data_" + ch.name + "_" + ch.task);
+ rd.setSecurityContext(ch.nonceName);
+ tad.addComponent(rd, xc, 350, false, true);
+
+
+ fromStart.setP2(rd.getTGConnectingPointAtIndex(0));
+
+ fromStart = new TGConnectorTMLAD(xc, 350, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(rd.getTGConnectingPointAtIndex(1));
+
+ }
+
+
+ //Send data back to task
+ TMLADWriteChannel wr = new TMLADWriteChannel(xc, 600, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ wr.setChannelName("retData_" + ch.name + "_" + ch.task);
+
+
+
+ tad.addComponent(wr, xc, 600, false, true);
+ wr.setSecurityContext(channelSecMap.get(ch.name));
+
+
+ if (ch.secType == HSMChannel.DEC) {
+ //Add Decrypt operator
+ TMLADDecrypt dec = new TMLADDecrypt(xc, 500, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ dec.securityContext = channelSecMap.get(ch.name);
+ tad.addComponent(dec, xc, 500, false, true);
+
+ //Connect decrypt and readchannel
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(rd.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(dec.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+ //Connect encrypt and writechannel
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(dec.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(wr.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+ //Add Stop
+ TMLADStopState stop = new TMLADStopState(xc, 700, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ tad.addComponent(stop, xc, 700, false, true);
+
+
+ //Connect stop and write channel
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(wr.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(stop.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+ } else {
+ TMLADEncrypt enc = new TMLADEncrypt(xc, 500, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ enc.securityContext = channelSecMap.get(ch.name);
+ if (ch.secType == HSMChannel.SENC) {
+ enc.type = "Symmetric Encryption";
+ } else if (ch.secType == HSMChannel.AENC) {
+ enc.type = "Asymmetric Encryption";
+ } else if (ch.secType == HSMChannel.MAC) {
+ enc.type = "MAC";
+ } else if (ch.secType == HSMChannel.NONCE) {
+ enc.type = "Nonce";
+ }
+
+ enc.message_overhead = overhead;
+ enc.encTime = encComp;
+ enc.decTime = decComp;
+ tad.addComponent(enc, xc, 500, false, true);
+
+ //Connect encrypt and readchannel
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(rd.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(enc.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+ //Connect encrypt and writechannel
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(enc.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(wr.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+ //Add Stop
+ TMLADStopState stop = new TMLADStopState(xc, 700, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ tad.addComponent(stop, xc, 700, false, true);
+
+
+ //Connect stop and write channel
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(wr.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(stop.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, 300, 200, false, true);
+
+
+ }
+
+
+ xc += 300;
+ i++;
+ }
+
+ }
+
+ }
+
+ class HSMChannel {
+ public String name;
+ public static final int SENC = 0;
+ public static final int NONCE_ENC = 1;
+ public static final int MAC = 2;
+ public static final int DEC = 3;
+ public static final int AENC = 4;
+ public static final int NONCE = 5;
+ public String task;
+ public String securityContext = "";
+ public int secType;
+ public String nonceName = "";
+
+ public HSMChannel(String n, String t, int type) {
+ name = n;
+ task = t;
+ secType = type;
+ }
+ }
+
+ class ChannelData {
+ public String name;
+ public boolean isOrigin;
+ public boolean isChan;
+
+ public ChannelData(String n, boolean orig, boolean isCh) {
+ name = n;
+ isOrigin = orig;
+ isChan = isCh;
+ }
+
+ }
+
}
diff --git a/src/main/java/ui/tmlad/TMLADWriteChannel.java b/src/main/java/ui/tmlad/TMLADWriteChannel.java
index 9fd95d7744d6e20a315e84c42556903c699f0fae..07ca8cde9fa33edd50e9d451e73f780af1526fb9 100755
--- a/src/main/java/ui/tmlad/TMLADWriteChannel.java
+++ b/src/main/java/ui/tmlad/TMLADWriteChannel.java
@@ -283,15 +283,24 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
values[0] = channelName;
labels[1] = "Nb of samples";
values[1] = nbOfSamples;
+
+ /* labels[2] = "Security Pattern";
+ values[2] = securityContext;
+ labels[3] = "Attacker?";
+ values[3] = isAttacker ? "Yes" : "No"; */
+ ArrayList<String []> help = new ArrayList<String []>();
+ String[] allOutChannels = tdp.getMGUI().getAllOutChannels();
+ if (isAttacker){
+ allOutChannels =tdp.getMGUI().getAllCompOutChannels();
+ }
+ String[] choice = new String[]{"Yes", "No"};
+ help.add(allOutChannels);
+ help.add(null);
+ // help.add(tdp.getMGUI().getCurrentCryptoConfig());
+ //help.add(choice);
+
tab1.labels=labels;
tab1.values = values;
- ArrayList<String[]> help = new ArrayList<String[]>();
- String[] allOutChannels = tdp.getMGUI().getAllOutChannels();
- if (isAttacker) {
- allOutChannels = tdp.getMGUI().getAllCompOutChannels();
- }
- help.add(allOutChannels);
- help.add(null);
tab1.help = help;
TabInfo tab2 = new TabInfo("Security");
@@ -302,7 +311,7 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
labels[1] = "Attacker?";
values[1] = isAttacker ? "Yes" : "No";
help = new ArrayList<String[]>();
- String[] choice = new String[]{"Yes", "No"};
+
help.add(tdp.getMGUI().getCurrentCryptoConfig());
help.add(choice);
tab2.labels=labels;
@@ -313,6 +322,7 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
tabs.add(tab1);
tabs.add(tab2);
+
//JDialogTwoString jdts = new JDialogTwoString(frame, "Setting channel's properties", "Channel name", channelName, "Nb of samples", nbOfSamples);
JDialogMultiStringAndTabs jdmsat = new JDialogMultiStringAndTabs(frame, "Write in channel", tabs);
//jdms.setSize(600, 300);
@@ -325,6 +335,9 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
securityContext = jdmsat.getString(1, 0);
isAttacker = jdmsat.getString(1, 1).equals("Yes");
makeValue();
+
+ System.out.println(channelName + " " + securityContext + " " + isAttacker);
+
return true;
}
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 077b43ce7e25dede1bcaaea42c2d91c6daaa7e7c..2ea0ef7164a7881bc9cc2b5c1e7fc4a7725dc985 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -178,10 +178,11 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
//security generation buttons
ButtonGroup secGroup;
- protected JCheckBox autoConf, autoWeakAuth, autoStrongAuth, custom;
- protected JRadioButton autoSec, autoMapKeys, addHSM;
+ protected JCheckBox autoConf, autoWeakAuth, autoStrongAuth, custom, addHSM;
+ protected JRadioButton autoSec, autoMapKeys;
protected JTextField encTime, decTime, secOverhead;
protected JComboBox<String> addtoCPU;
+ protected JButton allValidated, addOneValidated, allIgnored, addOneIgnored;
protected JCheckBox removeForkAndJoin;
@@ -347,19 +348,17 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
jp02.add(autoStrongAuth, c01);
autoStrongAuth.addActionListener(this);
- autoMapKeys= new JRadioButton("Add Keys");
- autoMapKeys.addActionListener(this);
- jp02.add(autoMapKeys, c01);
- secGroup.add(autoMapKeys);
- addHSM = new JRadioButton("Add HSM");
- jp02.add(addHSM,c01);
- addHSM.addActionListener(this);
- secGroup.add(addHSM);
- jp02.add(new JLabel("Add HSM to component:"),c01);
+
+ addHSM = new JCheckBox("Add HSM to component:");
+ addHSM.setEnabled(false);
+ jp02.add(addHSM, c01);
+
+
listIgnored = new JList<String>(ignoredTasks);
listPanel = new JPanel();
+ listPanel.setPreferredSize(new Dimension(250, 200));
GridBagConstraints c02 = new GridBagConstraints();
c02.gridwidth=1;
c02.gridheight=1;
@@ -375,27 +374,36 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
GridBagConstraints c13 = new GridBagConstraints();
c13.gridwidth = GridBagConstraints.REMAINDER;
c13.gridheight = 1;
- JButton allValidated = new JButton(IconManager.imgic50);
+
+ allValidated = new JButton(IconManager.imgic50);
allValidated.setPreferredSize(new Dimension(50, 25));
allValidated.addActionListener(this);
allValidated.setActionCommand("allValidated");
buttonPanel.add(allValidated, c13);
- JButton addOneValidated = new JButton(IconManager.imgic48);
+ allValidated.setEnabled(false);
+
+
+ addOneValidated = new JButton(IconManager.imgic48);
addOneValidated.setPreferredSize(new Dimension(50, 25));
addOneValidated.addActionListener(this);
addOneValidated.setActionCommand("addOneValidated");
buttonPanel.add(addOneValidated, c13);
+
+ addOneValidated.setEnabled(false);
+
buttonPanel.add(new JLabel(" "), c13);
- JButton addOneIgnored = new JButton(IconManager.imgic46);
+ addOneIgnored = new JButton(IconManager.imgic46);
addOneIgnored.addActionListener(this);
addOneIgnored.setPreferredSize(new Dimension(50, 25));
addOneIgnored.setActionCommand("addOneIgnored");
buttonPanel.add(addOneIgnored, c13);
- JButton allIgnored = new JButton(IconManager.imgic44);
+ addOneIgnored.setEnabled(false);
+
+ allIgnored = new JButton(IconManager.imgic44);
allIgnored.addActionListener(this);
allIgnored.setPreferredSize(new Dimension(50, 25));
allIgnored.setActionCommand("allIgnored");
@@ -403,6 +411,8 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
listPanel.add(buttonPanel, c02);
buttonPanel.setPreferredSize(new Dimension(50, 200));
+ allIgnored.setEnabled(false);
+
listSelected = new JList<String>(selectedTasks);
//listValidated.setPreferredSize(new Dimension(200, 250));
@@ -417,6 +427,31 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
jp02.add(listPanel, c01);
c02.gridheight = 1;
+ custom = new JCheckBox("Custom performance attributes");
+ jp02.add(custom, c01);
+ custom.addActionListener(this);
+
+ jp02.add(new JLabel("Encryption Computational Complexity"), c01);
+ encTime = new JTextField(encCC);
+ encTime.setEnabled(false);
+ jp02.add(encTime, c01);
+
+ jp02.add(new JLabel("Decryption Computational Complexity"), c01);
+ decTime = new JTextField(decCC);
+ decTime.setEnabled(false);
+ jp02.add(decTime, c01);
+
+ jp02.add(new JLabel("Data Overhead (bits)"), c01);
+ secOverhead = new JTextField(secOv);
+ secOverhead.setEnabled(false);
+ jp02.add(secOverhead, c01);
+
+
+ autoMapKeys= new JRadioButton("Add Keys Only");
+ autoMapKeys.addActionListener(this);
+ jp02.add(autoMapKeys, c01);
+ secGroup.add(autoMapKeys);
+
/*
for (String cpuName: cpuTaskMap.keySet()){
@@ -442,30 +477,13 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
// addToComp = new JTextField(compName);
//jp01.add(addToComp,c01);
- removeForkAndJoin = new JCheckBox("Remove fork and join operators");
+ /* removeForkAndJoin = new JCheckBox("Remove fork and join operators");
if (mgui.isExperimentalOn()) {
//jp02.add(removeForkAndJoin, c01);
//removeForkAndJoin.addActionListener(this);
- }
+ }*/
- custom = new JCheckBox("Custom performance attributes");
- jp02.add(custom, c01);
- custom.addActionListener(this);
-
- jp02.add(new JLabel("Encryption Computational Complexity"), c01);
- encTime = new JTextField(encCC);
- encTime.setEnabled(false);
- jp02.add(encTime, c01);
-
- jp02.add(new JLabel("Decryption Computational Complexity"), c01);
- decTime = new JTextField(decCC);
- decTime.setEnabled(false);
- jp02.add(decTime, c01);
-
- jp02.add(new JLabel("Data Overhead (bits)"), c01);
- secOverhead = new JTextField(secOv);
- secOverhead.setEnabled(false);
- jp02.add(secOverhead, c01);
+
JPanel jp01 = new JPanel();
@@ -715,14 +733,17 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
} else if (command.equals("allIgnored")) {
allIgnored();
}
- if (evt.getSource() == addHSM) {
- listPanel.setEnabled(addHSM.isSelected());
- }
- if (evt.getSource() == autoConf || evt.getSource() == autoSec || evt.getSource() == autoMapKeys || evt.getSource() == addHSM || evt.getSource() == autoWeakAuth) {
+ if (evt.getSource() == autoConf || evt.getSource() == autoSec || evt.getSource() == autoMapKeys || evt.getSource() == autoWeakAuth) {
//autoWeakAuth.setEnabled(autoConf.isSelected());
autoConf.setEnabled(autoSec.isSelected());
+ addHSM.setEnabled(autoSec.isSelected());
+ addOneValidated.setEnabled(autoSec.isSelected());
+ allValidated.setEnabled(autoSec.isSelected());
+ addOneIgnored.setEnabled(autoSec.isSelected());
+ allIgnored.setEnabled(autoSec.isSelected());
autoWeakAuth.setEnabled(autoSec.isSelected());
autoStrongAuth.setEnabled(autoWeakAuth.isSelected());
+
if (!autoSec.isSelected()) {
autoConf.setSelected(false);
autoWeakAuth.setSelected(false);
@@ -788,50 +809,38 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
public void run() {
TraceManager.addDev("Thread started");
File testFile;
+ Map<String, java.util.List<String>> selectedCpuTasks = new HashMap<String, java.util.List<String>>();
try {
if (jp1.getSelectedIndex() == 1) {
- encCC = encTime.getText();
- decCC = decTime.getText();
- secOv = secOverhead.getText();
- TMLMapping map;
- if (autoConf.isSelected() || autoWeakAuth.isSelected() || autoStrongAuth.isSelected()) {
- if (custom.isSelected()) {
- map = mgui.gtm.autoSecure(mgui, encCC, secOv, decCC, autoConf.isSelected(), autoWeakAuth.isSelected(), autoStrongAuth
- .isSelected());
- } else {
- map = mgui.gtm.autoSecure(mgui, autoConf.isSelected(), autoWeakAuth.isSelected(), autoStrongAuth.isSelected());
- }
- } else if (addHSM.isSelected()) {
-
- // ArrayList<String> comps = new ArrayList<String>();
- // comps.add(addToComp.getText());
- Map<String, java.util.List<String>> selectedCpuTasks = new HashMap<String, java.util.List<String>>();
-
- for (String task : selectedTasks) {
- String cpu = taskCpuMap.get(task);
- if (selectedCpuTasks.containsKey(cpu)) {
- selectedCpuTasks.get(cpu).add(task);
- } else {
- ArrayList<String> tasks = new ArrayList<String>();
- tasks.add(task);
- selectedCpuTasks.put(cpu, tasks);
- }
- }
- /*for (JCheckBox cpu: cpuTaskObjs.keySet()){
- ArrayList<String> tasks = new ArrayList<String>();
- for (JCheckBox task: cpuTaskObjs.get(cpu)){
- if (task.isSelected()){
- tasks.add(task.getText());
- }
- }
- if (tasks.size()>0){
- selectedCpuTasks.put(cpu.getText(), tasks);
- }
- }
- mgui.gtm.addHSM(mgui, selectedCpuTasks);*/
- mgui.gtm.addHSM(mgui, selectedCpuTasks);
- }
- if (autoMapKeys.isSelected()) {
+ if (autoSec.isSelected()){
+ encCC = encTime.getText();
+ decCC = decTime.getText();
+ secOv = secOverhead.getText();
+ TMLMapping map;
+ if (addHSM.isSelected() && selectedTasks.size()>0) {
+
+
+ for (String task : selectedTasks) {
+ String cpu = taskCpuMap.get(task);
+ if (selectedCpuTasks.containsKey(cpu)) {
+ selectedCpuTasks.get(cpu).add(task);
+ } else {
+ ArrayList<String> tasks = new ArrayList<String>();
+ tasks.add(task);
+ selectedCpuTasks.put(cpu, tasks);
+ }
+ }
+ //mgui.gtm.addHSM(mgui, selectedCpuTasks);
+ }
+ if (autoConf.isSelected() || autoWeakAuth.isSelected() || autoStrongAuth.isSelected()) {
+ if (custom.isSelected()) {
+ map = mgui.gtm.autoSecure(mgui, encCC, secOv, decCC, autoConf.isSelected(), autoWeakAuth.isSelected(), autoStrongAuth.isSelected(), selectedCpuTasks);
+ } else {
+ map = mgui.gtm.autoSecure(mgui, "100", "0", "100", autoConf.isSelected(), autoWeakAuth.isSelected(), autoStrongAuth.isSelected(), selectedCpuTasks);
+ }
+ }
+ }
+ else if (autoMapKeys.isSelected()) {
mgui.gtm.autoMapKeys();
}
mode = NOT_STARTED;
@@ -840,11 +849,6 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
testGo();
pathCode = code1.getText().trim();
- // Issue #131: Not needed. Would duplicate file name
-// if (pathCode.isEmpty()) {
-// pathCode += "pvspec";
-// }
-
SpecConfigTTool.checkAndCreateProverifDir(pathCode);
pathCode += "pvspec";