diff --git a/src/Main.java b/src/Main.java index 7f94cfc29f19192731b840be5dd968a788f5374d..34435c5bfc409582836617ffa0f38d435982af38 100755 --- a/src/Main.java +++ b/src/Main.java @@ -161,7 +161,7 @@ public class Main implements ActionListener { } Locale.setDefault(new Locale("en")); - boolean startLauncher = false; + boolean startLauncher = true; // Analyzing arguments String config = "config.xml"; @@ -274,7 +274,7 @@ public class Main implements ActionListener { } - ConfigurationTTool.makeDefaultConfiguration(); + //ConfigurationTTool.makeDefaultConfiguration(); try { ConfigurationTTool.loadConfiguration(config, systemc); } catch (Exception e) { diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java index 2d01dc289fc38d92c27fbe8660d1d3a02aeab0bf..4a9a8bfd15ca66247a3d057892e5f1dfd13c4ef1 100755 --- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java +++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java @@ -827,7 +827,7 @@ public class AVATAR2ProVerif { action += "let " + makeAttrName(blockName, pubK) + " = pk(" + makeAttrName(blockName, privK) + ") in \n"; action += "out(ch, " + makeAttrName(blockName, pubK) + ");\n"; - TraceManager.addDev("Putting :" + makeAttrName(blockName, pubK + " -> " + makeAttrName(blockName, pubK))); + //TraceManager.addDev("********************************* Putting :" + makeAttrName(blockName, pubK + " -> " + makeAttrName(blockName, pubK))); declarations.put(makeAttrName(blockName, pubK), makeAttrName(blockName, pubK)); } } diff --git a/src/ui/AvatarDesignPanel.java b/src/ui/AvatarDesignPanel.java index 3bdbfe9f7ad82ab5d58a73eb0f97f4c135596c89..77502b6fb50cca6b56f5470f8d7c61c5f0c4fe01 100644 --- a/src/ui/AvatarDesignPanel.java +++ b/src/ui/AvatarDesignPanel.java @@ -53,6 +53,9 @@ import java.util.*; import ui.avatarbd.*; import ui.avatarsmd.*; + +import proverifspec.*; + import myutil.*; public class AvatarDesignPanel extends TURTLEPanel { @@ -60,8 +63,6 @@ public class AvatarDesignPanel extends TURTLEPanel { // public Vector validated, ignored; - - public AvatarDesignPanel(MainGUI _mgui) { super(_mgui); tabbedPane = new JTabbedPane(); @@ -300,6 +301,124 @@ public class AvatarDesignPanel extends TURTLEPanel { } + public void modelBacktracingProVerif(ProVerifOutputAnalyzer pvoa) { + + + if (abdp == null) { + return; + } + + String block, attr, state; + int index; + TAttribute a; + int i; + ListIterator iterator; + TGComponent tgc; + + // Confidential attributes + for(AvatarBDBlock block1: abdp.getFullBlockList()) { + block1.resetConfidentialityOfAttributes(); + } + + for(String s: pvoa.getSecretTerms()) { + index = s.indexOf("__"); + if (index != -1) { + block = s.substring(0, index); + attr = s.substring(index+2, s.length()); + index = attr.indexOf("__"); + if (index != -1) { + attr = attr.substring(0, index); + } + TraceManager.addDev("Analyzing block=" + block + " attr=" + attr); + a = abdp.getAttributeByBlockName(block, attr); + if (a != null) { + TraceManager.addDev("Setting conf to ok"); + a.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_OK); + } + } + } + + for(String s: pvoa.getNonSecretTerms()) { + index = s.indexOf("__"); + if (index != -1) { + block = s.substring(0, index); + attr = s.substring(index+2, s.length()); + index = attr.indexOf("__"); + if (index != -1) { + attr = attr.substring(0, index); + } + TraceManager.addDev("Analyzing block=" + block + " attr=" + attr); + a = abdp.getAttributeByBlockName(block, attr); + if (a != null) { + TraceManager.addDev("Setting conf to ok"); + a.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_KO); + } + } + } + + // Reachable states + // Reset states + for(i=0; i<panels.size(); i++) { + tdp = (TDiagramPanel)(panels.get(i)); + if (tdp instanceof AvatarSMDPanel) { + ((AvatarSMDPanel)tdp).resetStateSecurityInfo(); + } + } + + 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); + 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.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); + } + } + + } + } + } + } + } + + } + } \ No newline at end of file diff --git a/src/ui/ConfigurationTTool.java b/src/ui/ConfigurationTTool.java index 75705a3c829d03c80b1af2a74816542933065962..be8715f4414da338a9b83006fdf440dbb6b67384 100755 --- a/src/ui/ConfigurationTTool.java +++ b/src/ui/ConfigurationTTool.java @@ -1271,4 +1271,8 @@ public class ConfigurationTTool { } } + public static boolean isConfigured(String s) { + return ((s != null) && (s.trim().length() > 0)); + } + } // \ No newline at end of file diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java index ad94e71274a89f43e10cfac48bb2d4a437d959cb..0027a10eaa90158db5014162f321743f203e5458 100755 --- a/src/ui/MainGUI.java +++ b/src/ui/MainGUI.java @@ -96,6 +96,8 @@ import ui.avatarpd.*; import ui.avatarcd.*; import ui.avatarad.*; +import proverifspec.*; + public class MainGUI implements ActionListener, WindowListener, KeyListener, PeriodicBehavior { public static boolean systemcOn; @@ -3309,6 +3311,21 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per public Vector getCheckingWarnings() { return gtm.getCheckingWarnings(); } + + public void modelBacktracingProVerif(ProVerifOutputAnalyzer pvoa) { + TURTLEPanel tp = getCurrentTURTLEPanel(); + if (tp == null) { + return; + } + + if (!(tp instanceof AvatarDesignPanel)) { + return; + } + + AvatarDesignPanel adp = (AvatarDesignPanel)tp; + adp.modelBacktracingProVerif(pvoa); + getCurrentTDiagramPanel().repaint(); + } public void generateRTLOTOS() { generateRTLOTOS(false); diff --git a/src/ui/TAttribute.java b/src/ui/TAttribute.java index 7309d0b5a77da5b5e1cdbc4b8a32b6101881d736..72d193b63abeedec2d2b6aa16bbd1a960f212ad6 100755 --- a/src/ui/TAttribute.java +++ b/src/ui/TAttribute.java @@ -73,6 +73,12 @@ public class TAttribute { public final static int ARRAY_NAT = 7; public final static int INTEGER = 8; public final static int TIMER = 9; + + // Confidentiality verififcation + public final static int NOT_VERIFIED = 0; + public final static int CONFIDENTIALITY_OK = 1; + public final static int CONFIDENTIALITY_KO = 2; + public final static int COULD_NOT_VERIFY_CONFIDENTIALITY = 3; private int access; @@ -80,6 +86,8 @@ public class TAttribute { private String initialValue; private int type; private String typeOther; + + private int confidentialityVerification = NOT_VERIFIED; public boolean isAvatar; @@ -459,4 +467,12 @@ public class TAttribute { ta.isAvatar = isAvatar; return ta; } + + public int getConfidentialityVerification() { + return confidentialityVerification; + } + + public void setConfidentialityVerification(int _confidentialityVerification) { + confidentialityVerification = _confidentialityVerification; + } } \ No newline at end of file diff --git a/src/ui/avatarbd/AvatarBDBlock.java b/src/ui/avatarbd/AvatarBDBlock.java index f0946a57356e5f708de2fce36afa8d783c6bf1c9..af69cad7006ec5bcf3f6f05529fb2008920db1f1 100644 --- a/src/ui/avatarbd/AvatarBDBlock.java +++ b/src/ui/avatarbd/AvatarBDBlock.java @@ -63,7 +63,8 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S private static String GLOBAL_CODE_INFO = "(global code)"; private int textY1 = 3; - private String stereotype = "block"; + private static String stereotype = "block"; + private static String stereotypeCrypto = "cryptoblock"; private int maxFontSize = 12; private int minFontSize = 4; @@ -79,6 +80,8 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S private int iconSize = 15; private boolean iconIsDrawn = false; + private boolean isCryptoBlock = false; + // TAttribute, AvatarMethod, AvatarSignal protected Vector myAttributes, myMethods, mySignals; @@ -143,7 +146,12 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S } public void internalDrawing(Graphics g) { - String ster = "<<" + stereotype + ">>"; + String ster; + if (!isCryptoBlock) { + ster = "<<" + stereotype + ">>"; + } else { + ster = "<<" + stereotypeCrypto + ">>"; + } Font f = g.getFont(); Font fold = f; @@ -265,12 +273,17 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S w = g.getFontMetrics().stringWidth(attr); if ((w + (2 * textX) + 1) < width) { g.drawString(attr, x + textX, y + cpt); + if (a.getConfidentialityVerification() > 0) { + //TraceManager.addDev("Drawing confidentiality for " + a.getId()); + drawConfidentialityVerification(a.getConfidentialityVerification(), g, x, y+cpt); + } limitAttr = y + cpt; } else { attr = "..."; w = g.getFontMetrics().stringWidth(attr); if ((w + textX + 2) < width) { g.drawString(attr, x + textX + 1, y + cpt); + limitAttr = y + cpt; } else { // skip attribute @@ -404,7 +417,33 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S //g.drawImage(IconManager.imgic1100.getImage(), x + 4, y + 4, null); //g.drawImage(IconManager.img9, x + width - 20, y + 4, null); } - + + + private void drawConfidentialityVerification(int confidentialityVerification, Graphics g, int _x, int _y) { + Color c = g.getColor(); + Color c1; + switch(confidentialityVerification) { + case TAttribute.CONFIDENTIALITY_OK: + c1 = Color.green; + break; + case TAttribute.CONFIDENTIALITY_KO: + c1 = Color.red; + break; + case TAttribute.COULD_NOT_VERIFY_CONFIDENTIALITY: + c1 = Color.orange; + break; + default: + return; + } + + 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 TGComponent isOnOnlyMe(int x1, int y1) { @@ -647,6 +686,7 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S //System.out.println("Loading extra params of " + value); //value = ""; StringBuffer sb = new StringBuffer("<extraparam>\n"); + sb.append("<CryptoBlock value=\"" + isCryptoBlock + "\" />\n"); for(int i=0; i<myAttributes.size(); i++) { //System.out.println("Attribute:" + i); a = (TAttribute)(myAttributes.elementAt(i)); @@ -710,6 +750,7 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S AvatarMethod am; AvatarSignal as; boolean implementation = false; + String crypt; //System.out.println("Loading attributes"); @@ -725,6 +766,12 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S //System.out.println(n2); if (n2.getNodeType() == Node.ELEMENT_NODE) { elt = (Element) n2; + if (elt.getTagName().equals("CryptoBlock")) { + crypt = elt.getAttribute("value"); + if (crypt.compareTo("true") == 0) { + isCryptoBlock = true; + } + } if (elt.getTagName().equals("Attribute")) { //System.out.println("Analyzing attribute"); access = Integer.decode(elt.getAttribute("access")).intValue(); @@ -764,6 +811,10 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S implementation = false; } + if (method.startsWith("aencrypt(")) { + isCryptoBlock = true; + } + am = AvatarMethod.isAValidMethod(method); if (am != null) { TraceManager.addDev("Setting to " + implementation + " the implementation of " + am); @@ -912,6 +963,17 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S return myAttributes; } + public TAttribute getAttributeByName(String _name) { + TAttribute a; + for(int i=0; i<myAttributes.size(); i++) { + a = (TAttribute)(myAttributes.elementAt(i)); + if (a.getId().compareTo(_name) == 0) { + return a; + } + } + return null; + } + public Vector getMethodList() { return myMethods; } @@ -1006,6 +1068,8 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S } public void addCryptoElements() { + isCryptoBlock = true; + // Adding function String method = "Message aencrypt(Message msg, Key k)"; addMethodIfApplicable(myMethods, method); @@ -1163,6 +1227,15 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S public ImageIcon getImageIcon() { return myImageIcon; } + + public void resetConfidentialityOfAttributes() { + TAttribute a; + + for(int i=0; i<myAttributes.size(); i++) { + a = (TAttribute)(myAttributes.elementAt(i)); + a.setConfidentialityVerification(TAttribute.NOT_VERIFIED); + } + } diff --git a/src/ui/avatarbd/AvatarBDPanel.java b/src/ui/avatarbd/AvatarBDPanel.java index c9115863043e26b9f81bd8ff9d0370d23156af95..e24bd45f74d39da9986e3dbfad19fdd1c58b1068 100644 --- a/src/ui/avatarbd/AvatarBDPanel.java +++ b/src/ui/avatarbd/AvatarBDPanel.java @@ -410,6 +410,16 @@ public class AvatarBDPanel extends TDiagramPanel { return list; } + public TAttribute getAttributeByBlockName(String _blockName, String attributeName) { + TAttribute a; + for(AvatarBDBlock block: getFullBlockList()) { + if (block.getBlockName().compareTo(_blockName) == 0) { + return block.getAttributeByName(attributeName); + } + } + return null; + } + public Vector getAllAttributesOfBlock(String _name) { LinkedList<AvatarBDBlock> list = getFullBlockList(); for(AvatarBDBlock block: list) { diff --git a/src/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java b/src/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java index 4f993340d8f4af54f3fb60b470dc3e5cbb8961a5..45210b89f1471b11768c66cec05c4e29b0a14900 100755 --- a/src/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java +++ b/src/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java @@ -1399,15 +1399,16 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements AvatarS } - if (ConfigurationTTool.IMGPath != null) { + if (ConfigurationTTool.isConfigured(ConfigurationTTool.IMGPath)) { fileName = ConfigurationTTool.IMGPath + System.getProperty("file.separator") + fileName; } else { // Using model directory String path = mgui.getModelFileFullPath(); fileName = path.substring(0,path.lastIndexOf(File.separator)+1) + fileName; + TraceManager.addDev("New Filename = " + fileName); } - TraceManager.addDev("New Filename = " + fileName); + boolean ok = true; @@ -1458,8 +1459,13 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements AvatarS fileName += "simulationtrace_fromttool.svg"; } - if (ConfigurationTTool.IMGPath != null) { + if (ConfigurationTTool.isConfigured(ConfigurationTTool.IMGPath)) { fileName = ConfigurationTTool.IMGPath + System.getProperty("file.separator") + fileName; + } else { + // Using model directory + String path = mgui.getModelFileFullPath(); + fileName = path.substring(0,path.lastIndexOf(File.separator)+1) + fileName; + TraceManager.addDev("New Filename = " + fileName); } boolean ok = true; @@ -1527,11 +1533,14 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements AvatarS bi = sdpanel.performCapture(); String filePath=""; - if (ConfigurationTTool.IMGPath != null) { + if (ConfigurationTTool.isConfigured(ConfigurationTTool.IMGPath)) { filePath += ConfigurationTTool.IMGPath; if (!filePath.endsWith(File.separator)) { filePath += File.separator; } + } else { + String path = mgui.getModelFileFullPath(); + filePath = path.substring(0,path.lastIndexOf(File.separator)+1); } if ((saveFileName.getText() != null) && (saveFileName.getText().length() > 0)) { diff --git a/src/ui/avatarsmd/AvatarSMDPanel.java b/src/ui/avatarsmd/AvatarSMDPanel.java index 084e58ec42c4cee2782f56fdd10c38e3e844500d..4b07a3a33c6554e37d799867d047af7eb43a8de5 100755 --- a/src/ui/avatarsmd/AvatarSMDPanel.java +++ b/src/ui/avatarsmd/AvatarSMDPanel.java @@ -332,5 +332,17 @@ public class AvatarSMDPanel extends TDiagramPanel implements TDPWithAttributes { } //TraceManager.addDev("End Autoconnect"); } + + public void resetStateSecurityInfo() { + ListIterator iterator = getComponentList().listIterator(); + TGComponent tgc; + + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + if (tgc instanceof AvatarSMDState) { + ((AvatarSMDState)tgc).resetSecurityInfo(); + } + } + } } diff --git a/src/ui/avatarsmd/AvatarSMDState.java b/src/ui/avatarsmd/AvatarSMDState.java index 3e8cd107f0866001e51aa9f9ea623d83b3683e4f..2d3f7f10df908706025d01648703d7e6b906ff2f 100644 --- a/src/ui/avatarsmd/AvatarSMDState.java +++ b/src/ui/avatarsmd/AvatarSMDState.java @@ -73,6 +73,13 @@ public class AvatarSMDState extends TGCScalableWithInternalComponent implements protected String [] entryCode; + // Security + public final static int NOT_VERIFIED = 0; + public final static int REACHABLE = 1; + public final static int NOT_REACHABLE = 2; + + protected int securityInformation; + public String oldValue; protected Vector<AvatarSMDState> mutexStates; @@ -287,6 +294,35 @@ public class AvatarSMDState extends TGCScalableWithInternalComponent implements } drawAttributes(g, s); }*/ + + drawSecurityInformation(g); + } + + public void drawSecurityInformation(Graphics g) { + if (securityInformation > 0) { + + Color c = g.getColor(); + Color c1; + switch(securityInformation) { + case REACHABLE: + c1 = Color.green; + break; + case NOT_REACHABLE: + c1 = Color.red; + break; + default: + return; + } + + GraphicLib.arrowWithLine(g, 1, 0, 10, x-30, y+4, x-15, y+4, true); + g.drawOval(x-11, y-3, 7, 9); + g.setColor(c1); + g.fillRect(x-12, y, 9, 7); + g.setColor(c); + g.drawRect(x-12, y, 9, 7); + + } + } @@ -726,5 +762,30 @@ public class AvatarSMDState extends TGCScalableWithInternalComponent implements return ret; } + + public void resetSecurityInfo() { + securityInformation = NOT_VERIFIED; + for(int i=0; i<nbInternalTGComponent; i++) { + if (tgcomponent[i] instanceof AvatarSMDState) { + ((AvatarSMDState)tgcomponent[i]).resetSecurityInfo(); + } + } + + } + + public void setSecurityInfo(int _info, String _name) { + //TraceManager.addDev("Testing " + getValue() + " with state " + _name); + if (getValue().compareTo(_name) == 0) { + //TraceManager.addDev("Setting state " + _name + " as info=" + _info); + securityInformation = _info; + } + for(int i=0; i<nbInternalTGComponent; i++) { + if (tgcomponent[i] instanceof AvatarSMDState) { + ((AvatarSMDState)tgcomponent[i]).setSecurityInfo(_info, _name); + } + } + + } + } diff --git a/src/ui/window/JDialogProVerifGeneration.java b/src/ui/window/JDialogProVerifGeneration.java index 17dcbce3025948edfac9b4f4e15571ffa929d5c3..a858cb2fcd8252cd8af0740ddcbef57bfe467cf0 100644 --- a/src/ui/window/JDialogProVerifGeneration.java +++ b/src/ui/window/JDialogProVerifGeneration.java @@ -399,6 +399,8 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac } } + mgui.modelBacktracingProVerif(pvoa); + jta.append("\nAll done\n"); } catch (LauncherException le) { jta.append("Error: " + le.getMessage() + "\n");