From d9a033061b290f3421522598f06a51a138a70d65 Mon Sep 17 00:00:00 2001
From: Letitia Li <leli@enst.fr>
Date: Tue, 16 Feb 2016 16:33:55 +0000
Subject: [PATCH] Channel Confidentiality Check
---
src/ui/GTMLModeling.java | 118 ++++++++++++++++++++++++++++-----------
1 file changed, 86 insertions(+), 32 deletions(-)
diff --git a/src/ui/GTMLModeling.java b/src/ui/GTMLModeling.java
index 71d16699af..2c3a200322 100755
--- a/src/ui/GTMLModeling.java
+++ b/src/ui/GTMLModeling.java
@@ -58,6 +58,8 @@ import ui.tmlcp.*;
import ui.tmlsd.*;
import tmltranslator.*;
import tmltranslator.tmlcp.*;
+import tmltranslator.toproverif.*;
+import proverifspec.*;
import myutil.*;
import tmltranslator.ctranslator.*;
@@ -73,6 +75,7 @@ public class GTMLModeling {
private LinkedList removedChannels, removedRequests, removedEvents;
private static CorrespondanceTGElement listE;
private Hashtable<String, String> table;
+ public Map<String, Boolean> channelConfMap = new HashMap<String, Boolean>();
//private ArrayList<HwNode> nodesToTakeIntoAccount;
private LinkedList nodesToTakeIntoAccount;
@@ -3081,42 +3084,93 @@ public class GTMLModeling {
}
}
- TMLTask a;
- addTMLPragmas();
- for (String[] ss: tmlm.getPragmas()){
- if (ss[0].equals("#Confidentiality") && ss.length > 1){
- String task1 = ss[1].split("\\.")[0];
- String attr1 = ss[1].split("\\.")[1];
- a = tmlm.getTMLTaskByName(task1);
- if (a ==null){
- continue;
+ addTMLPragmas();
+ ArrayList<TMLChannel> channels = tmlm.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) map.getHwNodeOf(a);
+ for (TMLTask t: destinations){
+ List<HwBus> buses = new ArrayList<HwBus>();
+ HwNode node2 = map.getHwNodeOf(t);
+ if (node1==node2){
+ System.out.println("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is confidential");
+ channelConfMap.put(channel.getName(), true);
}
- HwCPU node1 = (HwCPU) map.getHwNodeOf(a);
- if (node1.encryption ==0){
- //If unencrypted
- ArrayList<TMLSendEvent> events = a.getSendEvents();
- List<TMLTask> destinations = new ArrayList<TMLTask>();
- for (TMLSendEvent event: events){
- String params = event.getAllParams();
- for (String param: params.split(",")){
- if (attr1.equals(param)){
- destinations.add(event.getEvent().getDestinationTask());
- }
+ if (node1!=node2){
+ //Navigate architecture for node
+ List<HwLink> links = archi.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);
+ }
}
- }
- for (TMLTask t: destinations){
- HwNode node2 = map.getHwNodeOf(t);
- if (node1!=node2){
- CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Confidentiality of " + ss[1]+ " not preserved.");
- ce.setTDiagramPanel(tmlap.tmlap);
- ce.setTGComponent(null);
- checkingErrors.add(ce);
- }
- }
+ 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());
+ }
+ else {
+ boolean priv=true;
+ HwBus bus;
+ //Check if all buses and bridges are private
+ for (HwNode n: path){
+ if (n instanceof HwBus){
+ bus = (HwBus) n;
+ if (bus.privacy ==0){
+ priv=false;
+ break;
+ }
+ }
+ }
+ channelConfMap.put(channel.getName(), priv);
+ System.out.println("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is " + (priv ? "confidential" : "not confidential"));
+ }
}
- }
}
-
+ }
}
public void addToTable(String s1, String s2) {
--
GitLab