diff --git a/src/main/java/tmltranslator/SecurityBacktracer.java b/src/main/java/tmltranslator/SecurityBacktracer.java
index ae8086a1181a448c9421c6cc0233bbc68f845bbb..8dfc4185cfefce827304400fa20f9800146e55a9 100644
--- a/src/main/java/tmltranslator/SecurityBacktracer.java
+++ b/src/main/java/tmltranslator/SecurityBacktracer.java
@@ -68,5 +68,9 @@ public interface SecurityBacktracer {
public void setStrongAuthStatus(int _strongAuthStatus);
+ public boolean getConfCheck();
+ public void setConfCheck(boolean _confCheck);
+ public int getConfStatus();
+ void setConfStatus(int _confStatus);
}
diff --git a/src/main/java/tmltranslator/TMLModeling.java b/src/main/java/tmltranslator/TMLModeling.java
index 19af02ff5bd8ccba902f843291855549e6e9cdb5..ce5f3d41554b55807edc6f8e8bed4433455ac462 100755
--- a/src/main/java/tmltranslator/TMLModeling.java
+++ b/src/main/java/tmltranslator/TMLModeling.java
@@ -64,6 +64,7 @@ public class TMLModeling<E> {
// Security
private List<SecurityPattern> secPatterns;
private Map<TMLChannel, Set<AvatarPragma>> secChannelMap;
+ private Map<TMLWriteChannel, Set<AvatarPragma>> wrPragmaMap;
private Map<SecurityPattern, List<TMLTask>> securityTaskMap;
// Tasks and communication
@@ -132,6 +133,14 @@ public class TMLModeling<E> {
this.secChannelMap = secChannelMap;
}
+ public Map<TMLWriteChannel, Set<AvatarPragma>> getWrPragmaMap() {
+ return wrPragmaMap;
+ }
+
+ public void setWrPragmaMap(Map<TMLWriteChannel, Set<AvatarPragma>> wrPragmaMap) {
+ this.wrPragmaMap = wrPragmaMap;
+ }
+
public TMLMapping<E> getDefaultMapping() {
TMLMapping<E> tmlmapping;
tmlmapping = new TMLMapping<>(this, new TMLArchitecture(), false);
@@ -782,20 +791,69 @@ public class TMLModeling<E> {
return list;
}
+ private void backtraceConfidentialityInAD(Map<AvatarPragmaSecret, ProVerifQueryResult> confResults, TMLChannel ch) {
+ if (ch.isCheckConfChannel()) {
+ List<TMLTask> tasks = new ArrayList<TMLTask>();
+ if (!ch.getOriginTasks().isEmpty()) {
+ tasks.addAll(ch.getOriginTasks());
+ } else {
+ tasks.add(ch.getOriginTask());
+ }
+ for (TMLTask task : tasks) {
+ for (TMLActivityElement actElem : task.getActivityDiagram().getElements()) {
+ if (actElem instanceof TMLWriteChannel) {
+ TMLWriteChannel wc = (TMLWriteChannel) actElem;
+ if (wrPragmaMap.containsKey(wc)) {
+ List<Integer> confStatus = new ArrayList<Integer>();
+ for (AvatarPragma pragma : wrPragmaMap.get(wc)) {
+ if (pragma instanceof AvatarPragmaSecret) {
+ AvatarPragmaSecret pragmaSecret = (AvatarPragmaSecret) pragma;
+ ProVerifQueryResult result = confResults.get(pragmaSecret);
+ if (result != null) {
+ if (!result.isProved()) {
+ confStatus.add(1);
+ } else {
+ int r = result.isSatisfied() ? 2 : 3;
+ confStatus.add(r);
+ }
+ }
+ }
+ }
+ int generalConfResult = 1;
+ if (!confStatus.isEmpty()) {
+ if (confStatus.contains(3)) {
+ generalConfResult = 3;
+ } else if (confStatus.contains(1)) {
+ generalConfResult = 1;
+ } else {
+ generalConfResult = 2;
+ }
+ }
+ if (wc.getReferenceObject() instanceof SecurityBacktracer) {
+ SecurityBacktracer sec = (SecurityBacktracer) wc.getReferenceObject();
+ sec.setConfCheck(ch.checkConf);
+ sec.setConfStatus(generalConfResult);
+ }
+ }
+ }
+ }
+ }
+ }
+ }
- public void backtrace(ProVerifOutputAnalyzer pvoa, String mappingName) {
+ public void backtraceConfidentiality(ProVerifOutputAnalyzer pvoa, String mappingName) {
//TraceManager.addDev("Backtracing Confidentiality");
Map<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
for (TMLChannel ch : secChannelMap.keySet()) {
if (ch.isCheckConfChannel()) {
List<Integer> confStatus = new ArrayList<Integer>();
- String secName = "";
+ Set<String> secNames = new HashSet<String>();
ProVerifResultTrace trace = null;
String pragmaString = "";
for (AvatarPragma pragma : secChannelMap.get(ch)) {
if (pragma instanceof AvatarPragmaSecret) {
AvatarPragmaSecret pragmaSecret = (AvatarPragmaSecret) pragma;
- secName += pragmaSecret.getArg().getName();
+ secNames.add(pragmaSecret.getArg().getName());
ProVerifQueryResult result = confResults.get(pragmaSecret);
if (result != null) {
if (!result.isProved()) {
@@ -804,6 +862,7 @@ public class TMLModeling<E> {
int r = result.isSatisfied() ? 2 : 3;
confStatus.add(r);
}
+ //backtraceConfidentialityInAD(pragmaSecret, ch, confStatus.get(confStatus.size() - 1));
trace = pvoa.getResults().get(pragma).getTrace();
pragmaString = pragma.toString();
}
@@ -823,8 +882,7 @@ public class TMLModeling<E> {
for (TMLPortWithSecurityInformation port : ch.ports) {
if (port.getCheckConf()) {
port.setConfStatus(generalConfResult);
- TraceManager.addDev("secName = " + secName);
- port.setSecName(secName);
+ port.setSecName(String.join(" ", secNames));
port.setMappingName(mappingName);
port.setPragmaString(pragmaString);
if (trace != null) {
@@ -832,6 +890,7 @@ public class TMLModeling<E> {
}
}
}
+ backtraceConfidentialityInAD(confResults, ch);
}
}
}
@@ -2761,20 +2820,6 @@ public class TMLModeling<E> {
return true;
}
- public int updateStrongAuthenticityStatus(int _lastStrongAuthStatus, int _lastWeakAuthStatus,
- boolean _isStrongAuthProved, boolean _isStrongAuthSatisfied, boolean _isWeakAuthProved,
- boolean _isWeakAuthSatisfied) {
- if (_isStrongAuthProved && _isStrongAuthSatisfied && _isWeakAuthProved && _isWeakAuthSatisfied
- && _lastStrongAuthStatus != 3 && _lastWeakAuthStatus != 3) {
- return 2;
- } else if (!_isStrongAuthProved && !(_isWeakAuthProved && !_isWeakAuthSatisfied) && _lastStrongAuthStatus < 3 && _lastWeakAuthStatus < 3) {
- return 1;
- }
- else {
- return 3;
- }
- }
-
@SuppressWarnings("unchecked")
public TMLModeling deepClone() throws TMLCheckingError {
TMLModeling tmlm = new TMLModeling();
diff --git a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
index e02dc4cedcfdf99b0878568485adda3d84d886b0..36a905a06c8570d06f74fa5400b1cc6e09fcb5a1 100644
--- a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
@@ -68,6 +68,7 @@ public class TML2Avatar {
private int loopLimit = 1;
private HashMap<TMLChannel, Set<String>> channelsSecAttributes = new HashMap<TMLChannel, Set<String>>();
private HashMap<TMLChannel, Set<AvatarPragma>> secChannelMap = new HashMap<TMLChannel, Set<AvatarPragma>>();
+ private Map<TMLWriteChannel, Set<AvatarPragma>> wrPragmaMap = new HashMap<TMLWriteChannel, Set<AvatarPragma>>();;
private HashMap<String, List<AvatarAttributeState>> signalAuthOriginMap = new HashMap<String, List<AvatarAttributeState>>();
private HashMap<String, List<AvatarAttributeState>> signalAuthDestMap = new HashMap<String, List<AvatarAttributeState>>();
private List<AvatarSignal> signals = new ArrayList<AvatarSignal>();
@@ -1465,6 +1466,12 @@ public class TML2Avatar {
if (!isAvSecretInSet) {
secChannelMap.get(ch).add(avPragmaSecret);
}
+
+ if (!wrPragmaMap.containsKey((TMLWriteChannel) ae)) {
+ Set<AvatarPragma> tmp = new HashSet<AvatarPragma>();
+ wrPragmaMap.put((TMLWriteChannel) ae, tmp);
+ }
+ wrPragmaMap.get((TMLWriteChannel) ae).add(avPragmaSecret);
}
}
}
@@ -1488,6 +1495,12 @@ public class TML2Avatar {
if (!isAvSecretInSet) {
secChannelMap.get(ch).add(avPragmaSecret);
}
+
+ if (!wrPragmaMap.containsKey((TMLWriteChannel) ae)) {
+ Set<AvatarPragma> tmp = new HashSet<AvatarPragma>();
+ wrPragmaMap.put((TMLWriteChannel) ae, tmp);
+ }
+ wrPragmaMap.get((TMLWriteChannel) ae).add(avPragmaSecret);
}
}
}
@@ -2132,7 +2145,12 @@ public class TML2Avatar {
if (!isAvSecretInSet) {
secChannelMap.get(ch).add(secPatternPragmaMap.get(secPattern));
}
- break;
+
+ if (!wrPragmaMap.containsKey(wc)) {
+ Set<AvatarPragma> tmp = new HashSet<AvatarPragma>();
+ wrPragmaMap.put(wc, tmp);
+ }
+ wrPragmaMap.get(wc).add(secPatternPragmaMap.get(secPattern));
}
}
}
@@ -2626,6 +2644,7 @@ public class TML2Avatar {
}
tmlmap.getTMLModeling().setSecChannelMap(secChannelMap);
+ tmlmap.getTMLModeling().setWrPragmaMap(wrPragmaMap);
// System.out.println("avatar spec\n" +avspec);
return avspec;
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index bf1ea9dbac4e5f0c0a96e6a4828301cb2eb9d160..babada70eafd7b0476218d1ac7f7cea0cfb4c285 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -4876,7 +4876,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
if (gtm.getTMLMapping() != null) {
gtm.getTMLMapping().getTMLModeling().clearBacktracing();
getCurrentTDiagramPanel().clearAuthenticityBacktracing();
- gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, getTabName(tp));
+ gtm.getTMLMapping().getTMLModeling().backtraceConfidentiality(pvoa, getTabName(tp));
gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
gtm.getTML2Avatar().backtraceAuthenticityADReadChannels(pvoa, getTabName(tp));
gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa, getTabName(tp));
@@ -4887,7 +4887,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
if (gtm.getTMLMapping() != null) {
gtm.getTMLMapping().getTMLModeling().clearBacktracing();
getCurrentTDiagramPanel().clearAuthenticityBacktracing();
- gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, "Default Mapping");
+ gtm.getTMLMapping().getTMLModeling().backtraceConfidentiality(pvoa, "Default Mapping");
gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
gtm.getTML2Avatar().backtraceAuthenticityADReadChannels(pvoa, "Default Mapping");
gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa, "Default Mapping");
diff --git a/src/main/java/ui/tmlad/TMLADReadChannel.java b/src/main/java/ui/tmlad/TMLADReadChannel.java
index 01486295204cddf71639122e1113fdb4f2dba915..df74b53c7dcce827cae6fb4a0e4c8aac86bb150d 100755
--- a/src/main/java/ui/tmlad/TMLADReadChannel.java
+++ b/src/main/java/ui/tmlad/TMLADReadChannel.java
@@ -594,6 +594,26 @@ public class TMLADReadChannel extends TADComponentWithoutSubcomponents/* Issue #
strongAuthStatus = _strongAuthStatus;
}
+ @Override
+ public boolean getConfCheck() {
+ return false;
+ }
+
+ @Override
+ public void setConfCheck(boolean _confCheck) {
+
+ }
+
+ @Override
+ public int getConfStatus() {
+ return 0;
+ }
+
+ @Override
+ public void setConfStatus(int _confStatus) {
+
+ }
+
public String getCommunicationName() {
return channelName;
}
diff --git a/src/main/java/ui/tmlad/TMLADWriteChannel.java b/src/main/java/ui/tmlad/TMLADWriteChannel.java
index 6c75be7719b8c26392a0074e34c5d18dd1368014..d2785468efa53e57d533adbae5c70365cd27a32c 100755
--- a/src/main/java/ui/tmlad/TMLADWriteChannel.java
+++ b/src/main/java/ui/tmlad/TMLADWriteChannel.java
@@ -55,6 +55,7 @@ import org.w3c.dom.NodeList;
import myutil.Conversion;
import myutil.GraphicLib;
+import tmltranslator.SecurityBacktracer;
import tmltranslator.SecurityCheckable;
import ui.AllowedBreakpoint;
import ui.BasicErrorHighlight;
@@ -83,7 +84,7 @@ import ui.window.TabInfo;
* @version 1.0 17/11/2005
*/
public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue #69 TGCWithoutInternalComponent*/ implements CheckableAccessibility,
- LinkedReference, CheckableLatency, EmbeddedComment, AllowedBreakpoint, BasicErrorHighlight, SecurityCheckable {
+ LinkedReference, CheckableLatency, EmbeddedComment, AllowedBreakpoint, BasicErrorHighlight, SecurityCheckable, SecurityBacktracer {
// Issue #31
// protected int lineLength = 5;
@@ -115,6 +116,8 @@ public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue
// public boolean isEncForm = true;
private int securityMaxX;
+ private boolean confCheck;
+ private int confStatus;
public TMLADWriteChannel(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp);
@@ -217,6 +220,9 @@ public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue
}
g.setColor(c);
}
+ if (confCheck) {
+ drawConfidentialityInformation(g);
+ }
if (getCheckLatency()) {
ConcurrentHashMap<String, String> latency = tdp.getMGUI().getLatencyVals(getDIPLOID());
@@ -279,6 +285,51 @@ public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue
}
}
+ public void drawConfidentialityInformation(Graphics g) {
+ final double coeffSpacePortConfLock = 0.1;
+ final double coeffConfLock = 0.9;
+ final double coeffConfOval = 0.8;
+ //final double coeffYCoordinateOffsetDrawConf = 1.01;
+ double spacePortConfLock = width * coeffSpacePortConfLock;
+ double confLockWidth = height * coeffConfLock;
+ double confLockHeight = height * coeffConfLock;
+ double confOvalWidth = height * coeffConfOval;
+ double confOvalHeight = height * coeffConfOval;
+ double xCoordinateConfLockLeft = x + width + spacePortConfLock;
+ double xCoordinateConfLockRight = x + width + confLockWidth + spacePortConfLock;
+ double yCoordinateConfLockTop = y + height - confLockHeight;
+ double yCoordinateConfLockBottom = y + height;
+ double xCoordinateConfOvalLeft = xCoordinateConfLockLeft + (confLockWidth - confOvalWidth)/2;
+ double yCoordinateConfOvalTop = yCoordinateConfLockTop - confOvalHeight/2;
+
+ Color c = g.getColor();
+ Color c1;
+ switch (confStatus) {
+ case 1:
+ c1 = Color.gray;
+ break;
+ case 2:
+ c1 = Color.green;
+ break;
+ case 3:
+ c1 = Color.red;
+ break;
+ default:
+ return;
+ }
+ g.drawOval((int) (xCoordinateConfOvalLeft), (int) (yCoordinateConfOvalTop), (int)confOvalWidth, (int)confOvalHeight);
+ g.setColor(c1);
+ g.fillRect((int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
+ g.setColor(c);
+ g.drawRect((int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
+ if (confStatus == 3) {
+ g.drawLine((int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockTop),
+ (int) (xCoordinateConfLockRight), (int) (yCoordinateConfLockBottom));
+ g.drawLine((int) (xCoordinateConfLockRight), (int) (yCoordinateConfLockTop),
+ (int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockBottom));
+ }
+ }
+
@Override
public TGComponent isOnMe(int _x, int _y) {
if (GraphicLib.isInRectangle(_x, _y, x, y, width, height)) {
@@ -507,4 +558,55 @@ public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue
public String getCommunicationName() {
return channelName;
}
+
+ @Override
+ public boolean getConfCheck() {
+ return confCheck;
+ }
+
+ @Override
+ public void setConfCheck(boolean _confCheck) {
+ confCheck = _confCheck;
+ makeValue();
+ }
+
+ @Override
+ public int getConfStatus() {
+ return confStatus;
+ }
+
+ @Override
+ public void setConfStatus(int _confStatus) {
+ confStatus = _confStatus;
+ }
+
+ @Override
+ public boolean getAuthCheck() {
+ return false;
+ }
+
+ @Override
+ public void setAuthCheck(boolean _authCheck) {
+
+ }
+
+ @Override
+ public int getWeakAuthStatus() {
+ return 0;
+ }
+
+ @Override
+ public void setWeakAuthStatus(int _weakAuthStatus) {
+
+ }
+
+ @Override
+ public int getStrongAuthStatus() {
+ return 0;
+ }
+
+ @Override
+ public void setStrongAuthStatus(int _strongAuthStatus) {
+
+ }
}