diff --git a/src/tmltranslator/TMLChannel.java b/src/tmltranslator/TMLChannel.java
index 00ceb3b385fde1a513445af621afb805d01a6c22..fd0cb9548029448b7b1ca4f678f05e3de528c78c 100755
--- a/src/tmltranslator/TMLChannel.java
+++ b/src/tmltranslator/TMLChannel.java
@@ -55,7 +55,8 @@ public class TMLChannel extends TMLCommunicationElement {
public static final int BRBW = 0;
public static final int BRNBW = 1;
public static final int NBRNBW = 2;
-
+ public static int confStatus;
+ public static boolean checkConf;
private int size;
private int type;
private int max;
diff --git a/src/tmltranslator/TMLEvent.java b/src/tmltranslator/TMLEvent.java
index c76654b565cbbf143d348f32ea17ec9364db378f..3e344ab97197f13fbff159b9d97375e0fdb74851 100755
--- a/src/tmltranslator/TMLEvent.java
+++ b/src/tmltranslator/TMLEvent.java
@@ -54,7 +54,8 @@ public class TMLEvent extends TMLCommunicationElement {
protected boolean isBlocking = false; // By default, latest events is removed when the FIFO is full
protected boolean canBeNotified = false;
protected TMLTask origin, destination;
-
+ public static int confStatus;
+ public static boolean checkConf;
/*public TMLEvent(String name, Object reference) {
super(name, reference);
params = new Vector();
diff --git a/src/tmltranslator/TMLRequest.java b/src/tmltranslator/TMLRequest.java
index 7484381d38772dbed5db1d5929408ef1ab426569..a951d8cfac1e3eb6b989b39e55cdf6409fa3c98e 100755
--- a/src/tmltranslator/TMLRequest.java
+++ b/src/tmltranslator/TMLRequest.java
@@ -53,6 +53,8 @@ public class TMLRequest extends TMLCommunicationElement {
protected ArrayList<TMLTask> originTasks; // list of tasks from which request starts
protected TMLTask destinationTask;
protected ArrayList<String> paramNames;
+ public static int confStatus;
+ public static boolean checkConf;
public TMLRequest(String name, Object reference) {
super(name, reference);
params = new Vector();
diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java
index 6494ee7d5879d393b3aac4c486ec0b683afabaef..2d8561319059766506759e1d599b1726f0c4dbd4 100644
--- a/src/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/tmltranslator/toavatar/TML2Avatar.java
@@ -595,7 +595,14 @@ public class TML2Avatar {
block.addSignal(sig);
signalMap.put(block.getName()+"__OUT__"+ch.getName(), sig);
AvatarAttribute channelData= new AvatarAttribute(ch.getName()+"__chData", AvatarType.INTEGER, block, null);
+ LinkedList<AvatarAttribute> attrs = new LinkedList<AvatarAttribute>();
block.addAttribute(channelData);
+ attrs.add(channelData);
+ if (ch.checkConf){
+ System.out.println("channel " + ch.getName());
+ System.out.println("block " + block.getName());
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ch.getName()+"__chData", ch.getReferenceObject(), attrs));
+ }
}
else {
sig=signalMap.get(block.getName()+"__OUT__"+ch.getName());
@@ -772,7 +779,7 @@ public class TML2Avatar {
//TODO: Put back numeric guards
//TODO: Calcuate for temp variable
//TODO: Cry
- AvatarSpecification avspec = new AvatarSpecification("spec", tmlmap.getTMLCDesignPanel());
+ this.avspec = new AvatarSpecification("spec", tmlmap.getTMLCDesignPanel());
if (tmlmap.getTMLCDesignPanel()==null){
System.out.println("Failed to generate specification");
return avspec;
diff --git a/src/ui/GTMLModeling.java b/src/ui/GTMLModeling.java
index 7f0bc7bff4170ce76779d285d27bde4eed206853..fdcec189289ece138a3870498ddbee0a0299c02b 100755
--- a/src/ui/GTMLModeling.java
+++ b/src/ui/GTMLModeling.java
@@ -717,6 +717,7 @@ public class GTMLModeling {
addToTable(makeName(port2, port2.getFather().getValue()) + "/" + name2, name);
channel = new TMLChannel(name, port1);
+ channel.checkConf= port1.checkConf;
channel.setSize(port1.getSize());
channel.setMax(port1.getMax());
if (port1.isBlocking() && port2.isBlocking()) {
@@ -812,6 +813,7 @@ public class GTMLModeling {
// Channel attributes
port = (TMLCPrimitivePort)(portstome.get(0));
channel = new TMLChannel(name, port1);
+ channel.checkConf= port1.checkConf;
channel.setSize(port1.getSize());
channel.setMax(port1.getMax());
if (port1.isBlocking() && port.isBlocking()) {
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index 590ad4814b29e99ea48ffd13d5500c063fc25916..a1af6246fe5c0eea4cd3ee810413631e17c2c0b4 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -3759,8 +3759,8 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
}
else if (tp instanceof TMLArchiPanel) {
}
- else if (tp instanceof TMLDesignPanel){
- TMLDesignPanel tap = (TMLDesignPanel) tp;
+ else if (tp instanceof TMLComponentDesignPanel){
+ TMLComponentDesignPanel tap = (TMLComponentDesignPanel) tp;
tap.modelBacktracingProVerif(pvoa);
getCurrentTDiagramPanel().repaint();
}
diff --git a/src/ui/TMLComponentDesignPanel.java b/src/ui/TMLComponentDesignPanel.java
index 2246a99c8ee49a3717771dc9df9c41ff21ba9518..dbcfc2c795f8ccaccba6b67612d2142182babb46 100755
--- a/src/ui/TMLComponentDesignPanel.java
+++ b/src/ui/TMLComponentDesignPanel.java
@@ -56,7 +56,8 @@ import ui.tmlcompd.*;
import ui.tmlad.*;
import ui.tmldd.*;
import ui.tmlcd.*;
-
+import avatartranslator.*;
+import proverifspec.*;
import myutil.*;
public class TMLComponentDesignPanel extends TURTLEPanel {
@@ -229,5 +230,82 @@ public class TMLComponentDesignPanel extends TURTLEPanel {
public String[] getAllOutRequests(String nameOfComponent) {
return tmlctdp.getAllOutRequests(nameOfComponent);
}
+ public void modelBacktracingProVerif(ProVerifOutputAnalyzer pvoa) {
+ resetModelBacktracingProVerif();
+ TGComponent tgc;
+ int index;
+ ListIterator iterator;
+ // Confidential attributes
+ LinkedList<AvatarAttribute> secretAttributes = pvoa.getSecretTerms ();
+ LinkedList<AvatarAttribute> nonSecretAttributes = pvoa.getNonSecretTerms ();
+ for (AvatarAttribute attr: secretAttributes){
+ System.out.println("!!!");
+ iterator = tmlctdp.getComponentList().listIterator();
+ while (iterator.hasNext()){
+ tgc = (TGComponent)(iterator.next());
+ if (tgc instanceof TMLCPrimitivePort){
+ System.out.println("port "+tgc);
+ ((TMLCPrimitivePort)tgc).checkStatus =2;
+ }
+ }
+ }
+/*
+ for(String s: pvoa.getNonReachableEvents()) {
+ index = s.indexOf("__");
+ if (index != -1) {
+ block = s.substring(index+2, s.length());
+ index = block.indexOf("__");
+ if (index != -1) {
+ state = block.substring(index+2, block.length());
+ block = block.substring(0, index);
+ TraceManager.addDev("Block=" + block + " state=" + state);
+ for(i=0; i<panels.size(); i++) {
+ tdp = (TDiagramPanel)(panels.get(i));
+ if ((tdp instanceof AvatarSMDPanel) && (tdp.getName().compareTo(block) == 0)){
+ iterator = ((TDiagramPanel)(panels.get(i))).getComponentList().listIterator();
+ while(iterator.hasNext()) {
+ tgc = (TGComponent)(iterator.next());
+ if (tgc instanceof AvatarSMDState) {
+ ((AvatarSMDState)tgc).setSecurityInfo(AvatarSMDState.NOT_REACHABLE, state);
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+*/
+ LinkedList<String> notProved = pvoa.getNotProved ();
+ LinkedList<String> satisfied = pvoa.getSatisfiedAuthenticity ();
+ LinkedList<String> satisfiedWeak = pvoa.getSatisfiedWeakAuthenticity ();
+ LinkedList<String> nonSatisfied = pvoa.getNonSatisfiedAuthenticity ();
+ }
+
+
+ public void resetModelBacktracingProVerif() {
+ /*if (abdp == null) {
+ return;
+ }
+
+ // Reset confidential attributes
+ for(AvatarBDBlock block1: abdp.getFullBlockList()) {
+ block1.resetConfidentialityOfAttributes();
+ }
+ for (Object tgc: abdp.getComponentList()){
+ if (tgc instanceof AvatarBDPragma){
+ AvatarBDPragma pragma = (AvatarBDPragma) tgc;
+ pragma.authStrongMap.clear();
+ pragma.authWeakMap.clear();
+
+ }
+ }
+ // Reset reachable states
+ for(int i=0; i<panels.size(); i++) {
+ tdp = (TDiagramPanel)(panels.get(i));
+ if (tdp instanceof AvatarSMDPanel) {
+ ((AvatarSMDPanel)tdp).resetStateSecurityInfo();
+ }
+ }*/
+ }
}
diff --git a/src/ui/TMLDesignPanel.java b/src/ui/TMLDesignPanel.java
index 2f50a2ed96adbe4e8fcf53904e8de9e4c9782aa4..c95954086d7ba8276c4739d2f958e271cfdb2259 100755
--- a/src/ui/TMLDesignPanel.java
+++ b/src/ui/TMLDesignPanel.java
@@ -182,103 +182,4 @@ public class TMLDesignPanel extends TURTLEPanel {
}
}
}
- public void modelBacktracingProVerif(ProVerifOutputAnalyzer pvoa) {
-
- resetModelBacktracingProVerif();
- TMLActivityDiagramPanel tmladp;
- for(int i=1; i<panels.size(); i++) {
- tmladp = (TMLActivityDiagramPanel)(panels.elementAt(i));
- }
- String block;
- String state;
- int index;
- ListIterator iterator;
- // Confidential attributes
- // LinkedList<AvatarAttribute> secretAttributes = pvoa.getSecretTerms ();
- // LinkedList<AvatarAttribute> nonSecretAttributes = pvoa.getNonSecretTerms ();
- // Reachable states
- for(String s: pvoa.getReachableEvents()) {
- index = s.indexOf("__");
- if (index != -1) {
- block = s.substring(index+2, s.length());
- index = block.indexOf("__");
- if (index != -1) {
- state = block.substring(index+2, block.length());
- block = block.substring(0, index);
-
- System.out.println("reachable event "+block+ " "+state);
- for(int i=0; i<panels.size(); i++) {
- tdp = (TDiagramPanel)(panels.get(i));
- if ((tdp instanceof TMLActivityDiagramPanel) && (tdp.getName().compareTo(block) == 0)){
- iterator = ((TDiagramPanel)(panels.get(i))).getComponentList().listIterator();
- /* while(iterator.hasNext()) {
- tgc = (TGComponent)(iterator.next());
- if (tgc instanceof TMLADChoicee) {
- ((AvatarSMDState)tgc).setSecurityInfo(AvatarSMDState.REACHABLE, state);
- }
- }
- */
- }
- }
- }
- }
- }
-/*
- for(String s: pvoa.getNonReachableEvents()) {
- index = s.indexOf("__");
- if (index != -1) {
- block = s.substring(index+2, s.length());
- index = block.indexOf("__");
- if (index != -1) {
- state = block.substring(index+2, block.length());
- block = block.substring(0, index);
- TraceManager.addDev("Block=" + block + " state=" + state);
- for(i=0; i<panels.size(); i++) {
- tdp = (TDiagramPanel)(panels.get(i));
- if ((tdp instanceof AvatarSMDPanel) && (tdp.getName().compareTo(block) == 0)){
- iterator = ((TDiagramPanel)(panels.get(i))).getComponentList().listIterator();
- while(iterator.hasNext()) {
- tgc = (TGComponent)(iterator.next());
- if (tgc instanceof AvatarSMDState) {
- ((AvatarSMDState)tgc).setSecurityInfo(AvatarSMDState.NOT_REACHABLE, state);
- }
- }
- }
- }
- }
- }
- }
-*/
- LinkedList<String> notProved = pvoa.getNotProved ();
- LinkedList<String> satisfied = pvoa.getSatisfiedAuthenticity ();
- LinkedList<String> satisfiedWeak = pvoa.getSatisfiedWeakAuthenticity ();
- LinkedList<String> nonSatisfied = pvoa.getNonSatisfiedAuthenticity ();
- }
-
-
- public void resetModelBacktracingProVerif() {
- /*if (abdp == null) {
- return;
- }
-
- // Reset confidential attributes
- for(AvatarBDBlock block1: abdp.getFullBlockList()) {
- block1.resetConfidentialityOfAttributes();
- }
- for (Object tgc: abdp.getComponentList()){
- if (tgc instanceof AvatarBDPragma){
- AvatarBDPragma pragma = (AvatarBDPragma) tgc;
- pragma.authStrongMap.clear();
- pragma.authWeakMap.clear();
-
- }
- }
- // Reset reachable states
- for(int i=0; i<panels.size(); i++) {
- tdp = (TDiagramPanel)(panels.get(i));
- if (tdp instanceof AvatarSMDPanel) {
- ((AvatarSMDPanel)tdp).resetStateSecurityInfo();
- }
- }*/
- }
}
diff --git a/src/ui/tmlcompd/TMLCPrimitivePort.java b/src/ui/tmlcompd/TMLCPrimitivePort.java
index 3de904fa193c8641eec765dd25f0c254478d76c2..cd667a7e6f7c38b7037f614c01323fb4b856f217 100755
--- a/src/ui/tmlcompd/TMLCPrimitivePort.java
+++ b/src/ui/tmlcompd/TMLCPrimitivePort.java
@@ -81,14 +81,21 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
protected boolean isPrex = false;
protected int lossPercentage;
protected int maxNbOfLoss; //-1 means no max
-
+
+ public int checkStatus;
+ public boolean checkConf;
+ public static int NOCHECK= 0;
+ public static int TOCHECK = 1;
+ public static int CHECKED_CONF = 2;
+ public static int CHECKED_UNCONF = 3;
+ public String mappingName="???";
protected int decPoint = 3;
protected boolean conflict = false;
protected String conflictMessage;
protected String dataFlowType = "VOID";
protected String associatedEvent = "VOID";
-
+ public int verification;
public TMLCPrimitivePort(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);
@@ -105,12 +112,12 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
editable = true;
removable = true;
userResizable = false;
-
+ checkConf=false;
commName = "comm";
//value = "MyName";
makeValue();
setName("Primitive port");
-
+ checkStatus= NOCHECK;
list = new TType[nbMaxAttribute];
for(int i=0; i<nbMaxAttribute; i++) {
list[i] = new TType();
@@ -311,14 +318,39 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
g.drawString(lname, x+width - w - 1, y+(int)(si)-2);
}
}*/
-
+ drawVerification(g);
g.setFont(fold);
-
+
drawParticularity(g);
}
public abstract void drawParticularity(Graphics g);
+ public void drawVerification(Graphics g){
+ Color c = g.getColor();
+ Color c1;
+ switch(checkStatus) {
+ case 1:
+ c1 = Color.gray;
+ break;
+ case 2:
+ c1 = Color.green;
+ break;
+ case 3:
+ c1 = Color.red;
+ break;
+ default:
+ return;
+ }
+ g.drawString(mappingName, x, y);
+ g.drawOval(x+6, y-10, 6, 9);
+ g.setColor(c1);
+ g.fillRect(x+4, y-7, 9, 7);
+ g.setColor(c);
+ g.drawRect(x+4, y-7, 9, 7);
+
+ }
+
public void manageMove() {
//System.out.println("Manage move!");
if (father != null) {
@@ -418,7 +450,7 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
otherTypes = tgc.getAllRecords();
}
- JDialogTMLCompositePort jda = new JDialogTMLCompositePort(commName, typep, list[0], list[1], list[2], list[3], list[4], isOrigin, isFinite, isBlocking, ""+maxSamples, ""+widthSamples, isLossy, lossPercentage, maxNbOfLoss, frame, "Port properties", otherTypes, dataFlowType, associatedEvent, isPrex, isPostex );
+ JDialogTMLCompositePort jda = new JDialogTMLCompositePort(commName, typep, list[0], list[1], list[2], list[3], list[4], isOrigin, isFinite, isBlocking, ""+maxSamples, ""+widthSamples, isLossy, lossPercentage, maxNbOfLoss, frame, "Port properties", otherTypes, dataFlowType, associatedEvent, isPrex, isPostex, checkConf);
jda.setSize(350, 700);
GraphicLib.centerOnParent(jda);
jda.show(); // blocked until dialog has been closed
@@ -447,6 +479,17 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
maxNbOfLoss = jda.getMaxNbOfLoss();
oldTypep = typep;
typep = jda.getPortType();
+ checkConf = jda.checkConf;
+ if (checkConf){
+ if (checkStatus==NOCHECK){
+ checkStatus=TOCHECK;
+ }
+ }
+ else {
+ if (checkStatus!=NOCHECK){
+ checkStatus=NOCHECK;
+ }
+ }
for(int i=0; i<nbMaxAttribute; i++) {
//TraceManager.addDev("Getting string type: " + jda.getStringType(i));
list[i].setType(jda.getStringType(i));
@@ -460,7 +503,7 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
((TMLComponentTaskDiagramPanel)tdp).updatePorts();
-
+
return true;
}
@@ -498,6 +541,8 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
sb.append("\" maxNbOfLoss=\"" + maxNbOfLoss);
sb.append("\" dataFlowType=\"" + dataFlowType);
sb.append("\" associatedEvent=\"" + associatedEvent);
+ sb.append("\" checkConf=\"" + checkConf);
+ sb.append("\" checkStatus=\"" + checkStatus);
sb.append("\" />\n");
for(int i=0; i<nbMaxAttribute; i++) {
//System.out.println("Attribute:" + i);
@@ -575,6 +620,8 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
maxNbOfLoss = Integer.decode(elt.getAttribute("maxNbOfLoss")).intValue();
dataFlowType = elt.getAttribute("dataFlowType");
associatedEvent = elt.getAttribute("associatedEvent");
+ checkConf = (elt.getAttribute("checkConf").compareTo("true")==0);
+ checkStatus = Integer.valueOf(elt.getAttribute("checkStatus"));
isLossy = (elt.getAttribute("isLossy").compareTo("true") ==0);
isPrex = (elt.getAttribute("isPrex").compareTo("true") ==0);
isPostex = (elt.getAttribute("isPostex").compareTo("true") ==0);
diff --git a/src/ui/window/JDialogTMLCompositePort.java b/src/ui/window/JDialogTMLCompositePort.java
index 55bb4cc7d3beda432470f1b38cf92ecc4d869795..ea71a81377f55764479f0498663f00c3c4d32dcf 100755
--- a/src/ui/window/JDialogTMLCompositePort.java
+++ b/src/ui/window/JDialogTMLCompositePort.java
@@ -72,9 +72,8 @@ public class JDialogTMLCompositePort extends javax.swing.JDialog implements Acti
private int maxNbOfLoss; //-1 means no max
public boolean data;
-
-
-
+ public boolean checkConf;
+ public boolean checkAuth = false;
// Panel1
private JTextField nameText, maxText, widthText, associatedEventJT;
private JComboBox typePort, typeList1, typeList2, typeList3, typeList4, typeList5;
@@ -85,7 +84,7 @@ public class JDialogTMLCompositePort extends javax.swing.JDialog implements Acti
private Vector<String> types;
// Robustness
- private JCheckBox isLossyBox, isPrexCB, isPostexCB;
+ private JCheckBox isLossyBox, isPrexCB, isPostexCB, confCheckBox, authCheckBox;
private JTextField lossPercentageText, maxNbOfLossText;
@@ -93,7 +92,7 @@ public class JDialogTMLCompositePort extends javax.swing.JDialog implements Acti
private JButton closeButton;
private JButton cancelButton;
- public JDialogTMLCompositePort(String _name, int _portIndex, TType _type1, TType _type2, TType _type3, TType _type4, TType _type5, boolean _isOrigin, boolean _isFinite, boolean _isBlocking, String _maxInFIFO, String _widthSamples, boolean _isLossy, int _lossPercentage, int _maxNbOfLoss, Frame f, String title, Vector<String> _types, String _dataFlowType, String _associatedEvent, boolean _isPrex, boolean _isPostex ) {
+ public JDialogTMLCompositePort(String _name, int _portIndex, TType _type1, TType _type2, TType _type3, TType _type4, TType _type5, boolean _isOrigin, boolean _isFinite, boolean _isBlocking, String _maxInFIFO, String _widthSamples, boolean _isLossy, int _lossPercentage, int _maxNbOfLoss, Frame f, String title, Vector<String> _types, String _dataFlowType, String _associatedEvent, boolean _isPrex, boolean _isPostex , boolean _checkConf) {
super(f, title, true);
frame = f;
@@ -105,20 +104,21 @@ public class JDialogTMLCompositePort extends javax.swing.JDialog implements Acti
data = false;
- dataFlowType = _dataFlowType;
- associatedEvent = _associatedEvent;
+ dataFlowType = _dataFlowType;
+ associatedEvent = _associatedEvent;
maxInFIFO = _maxInFIFO;
- widthSamples = _widthSamples;
- isOrigin = _isOrigin;
+ widthSamples = _widthSamples;
+ isOrigin = _isOrigin;
isFinite = _isFinite;
isBlocking = _isBlocking;
- isPrex = _isPrex;
- isPostex = _isPostex;
- isLossy = _isLossy;
- lossPercentage = _lossPercentage;
- maxNbOfLoss = _maxNbOfLoss;
-
+ isPrex = _isPrex;
+ isPostex = _isPostex;
+ isLossy = _isLossy;
+ lossPercentage = _lossPercentage;
+ maxNbOfLoss = _maxNbOfLoss;
+ checkConf = _checkConf;
+
myInitComponents();
initComponents();
checkMode();
@@ -273,6 +273,11 @@ public class JDialogTMLCompositePort extends javax.swing.JDialog implements Acti
c2.gridheight = 3;
panel2.add(new JLabel(" "), c2);
+ confCheckBox = new JCheckBox("Check Confidentiality");
+ panel2.add(confCheckBox, c2);
+ confCheckBox.setSelected(checkConf);
+ authCheckBox = new JCheckBox("Check Authenticity");
+ panel2.add(authCheckBox,c2);
c2.gridwidth = 1;
c2.fill = GridBagConstraints.HORIZONTAL;
c2.anchor = GridBagConstraints.CENTER;
@@ -562,6 +567,7 @@ public class JDialogTMLCompositePort extends javax.swing.JDialog implements Acti
associatedEvent = (String)associatedEventJT.getText();
isPrex = isPrexCB.isSelected();
isPostex = isPostexCB.isSelected();
+ checkConf = confCheckBox.isSelected();
if( isPrex && isPostex ) {
JOptionPane.showMessageDialog( frame, "A channel cannot be marked as both prex and postex", "Error",
JOptionPane.INFORMATION_MESSAGE );