diff --git a/simulators/c++2/src_simulator/definitions.h b/simulators/c++2/src_simulator/definitions.h
index cc088c70f6f0339ff5b2513b00fe2cfe88514b62..b722220a211c91eb85c53b4b4a9202fb65efde62 100644
--- a/simulators/c++2/src_simulator/definitions.h
+++ b/simulators/c++2/src_simulator/definitions.h
@@ -89,7 +89,7 @@ using std::max;
//cost of a send/wait command
#define WAIT_SEND_VLEN 1
//activate tis flag to take penalties (energy mode, branch prediction, context switch) into account
-#undef PENALTIES_ENABLED
+#define PENALTIES_ENABLED
//enables the state hash feature
#undef STATE_HASH_ENABLED
//enables listerns for interactive simulation, switch off for fast simulation in command line mode
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index 173936184000565f17413b2bdb55495c729ffbe4..0e17581850c5a654c38a845c05032270f8ee672f 100644
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -1038,38 +1038,6 @@ public class GTURTLEModeling {
return map;
}
- 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;
- }
-
- }
-
- 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;
- }
- }
public HashMap<String, HashSet<String>> getCPUTaskMap() {
HashMap<String, HashSet<String>> cpuTaskMap = new HashMap<String, HashSet<String>>();
@@ -1087,879 +1055,8 @@ public class GTURTLEModeling {
}
public void addHSM(MainGUI gui, Map<String, List<String>> selectedCpuTasks) {
- System.out.println("Adding HSM");
- String encComp = "100";
- String decComp = "100";
- String overhead = "0";
- String name = "hsm";
- if (tmap == null) {
- return;
- }
- //Clone diagrams
- TURTLEPanel tmlap = tmap.getCorrespondanceList().getTG(tmap.getArch().getFirstCPU()).getTDiagramPanel().tp;
- int arch = gui.tabs.indexOf(tmlap);
- gui.cloneRenameTab(arch, "hsm");
- TMLArchiPanel newarch = (TMLArchiPanel) gui.tabs.get(gui.tabs.size() - 1);
-
- TGComponent tgcomp = tmap.getTMLModeling().getTGComponent();
- TMLComponentDesignPanel tmlcdp = (TMLComponentDesignPanel) tgcomp.getTDiagramPanel().tp;
-
-// TMLComponentDesignPanel tmlcdp = tmap.getTMLCDesignPanel();
- int ind = gui.tabs.indexOf(tmlcdp);
- String tabName = gui.getTitleAt(tmlcdp);
- gui.cloneRenameTab(ind, name);
- TMLComponentDesignPanel t = (TMLComponentDesignPanel) gui.tabs.get(gui.tabs.size() - 1);
- TMLComponentTaskDiagramPanel tcdp = t.tmlctdp;
- //Create clone of architecture panel and map tasks to it
- newarch.renameMapping(tabName, tabName + "_" + name);
-
-
- //ProVerif analysis
- List<String> nonAuthChans = new ArrayList<String>();
- List<String> nonSecChans = new ArrayList<String>();
-
- proverifAnalysis(tmap, nonAuthChans, nonSecChans);
-
- TGConnector fromStart;
- Map<String, HSMChannel> secChannels = new HashMap<String, HSMChannel>();
- //Add a HSM 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);
- //TAttribute isEnc = new TAttribute(2, "isEnc", "true", 4);
- //hsm.getAttributeList().add(isEnc);
- 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;
- }
- // System.out.println("nonAuthChans " + nonAuthChans);
- //System.out.println("nonSecChans "+ nonSecChans);
- for (TMLCPrimitiveComponent comp : comps) {
-
- Map<String, HSMChannel> compChannels = new HashMap<String, HSMChannel>();
- String compName = comp.getValue();
- TMLActivityDiagramPanel tad = t.getTMLActivityDiagramPanel(compName);
- Set<TGComponent> channelInstances = new HashSet<TGComponent>();
- Set<TGComponent> secOperators = new HashSet<TGComponent>();
- // isEnc = new TAttribute(2, "isEnc", "true", 4);
- //comp.getAttributeList().add(isEnc);
- //Find all unsecured channels
- //For previously secured channels, relocate encryption to the hsm
-
- for (TGComponent tg : tad.getComponentList()) {
- if (tg instanceof TMLADWriteChannel) {
- TMLADWriteChannel writeChannel = (TMLADWriteChannel) tg;
- if (writeChannel.getSecurityContext().equals("")) {
- String nonceName = "";
- int type = -1;
- if (nonSecChans.contains(compName + "__" + writeChannel.getChannelName() + "_chData")) {
- type = HSMChannel.SENC;
- if (nonAuthChans.contains(compName + "__" + writeChannel.getChannelName())) {
- nonceName = "nonce_" + writeChannel.getChannelName();
- }
- } else if (nonAuthChans.contains(compName + "__" + writeChannel.getChannelName())) {
- type = HSMChannel.MAC;
- }
- HSMChannel ch = new HSMChannel(writeChannel.getChannelName(), compName, type);
- ch.securityContext = "hsmSec_" + writeChannel.getChannelName();
- ch.nonceName = nonceName;
- fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
- if (fromStart != null) {
- if (type != -1) {
- compChannels.put(writeChannel.getChannelName(), ch);
- channelInstances.add(tg);
- }
- }
- } else {
- //System.out.println("security context:"+writeChannel.securityContext);
- fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
- if (fromStart != null) {
- channelInstances.add(tg);
- SecurityPattern sp = tmap.getSecurityPatternByName(writeChannel.getSecurityContext());
- int type = -1;
- if (sp.type.equals("Symmetric Encryption")) {
- type = HSMChannel.SENC;
- } else if (sp.type.equals("Asymmetric Encryption")) {
- type = HSMChannel.AENC;
- } else if (sp.type.equals("MAC")) {
- type = HSMChannel.MAC;
- } else if (sp.type.equals("Nonce")) {
- type = HSMChannel.NONCE;
- }
- HSMChannel ch = new HSMChannel(writeChannel.getChannelName(), compName, type);
- ch.securityContext = writeChannel.getSecurityContext();
- compChannels.put(writeChannel.getChannelName(), ch);
- //chanNames.add(writeChannel.getChannelName()+compName);
- }
- }
- }
- if (tg instanceof TMLADReadChannel) {
- TMLADReadChannel readChannel = (TMLADReadChannel) tg;
- if (readChannel.getSecurityContext().equals("")) {
- fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
- if (fromStart != null) {
- if (nonSecChans.contains(compName + "__" + readChannel.getChannelName() + "_chData") || nonAuthChans.contains(compName + "__" + readChannel.getChannelName())) {
- channelInstances.add(tg);
- HSMChannel ch = new HSMChannel(readChannel.getChannelName(), compName, HSMChannel.DEC);
- ch.securityContext = "hsmSec_" + readChannel.getChannelName();
- compChannels.put(readChannel.getChannelName(), ch);
- if (nonSecChans.contains(compName + "__" + readChannel.getChannelName() + "_chData") && nonAuthChans.contains(compName + "__" + readChannel.getChannelName())) {
- ch.nonceName = "nonce_" + readChannel.getChannelName();
- }
- }
- }
- } else {
- fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
- if (fromStart != null) {
- channelInstances.add(tg);
- HSMChannel ch = new HSMChannel(readChannel.getChannelName(), compName, HSMChannel.DEC);
- ch.securityContext = readChannel.getSecurityContext();
- compChannels.put(readChannel.getChannelName(), ch);
- }
- }
- }
- if (tg instanceof TMLADEncrypt) {
- // TMLADEncrypt enc = (TMLADEncrypt) tg;
- secOperators.add(tg);
- //}
- }
- if (tg instanceof TMLADDecrypt) {
- // TMLADDecrypt dec = (TMLADDecrypt) tg;
- secOperators.add(tg);
- //}
- }
- }
- //System.out.println("compchannels " +compChannels);
- List<ChannelData> hsmChans = new ArrayList<ChannelData>();
- ChannelData chd = new ChannelData("startHSM_" + cpuName, false, false);
- hsmChans.add(chd);
- for (String s : compChannels.keySet()) {
- hsmChannels.put(s, compChannels.get(s));
- chd = new ChannelData("data_" + s + "_" + compChannels.get(s).task, false, true);
- hsmChans.add(chd);
- chd = new ChannelData("retData_" + s + "_" + compChannels.get(s).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(2));
- }
- 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);
- }
- int xpos = 0;
- int ypos = 0;
-
- //Remove existing security elements
- for (TGComponent op : secOperators) {
- TGConnector prev = tad.findTGConnectorEndingAt(op.getTGConnectingPointAtIndex(0));
- //TGConnectingPoint point = prev.getTGConnectingPointP1();
- TGConnector end = tad.findTGConnectorStartingAt(op.getTGConnectingPointAtIndex(1));
- TGConnectingPoint point2 = end.getTGConnectingPointP2();
- tad.removeComponent(op);
- tad.removeComponent(end);
- tad.addComponent(prev, 0, 0, false, true);
- prev.setP2(point2);
- }
-
- //Modify component activity diagram to add read/write to HSM
-
- //Add actions before Write Channel
- for (TGComponent chan : channelInstances) {
- String chanName = "";
- if (!(chan instanceof TMLADWriteChannel)) {
- continue;
- }
- TMLADWriteChannel writeChannel = (TMLADWriteChannel) chan;
- chanName = writeChannel.getChannelName();
- HSMChannel ch = hsmChannels.get(chanName);
- writeChannel.setSecurityContext(ch.securityContext);
- xpos = chan.getX();
- ypos = chan.getY();
- fromStart = tad.findTGConnectorEndingAt(chan.getTGConnectingPointAtIndex(0));
- TGConnectingPoint 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_" + cpuName);
- // req.setParam(0, "isEnc");
- 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 + "_" + compName);
- wr.setSecurityContext(ch.securityContext);
- 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));
-
-
- //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 + "_" + compName);
- rd.setSecurityContext(ch.securityContext);
- 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 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.setCd(tg.getX(), tg.getY() + yShift);
- }
- }
- tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
- tad.repaint();
-
- }
- //Add actions after Read Channel
- for (TGComponent chan : channelInstances) {
- String chanName = "";
- if (!(chan instanceof TMLADReadChannel)) {
- continue;
- }
- TMLADReadChannel readChannel = (TMLADReadChannel) chan;
- chanName = readChannel.getChannelName();
- HSMChannel ch = hsmChannels.get(chanName);
- readChannel.setSecurityContext(ch.securityContext);
- xpos = chan.getX() + 10;
- ypos = chan.getY();
- fromStart = tad.findTGConnectorStartingAt(chan.getTGConnectingPointAtIndex(1));
- if (fromStart == null) {
- fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
- fromStart.setP1(chan.getTGConnectingPointAtIndex(1));
- tad.addComponent(fromStart, xpos, ypos, false, true);
- }
- 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));
-
-
- //Add send request operator
-
- yShift += 50;
- TMLADSendRequest req = new TMLADSendRequest(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- req.setRequestName("startHSM_" + cpuName);
- // req.setParam(0, "isEnc");
- req.makeValue();
- 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;
- //Add write channel operator
- TMLADWriteChannel wr = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- wr.setChannelName("data_" + chanName + "_" + compName);
- wr.setSecurityContext(ch.securityContext);
- tad.addComponent(wr, 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(req.getTGConnectingPointAtIndex(1));
- fromStart.setP2(wr.getTGConnectingPointAtIndex(0));
- tad.addComponent(fromStart, xpos, ypos, false, true);
-
- //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 + "_" + compName);
- rd.setSecurityContext(ch.securityContext);
- tad.addComponent(rd, xpos, ypos + yShift, 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));
- fromStart.setP2(rd.getTGConnectingPointAtIndex(0));
- yShift += 50;
-
- if (point != null) {
- 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));
- //Direct the last TGConnector back to the start of the write channel operator
-
- fromStart.setP2(point);
- }
- yShift += 50;
-
- //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 != chan) {
- tg.setCd(tg.getX(), tg.getY() + yShift);
- }
- }
- tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
- tad.repaint();
- }
- //for (String chan: chanNames){
- // hsmChannels.put(chan, compName);
- //}
- }
-
- int xpos = 0;
- int ypos = 0;
-
-
- //Build HSM Activity diagram
-
- TMLActivityDiagramPanel tad = t.getTMLActivityDiagramPanel("HSM_" + cpuName);
-
- 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, "isEnc");
- 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(start.getTGConnectingPointAtIndex(0));
- 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
- TMLADChoice choice2 = new TMLADChoice(xc, 400, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- if (hsmChannels.keySet().size() > 3) {
- int i = 0;
- for (String chan : hsmChannels.keySet()) {
- HSMChannel ch = hsmChannels.get(chan);
- 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_" + chan + "_" + hsmChannels.get(chan).task);
- rd.setSecurityContext(ch.securityContext);
- 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_" + chan + "_" + hsmChannels.get(chan).task);
- tad.addComponent(wr, xc, 600, false, true);
- wr.setSecurityContext(ch.securityContext);
-
-
- if (hsmChannels.get(chan).secType == HSMChannel.DEC) {
- TMLADDecrypt dec = new TMLADDecrypt(xc, 500, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- dec.securityContext = ch.securityContext;
- 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 = ch.securityContext;
- if (hsmChannels.get(chan).secType == HSMChannel.SENC) {
- enc.type = "Symmetric Encryption";
- } else if (hsmChannels.get(chan).secType == HSMChannel.AENC) {
- enc.type = "Asymmetric Encryption";
- } else if (hsmChannels.get(chan).secType == HSMChannel.MAC) {
- enc.type = "MAC";
- } else if (hsmChannels.get(chan).secType == HSMChannel.NONCE) {
- enc.type = "Nonce";
- }
-
- enc.message_overhead = overhead;
- enc.encTime = encComp;
- enc.decTime = decComp;
- enc.nonce = hsmChannels.get(chan).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 (String chan : hsmChannels.keySet()) {
- HSMChannel ch = hsmChannels.get(chan);
- TMLADReadChannel rd = new TMLADReadChannel(xc, 300, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- rd.setChannelName("data_" + chan + "_" + hsmChannels.get(chan).task);
- rd.setSecurityContext(ch.securityContext);
- 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, 300, 200, false, true);
-
- TMLADWriteChannel wr = new TMLADWriteChannel(xc, 600, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- wr.setChannelName("retData_" + chan + "_" + hsmChannels.get(chan).task);
- tad.addComponent(wr, xc, 600, false, true);
- wr.setSecurityContext(ch.securityContext);
-
-
- if (hsmChannels.get(chan).secType == HSMChannel.DEC) {
- TMLADDecrypt dec = new TMLADDecrypt(xc, 500, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- dec.securityContext = ch.securityContext;
- 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);
-
- //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 = ch.securityContext;
- if (hsmChannels.get(chan).secType == HSMChannel.SENC) {
- enc.type = "Symmetric Encryption";
- } else if (hsmChannels.get(chan).secType == HSMChannel.AENC) {
- enc.type = "Asymmetric Encryption";
- } else if (hsmChannels.get(chan).secType == HSMChannel.MAC) {
- enc.type = "MAC";
- } else if (hsmChannels.get(chan).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, 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);
-
-
- }
-
-
- /*MLADChoice choice2 = new TMLADChoice(xc, 400, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- tad.addComponent(choice2, xc, 400,false,true);
- choice2.setGuard("[isEnc]", 0);
- choice2.setGuard("[else]",1);
-
- //connect readchannel and choice 2
- fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector());
- fromStart.setP1(rd.getTGConnectingPointAtIndex(1));
- fromStart.setP2(choice2.getTGConnectingPointAtIndex(0));
- tad.addComponent(fromStart, 300,200,false,true);
-
- TMLADEncrypt enc = new TMLADEncrypt(xc-75, 500, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- enc.securityContext = "hsmSec_"+chan;
- enc.type = "Symmetric Encryption";
- enc.message_overhead = overhead;
- enc.encTime= encComp;
- enc.decTime=decComp;
- tad.addComponent(enc, xc-75, 500,false,true);
-
- //Connect choice 2 and encrypt
- fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector());
- fromStart.setP1(choice2.getTGConnectingPointAtIndex(1));
- fromStart.setP2(enc.getTGConnectingPointAtIndex(0));
- tad.addComponent(fromStart, 300,200,false,true);
-
- TMLADWriteChannel wr = new TMLADWriteChannel(xc-75, 600, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- wr.setChannelName("retData_"+chan+hsmChannels.get(chan));
- tad.addComponent(wr, xc-75, 600,false,true);
- wr.securityContext = "hsmSec_"+chan;
-
- //Connect encrypt and writeChannel
- fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector());
- fromStart.setP1(enc.getTGConnectingPointAtIndex(1));
- fromStart.setP2(wr.getTGConnectingPointAtIndex(0));
- tad.addComponent(fromStart, 300,200,false,true);
-
-
- TMLADDecrypt dec = new TMLADDecrypt(xc+75, 500, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- dec.securityContext = "hsmSec_"+chan;
- tad.addComponent(dec, xc+75, 500,false,true);
-
- //Connect choice2 and decrypt
-
- fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector());
- fromStart.setP1(choice2.getTGConnectingPointAtIndex(2));
- fromStart.setP2(dec.getTGConnectingPointAtIndex(0));
- tad.addComponent(fromStart, 300,200,false,true);
-
- TMLADWriteChannel wr2 = new TMLADWriteChannel(xc+75, 600, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- wr2.setChannelName("retData_"+chan+hsmChannels.get(chan));
- wr2.securityContext = "hsmSec_"+chan;
-
- //Connect decrypt and writeChannel
- fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector());
- fromStart.setP1(dec.getTGConnectingPointAtIndex(1));
- fromStart.setP2(wr2.getTGConnectingPointAtIndex(0));
- tad.addComponent(fromStart, 300,200,false,true);
- tad.addComponent(wr2, xc+75, 600,false,true);
-
- */
- xc += 300;
- i++;
- }
-
- }
-
- secChannels.putAll(hsmChannels);
- }
- //For all the tasks that receive encrypted data, decrypt it, assuming it has no associated HSM
- for (TMLTask task : tmap.getTMLModeling().getTasks()) {
- int xpos, ypos;
- //System.out.println("loop 2");
- TMLActivityDiagramPanel tad = t.getTMLActivityDiagramPanel(task.getName());
- HashSet<TGComponent> channelInstances = new HashSet<TGComponent>();
- for (String chan : secChannels.keySet()) {
- HSMChannel ch = secChannels.get(chan);
- channelInstances.clear();
- for (TGComponent tg : tad.getComponentList()) {
- if (tg instanceof TMLADReadChannel) {
- TMLADReadChannel readChannel = (TMLADReadChannel) tg;
- if (readChannel.getChannelName().equals(chan) && readChannel.getSecurityContext().equals("")) {
- fromStart = tad.findTGConnectorStartingAt(tg.getTGConnectingPointAtIndex(1));
- if (fromStart != null) {
- channelInstances.add(tg);
- }
- }
- }
- }
- for (TGComponent chI : channelInstances) {
- TMLADReadChannel readChannel = (TMLADReadChannel) chI;
- readChannel.setSecurityContext(ch.securityContext);
- xpos = chI.getX();
- ypos = chI.getY() + 10;
- fromStart = tad.findTGConnectorStartingAt(chI.getTGConnectingPointAtIndex(1));
- if (fromStart == null) {
- fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
- fromStart.setP1(chI.getTGConnectingPointAtIndex(1));
- tad.addComponent(fromStart, xpos, ypos, false, true);
- }
- TGConnectingPoint point = fromStart.getTGConnectingPointP2();
- //Add decryption operator
- int yShift = 100;
- TMLADDecrypt dec = new TMLADDecrypt(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- dec.securityContext = ch.securityContext;
- tad.addComponent(dec, xpos, ypos + yShift, false, true);
-
-
- fromStart.setP2(dec.getTGConnectingPointAtIndex(0));
- if (point != null) {
- fromStart = new TGConnectorTMLAD(dec.getX(), dec.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(dec.getTGConnectingPointAtIndex(1));
-
- //Direct the last TGConnector back to the next action
-
- 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 != dec) {
- tg.setCd(tg.getX(), tg.getY() + yShift);
- }
- }
- tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
- tad.repaint();
-
- }
- }
- //Next find channels that send encrypted data, and add the encryption operator
- for (String chan : secChannels.keySet()) {
- channelInstances.clear();
- HSMChannel ch = secChannels.get(chan);
- for (TGComponent tg : tad.getComponentList()) {
- if (tg instanceof TMLADWriteChannel) {
- TMLADWriteChannel writeChannel = (TMLADWriteChannel) tg;
- if (writeChannel.getChannelName().equals(chan) && writeChannel.getSecurityContext().equals("")) {
- fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
- if (fromStart != null) {
- channelInstances.add(tg);
- }
- }
- }
- }
- for (TGComponent chI : channelInstances) {
- TMLADWriteChannel writeChannel = (TMLADWriteChannel) chI;
- writeChannel.setSecurityContext(ch.securityContext);
- xpos = chI.getX();
- ypos = chI.getY() - 10;
- fromStart = tad.findTGConnectorEndingAt(chI.getTGConnectingPointAtIndex(0));
- TGConnectingPoint point = fromStart.getTGConnectingPointP2();
- //Add encryption operator
- int yShift = 100;
-
- TMLADEncrypt enc = new TMLADEncrypt(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- tad.addComponent(enc, xpos, ypos, false, true);
- enc.securityContext = ch.securityContext;
- enc.type = "Symmetric Encryption";
- enc.message_overhead = overhead;
- enc.encTime = encComp;
- enc.decTime = decComp;
- enc.size = overhead;
-
-
- fromStart.setP2(enc.getTGConnectingPointAtIndex(0));
- fromStart = new TGConnectorTMLAD(enc.getX(), enc.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(enc.getTGConnectingPointAtIndex(1));
-
- //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 != enc) {
- tg.setCd(tg.getX(), tg.getY() + yShift);
- }
- }
- tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
- tad.repaint();
-
- }
- }
-
- }
- for (String cpuName : selectedCpuTasks.keySet()) {
- //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() + 100, cpu.getY() + 100, archPanel.getMinX(), archPanel.getMaxX(), archPanel.getMinY(), archPanel.getMaxY(), true, null, archPanel);
- archPanel.addComponent(mem, cpu.getX() + 100, cpu.getY() + 100, 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);
- }
-
+ HSMGeneration hsm = new HSMGeneration(gui, selectedCpuTasks, tmap);
+ hsm.startThread();
}
@@ -2014,660 +1111,12 @@ public class GTURTLEModeling {
return autoSecure(gui, name, tmap, newarch, encComp, overhead, decComp, true, false, false);
}
- public void proverifAnalysis(TMLMapping<TGComponent> map, List<String> nonAuthChans, List<String> nonSecChans) {
- if (map == null) {
- TraceManager.addDev("No mapping");
- return;
- }
- //Perform ProVerif Analysis
- TML2Avatar t2a = new TML2Avatar(map, false, true);
- AvatarSpecification avatarspec = t2a.generateAvatarSpec("1");
- if (avatarspec == null) {
- TraceManager.addDev("No avatar spec");
- return;
- }
-
- avatar2proverif = new AVATAR2ProVerif(avatarspec);
- try {
- proverif = avatar2proverif.generateProVerif(true, true, 1, true, false);
- warnings = avatar2proverif.getWarnings();
-
- // Issue #131
- final String proverifSpecFile = SpecConfigTTool.ProVerifCodeDirectory + "pvspec";
-
- if (!avatar2proverif.saveInFile( proverifSpecFile )) {
-// if (!avatar2proverif.saveInFile("pvspec")) {
- return;
- }
-
- RshClient rshc = new RshClient(ConfigurationTTool.ProVerifVerifierHost);
-
- // Issue #131
- rshc.setCmd(ConfigurationTTool.ProVerifVerifierPath + " -in pitype " + proverifSpecFile );
-// rshc.setCmd(ConfigurationTTool.ProVerifVerifierPath + " -in pitype pvspec");
- rshc.sendExecuteCommandRequest();
- Reader data = rshc.getDataReaderFromProcess();
-
- ProVerifOutputAnalyzer pvoa = getProVerifOutputAnalyzer();
- pvoa.analyzeOutput(data, true);
- Map<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
- for (AvatarPragmaSecret pragma : confResults.keySet()) {
- if (confResults.get(pragma).isProved() && !confResults.get(pragma).isSatisfied()) {
- nonSecChans.add(pragma.getArg().getBlock().getName() + "__" + pragma.getArg().getName());
- TraceManager.addDev(pragma.getArg().getBlock().getName() + "." + pragma.getArg().getName() + " is not secret");
- TMLChannel chan = map.getTMLModeling().getChannelByShortName(pragma.getArg().getName().replaceAll("_chData", ""));
- for (String block : chan.getTaskNames()) {
- nonSecChans.add(block + "__" + pragma.getArg().getName());
- }
- }
- }
- Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authResults = pvoa.getAuthenticityResults();
- for (AvatarPragmaAuthenticity pragma : authResults.keySet()) {
- if (authResults.get(pragma).isProved() && !authResults.get(pragma).isSatisfied()) {
- nonAuthChans.add(pragma.getAttrA().getAttribute().getBlock().getName() + "__" + pragma.getAttrA().getAttribute().getName().replaceAll("_chData", ""));
- nonAuthChans.add(pragma.getAttrB().getAttribute().getBlock().getName() + "__" + pragma.getAttrB().getAttribute().getName().replaceAll("_chData", ""));
- }
- }
- TraceManager.addDev("nonsecchans " + nonSecChans);
- TraceManager.addDev("nonauthchans " + nonAuthChans);
- TraceManager.addDev("all results displayed");
-
- } catch (Exception e) {
- System.out.println("ProVerif Analysis Failed " + e);
- }
- }
-
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<TMLTask, List<TMLTask>> toSecure = new HashMap<TMLTask, List<TMLTask>>();
- Map<TMLTask, List<TMLTask>> toSecureRev = new HashMap<TMLTask, List<TMLTask>>();
- Map<TMLTask, List<String>> secOutChannels = new HashMap<TMLTask, List<String>>();
- Map<TMLTask, List<String>> secInChannels = new HashMap<TMLTask, List<String>>();
- Map<TMLTask, List<String>> nonceOutChannels = new HashMap<TMLTask, List<String>>();
- 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());
- List<String> nonAuthChans = new ArrayList<String>();
- List<String> nonSecChans = new ArrayList<String>();
-
- proverifAnalysis(map, nonAuthChans, nonSecChans);
-
- TMLModeling<TGComponent> tmlmodel = map.getTMLModeling();
- List<TMLChannel> channels = tmlmodel.getChannels();
- for (TMLChannel channel : channels) {
- for (TMLCPrimitivePort p : channel.ports) {
- channel.checkConf = channel.checkConf || p.checkConf;
- channel.checkAuth = channel.checkAuth || p.checkAuth;
- }
- }
-
- //Create clone of Component Diagram + Activity diagrams to secure
- TGComponent tgcomp = map.getTMLModeling().getTGComponent();
- TMLComponentDesignPanel tmlcdp = (TMLComponentDesignPanel) tgcomp.getTDiagramPanel().tp;
-// TMLComponentDesignPanel tmlcdp = map.getTMLCDesignPanel();
- int ind = gui.tabs.indexOf(tmlcdp);
- if (ind == -1) {
- TraceManager.addDev("No Component Design Panel");
- return null;
- }
- String tabName = gui.getTitleAt(tmlcdp);
- gui.cloneRenameTab(ind, name);
- TMLComponentDesignPanel t = (TMLComponentDesignPanel) gui.tabs.get(gui.tabs.size() - 1);
-
- TMLComponentTaskDiagramPanel tcdp = t.tmlctdp;
- //Create clone of architecture panel and map tasks to it
- newarch.renameMapping(tabName, tabName + "_" + name);
-
- for (TMLTask task : map.getTMLModeling().getTasks()) {
- List<String> tmp = new ArrayList<String>();
- List<String> tmp2 = new ArrayList<String>();
- List<TMLTask> tmp3 = new ArrayList<TMLTask>();
- List<TMLTask> tmp4 = new ArrayList<TMLTask>();
- List<String> tmp5 = new ArrayList<String>();
- List<String> tmp6 = new ArrayList<String>();
- List<String> tmp7 = new ArrayList<String>();
- 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);
- toSecureRev.put(task, tmp4);
- nonceInChannels.put(task, tmp5);
- nonceOutChannels.put(task, tmp6);
- macInChannels.put(task, tmp7);
- macOutChannels.put(task, tmp8);
- macNonceOutChannels.put(task, tmp9);
- macNonceInChannels.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());
- for (TGComponent tg : tad.getComponentList()) {
- if (tg instanceof TMLADWriteChannel) {
- TMLADWriteChannel writeChannel = (TMLADWriteChannel) tg;
- if (writeChannel.getSecurityContext().equals("")) {
-
- TMLChannel chan = tmlmodel.getChannelByName(tabName + "__" + writeChannel.getChannelName());
- //System.out.println("channel " + chan);
- if (chan != null) {
- if (chan.checkConf && autoConf) {
- // System.out.println(chan.getOriginTask().getName().split("__")[1]);
- 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());
- }
- }
- } 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());
- }
- }
-
- }
- }
- }
- }
- }
- }
- TraceManager.addDev("macoutchans " + macOutChannels);
- TraceManager.addDev("macinchans " + macInChannels);
- TraceManager.addDev("nonsecin " + secInChannels);
- TraceManager.addDev("nonsecout " + secOutChannels);
- TraceManager.addDev("noncein " + nonceInChannels);
- TraceManager.addDev("nonceout " + nonceOutChannels);
-
- // System.out.println(secOutChanannels.toString());
- // 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);
-
- for (TMLTask task2 : toSecureRev.get(task)) {
- boolean addChan = true;
- for (TMLChannel chan : chans) {
- if (chan.getDestinationTask() == task2) {
- addChan = false;
- }
- }
-
- if (addChan) {
- TMLCChannelOutPort originPort = new TMLCChannelOutPort(0, 0, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, null, tcdp);
- TMLCChannelOutPort destPort = new TMLCChannelOutPort(0, 0, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, null, tcdp);
- for (TGComponent tg : tcdp.getComponentList()) {
- if (tg instanceof TMLCPrimitiveComponent) {
- if (tg.getValue().equals(task.getName().split("__")[1])) {
- originPort = new TMLCChannelOutPort(tg.getX(), tg.getY(), tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, tg, tcdp);
- originPort.commName = "nonceCh" + task.getName().split("__")[1] + "_" + task2.getName().split("__")[1];
- tcdp.addComponent(originPort, tg.getX(), tg.getY(), true, true);
- } else if (tg.getValue().equals(task2.getName().split("__")[1])) {
- destPort = new TMLCChannelOutPort(tg.getX(), tg.getY(), tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, tg, tcdp);
- destPort.isOrigin = false;
- destPort.commName = "nonceCh" + task.getName().split("__")[1] + "_" + task2.getName().split("__")[1];
- tcdp.addComponent(destPort, tg.getX(), tg.getY(), true, true);
- }
- }
- }
- tmlmodel.addChannel(new TMLChannel("nonceCh" + task.getName().split("__")[1] + "_" + task2.getName().split("__")[1], originPort));
- //Add connection
- 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);
- }
- }
- }
- // }
- //Add encryption/nonces to activity diagram
- for (TMLTask task : toSecure.keySet()) {
- String title = task.getName().split("__")[0];
- TraceManager.addDev("Securing task " + task.getName());
- TMLActivityDiagramPanel tad = t.getTMLActivityDiagramPanel(task.getName());
- //Get start state position, shift everything down
- int xpos = 0;
- int ypos = 0;
- TGConnector fromStart = new TGConnectorTMLAD(0, 0, 0, 0, 0, 0, false, null, tad, null, null, new Vector<Point>());
- TGConnectingPoint point = new TGConnectingPoint(null, 0, 0, false, false);
- //Find states immediately before the write channel operator
-
- //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;
- TMLChannel tmlc = tmlmodel.getChannelByName(title + "__" + channel);
- //First, find the connector that points to it. We will add the encryption, nonce operators directly before the write channel operator
- for (TGComponent tg : tad.getComponentList()) {
- if (tg instanceof TMLADWriteChannel) {
- TMLADWriteChannel writeChannel = (TMLADWriteChannel) tg;
- if (writeChannel.getChannelName().equals(channel) && writeChannel.getSecurityContext().equals("")) {
-
- if (fromStart != null) {
- channelInstances.add(tg);
- }
- }
- }
- }
- for (TGComponent comp : channelInstances) {
- //TMLADWriteChannel writeChannel = (TMLADWriteChannel) comp;
- xpos = comp.getX();
- ypos = comp.getY();
- fromStart = tad.findTGConnectorEndingAt(comp.getTGConnectingPointAtIndex(0));
- point = fromStart.getTGConnectingPointP2();
- //Add encryption operator
- TMLADEncrypt enc = new TMLADEncrypt(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- TMLADReadChannel rd = new TMLADReadChannel(0, 0, 0, 0, 0, 0, false, null, tad);
- 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());
-
- 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(enc.getX(), enc.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));
- yShift += 60;
- //Move encryption operator after receive nonce component
- enc.setCd(xpos, ypos + yShift);
- if (tmlc != null) {
- enc.nonce = "nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1];
- }
- }
-
- enc.securityContext = "autoEncrypt_" + channel;
- enc.type = "Symmetric Encryption";
- enc.message_overhead = overhead;
- enc.encTime = encComp;
- enc.decTime = decComp;
- tad.addComponent(enc, xpos, ypos + yShift, false, true);
- yShift += 60;
- fromStart.setP2(enc.getTGConnectingPointAtIndex(0));
- fromStart = new TGConnectorTMLAD(enc.getX(), enc.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(enc.getTGConnectingPointAtIndex(1));
-
- //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 instanceof TMLADWriteChannel) {
- TMLADWriteChannel wChannel = (TMLADWriteChannel) tg;
- 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());
-
- }
- }
- if (tg.getY() >= ypos && tg != enc && tg != rd) {
- tg.setCd(tg.getX(), tg.getY() + yShift);
- }
- }
- tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
- tad.repaint();
- }
- }
-
- for (String channel : macOutChannels.get(task)) {
- //Add MAC before writechannel
- int yShift = 50;
- TMLChannel tmlc = tmlmodel.getChannelByName(title + "__" + channel);
- //First, find the connector that points to it. We will add the encryption, nonce operators directly before the write channel operator
- Set<TGComponent> channelInstances = new HashSet<TGComponent>();
- for (TGComponent tg : tad.getComponentList()) {
- if (tg instanceof TMLADWriteChannel) {
- TMLADWriteChannel writeChannel = (TMLADWriteChannel) tg;
- if (writeChannel.getChannelName().equals(channel) && writeChannel.getSecurityContext().equals("")) {
- xpos = tg.getX();
- ypos = tg.getY();
- fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
- if (fromStart != null) {
- channelInstances.add(tg);
- }
- }
- }
- }
- for (TGComponent comp : channelInstances) {
- //TMLADWriteChannel writeChannel = (TMLADWriteChannel) comp;
- xpos = comp.getX();
- ypos = comp.getY();
- fromStart = tad.findTGConnectorEndingAt(comp.getTGConnectingPointAtIndex(0));
- point = fromStart.getTGConnectingPointP2();
-
- TMLADEncrypt enc = new TMLADEncrypt(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
-
- //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)) {
- //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());
-
- 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(enc.getX(), enc.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));
- yShift += 60;
- //Move encryption operator after receive nonce component
- enc.setCd(xpos, ypos + yShift);
- if (tmlc != null) {
- enc.nonce = "nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1];
- }
- }
-
- //Add encryption operator
-
- enc.securityContext = "autoEncrypt_" + channel;
- enc.type = "MAC";
- enc.message_overhead = overhead;
- enc.encTime = encComp;
- enc.decTime = decComp;
- enc.size = overhead;
- tad.addComponent(enc, xpos, ypos + yShift, false, true);
- yShift += 60;
- fromStart.setP2(enc.getTGConnectingPointAtIndex(0));
- fromStart = new TGConnectorTMLAD(enc.getX(), enc.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(enc.getTGConnectingPointAtIndex(1));
-
- //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 instanceof TMLADWriteChannel) {
- TMLADWriteChannel wChannel = (TMLADWriteChannel) tg;
- 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());
- tad.repaint();
- }
- }
- if (tg.getY() >= ypos && tg != enc && tg != rd) {
- tg.setCd(tg.getX(), tg.getY() + yShift);
- }
- }
- tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
- }
- }
- for (String channel : macInChannels.get(task)) {
- //Add decryptmac after readchannel
- int yShift = 50;
- 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);
- //Find read channel operator
-
- 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 comp : channelInstances) {
-
- fromStart = tad.findTGConnectorEndingAt(comp.getTGConnectingPointAtIndex(0));
- point = fromStart.getTGConnectingPointP2();
- conn = tad.findTGConnectorStartingAt(comp.getTGConnectingPointAtIndex(1));
- next = conn.getTGConnectingPointP2();
- xpos = fromStart.getX();
- ypos = fromStart.getY();
-
-
- TMLADReadChannel readChannel = (TMLADReadChannel) comp;
- TraceManager.addDev("Securing read channel " + readChannel.getChannelName());
- readChannel.setSecurityContext("autoEncrypt_" + 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)) {
- //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];
- 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;
- wr = 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) {
- wr.setChannelName(matches.get(0).getName().replaceAll(title + "__", ""));
- } else {
- wr.setChannelName("nonceCh" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
- }
- //send the nonce along the channel
- wr.setSecurityContext("nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
- tad.addComponent(wr, xpos, ypos + yShift, false, true);
- wr.makeValue();
- TGConnector tmp = new TGConnectorTMLAD(wr.getX(), wr.getY() + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, nonce.getTGConnectingPointAtIndex(1), wr.getTGConnectingPointAtIndex(0), new Vector<Point>());
- tad.addComponent(tmp, xpos, ypos, false, true);
- fromStart = new TGConnectorTMLAD(wr.getX(), wr.getY(), tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, wr.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(wr.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 != wr) {
- tg.setCd(tg.getX(), tg.getY() + yShift);
- }
- }
- }
-
- //Add decryption operator if it does not already exist
- xpos = conn.getX();
- 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();
- tad.addComponent(dec, dec.getX(), dec.getY(), false, true);
- conn.setP2(dec.getTGConnectingPointAtIndex(0));
- 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));
- conn.setP2(next);
- tad.addComponent(conn, conn.getX(), conn.getY(), false, true);
- //Shift everything down
- for (TGComponent tg : tad.getComponentList()) {
- if (tg instanceof TMLADReadChannel) {
- readChannel = (TMLADReadChannel) tg;
- 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());
-
- }
- }
- if (tg.getY() > ypos && tg != dec && tg != comp) {
-
- tg.setCd(tg.getX(), tg.getY() + yShift);
- }
- }
-
-
- tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
- tad.repaint();
- }
- }
- for (String channel : secInChannels.get(task)) {
- TraceManager.addDev("securing channel " + channel);
- int yShift = 20;
- // String title = task.getName().split("__")[0];
- TMLChannel tmlc = tmlmodel.getChannelByName(title + "__" + channel);
- 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);
- //Find read channel operator
- TMLADReadChannel readChannel = new TMLADReadChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
- HashSet<TGComponent> channelInstances = new HashSet<TGComponent>();
- for (TGComponent tg : tad.getComponentList()) {
- if (tg instanceof 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 comp : channelInstances) {
-
- fromStart = tad.findTGConnectorEndingAt(comp.getTGConnectingPointAtIndex(0));
- point = fromStart.getTGConnectingPointP2();
- conn = tad.findTGConnectorStartingAt(comp.getTGConnectingPointAtIndex(1));
- next = conn.getTGConnectingPointP2();
- xpos = fromStart.getX();
- ypos = fromStart.getY();
- TMLADWriteChannel wr = new TMLADWriteChannel(0, 0, 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
- 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];
- 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;
- wr = 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) {
- wr.setChannelName(matches.get(0).getName().replaceAll(title + "__", ""));
- } else {
- wr.setChannelName("nonceCh" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
- }
- //send the nonce along the channel
- wr.setSecurityContext("nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
- tad.addComponent(wr, xpos, ypos + yShift, false, true);
- wr.makeValue();
- TGConnector tmp = new TGConnectorTMLAD(wr.getX(), wr.getY() + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, nonce.getTGConnectingPointAtIndex(1), wr.getTGConnectingPointAtIndex(0), new Vector<Point>());
- tad.addComponent(tmp, xpos, ypos, false, true);
- fromStart = new TGConnectorTMLAD(wr.getX(), wr.getY(), tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, wr.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(wr.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 != wr) {
- tg.setCd(tg.getX(), tg.getY() + yShift);
- }
- }
- }
- //tad.repaint();
-
- //Now add the decrypt operator
- yShift = 40;
- TraceManager.addDev("Securing read channel " + readChannel.getChannelName());
- readChannel.setSecurityContext("autoEncrypt_" + 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();
- tad.addComponent(dec, dec.getX(), dec.getY(), false, true);
- conn.setP2(dec.getTGConnectingPointAtIndex(0));
- yShift += 100;
- 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));
-
- conn.setP2(next);
- tad.addComponent(conn, conn.getX(), conn.getY(), false, true);
- //Shift everything down
- for (TGComponent tg : tad.getComponentList()) {
- if (tg instanceof TMLADReadChannel) {
- readChannel = (TMLADReadChannel) tg;
- 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());
-
- }
- }
- if (tg.getY() > ypos && tg != dec) {
-
- tg.setCd(tg.getX(), tg.getY() + yShift);
- }
- }
-
- tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
-
- tad.repaint();
- }
- }
- }
- GTMLModeling gtm = new GTMLModeling(t, false);
- TMLModeling<TGComponent> newmodel = gtm.translateToTMLModeling(false, false);
- for (TMLTask task : newmodel.getTasks()) {
- task.setName(tabName + "_" + name + "__" + task.getName());
- }
- for (TMLTask task : tmlmodel.getTasks()) {
- HwExecutionNode node = (HwExecutionNode) map.getHwNodeOf(task);
- if (newmodel.getTMLTaskByName(task.getName().replace(tabName, tabName + "_" + name)) != null) {
- map.addTaskToHwExecutionNode(newmodel.getTMLTaskByName(task.getName().replace(tabName, tabName + "_" + name)), node);
- map.removeTask(task);
- } else {
- System.out.println("Can't find " + task.getName());
- }
- }
- //map.setTMLModeling(newmodel);
- //System.out.println(map);
- //TMLMapping newMap = gtm.translateToTMLMapping();
- map.setTMLModeling(newmodel);
- return map;
+
+
+ //move to another thread
+ SecurityGeneration secgen = new SecurityGeneration(gui, name, map, newarch, encComp, overhead, decComp, autoConf, autoWeakAuth, autoStrongAuth);
+ return secgen.startThread();
}
diff --git a/src/main/java/ui/HSMGeneration.java b/src/main/java/ui/HSMGeneration.java
new file mode 100644
index 0000000000000000000000000000000000000000..e081057a123823befab08f2202a9f9675734a276
--- /dev/null
+++ b/src/main/java/ui/HSMGeneration.java
@@ -0,0 +1,996 @@
+package ui;
+/**
+ * Class HSMGeneration
+ * HSM Generation in separate thread
+ * Creation: 1/06/2016
+ *
+ * @author Letitia LI
+ * @version 1.1 5/30/2018
+ */
+
+ import avatartranslator.*;
+import myutil.BoolExpressionEvaluator;
+import myutil.Conversion;
+import myutil.IntExpressionEvaluator;
+import myutil.TraceManager;
+
+import tmltranslator.*;
+import tmltranslator.toavatar.TML2Avatar;
+
+import avatartranslator.*;
+import avatartranslator.toproverif.AVATAR2ProVerif;
+
+
+import launcher.LauncherException;
+import launcher.RemoteExecutionThread;
+import launcher.RshClient;
+
+import ui.tmlad.*;
+import ui.tmlcd.TMLTaskDiagramPanel;
+import ui.tmlcd.TMLTaskOperator;
+import ui.tmlcompd.*;
+import ui.tmlcp.TMLCPPanel;
+import ui.tmldd.*;
+import common.ConfigurationTTool;
+
+import ui.tmlsd.TMLSDPanel;
+
+import proverifspec.ProVerifOutputAnalyzer;
+import proverifspec.ProVerifQueryAuthResult;
+import proverifspec.ProVerifQueryResult;
+import proverifspec.ProVerifSpec;
+
+import java.awt.Point;
+
+import java.util.*;
+import java.io.*;
+
+public class HSMGeneration implements Runnable {
+ MainGUI gui;
+ Map<String, List<String>> selectedCpuTasks;
+
+ AVATAR2ProVerif avatar2proverif;
+ AvatarSpecification avatarspec;
+ ProVerifSpec proverif;
+ TMLMapping<TGComponent> tmap;
+
+ public HSMGeneration(MainGUI gui, Map<String, List<String>> selectedCpuTasks, TMLMapping<TGComponent> tmap){
+ this.gui = gui;
+ this.selectedCpuTasks = selectedCpuTasks;
+ this.tmap = tmap;
+ }
+ public void proverifAnalysis(TMLMapping<TGComponent> map, List<String> nonAuthChans, List<String> nonSecChans) {
+ if (map == null) {
+ TraceManager.addDev("No mapping");
+ return;
+ }
+
+ //Perform ProVerif Analysis
+ TML2Avatar t2a = new TML2Avatar(map, false, true);
+ AvatarSpecification avatarspec = t2a.generateAvatarSpec("1");
+ if (avatarspec == null) {
+ TraceManager.addDev("No avatar spec");
+ return;
+ }
+
+ avatar2proverif = new AVATAR2ProVerif(avatarspec);
+ try {
+ proverif = avatar2proverif.generateProVerif(true, true, 3, true, false);
+ //warnings = avatar2proverif.getWarnings();
+
+ if (!avatar2proverif.saveInFile("pvspec")) {
+ return;
+ }
+
+ RshClient rshc = new RshClient(ConfigurationTTool.ProVerifVerifierHost);
+
+ rshc.setCmd(ConfigurationTTool.ProVerifVerifierPath + " -in pitype pvspec");
+ rshc.sendExecuteCommandRequest();
+ Reader data = rshc.getDataReaderFromProcess();
+
+ ProVerifOutputAnalyzer pvoa = avatar2proverif.getOutputAnalyzer();
+ pvoa.analyzeOutput(data, true);
+ Map<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
+ for (AvatarPragmaSecret pragma : confResults.keySet()) {
+ if (confResults.get(pragma).isProved() && !confResults.get(pragma).isSatisfied()) {
+ nonSecChans.add(pragma.getArg().getBlock().getName() + "__" + pragma.getArg().getName());
+ TraceManager.addDev(pragma.getArg().getBlock().getName() + "." + pragma.getArg().getName() + " is not secret");
+ TMLChannel chan = map.getTMLModeling().getChannelByShortName(pragma.getArg().getName().replaceAll("_chData", ""));
+ for (String block : chan.getTaskNames()) {
+ nonSecChans.add(block + "__" + pragma.getArg().getName());
+ }
+ }
+ }
+ Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authResults = pvoa.getAuthenticityResults();
+ for (AvatarPragmaAuthenticity pragma : authResults.keySet()) {
+ if (authResults.get(pragma).isProved() && !authResults.get(pragma).isSatisfied()) {
+ nonAuthChans.add(pragma.getAttrA().getAttribute().getBlock().getName() + "__" + pragma.getAttrA().getAttribute().getName().replaceAll("_chData", ""));
+ nonAuthChans.add(pragma.getAttrB().getAttribute().getBlock().getName() + "__" + pragma.getAttrB().getAttribute().getName().replaceAll("_chData", ""));
+ }
+ }
+ TraceManager.addDev("nonsecchans " + nonSecChans);
+ TraceManager.addDev("nonauthchans " + nonAuthChans);
+ TraceManager.addDev("all results displayed");
+
+ } catch (Exception e) {
+ System.out.println("ProVerif Analysis Failed " + e);
+ }
+ }
+
+
+ public void startThread(){
+ Thread t = new Thread(this);
+ t.start();
+ try {
+ t.join();
+ }
+ catch (Exception e){
+ TraceManager.addDev("Error in HSM Generation Thread");
+ }
+ return;
+ }
+
+ public void run(){
+ TraceManager.addDev("Adding HSM");
+
+ String encComp = "100";
+ String decComp = "100";
+ String overhead = "0";
+ String name = "hsm";
+ if (tmap == null) {
+ return;
+ }
+ //Clone diagrams
+ TURTLEPanel tmlap = tmap.getCorrespondanceList().getTG(tmap.getArch().getFirstCPU()).getTDiagramPanel().tp;
+ int arch = gui.tabs.indexOf(tmlap);
+ gui.cloneRenameTab(arch, "hsm");
+ TMLArchiPanel newarch = (TMLArchiPanel) gui.tabs.get(gui.tabs.size() - 1);
+
+ TGComponent tgcomp = tmap.getTMLModeling().getTGComponent();
+ TMLComponentDesignPanel tmlcdp = (TMLComponentDesignPanel) tgcomp.getTDiagramPanel().tp;
+
+// TMLComponentDesignPanel tmlcdp = tmap.getTMLCDesignPanel();
+ int ind = gui.tabs.indexOf(tmlcdp);
+ String tabName = gui.getTitleAt(tmlcdp);
+ gui.cloneRenameTab(ind, name);
+ TMLComponentDesignPanel t = (TMLComponentDesignPanel) gui.tabs.get(gui.tabs.size() - 1);
+ TMLComponentTaskDiagramPanel tcdp = t.tmlctdp;
+ //Create clone of architecture panel and map tasks to it
+ newarch.renameMapping(tabName, tabName + "_" + name);
+
+
+ //ProVerif analysis
+ List<String> nonAuthChans = new ArrayList<String>();
+ List<String> nonSecChans = new ArrayList<String>();
+
+ proverifAnalysis(tmap, nonAuthChans, nonSecChans);
+
+ TGConnector fromStart;
+ Map<String, HSMChannel> secChannels = new HashMap<String, HSMChannel>();
+ //Add a HSM 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);
+ //TAttribute isEnc = new TAttribute(2, "isEnc", "true", 4);
+ //hsm.getAttributeList().add(isEnc);
+ 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;
+ }
+ // System.out.println("nonAuthChans " + nonAuthChans);
+ //System.out.println("nonSecChans "+ nonSecChans);
+ for (TMLCPrimitiveComponent comp : comps) {
+
+ Map<String, HSMChannel> compChannels = new HashMap<String, HSMChannel>();
+ String compName = comp.getValue();
+ TMLActivityDiagramPanel tad = t.getTMLActivityDiagramPanel(compName);
+ Set<TGComponent> channelInstances = new HashSet<TGComponent>();
+ Set<TGComponent> secOperators = new HashSet<TGComponent>();
+ // isEnc = new TAttribute(2, "isEnc", "true", 4);
+ //comp.getAttributeList().add(isEnc);
+ //Find all unsecured channels
+ //For previously secured channels, relocate encryption to the hsm
+
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg instanceof TMLADWriteChannel) {
+ TMLADWriteChannel writeChannel = (TMLADWriteChannel) tg;
+ if (writeChannel.getSecurityContext().equals("")) {
+ String nonceName = "";
+ int type = -1;
+ if (nonSecChans.contains(compName + "__" + writeChannel.getChannelName() + "_chData")) {
+ type = HSMChannel.SENC;
+ if (nonAuthChans.contains(compName + "__" + writeChannel.getChannelName())) {
+ nonceName = "nonce_" + writeChannel.getChannelName();
+ }
+ } else if (nonAuthChans.contains(compName + "__" + writeChannel.getChannelName())) {
+ type = HSMChannel.MAC;
+ }
+ HSMChannel ch = new HSMChannel(writeChannel.getChannelName(), compName, type);
+ ch.securityContext = "hsmSec_" + writeChannel.getChannelName();
+ ch.nonceName = nonceName;
+ fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
+ if (fromStart != null) {
+ if (type != -1) {
+ compChannels.put(writeChannel.getChannelName(), ch);
+ channelInstances.add(tg);
+ }
+ }
+ } else {
+ //System.out.println("security context:"+writeChannel.securityContext);
+ fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
+ if (fromStart != null) {
+ channelInstances.add(tg);
+ SecurityPattern sp = tmap.getSecurityPatternByName(writeChannel.getSecurityContext());
+ int type = -1;
+ if (sp.type.equals("Symmetric Encryption")) {
+ type = HSMChannel.SENC;
+ } else if (sp.type.equals("Asymmetric Encryption")) {
+ type = HSMChannel.AENC;
+ } else if (sp.type.equals("MAC")) {
+ type = HSMChannel.MAC;
+ } else if (sp.type.equals("Nonce")) {
+ type = HSMChannel.NONCE;
+ }
+ HSMChannel ch = new HSMChannel(writeChannel.getChannelName(), compName, type);
+ ch.securityContext = writeChannel.getSecurityContext();
+ compChannels.put(writeChannel.getChannelName(), ch);
+ //chanNames.add(writeChannel.getChannelName()+compName);
+ }
+ }
+ }
+ if (tg instanceof TMLADReadChannel) {
+ TMLADReadChannel readChannel = (TMLADReadChannel) tg;
+ if (readChannel.getSecurityContext().equals("")) {
+ fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
+ if (fromStart != null) {
+ if (nonSecChans.contains(compName + "__" + readChannel.getChannelName() + "_chData") || nonAuthChans.contains(compName + "__" + readChannel.getChannelName())) {
+ channelInstances.add(tg);
+ HSMChannel ch = new HSMChannel(readChannel.getChannelName(), compName, HSMChannel.DEC);
+ ch.securityContext = "hsmSec_" + readChannel.getChannelName();
+ compChannels.put(readChannel.getChannelName(), ch);
+ if (nonSecChans.contains(compName + "__" + readChannel.getChannelName() + "_chData") && nonAuthChans.contains(compName + "__" + readChannel.getChannelName())) {
+ ch.nonceName = "nonce_" + readChannel.getChannelName();
+ }
+ }
+ }
+ } else {
+ fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
+ if (fromStart != null) {
+ channelInstances.add(tg);
+ HSMChannel ch = new HSMChannel(readChannel.getChannelName(), compName, HSMChannel.DEC);
+ ch.securityContext = readChannel.getSecurityContext();
+ compChannels.put(readChannel.getChannelName(), ch);
+ }
+ }
+ }
+ if (tg instanceof TMLADEncrypt) {
+ // TMLADEncrypt enc = (TMLADEncrypt) tg;
+ secOperators.add(tg);
+ //}
+ }
+ if (tg instanceof TMLADDecrypt) {
+ // TMLADDecrypt dec = (TMLADDecrypt) tg;
+ secOperators.add(tg);
+ //}
+ }
+ }
+ //System.out.println("compchannels " +compChannels);
+ List<ChannelData> hsmChans = new ArrayList<ChannelData>();
+ ChannelData chd = new ChannelData("startHSM_" + cpuName, false, false);
+ hsmChans.add(chd);
+ for (String s : compChannels.keySet()) {
+ hsmChannels.put(s, compChannels.get(s));
+ chd = new ChannelData("data_" + s + "_" + compChannels.get(s).task, false, true);
+ hsmChans.add(chd);
+ chd = new ChannelData("retData_" + s + "_" + compChannels.get(s).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(2));
+ }
+ 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);
+ }
+ int xpos = 0;
+ int ypos = 0;
+
+ //Remove existing security elements
+ for (TGComponent op : secOperators) {
+ TGConnector prev = tad.findTGConnectorEndingAt(op.getTGConnectingPointAtIndex(0));
+ //TGConnectingPoint point = prev.getTGConnectingPointP1();
+ TGConnector end = tad.findTGConnectorStartingAt(op.getTGConnectingPointAtIndex(1));
+ TGConnectingPoint point2 = end.getTGConnectingPointP2();
+ tad.removeComponent(op);
+ tad.removeComponent(end);
+ tad.addComponent(prev, 0, 0, false, true);
+ prev.setP2(point2);
+ }
+
+ //Modify component activity diagram to add read/write to HSM
+
+ //Add actions before Write Channel
+ for (TGComponent chan : channelInstances) {
+ String chanName = "";
+ if (!(chan instanceof TMLADWriteChannel)) {
+ continue;
+ }
+ TMLADWriteChannel writeChannel = (TMLADWriteChannel) chan;
+ chanName = writeChannel.getChannelName();
+ HSMChannel ch = hsmChannels.get(chanName);
+ writeChannel.setSecurityContext(ch.securityContext);
+ xpos = chan.getX();
+ ypos = chan.getY();
+ fromStart = tad.findTGConnectorEndingAt(chan.getTGConnectingPointAtIndex(0));
+ TGConnectingPoint 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_" + cpuName);
+ // req.setParam(0, "isEnc");
+ 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 + "_" + compName);
+ wr.setSecurityContext(ch.securityContext);
+ 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));
+
+
+ //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 + "_" + compName);
+ rd.setSecurityContext(ch.securityContext);
+ 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 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.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }
+ tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
+ tad.repaint();
+
+ }
+ //Add actions after Read Channel
+ for (TGComponent chan : channelInstances) {
+ String chanName = "";
+ if (!(chan instanceof TMLADReadChannel)) {
+ continue;
+ }
+ TMLADReadChannel readChannel = (TMLADReadChannel) chan;
+ chanName = readChannel.getChannelName();
+ HSMChannel ch = hsmChannels.get(chanName);
+ readChannel.setSecurityContext(ch.securityContext);
+ xpos = chan.getX() + 10;
+ ypos = chan.getY();
+ fromStart = tad.findTGConnectorStartingAt(chan.getTGConnectingPointAtIndex(1));
+ if (fromStart == null) {
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(chan.getTGConnectingPointAtIndex(1));
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+ }
+ 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));
+
+
+ //Add send request operator
+
+ yShift += 50;
+ TMLADSendRequest req = new TMLADSendRequest(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ req.setRequestName("startHSM_" + cpuName);
+ // req.setParam(0, "isEnc");
+ req.makeValue();
+ 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;
+ //Add write channel operator
+ TMLADWriteChannel wr = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ wr.setChannelName("data_" + chanName + "_" + compName);
+ wr.setSecurityContext(ch.securityContext);
+ tad.addComponent(wr, 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(req.getTGConnectingPointAtIndex(1));
+ fromStart.setP2(wr.getTGConnectingPointAtIndex(0));
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+
+ //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 + "_" + compName);
+ rd.setSecurityContext(ch.securityContext);
+ tad.addComponent(rd, xpos, ypos + yShift, 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));
+ fromStart.setP2(rd.getTGConnectingPointAtIndex(0));
+ yShift += 50;
+
+ if (point != null) {
+ 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));
+ //Direct the last TGConnector back to the start of the write channel operator
+
+ fromStart.setP2(point);
+ }
+ yShift += 50;
+
+ //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 != chan) {
+ tg.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }
+ tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
+ tad.repaint();
+ }
+ //for (String chan: chanNames){
+ // hsmChannels.put(chan, compName);
+ //}
+ }
+
+ int xpos = 0;
+ int ypos = 0;
+
+
+ //Build HSM Activity diagram
+
+ TMLActivityDiagramPanel tad = t.getTMLActivityDiagramPanel("HSM_" + cpuName);
+
+ 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, "isEnc");
+ 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(start.getTGConnectingPointAtIndex(0));
+ 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
+ TMLADChoice choice2 = new TMLADChoice(xc, 400, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ if (hsmChannels.keySet().size() > 3) {
+ int i = 0;
+ for (String chan : hsmChannels.keySet()) {
+ HSMChannel ch = hsmChannels.get(chan);
+ 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_" + chan + "_" + hsmChannels.get(chan).task);
+ rd.setSecurityContext(ch.securityContext);
+ 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_" + chan + "_" + hsmChannels.get(chan).task);
+ tad.addComponent(wr, xc, 600, false, true);
+ wr.setSecurityContext(ch.securityContext);
+
+
+ if (hsmChannels.get(chan).secType == HSMChannel.DEC) {
+ TMLADDecrypt dec = new TMLADDecrypt(xc, 500, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ dec.securityContext = ch.securityContext;
+ 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 = ch.securityContext;
+ if (hsmChannels.get(chan).secType == HSMChannel.SENC) {
+ enc.type = "Symmetric Encryption";
+ } else if (hsmChannels.get(chan).secType == HSMChannel.AENC) {
+ enc.type = "Asymmetric Encryption";
+ } else if (hsmChannels.get(chan).secType == HSMChannel.MAC) {
+ enc.type = "MAC";
+ } else if (hsmChannels.get(chan).secType == HSMChannel.NONCE) {
+ enc.type = "Nonce";
+ }
+
+ enc.message_overhead = overhead;
+ enc.encTime = encComp;
+ enc.decTime = decComp;
+ enc.nonce = hsmChannels.get(chan).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 (String chan : hsmChannels.keySet()) {
+ HSMChannel ch = hsmChannels.get(chan);
+ TMLADReadChannel rd = new TMLADReadChannel(xc, 300, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ rd.setChannelName("data_" + chan + "_" + hsmChannels.get(chan).task);
+ rd.setSecurityContext(ch.securityContext);
+ 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, 300, 200, false, true);
+
+ TMLADWriteChannel wr = new TMLADWriteChannel(xc, 600, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ wr.setChannelName("retData_" + chan + "_" + hsmChannels.get(chan).task);
+ tad.addComponent(wr, xc, 600, false, true);
+ wr.setSecurityContext(ch.securityContext);
+
+
+ if (hsmChannels.get(chan).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 = ch.securityContext;
+ 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 = ch.securityContext;
+ if (hsmChannels.get(chan).secType == HSMChannel.SENC) {
+ enc.type = "Symmetric Encryption";
+ } else if (hsmChannels.get(chan).secType == HSMChannel.AENC) {
+ enc.type = "Asymmetric Encryption";
+ } else if (hsmChannels.get(chan).secType == HSMChannel.MAC) {
+ enc.type = "MAC";
+ } else if (hsmChannels.get(chan).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++;
+ }
+
+ }
+
+ secChannels.putAll(hsmChannels);
+ }
+ //For all the tasks that receive encrypted data, decrypt it, assuming it has no associated HSM
+ for (TMLTask task : tmap.getTMLModeling().getTasks()) {
+ int xpos, ypos;
+ //System.out.println("loop 2");
+ TMLActivityDiagramPanel tad = t.getTMLActivityDiagramPanel(task.getName());
+ HashSet<TGComponent> channelInstances = new HashSet<TGComponent>();
+ for (String chan : secChannels.keySet()) {
+ HSMChannel ch = secChannels.get(chan);
+ channelInstances.clear();
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg instanceof TMLADReadChannel) {
+ TMLADReadChannel readChannel = (TMLADReadChannel) tg;
+ if (readChannel.getChannelName().equals(chan) && readChannel.getSecurityContext().equals("")) {
+ fromStart = tad.findTGConnectorStartingAt(tg.getTGConnectingPointAtIndex(1));
+ if (fromStart != null) {
+ channelInstances.add(tg);
+ }
+ }
+ }
+ }
+ for (TGComponent chI : channelInstances) {
+ TMLADReadChannel readChannel = (TMLADReadChannel) chI;
+ readChannel.setSecurityContext(ch.securityContext);
+ xpos = chI.getX();
+ ypos = chI.getY() + 10;
+ fromStart = tad.findTGConnectorStartingAt(chI.getTGConnectingPointAtIndex(1));
+ if (fromStart == null) {
+ fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
+ fromStart.setP1(chI.getTGConnectingPointAtIndex(1));
+ tad.addComponent(fromStart, xpos, ypos, false, true);
+ }
+ TGConnectingPoint point = fromStart.getTGConnectingPointP2();
+ //Add decryption operator
+ int yShift = 100;
+ TMLADDecrypt dec = new TMLADDecrypt(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ dec.securityContext = ch.securityContext;
+ tad.addComponent(dec, xpos, ypos + yShift, false, true);
+
+
+ fromStart.setP2(dec.getTGConnectingPointAtIndex(0));
+ if (point != null) {
+ fromStart = new TGConnectorTMLAD(dec.getX(), dec.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(dec.getTGConnectingPointAtIndex(1));
+
+ //Direct the last TGConnector back to the next action
+
+ 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 != dec) {
+ tg.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }
+ tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
+ tad.repaint();
+
+ }
+ }
+ //Next find channels that send encrypted data, and add the encryption operator
+ for (String chan : secChannels.keySet()) {
+ channelInstances.clear();
+ HSMChannel ch = secChannels.get(chan);
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg instanceof TMLADWriteChannel) {
+ TMLADWriteChannel writeChannel = (TMLADWriteChannel) tg;
+ if (writeChannel.getChannelName().equals(chan) && writeChannel.getSecurityContext().equals("")) {
+ fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
+ if (fromStart != null) {
+ channelInstances.add(tg);
+ }
+ }
+ }
+ }
+ for (TGComponent chI : channelInstances) {
+ TMLADWriteChannel writeChannel = (TMLADWriteChannel) chI;
+ writeChannel.setSecurityContext(ch.securityContext);
+ xpos = chI.getX();
+ ypos = chI.getY() - 10;
+ fromStart = tad.findTGConnectorEndingAt(chI.getTGConnectingPointAtIndex(0));
+ TGConnectingPoint point = fromStart.getTGConnectingPointP2();
+ //Add encryption operator
+ int yShift = 100;
+
+ TMLADEncrypt enc = new TMLADEncrypt(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ tad.addComponent(enc, xpos, ypos, false, true);
+ enc.securityContext = ch.securityContext;
+ enc.type = "Symmetric Encryption";
+ enc.message_overhead = overhead;
+ enc.encTime = encComp;
+ enc.decTime = decComp;
+ enc.size = overhead;
+
+
+ fromStart.setP2(enc.getTGConnectingPointAtIndex(0));
+ fromStart = new TGConnectorTMLAD(enc.getX(), enc.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(enc.getTGConnectingPointAtIndex(1));
+
+ //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 != enc) {
+ tg.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }
+ tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
+ tad.repaint();
+
+ }
+ }
+
+ }
+ for (String cpuName : selectedCpuTasks.keySet()) {
+ //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() + 100, cpu.getY() + 100, archPanel.getMinX(), archPanel.getMaxX(), archPanel.getMinY(), archPanel.getMaxY(), true, null, archPanel);
+ archPanel.addComponent(mem, cpu.getX() + 100, cpu.getY() + 100, 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);
+ }
+ }
+ 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/SecurityGeneration.java b/src/main/java/ui/SecurityGeneration.java
new file mode 100644
index 0000000000000000000000000000000000000000..bceba0449953637596a67a37b1782829b012af5c
--- /dev/null
+++ b/src/main/java/ui/SecurityGeneration.java
@@ -0,0 +1,750 @@
+package ui;
+
+import avatartranslator.*;
+import myutil.BoolExpressionEvaluator;
+import myutil.Conversion;
+import myutil.IntExpressionEvaluator;
+import myutil.TraceManager;
+
+import tmltranslator.*;
+import tmltranslator.toavatar.TML2Avatar;
+
+import avatartranslator.*;
+import avatartranslator.toproverif.AVATAR2ProVerif;
+
+
+import launcher.LauncherException;
+import launcher.RemoteExecutionThread;
+import launcher.RshClient;
+
+import ui.tmlad.*;
+import ui.tmlcd.TMLTaskDiagramPanel;
+import ui.tmlcd.TMLTaskOperator;
+import ui.tmlcompd.*;
+import ui.tmlcp.TMLCPPanel;
+import ui.tmldd.*;
+import common.ConfigurationTTool;
+
+import ui.tmlsd.TMLSDPanel;
+
+import proverifspec.ProVerifOutputAnalyzer;
+import proverifspec.ProVerifQueryAuthResult;
+import proverifspec.ProVerifQueryResult;
+import proverifspec.ProVerifSpec;
+
+import java.awt.Point;
+
+import java.util.*;
+import java.io.*;
+
+
+public class SecurityGeneration implements Runnable {
+ MainGUI gui;
+ String name;
+ TMLMapping<TGComponent> map;
+ TMLArchiPanel newarch;
+ String encComp;
+ String overhead;
+ String decComp;
+ boolean autoConf;
+ boolean autoWeakAuth;
+ boolean autoStrongAuth;
+
+ AVATAR2ProVerif avatar2proverif;
+ AvatarSpecification avatarspec;
+ ProVerifSpec proverif;
+
+
+
+ public SecurityGeneration(MainGUI gui, String name, TMLMapping<TGComponent> map, TMLArchiPanel newarch, String encComp, String overhead, String decComp, boolean autoConf, boolean autoWeakAuth, boolean autoStrongAuth){
+
+ this.gui = gui;
+ this.name=name;
+ this.map=map;
+ this.newarch=newarch;
+ this.encComp = encComp;
+ this.overhead = overhead;
+ this.decComp = decComp;
+ this.autoConf=autoConf;
+ this.autoWeakAuth = autoWeakAuth;
+ this.autoStrongAuth = autoStrongAuth;
+ }
+ public void proverifAnalysis(TMLMapping<TGComponent> map, List<String> nonAuthChans, List<String> nonSecChans) {
+ if (map == null) {
+ TraceManager.addDev("No mapping");
+ return;
+ }
+
+ //Perform ProVerif Analysis
+ TML2Avatar t2a = new TML2Avatar(map, false, true);
+ AvatarSpecification avatarspec = t2a.generateAvatarSpec("1");
+ if (avatarspec == null) {
+ TraceManager.addDev("No avatar spec");
+ return;
+ }
+
+ avatar2proverif = new AVATAR2ProVerif(avatarspec);
+ try {
+ proverif = avatar2proverif.generateProVerif(true, true, 3, true, false);
+ //warnings = avatar2proverif.getWarnings();
+
+ if (!avatar2proverif.saveInFile("pvspec")) {
+ return;
+ }
+
+ RshClient rshc = new RshClient(ConfigurationTTool.ProVerifVerifierHost);
+
+ rshc.setCmd(ConfigurationTTool.ProVerifVerifierPath + " -in pitype pvspec");
+ rshc.sendExecuteCommandRequest();
+ Reader data = rshc.getDataReaderFromProcess();
+
+ ProVerifOutputAnalyzer pvoa = avatar2proverif.getOutputAnalyzer();
+ pvoa.analyzeOutput(data, true);
+ Map<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
+ for (AvatarPragmaSecret pragma : confResults.keySet()) {
+ if (confResults.get(pragma).isProved() && !confResults.get(pragma).isSatisfied()) {
+ nonSecChans.add(pragma.getArg().getBlock().getName() + "__" + pragma.getArg().getName());
+ TraceManager.addDev(pragma.getArg().getBlock().getName() + "." + pragma.getArg().getName() + " is not secret");
+ TMLChannel chan = map.getTMLModeling().getChannelByShortName(pragma.getArg().getName().replaceAll("_chData", ""));
+ for (String block : chan.getTaskNames()) {
+ nonSecChans.add(block + "__" + pragma.getArg().getName());
+ }
+ }
+ }
+ Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authResults = pvoa.getAuthenticityResults();
+ for (AvatarPragmaAuthenticity pragma : authResults.keySet()) {
+ if (authResults.get(pragma).isProved() && !authResults.get(pragma).isSatisfied()) {
+ nonAuthChans.add(pragma.getAttrA().getAttribute().getBlock().getName() + "__" + pragma.getAttrA().getAttribute().getName().replaceAll("_chData", ""));
+ nonAuthChans.add(pragma.getAttrB().getAttribute().getBlock().getName() + "__" + pragma.getAttrB().getAttribute().getName().replaceAll("_chData", ""));
+ }
+ }
+ TraceManager.addDev("nonsecchans " + nonSecChans);
+ TraceManager.addDev("nonauthchans " + nonAuthChans);
+ TraceManager.addDev("all results displayed");
+
+ } catch (Exception e) {
+ System.out.println("ProVerif Analysis Failed " + e);
+ }
+ }
+
+ public TMLMapping<TGComponent> startThread(){
+ Thread t = new Thread(this);
+ t.start();
+ try {
+ t.join();
+ }
+ catch (Exception e){
+ TraceManager.addDev("Error in Security Generation Thread");
+ }
+ return map;
+ }
+ public void run(){
+
+ Map<TMLTask, List<TMLTask>> toSecure = new HashMap<TMLTask, List<TMLTask>>();
+ Map<TMLTask, List<TMLTask>> toSecureRev = new HashMap<TMLTask, List<TMLTask>>();
+ Map<TMLTask, List<String>> secOutChannels = new HashMap<TMLTask, List<String>>();
+ Map<TMLTask, List<String>> secInChannels = new HashMap<TMLTask, List<String>>();
+ Map<TMLTask, List<String>> nonceOutChannels = new HashMap<TMLTask, List<String>>();
+ 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());
+ List<String> nonAuthChans = new ArrayList<String>();
+ List<String> nonSecChans = new ArrayList<String>();
+
+ proverifAnalysis(map, nonAuthChans, nonSecChans);
+
+ TMLModeling<TGComponent> tmlmodel = map.getTMLModeling();
+ List<TMLChannel> channels = tmlmodel.getChannels();
+ for (TMLChannel channel : channels) {
+ for (TMLCPrimitivePort p : channel.ports) {
+ channel.checkConf = channel.checkConf || p.checkConf;
+ channel.checkAuth = channel.checkAuth || p.checkAuth;
+ }
+ }
+
+ //Create clone of Component Diagram + Activity diagrams to secure
+ TGComponent tgcomp = map.getTMLModeling().getTGComponent();
+ TMLComponentDesignPanel tmlcdp = (TMLComponentDesignPanel) tgcomp.getTDiagramPanel().tp;
+// TMLComponentDesignPanel tmlcdp = map.getTMLCDesignPanel();
+ int ind = gui.tabs.indexOf(tmlcdp);
+ if (ind == -1) {
+ TraceManager.addDev("No Component Design Panel");
+ return;
+ }
+ String tabName = gui.getTitleAt(tmlcdp);
+ gui.cloneRenameTab(ind, name);
+ TMLComponentDesignPanel t = (TMLComponentDesignPanel) gui.tabs.get(gui.tabs.size() - 1);
+
+ TMLComponentTaskDiagramPanel tcdp = t.tmlctdp;
+ //Create clone of architecture panel and map tasks to it
+ newarch.renameMapping(tabName, tabName + "_" + name);
+
+ for (TMLTask task : map.getTMLModeling().getTasks()) {
+ List<String> tmp = new ArrayList<String>();
+ List<String> tmp2 = new ArrayList<String>();
+ List<TMLTask> tmp3 = new ArrayList<TMLTask>();
+ List<TMLTask> tmp4 = new ArrayList<TMLTask>();
+ List<String> tmp5 = new ArrayList<String>();
+ List<String> tmp6 = new ArrayList<String>();
+ List<String> tmp7 = new ArrayList<String>();
+ 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);
+ toSecureRev.put(task, tmp4);
+ nonceInChannels.put(task, tmp5);
+ nonceOutChannels.put(task, tmp6);
+ macInChannels.put(task, tmp7);
+ macOutChannels.put(task, tmp8);
+ macNonceOutChannels.put(task, tmp9);
+ macNonceInChannels.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());
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg instanceof TMLADWriteChannel) {
+ TMLADWriteChannel writeChannel = (TMLADWriteChannel) tg;
+ if (writeChannel.getSecurityContext().equals("")) {
+
+ TMLChannel chan = tmlmodel.getChannelByName(tabName + "__" + writeChannel.getChannelName());
+ //System.out.println("channel " + chan);
+ if (chan != null) {
+ if (chan.checkConf && autoConf) {
+ // System.out.println(chan.getOriginTask().getName().split("__")[1]);
+ 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());
+ }
+ }
+ } 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());
+ }
+ }
+
+ }
+ }
+ }
+ }
+ }
+ }
+ TraceManager.addDev("macoutchans " + macOutChannels);
+ TraceManager.addDev("macinchans " + macInChannels);
+ TraceManager.addDev("nonsecin " + secInChannels);
+ TraceManager.addDev("nonsecout " + secOutChannels);
+ TraceManager.addDev("noncein " + nonceInChannels);
+ TraceManager.addDev("nonceout " + nonceOutChannels);
+
+ // System.out.println(secOutChanannels.toString());
+ // 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);
+
+ for (TMLTask task2 : toSecureRev.get(task)) {
+ boolean addChan = true;
+ for (TMLChannel chan : chans) {
+ if (chan.getDestinationTask() == task2) {
+ addChan = false;
+ }
+ }
+
+ if (addChan) {
+ TMLCChannelOutPort originPort = new TMLCChannelOutPort(0, 0, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, null, tcdp);
+ TMLCChannelOutPort destPort = new TMLCChannelOutPort(0, 0, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, null, tcdp);
+ for (TGComponent tg : tcdp.getComponentList()) {
+ if (tg instanceof TMLCPrimitiveComponent) {
+ if (tg.getValue().equals(task.getName().split("__")[1])) {
+ originPort = new TMLCChannelOutPort(tg.getX(), tg.getY(), tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, tg, tcdp);
+ originPort.commName = "nonceCh" + task.getName().split("__")[1] + "_" + task2.getName().split("__")[1];
+ tcdp.addComponent(originPort, tg.getX(), tg.getY(), true, true);
+ } else if (tg.getValue().equals(task2.getName().split("__")[1])) {
+ destPort = new TMLCChannelOutPort(tg.getX(), tg.getY(), tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, tg, tcdp);
+ destPort.isOrigin = false;
+ destPort.commName = "nonceCh" + task.getName().split("__")[1] + "_" + task2.getName().split("__")[1];
+ tcdp.addComponent(destPort, tg.getX(), tg.getY(), true, true);
+ }
+ }
+ else if (tg instanceof TMLCCompositeComponent){
+ for (TGComponent internalComp: tg.getRecursiveAllInternalComponent()){
+ if (internalComp instanceof TMLCPrimitiveComponent){
+ if (internalComp.getValue().equals(task.getName().split("__")[1])) {
+ originPort = new TMLCChannelOutPort(internalComp.getX(), internalComp.getY(), tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, internalComp, tcdp);
+ originPort.commName = "nonceCh" + task.getName().split("__")[1] + "_" + task2.getName().split("__")[1];
+ tcdp.addComponent(originPort, internalComp.getX(), internalComp.getY(), true, true);
+ } else if (internalComp.getValue().equals(task2.getName().split("__")[1])) {
+ destPort = new TMLCChannelOutPort(internalComp.getX(), internalComp.getY(), tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, internalComp, tcdp);
+ destPort.isOrigin = false;
+ destPort.commName = "nonceCh" + task.getName().split("__")[1] + "_" + task2.getName().split("__")[1];
+ tcdp.addComponent(destPort, internalComp.getX(), internalComp.getY(), true, true);
+ }
+ }
+ }
+ }
+ }
+ tmlmodel.addChannel(new TMLChannel("nonceCh" + task.getName().split("__")[1] + "_" + task2.getName().split("__")[1], originPort));
+ //Add connection
+ 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);
+ }
+ }
+ }
+ // }
+ //Add encryption/nonces to activity diagram
+ for (TMLTask task : toSecure.keySet()) {
+ String title = task.getName().split("__")[0];
+ TraceManager.addDev("Securing task " + task.getName());
+ TMLActivityDiagramPanel tad = t.getTMLActivityDiagramPanel(task.getName());
+ //Get start state position, shift everything down
+ int xpos = 0;
+ int ypos = 0;
+ TGConnector fromStart = new TGConnectorTMLAD(0, 0, 0, 0, 0, 0, false, null, tad, null, null, new Vector<Point>());
+ TGConnectingPoint point = new TGConnectingPoint(null, 0, 0, false, false);
+ //Find states immediately before the write channel operator
+
+ //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;
+ TMLChannel tmlc = tmlmodel.getChannelByName(title + "__" + channel);
+ //First, find the connector that points to it. We will add the encryption, nonce operators directly before the write channel operator
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg instanceof TMLADWriteChannel) {
+ TMLADWriteChannel writeChannel = (TMLADWriteChannel) tg;
+ if (writeChannel.getChannelName().equals(channel) && writeChannel.getSecurityContext().equals("")) {
+
+ if (fromStart != null) {
+ channelInstances.add(tg);
+ }
+ }
+ }
+ }
+ for (TGComponent comp : channelInstances) {
+ //TMLADWriteChannel writeChannel = (TMLADWriteChannel) comp;
+ xpos = comp.getX();
+ ypos = comp.getY();
+ fromStart = tad.findTGConnectorEndingAt(comp.getTGConnectingPointAtIndex(0));
+ point = fromStart.getTGConnectingPointP2();
+ //Add encryption operator
+ TMLADEncrypt enc = new TMLADEncrypt(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ TMLADReadChannel rd = new TMLADReadChannel(0, 0, 0, 0, 0, 0, false, null, tad);
+ 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());
+
+ 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(enc.getX(), enc.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));
+ yShift += 60;
+ //Move encryption operator after receive nonce component
+ enc.setCd(xpos, ypos + yShift);
+ if (tmlc != null) {
+ enc.nonce = "nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1];
+ }
+ }
+
+ enc.securityContext = "autoEncrypt_" + channel;
+ enc.type = "Symmetric Encryption";
+ enc.message_overhead = overhead;
+ enc.encTime = encComp;
+ enc.decTime = decComp;
+ tad.addComponent(enc, xpos, ypos + yShift, false, true);
+ yShift += 60;
+ fromStart.setP2(enc.getTGConnectingPointAtIndex(0));
+ fromStart = new TGConnectorTMLAD(enc.getX(), enc.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(enc.getTGConnectingPointAtIndex(1));
+
+ //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 instanceof TMLADWriteChannel) {
+ TMLADWriteChannel wChannel = (TMLADWriteChannel) tg;
+ 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());
+
+ }
+ }
+ if (tg.getY() >= ypos && tg != enc && tg != rd) {
+ tg.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }
+ tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
+ tad.repaint();
+ }
+ }
+
+ for (String channel : macOutChannels.get(task)) {
+ //Add MAC before writechannel
+ int yShift = 50;
+ TMLChannel tmlc = tmlmodel.getChannelByName(title + "__" + channel);
+ //First, find the connector that points to it. We will add the encryption, nonce operators directly before the write channel operator
+ Set<TGComponent> channelInstances = new HashSet<TGComponent>();
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg instanceof TMLADWriteChannel) {
+ TMLADWriteChannel writeChannel = (TMLADWriteChannel) tg;
+ if (writeChannel.getChannelName().equals(channel) && writeChannel.getSecurityContext().equals("")) {
+ xpos = tg.getX();
+ ypos = tg.getY();
+ fromStart = tad.findTGConnectorEndingAt(tg.getTGConnectingPointAtIndex(0));
+ if (fromStart != null) {
+ channelInstances.add(tg);
+ }
+ }
+ }
+ }
+ for (TGComponent comp : channelInstances) {
+ //TMLADWriteChannel writeChannel = (TMLADWriteChannel) comp;
+ xpos = comp.getX();
+ ypos = comp.getY();
+ fromStart = tad.findTGConnectorEndingAt(comp.getTGConnectingPointAtIndex(0));
+ point = fromStart.getTGConnectingPointP2();
+
+ TMLADEncrypt enc = new TMLADEncrypt(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+
+ //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)) {
+ //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());
+
+ 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(enc.getX(), enc.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));
+ yShift += 60;
+ //Move encryption operator after receive nonce component
+ enc.setCd(xpos, ypos + yShift);
+ if (tmlc != null) {
+ enc.nonce = "nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1];
+ }
+ }
+
+ //Add encryption operator
+
+ enc.securityContext = "autoEncrypt_" + channel;
+ enc.type = "MAC";
+ enc.message_overhead = overhead;
+ enc.encTime = encComp;
+ enc.decTime = decComp;
+ enc.size = overhead;
+ tad.addComponent(enc, xpos, ypos + yShift, false, true);
+ yShift += 60;
+ fromStart.setP2(enc.getTGConnectingPointAtIndex(0));
+ fromStart = new TGConnectorTMLAD(enc.getX(), enc.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(enc.getTGConnectingPointAtIndex(1));
+
+ //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 instanceof TMLADWriteChannel) {
+ TMLADWriteChannel wChannel = (TMLADWriteChannel) tg;
+ 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());
+ tad.repaint();
+ }
+ }
+ if (tg.getY() >= ypos && tg != enc && tg != rd) {
+ tg.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }
+ tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
+ }
+ }
+ for (String channel : macInChannels.get(task)) {
+ //Add decryptmac after readchannel
+ int yShift = 50;
+ 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);
+ //Find read channel operator
+
+ 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 comp : channelInstances) {
+
+ fromStart = tad.findTGConnectorEndingAt(comp.getTGConnectingPointAtIndex(0));
+ point = fromStart.getTGConnectingPointP2();
+ conn = tad.findTGConnectorStartingAt(comp.getTGConnectingPointAtIndex(1));
+ next = conn.getTGConnectingPointP2();
+ xpos = fromStart.getX();
+ ypos = fromStart.getY();
+
+
+ TMLADReadChannel readChannel = (TMLADReadChannel) comp;
+ TraceManager.addDev("Securing read channel " + readChannel.getChannelName());
+ readChannel.setSecurityContext("autoEncrypt_" + 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)) {
+ //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];
+ 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;
+ wr = 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) {
+ wr.setChannelName(matches.get(0).getName().replaceAll(title + "__", ""));
+ } else {
+ wr.setChannelName("nonceCh" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
+ }
+ //send the nonce along the channel
+ wr.setSecurityContext("nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
+ tad.addComponent(wr, xpos, ypos + yShift, false, true);
+ wr.makeValue();
+ TGConnector tmp = new TGConnectorTMLAD(wr.getX(), wr.getY() + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, nonce.getTGConnectingPointAtIndex(1), wr.getTGConnectingPointAtIndex(0), new Vector<Point>());
+ tad.addComponent(tmp, xpos, ypos, false, true);
+ fromStart = new TGConnectorTMLAD(wr.getX(), wr.getY(), tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, wr.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(wr.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 != wr) {
+ tg.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }
+ }
+
+ //Add decryption operator if it does not already exist
+ xpos = conn.getX();
+ 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();
+ tad.addComponent(dec, dec.getX(), dec.getY(), false, true);
+ conn.setP2(dec.getTGConnectingPointAtIndex(0));
+ 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));
+ conn.setP2(next);
+ tad.addComponent(conn, conn.getX(), conn.getY(), false, true);
+ //Shift everything down
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg instanceof TMLADReadChannel) {
+ readChannel = (TMLADReadChannel) tg;
+ 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());
+
+ }
+ }
+ if (tg.getY() > ypos && tg != dec && tg != comp) {
+
+ tg.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }
+
+
+ tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
+ tad.repaint();
+ }
+ }
+ for (String channel : secInChannels.get(task)) {
+ TraceManager.addDev("securing channel " + channel);
+ int yShift = 20;
+ // String title = task.getName().split("__")[0];
+ TMLChannel tmlc = tmlmodel.getChannelByName(title + "__" + channel);
+ 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);
+ //Find read channel operator
+ TMLADReadChannel readChannel = new TMLADReadChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ HashSet<TGComponent> channelInstances = new HashSet<TGComponent>();
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg instanceof 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 comp : channelInstances) {
+
+ fromStart = tad.findTGConnectorEndingAt(comp.getTGConnectingPointAtIndex(0));
+ point = fromStart.getTGConnectingPointP2();
+ conn = tad.findTGConnectorStartingAt(comp.getTGConnectingPointAtIndex(1));
+ next = conn.getTGConnectingPointP2();
+ xpos = fromStart.getX();
+ ypos = fromStart.getY();
+ TMLADWriteChannel wr = new TMLADWriteChannel(0, 0, 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
+ 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];
+ 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;
+ wr = 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) {
+ wr.setChannelName(matches.get(0).getName().replaceAll(title + "__", ""));
+ } else {
+ wr.setChannelName("nonceCh" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
+ }
+ //send the nonce along the channel
+ wr.setSecurityContext("nonce_" + tmlc.getDestinationTask().getName().split("__")[1] + "_" + tmlc.getOriginTask().getName().split("__")[1]);
+ tad.addComponent(wr, xpos, ypos + yShift, false, true);
+ wr.makeValue();
+ TGConnector tmp = new TGConnectorTMLAD(wr.getX(), wr.getY() + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, nonce.getTGConnectingPointAtIndex(1), wr.getTGConnectingPointAtIndex(0), new Vector<Point>());
+ tad.addComponent(tmp, xpos, ypos, false, true);
+ fromStart = new TGConnectorTMLAD(wr.getX(), wr.getY(), tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, wr.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(wr.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 != wr) {
+ tg.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }
+ }
+ //tad.repaint();
+
+ //Now add the decrypt operator
+ yShift = 40;
+ TraceManager.addDev("Securing read channel " + readChannel.getChannelName());
+ readChannel.setSecurityContext("autoEncrypt_" + 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();
+ tad.addComponent(dec, dec.getX(), dec.getY(), false, true);
+ conn.setP2(dec.getTGConnectingPointAtIndex(0));
+ yShift += 100;
+ 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));
+
+ conn.setP2(next);
+ tad.addComponent(conn, conn.getX(), conn.getY(), false, true);
+ //Shift everything down
+ for (TGComponent tg : tad.getComponentList()) {
+ if (tg instanceof TMLADReadChannel) {
+ readChannel = (TMLADReadChannel) tg;
+ 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());
+
+ }
+ }
+ if (tg.getY() > ypos && tg != dec) {
+
+ tg.setCd(tg.getX(), tg.getY() + yShift);
+ }
+ }
+
+ tad.setMaxPanelSize(tad.getMaxX(), tad.getMaxY() + yShift);
+
+ tad.repaint();
+ }
+ }
+ }
+ GTMLModeling gtm = new GTMLModeling(t, false);
+ TMLModeling<TGComponent> newmodel = gtm.translateToTMLModeling(false, false);
+ for (TMLTask task : newmodel.getTasks()) {
+ task.setName(tabName + "_" + name + "__" + task.getName());
+ }
+ for (TMLTask task : tmlmodel.getTasks()) {
+ HwExecutionNode node = (HwExecutionNode) map.getHwNodeOf(task);
+ if (newmodel.getTMLTaskByName(task.getName().replace(tabName, tabName + "_" + name)) != null) {
+ map.addTaskToHwExecutionNode(newmodel.getTMLTaskByName(task.getName().replace(tabName, tabName + "_" + name)), node);
+ map.removeTask(task);
+ } else {
+ System.out.println("Can't find " + task.getName());
+ }
+ }
+ //map.setTMLModeling(newmodel);
+ //System.out.println(map);
+ //TMLMapping newMap = gtm.translateToTMLMapping();
+ map.setTMLModeling(newmodel);
+ return;
+ }
+}
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 1c1615bb1dd98eb2ae28ce5ed9ac16cc32beb3db..4d9cd7e0196717744f759522d6d565336a90ae35 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -1109,4 +1109,6 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
this.repaint();
this.revalidate();
}
+
+
}