tml2proveriftranslation

src/tmltranslator/toproverif/TML2ProVerif.java

@@ -47,7 +47,9 @@ package tmltranslator.toproverif;
 
 import java.util.LinkedList;
 import java.util.ArrayList;
+import java.util.List;
 import java.util.HashMap;
+import java.util.Map;
 import java.util.HashSet;
 import java.util.Vector;
 import java.io.*;
@@ -95,13 +97,16 @@ public class TML2ProVerif {
     private final static String CHCTRL_CH = "chControl";
     private final static String CHCTRL_ENCRYPT = "chControlEnc";
     private final static String CHCTRL_DECRYPT = "chControlDec";
-
+    private final static Integer channelPublic = 0;
+    private final static Integer channelPrivate = 1;
+    private final static Integer channelUnreachable = 2;
     private ProVerifSpec spec;
     private TMLMapping tmlmap;
     private TMLModeling tmlmodel;
     private boolean stateReachability;
 
     private Vector warnings;
+    public HashMap<String, Integer> channelMap = new HashMap<String,Integer>();
 
     public TML2ProVerif(TMLMapping _tmlmap) {
         this.tmlmap = _tmlmap;
@@ -109,6 +114,97 @@ public class TML2ProVerif {
 	this.tmlmodel= tmlmap.getTMLModeling();
     }
 
+
+    public void checkChannels(){
+	ArrayList<TMLChannel> channels = tmlmodel.getChannels();
+	List<TMLTask> destinations = new ArrayList<TMLTask>();
+	TMLTask a; 
+	for (TMLChannel channel: channels){	
+	    destinations.clear();
+	    if (channel.isBasicChannel()){
+	        a = channel.getOriginTask();
+		destinations.add(channel.getDestinationTask());
+	    }
+	    else {
+		a=channel.getOriginTasks().get(0);
+		destinations.addAll(channel.getDestinationTasks());
+	    }  
+	    HwCPU node1 = (HwCPU) tmlmap.getHwNodeOf(a);
+	    for (TMLTask t: destinations){
+	        List<HwBus> buses = new ArrayList<HwBus>();
+		HwNode node2 = tmlmap.getHwNodeOf(t);
+		if (node1==node2){
+		    System.out.println("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is confidential");
+		    channelMap.put(channel.getName(), channelPrivate);
+		}
+		if (node1!=node2){
+		    //Navigate architecture for node
+		    List<HwLink> links = tmlmap.getTMLArchitecture().getHwLinks();
+		    HwNode last = node1;
+		    List<HwNode> found = new ArrayList<HwNode>();	
+		    List<HwNode> done = new ArrayList<HwNode>();
+		    List<HwNode> path = new ArrayList<HwNode>();
+		    Map<HwNode, List<HwNode>> pathMap = new HashMap<HwNode, List<HwNode>>();
+		    for (HwLink link: links){
+			if (link.hwnode == node1){
+			    found.add(link.bus);
+			    List<HwNode> tmp = new ArrayList<HwNode>();
+			    tmp.add(link.bus);
+			    pathMap.put(link.bus, tmp);
+			}
+		    }
+		    outerloop:
+		        while (found.size()>0){
+			    HwNode curr = found.remove(0);
+			    for (HwLink link: links){
+			        if (curr == link.bus){
+			    	    if (link.hwnode == node2){
+			      		path = pathMap.get(curr);
+			      		break outerloop;
+			    	    }
+			    	    if (!done.contains(link.hwnode) && !found.contains(link.hwnode) && link.hwnode instanceof HwBridge){
+			      		found.add(link.hwnode);
+			      		List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
+			      		tmp.add(link.hwnode);
+			      		pathMap.put(link.hwnode, tmp);
+			    	    }
+			  	}
+			        else if (curr == link.hwnode){
+			      	    if (!done.contains(link.bus) && !found.contains(link.bus)){
+			        	found.add(link.bus);
+			        	List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
+			        	tmp.add(link.bus);
+			        	pathMap.put(link.bus, tmp);
+			      	    }
+			  	}
+			    }
+			    done.add(curr);
+		      }
+		      if (path.size() ==0){
+			  System.out.println("Path does not exist for channel " + channel.getName() + " between Task " + a.getTaskName() + " and Task " + t.getTaskName());
+			  channelMap.put(channel.getName(), channelUnreachable);
+		      }
+		      else {
+			  int priv=1;
+			  HwBus bus;
+			  //Check if all buses and bridges are private
+			  for (HwNode n: path){
+			      if (n instanceof HwBus){
+			          bus = (HwBus) n;
+				  System.out.println("BUS PRIVACY "+bus.privacy);
+			    	  if (bus.privacy ==0){
+			      	      priv=0;
+					break;
+			    	  }
+			      }
+			  }
+			  channelMap.put(channel.getName(), priv);
+			  System.out.println("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is " + (priv==1 ? "confidential" : "not confidential"));
+		      }
+		}
+	    }
+	}  
+    }
     public boolean saveInFile(String path) throws FileException {
 	//Our hash is saved in config
 	System.out.println(this.spec);
@@ -157,13 +253,14 @@ public class TML2ProVerif {
 
     public ProVerifSpec generateProVerif(boolean _debug, boolean _optimize, boolean _stateReachability, boolean _typed) {
 	System.out.println("generating spec...");
+
         this.stateReachability = _stateReachability;
         this.warnings = new Vector();
         if (_typed)
             this.spec = new ProVerifSpec (new ProVerifPitypeSyntaxer ());
         else
             this.spec = new ProVerifSpec (new ProVerifPiSyntaxer ());
-
+	checkChannels();
 
         LinkedList<TMLAttribute> allKnowledge = this.makeStartingProcess();
 
@@ -426,20 +523,32 @@ TMLActivity act= task.getActivityDiagram();
 	    stateNum++;
 	    if (ae instanceof TMLActivityElementChannel){
 	        TMLActivityElementChannel aec = (TMLActivityElementChannel) ae;
+		int channelStatus = channelMap.get(aec.getChannel(0).getName());
 	        if (aec instanceof TMLWriteChannel){
 		    tmp = "out (" + CH_MAINCH + ", ";
-		    //if (isPrivate)
-                    //  tmp += CH_ENCRYPT + " (";
-            	//if (isPrivate)
-                  //  tmp += ")";
-
-            	    tmp += "data__"+aec.getChannel(0).getName()+")";
-		    p = p.setNextInstr(new ProVerifProcRaw (tmp, true));
+		    //Look up privacy
+		    if (channelStatus!=channelUnreachable){
+		        if (channelStatus==channelPrivate)
+                            tmp += CH_ENCRYPT + " (";
+            	    	tmp += "data__"+aec.getChannel(0).getName()+")";
+		        if (channelStatus==channelPrivate)
+                            tmp += ")";
+		        p = p.setNextInstr(new ProVerifProcRaw (tmp, true));
+		    }
 	        }
 	        else {
-	            LinkedList<ProVerifVar> vars = new LinkedList<ProVerifVar> ();
-		    vars.add (new ProVerifVar ("data__"+ aec.getChannel(0).getName(), "bitstring"));
-		    p=p.setNextInstr(new ProVerifProcIn (CH_MAINCH, vars.toArray (new ProVerifVar[vars.size()])));
+		    if (channelStatus==channelPrivate) {
+			LinkedList<ProVerifVar> vars = new LinkedList<ProVerifVar> ();
+                	TraceManager.addDev("|    |    in (chPriv, ...)");
+			vars.add (new ProVerifVar ("data__"+ aec.getChannel(0).getName(), "bitstring"));
+                	p = p.setNextInstr (new ProVerifProcIn (CH_MAINCH, new ProVerifVar[] {new ProVerifVar ("privChData", "bitstring")}));
+                	p = p.setNextInstr (new ProVerifProcLet (vars.toArray (new ProVerifVar[vars.size()]), CH_DECRYPT + " (privChData)"));
+            	    }
+		    else {
+	                LinkedList<ProVerifVar> vars = new LinkedList<ProVerifVar> ();
+		        vars.add (new ProVerifVar ("data__"+ aec.getChannel(0).getName(), "bitstring"));
+		        p=p.setNextInstr(new ProVerifProcIn (CH_MAINCH, vars.toArray (new ProVerifVar[vars.size()])));
+		    }
 	        }
 	    }
 	    ae = ae.getNextElement(0);