From 1bd19b13ab91c8161e7bd068ed84c27abb557c30 Mon Sep 17 00:00:00 2001
From: Letitia Li <leli@enst.fr>
Date: Fri, 25 Mar 2016 15:22:23 +0000
Subject: [PATCH] security pattern backtracing
---
src/tmltranslator/TMLModeling.java | 84 +++++++++++++++++++++-
src/tmltranslator/toavatar/TML2Avatar.java | 19 +++--
src/ui/tmlcompd/TMLCPrimitivePort.java | 48 ++++++++++---
3 files changed, 129 insertions(+), 22 deletions(-)
diff --git a/src/tmltranslator/TMLModeling.java b/src/tmltranslator/TMLModeling.java
index 9901579b64..0bc9fc62b4 100755
--- a/src/tmltranslator/TMLModeling.java
+++ b/src/tmltranslator/TMLModeling.java
@@ -63,8 +63,9 @@ public class TMLModeling {
private ArrayList<String[]> pragmas;
public ArrayList<String> securityPatterns=new ArrayList<String>();
private TMLElement correspondance[];
-
+ public ArrayList<SecurityPattern> secPatterns = new ArrayList<SecurityPattern>();
private boolean optimized = false;
+ public HashMap<String, String> secChannelMap = new HashMap<String, String>();
private String[] ops = {">", "<", "+", "-", "*", "/", "[", "]", "(", ")", ":", "=", "==", ","};
@@ -634,6 +635,19 @@ public class TMLModeling {
ev.port2.mappingName=mappingName;
}
}
+ String channelName=secChannelMap.get(attr.getName());
+ if (channelName!=null){
+ System.out.println("CHANNEL FOUND "+channelName);
+ channel = getChannelByName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkConf){
+ port.checkSecConfStatus = 2;
+ port.secName= attr.getName();
+ }
+}
+ }
+ }
for (TMLTask t:getTasks()){
if (t.getReferenceObject()==null){
continue;
@@ -683,6 +697,19 @@ public class TMLModeling {
ev.port2.mappingName= mappingName;
}
}
+ String channelName=secChannelMap.get(attr.getName());
+ System.out.println("CHANNEL FOUND "+channelName);
+ if (channelName!=null){
+ channel = getChannelByName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkConf){
+ port.checkSecConfStatus = 3;
+ port.secName= attr.getName();
+ }
+ }
+ }
+}
for (TMLTask t:getTasks()){
if (t.getReferenceObject() instanceof TMLCPrimitiveComponent){
TMLCPrimitiveComponent comp = (TMLCPrimitiveComponent) t.getReferenceObject();
@@ -703,6 +730,7 @@ public class TMLModeling {
}
public void backtraceAuthenticity(LinkedList<String> satisfiedAuthenticity, LinkedList<String> satisfiedWeakAuthenticity,LinkedList<String> nonSatisfiedAuthenticity, String mappingName){
for (String s: satisfiedAuthenticity){
+ System.out.println("authenticity" +s);
String signalName = s.split("__chData")[0];
for (TMLTask t: getTasks()){
if (signalName.contains(t.getName())){
@@ -750,6 +778,25 @@ public class TMLModeling {
ev.port2.mappingName= mappingName;
}
}
+
+ signalName = s.split("__decrypt")[0];
+ for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }
+ System.out.println("auth on "+signalName);
+ String channelName=secChannelMap.get(signalName);
+ System.out.println("auth channel "+channelName);
+ channel = getChannelByName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkSecStrongAuthStatus = 2;
+ port.secName= signalName;
+ }
+ }
+ }
}
for (String s: satisfiedWeakAuthenticity){
String signalName = s.split("__chData")[0];
@@ -799,6 +846,22 @@ public class TMLModeling {
ev.port2.mappingName= mappingName;
}
}
+ signalName = s.split("__decrypt")[0];
+ for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }
+ String channelName=secChannelMap.get(signalName);
+ channel = getChannelByName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkSecWeakAuthStatus = 2;
+ port.secName= signalName;
+ }
+ }
+ }
}
for (String s: nonSatisfiedAuthenticity){
String signalName = s.split("__chData")[0];
@@ -848,6 +911,24 @@ public class TMLModeling {
ev.port2.mappingName= mappingName;
}
}
+ signalName = s.split("__decrypt")[0];
+ for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }
+ String channelName=secChannelMap.get(signalName);
+ if (channelName!=null){
+ channel = getChannelByName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkSecStrongAuthStatus = 3;
+ port.secName= signalName;
+ }
+ }
+ }
+ }
}
}
public void clearBacktracing(){
@@ -856,6 +937,7 @@ public class TMLModeling {
if (port.checkConfStatus>1){
port.checkConfStatus=1;
port.mappingName="???";
+ port.secName="";
}
if (port.checkStrongAuthStatus>1 || port.checkWeakAuthStatus>1){
port.checkStrongAuthStatus = 1;
diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java
index 9efd4ff302..7676b7580a 100644
--- a/src/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/tmltranslator/toavatar/TML2Avatar.java
@@ -78,10 +78,12 @@ public class TML2Avatar {
HashMap<String, AvatarSignal> signalMap = new HashMap<String, AvatarSignal>();
public HashMap<String, Object> stateObjectMap = new HashMap<String, Object>();
+ HashMap<String, String> secChannelMap = new HashMap<String, String>();
+
HashMap<String, AvatarAttributeState> signalAuthOriginMap = new HashMap<String, AvatarAttributeState>();
HashMap<String, AvatarAttributeState> signalAuthDestMap = new HashMap<String, AvatarAttributeState>();
- ArrayList<SecurityPattern> secPatterns = new ArrayList<SecurityPattern>();
+ public ArrayList<SecurityPattern> secPatterns = new ArrayList<SecurityPattern>();
List<AvatarSignal> signals = new ArrayList<AvatarSignal>();
private final static Integer channelPublic = 0;
@@ -739,6 +741,7 @@ public class TML2Avatar {
AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
if (ae.securityPattern!=null){
+ secChannelMap.put(ae.securityPattern.name,ch.getName());
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);
@@ -810,6 +813,7 @@ public class TML2Avatar {
as.addValue(ae.securityPattern.name+"_encrypted");
AvatarAttribute data= new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
block.addAttribute(data);
+ secChannelMap.put(ae.securityPattern.name,ch.getName());
}
else {
as.addValue(ch.getName()+"__chData");
@@ -1045,15 +1049,6 @@ public class TML2Avatar {
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);
@@ -1401,9 +1396,11 @@ public class TML2Avatar {
//Check if we matched up all signals
//System.out.println(avspec);
-
+ tmlmap.getTMLModeling().secChannelMap = secChannelMap;
return avspec;
}
+
+ // public void backtracePatterns(List<Stri
public void backtraceReachability(List<String> reachableStates, List<String> nonReachableStates){
for (String s: reachableStates){
diff --git a/src/ui/tmlcompd/TMLCPrimitivePort.java b/src/ui/tmlcompd/TMLCPrimitivePort.java
index a59b21a479..d360f8e31a 100755
--- a/src/ui/tmlcompd/TMLCPrimitivePort.java
+++ b/src/ui/tmlcompd/TMLCPrimitivePort.java
@@ -84,6 +84,12 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
//Security Verification
public int checkConfStatus;
+
+ public int checkSecConfStatus;
+ public int checkSecWeakAuthStatus;
+ public int checkSecStrongAuthStatus;
+ public String secName="";
+
public int checkWeakAuthStatus;
public int checkStrongAuthStatus;
public boolean checkConf;
@@ -304,7 +310,7 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
if (checkConf && isOrigin){
drawConfVerification(g);
}
- if (checkAuth && !isOrigin){
+ if (checkAuth && !isOrigin && !secName.equals("")){
drawAuthVerification(g);
}
g.setFont(fold);
@@ -316,10 +322,11 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
public void drawAuthVerification(Graphics g){
+ g.drawString(secName, x-20, y+8);
Color c = g.getColor();
Color c1;
Color c2;
- switch(checkStrongAuthStatus) {
+ switch(checkSecStrongAuthStatus) {
case 2:
c1 = Color.green;
break;
@@ -329,7 +336,7 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
default:
c1 = Color.gray;
}
- switch(checkWeakAuthStatus) {
+ switch(checkSecWeakAuthStatus) {
case 2:
c2 = Color.green;
break;
@@ -340,12 +347,12 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
c2= c1;
}
- g.drawOval(x-16, y, 10, 15);
+ g.drawOval(x-18, y+8, 10, 15);
g.setColor(c1);
- int[] xps = new int[]{x-18, x-18, x-2};
- int[] yps = new int[]{y+6, y+20, y+20};
- int[] xpw = new int[]{x-2, x-2, x-18};
- int[] ypw = new int[]{y+20, y+6, y+6};
+ int[] xps = new int[]{x-20, x-20, x-4};
+ int[] yps = new int[]{y+14, y+28, y+28};
+ int[] xpw = new int[]{x-4, x-4, x-20};
+ int[] ypw = new int[]{y+28, y+14, y+14};
g.fillPolygon(xps, yps,3);
g.setColor(c2);
@@ -353,8 +360,8 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
g.setColor(c);
g.drawPolygon(xps, yps,3);
g.drawPolygon(xpw, ypw, 3);
- g.drawString("S", x-16, y+18);
- g.drawString("W", x-9, y+14);
+ g.drawString("S", x-18, y+26);
+ g.drawString("W", x-11, y+22);
}
public void drawConfVerification(Graphics g){
Color c = g.getColor();
@@ -381,6 +388,27 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
+ if (!secName.equals("")){
+ switch(checkSecConfStatus) {
+ case 1:
+ c1 = Color.gray;
+ break;
+ case 2:
+ c1 = Color.green;
+ break;
+ case 3:
+ c1 = Color.red;
+ break;
+ default:
+ return;
+ }
+ g.drawString(secName, x-20, y+20);
+ g.drawOval(x-10, y+22, 6, 9);
+ g.setColor(c1);
+ g.fillRect(x-12, y+24, 9, 7);
+ g.setColor(c);
+ g.drawRect(x-12, y+24, 9, 7);
+ }
}
public void manageMove() {
--
GitLab