diff --git a/src/avatartranslator/AvatarTermFunction.java b/src/avatartranslator/AvatarTermFunction.java index 6f585ddccf726ac00598bc0b58aef5feba4c6f3d..be1b04ed833ff624c03b79284fc5b8d0da18c532 100644 --- a/src/avatartranslator/AvatarTermFunction.java +++ b/src/avatartranslator/AvatarTermFunction.java @@ -75,11 +75,12 @@ public class AvatarTermFunction extends AvatarTerm implements AvatarAction { } AvatarMethod meth = block.getAvatarMethodWithName (methodName); - if (meth != null && argsTuple != null && meth.getListOfAttributes ().size () == argsTuple.getComponents ().size ()) + if (meth != null && argsTuple != null && meth.getListOfAttributes ().size () == argsTuple.getComponents ().size ()){ // Method was found and the arguments provided are correct + TraceManager.addDev ("Function call '" + toParse + "' added parsed"); return new AvatarTermFunction (meth, argsTuple, block); - - //TraceManager.addDev ("Function call '" + toParse + "' couldn't be parsed"); +} + TraceManager.addDev ("Function call '" + toParse + "' couldn't be parsed"); return null; } diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java index 3a25bb590e50190c3ce3391ecacef6272175d374..551b228ff3e62e5ec05994523f71a61af61675da 100755 --- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java +++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java @@ -1156,10 +1156,12 @@ public class AVATAR2ProVerif implements AvatarTranslator { } else // Else use the function as is proVerifRightHand = AVATAR2ProVerif.translateTerm (rightHand, arg.attributeCmp); - } else + System.out.println("right hand "+ proVerifRightHand); + } else { // If it's not a function, use it as is proVerifRightHand = AVATAR2ProVerif.translateTerm (rightHand, arg.attributeCmp); - + System.out.println(" not right hand "+ proVerifRightHand); + } // Compute left hand part of the assignment LinkedList<ProVerifVar> proVerifLeftHand = new LinkedList<ProVerifVar> (); if (proVerifRightHand != null) { diff --git a/src/tmltranslator/TMLMapping.java b/src/tmltranslator/TMLMapping.java index 30b8042b3b17d1a4f49cdd56408bcbe0eabce25b..127ae3fc83e09bddef876871cddf8241ce081ea6 100755 --- a/src/tmltranslator/TMLMapping.java +++ b/src/tmltranslator/TMLMapping.java @@ -56,6 +56,7 @@ public class TMLMapping { private TMLModeling tmlm; private TMLArchitecture tmla; private TMLCP tmlcp; +public List<String> securityPatterns = new ArrayList<String>(); private ArrayList<HwExecutionNode> onnodes; private ArrayList<TMLTask> mappedtasks; diff --git a/src/tmltranslator/TMLModeling.java b/src/tmltranslator/TMLModeling.java index ea27efa40f70183cbbfa94c209f2eec62691032c..9901579b649ad6cdb04eb706b6faeb99874f2774 100755 --- a/src/tmltranslator/TMLModeling.java +++ b/src/tmltranslator/TMLModeling.java @@ -61,7 +61,7 @@ public class TMLModeling { private ArrayList<TMLRequest> requests; private ArrayList<TMLEvent> events; private ArrayList<String[]> pragmas; - public ArrayList<SecurityPattern> securityPatterns; + public ArrayList<String> securityPatterns=new ArrayList<String>(); private TMLElement correspondance[]; private boolean optimized = false; @@ -1054,6 +1054,9 @@ public class TMLModeling { tasks.add(task); } } + for (String s: tmlm.securityPatterns){ + securityPatterns.add(s); + } } diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java index 5eb4cf1f73f7e10de7d48a580572935a15f4f491..9efd4ff302cbbc4c101b9df2418cb5595b7c1eb1 100644 --- a/src/tmltranslator/toavatar/TML2Avatar.java +++ b/src/tmltranslator/toavatar/TML2Avatar.java @@ -654,7 +654,13 @@ public class TML2Avatar { secPatterns.add(ae.securityPattern); block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null)); block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null)); - tran.addAction(ae.securityPattern.name+"_encrypted= sencrypt("+ae.securityPattern.name+", key)"); + + AvatarMethod sencrypt = new AvatarMethod("sencrypt", ae); + sencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name)); + sencrypt.addParameter(block.getAvatarAttributeWithName("key")); + block.addMethod(sencrypt); + tran.addAction(ae.securityPattern.name+"_encrypted = sencrypt("+ae.securityPattern.name+", key)"); + System.out.println("ADDING ACTION ENCRYPT"); System.out.println("Found security pattern "+ae.securityPattern.name); ae.securityPattern.originTask=block.getName(); ae.securityPattern.state1=as; @@ -667,12 +673,27 @@ public class TML2Avatar { else if (ae.securityPattern!=null && ae.getName().contains("decrypt")){ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null)); block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null)); - tran.addAction(ae.securityPattern.name+"= sdecrypt("+ae.securityPattern.name+"_encrypted,key)"); + + + AvatarMethod sdecrypt = new AvatarMethod("sdecrypt", ae); + sdecrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name)); + sdecrypt.addParameter(block.getAvatarAttributeWithName("key")); + block.addMethod(sdecrypt); + + + tran.addAction(ae.securityPattern.name+" = sdecrypt("+ae.securityPattern.name+"_encrypted, key)"); + + + + System.out.println("ADDING ACTION DECRYPT"); ae.securityPattern.state2=as; System.out.println("Found security pattern decrypt "+ae.securityPattern.name); elementList.add(as); elementList.add(tran); + as.addNext(tran); + + AvatarState dummy = new AvatarState(ae.getName()+"_dummy", ae.getReferenceObject()); tran.addNext(dummy); tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject()); @@ -718,7 +739,7 @@ public class TML2Avatar { AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject()); if (ae.securityPattern!=null){ - System.out.println("has security pattern" + ae.securityPattern.name); + System.out.println(block.getName() + " readchannel has security pattern" + ae.securityPattern.name); as.addValue(ae.securityPattern.name+"_encrypted"); AvatarAttribute data= new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null); block.addAttribute(data); @@ -752,10 +773,7 @@ public class TML2Avatar { } } else { - //Write Channel - if (ae.securityPattern!=null){ - System.out.println("has security pattern "+ae.securityPattern.name); - } + //WriteChannel if (!signalMap.containsKey(block.getName()+"__OUT__"+ch.getName())){ sig = new AvatarSignal(block.getName()+"__OUT__"+ch.getName(), AvatarSignal.OUT, ch.getReferenceObject()); signals.add(sig); @@ -788,7 +806,7 @@ public class TML2Avatar { AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject()); if (ae.securityPattern!=null){ - System.out.println("has security pattern" + ae.securityPattern.name); + System.out.println(block.getName() + " writechannel has security pattern" + ae.securityPattern.name); as.addValue(ae.securityPattern.name+"_encrypted"); AvatarAttribute data= new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null); block.addAttribute(data); @@ -1022,7 +1040,20 @@ public class TML2Avatar { ArrayList<TMLTask> tasks = tmlmap.getTMLModeling().getTasks(); for (TMLTask task:tasks){ + + + + AvatarBlock block = new AvatarBlock(task.getName(), avspec, task.getReferenceObject()); + + tmlmap.getTMLModeling().securityPatterns.add("enc"); + for (String s:tmlmap.getTMLModeling().securityPatterns){ + System.out.println("Adding attr security pattern " + s); + AvatarAttribute tmp = new AvatarAttribute(s, AvatarType.INTEGER, block, null); + block.addAttribute(tmp); + tmp = new AvatarAttribute(s+"_encrypted", AvatarType.INTEGER, block, null); + block.addAttribute(tmp); + } taskBlockMap.put(task, block); //Add temp variable for unsendable signals AvatarAttribute tmp = new AvatarAttribute("tmp", AvatarType.INTEGER, block, null); @@ -1368,7 +1399,7 @@ public class TML2Avatar { } } //Check if we matched up all signals - System.out.println(avspec); + //System.out.println(avspec); return avspec; diff --git a/src/ui/GTMLModeling.java b/src/ui/GTMLModeling.java index 206f4e493e636e47ff2c9c4db169a0d09aa878f0..b4ce6a21f554a0e79d2817cc52d8436695b60814 100755 --- a/src/ui/GTMLModeling.java +++ b/src/ui/GTMLModeling.java @@ -2108,9 +2108,11 @@ public class GTMLModeling { if (!makeTMLModeling()) { return null; } + System.out.println("security patterns " + tmlm.securityPatterns); TraceManager.addDev("Making mapping"); makeMapping(); //fills map - +// map.securityPatterns.addAll(securityPatterns.keySet()); + System.out.println("security patterns " + securityPatterns); TraceManager.addDev("Making TMLCPLib"); makeTMLCPLib(); diff --git a/src/ui/tmlad/TMLADDecrypt.java b/src/ui/tmlad/TMLADDecrypt.java index cb56ac3713f95734077c25e00cc0613060399e38..4b99ae3a198a0db98c88af4004624fb24b2c9aa6 100755 --- a/src/ui/tmlad/TMLADDecrypt.java +++ b/src/ui/tmlad/TMLADDecrypt.java @@ -189,7 +189,7 @@ public boolean editOndoubleClick(JFrame frame) { elt = (Element) n2; if (elt.getTagName().equals("Data")) { securityContext = elt.getAttribute("secPattern"); - securityContext = elt.getAttribute("calcTime"); + calculationTime = elt.getAttribute("calcTime"); //System.out.println("eventName=" +eventName + " variable=" + result); } } diff --git a/src/ui/tmldd/TMLArchiBUSNode.java b/src/ui/tmldd/TMLArchiBUSNode.java index f567f9deb7e23f59b6baf52089727ad1fe634586..0980f74eb1755c85989e98a186516d1f94a6e692 100755 --- a/src/ui/tmldd/TMLArchiBUSNode.java +++ b/src/ui/tmldd/TMLArchiBUSNode.java @@ -155,16 +155,16 @@ public class TMLArchiBUSNode extends TMLArchiCommunicationNode implements Swallo } else { - int[] xps = new int[]{x+4, x+9, x+13, x+17, x+22, x+22, x+13, x+4}; - int[] yps = new int[]{y+20, y+20, y+15, y+20, y+20, y+35, y+43, y+35}; + int[] xps = new int[]{x+4, x+7, x+10, x+13, x+16, x+19, x+22, x+22, x+13, x+4}; + int[] yps = new int[]{y+18, y+22, y+22, y+18, y+22, y+22,y+18, y+35, y+43, y+35}; g.setColor(Color.green); - g.fillPolygon(xps, yps,8); + g.fillPolygon(xps, yps,10); // g.drawOval(x+6, y+19, 12, 18); // g.fillRect(x+4, y+25, 18, 14); g.setColor(c); - g.drawPolygon(xps, yps,8); + g.drawPolygon(xps, yps,10); // g.drawRect(x+4, y+25, 18, 14); } }