From 767072f4794ea393df3bacc5ca5c40c2a5edb07c Mon Sep 17 00:00:00 2001
From: Letitia Li <leli@enst.fr>
Date: Wed, 17 Feb 2016 15:21:05 +0000
Subject: [PATCH] tml2proveriftranslation
---
.../toproverif/TML2ProVerif.java | 133 ++++++++++++++++--
1 file changed, 121 insertions(+), 12 deletions(-)
diff --git a/src/tmltranslator/toproverif/TML2ProVerif.java b/src/tmltranslator/toproverif/TML2ProVerif.java
index d0628630ad..9c971e8288 100644
--- a/src/tmltranslator/toproverif/TML2ProVerif.java
+++ b/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);
--
GitLab