Skip to content
Snippets Groups Projects
Commit 705c3896 authored by jawher-j's avatar jawher-j
Browse files

Generate security for Conf and Weak Auth properties

parent 657e739d
No related branches found
No related tags found
1 merge request!500Auto security diplodocus
...@@ -40,13 +40,13 @@ ...@@ -40,13 +40,13 @@
package tmltranslator.patternhandling; package tmltranslator.patternhandling;
/** /**
* Class SecurityGenerationForTMAP * Class SecurityGenerationForTMAP
* *
* Creation: 28/09/2023 * Creation: 28/09/2023
* *
* @author Jawher JERRAY * @author Jawher JERRAY
* @version 1.0 28/09/2023 * @version 1.0 28/09/2023
*/ */
import avatartranslator.AvatarPragma; import avatartranslator.AvatarPragma;
import avatartranslator.AvatarPragmaAuthenticity; import avatartranslator.AvatarPragmaAuthenticity;
import avatartranslator.AvatarPragmaSecret; import avatartranslator.AvatarPragmaSecret;
...@@ -68,28 +68,26 @@ import java.util.*; ...@@ -68,28 +68,26 @@ import java.util.*;
public class SecurityGenerationForTMAP implements Runnable { public class SecurityGenerationForTMAP implements Runnable {
final private String SELECT_CHOICE_HSM = "channelIndex"; final private String SELECT_CHOICE_HSM = "channelIndex";
private String appName; private final String appName;
private TMLMapping<?> tmap; private final TMLMapping<?> tmap;
private String encComp; private final String encComp;
private String overhead; private final String overhead;
private String decComp; private final String decComp;
private Map<String, List<String>> selectedCPUTasks; private final Map<String, List<String>> selectedCPUTasks;
private AVATAR2ProVerif avatar2proverif; private final Map<TMLTask, TMLTask> taskAndItsHSMMap = new HashMap<>();
private final Map<TMLTask, List<HwCommunicationNode>> taskHSMCommunicationNodesMap = new HashMap<>();
private Map<TMLTask, TMLTask> taskAndItsHSMMap = new HashMap<TMLTask, TMLTask>(); private final Map<TMLTask, List<TMLActivityElement>> taskHSMBranchesMap = new HashMap<>();
private Map<TMLTask, List<HwCommunicationNode>> taskHSMCommunicationNodesMap = new HashMap<TMLTask, List<HwCommunicationNode>>(); private final Map<Pair<TMLTask, TMLTask>, SecurityPattern> tasksNonceSPMap = new HashMap<>();
private Map<TMLTask, List<TMLActivityElement>> taskHSMBranchesMap = new HashMap<TMLTask, List<TMLActivityElement>>(); private final Map<Pair<TMLTask, TMLTask>, TMLChannel> tasksNonceChannelMap = new HashMap<>();
private Map<Pair<TMLTask, TMLTask>, SecurityPattern> tasksNonceSPMap = new HashMap<Pair<TMLTask, TMLTask>, SecurityPattern>(); private final Map<TMLChannel, TMLChannel> channelNonceToHsmMap = new HashMap<>();
private Map<Pair<TMLTask, TMLTask>, TMLChannel> tasksNonceChannelMap = new HashMap<Pair<TMLTask, TMLTask>, TMLChannel>(); private final Map<TMLChannel, TMLChannel> channelNonceFromHsmMap = new HashMap<>();
private Map<TMLChannel, TMLChannel> channelNonceToHsmMap = new HashMap<TMLChannel, TMLChannel>(); private final Map<TMLTask, TMLRequest> hsmTaskRequestMap = new HashMap<>();
private Map<TMLChannel, TMLChannel> channelNonceFromHsmMap = new HashMap<TMLChannel, TMLChannel>(); private final Map<Pair<TMLTask, TMLChannel>, TMLChannel> channelToHsmMap = new HashMap<>();
private Map<TMLTask, TMLRequest> hsmTaskRequestMap = new HashMap<TMLTask, TMLRequest>(); private final Map<Pair<TMLTask, TMLChannel>, TMLChannel> channelFromHsmMap = new HashMap<>();
private Map<Pair<TMLTask, TMLChannel>, TMLChannel> channelToHsmMap = new HashMap<Pair<TMLTask, TMLChannel>, TMLChannel>();
private Map<Pair<TMLTask, TMLChannel>, TMLChannel> channelFromHsmMap = new HashMap<Pair<TMLTask, TMLChannel>, TMLChannel>(); public SecurityGenerationForTMAP(String appName, TMLMapping<?> tmap, String encComp, String overhead, String decComp,
private Map<TMLChannel, SecurityPattern> channelSecMap = new HashMap<TMLChannel, SecurityPattern>(); Map<String, List<String>> selectedCPUTasks) {
public SecurityGenerationForTMAP(String appName, TMLMapping<?> tmap, String encComp, String overhead, String decComp, Map<String, List<String>> selectedCPUTasks) {
this.appName = appName; this.appName = appName;
this.tmap = tmap; this.tmap = tmap;
this.overhead = overhead; this.overhead = overhead;
...@@ -98,14 +96,14 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -98,14 +96,14 @@ public class SecurityGenerationForTMAP implements Runnable {
this.selectedCPUTasks = selectedCPUTasks; this.selectedCPUTasks = selectedCPUTasks;
} }
public void proverifAnalysis(TMLMapping<?> tmap, List<TMLChannel> nonConfChans, List<TMLChannel> nonWeakAuthChans, List<TMLChannel> nonStrongAuthChans) { private void proverifAnalysis(TMLMapping<?> tmap, List<TMLChannel> nonConfChans, List<TMLChannel> nonWeakAuthChans,
List<TMLChannel> nonStrongAuthChans) {
if (tmap == null) { if (tmap == null) {
TraceManager.addDev("No mapping"); TraceManager.addDev("No mapping");
return; return;
} }
//Perform ProVerif Analysis //Perform ProVerif Analysis
Object o = null; Object o = null;
if (tmap.getTMLModeling().getReference() instanceof TGComponent) { if (tmap.getTMLModeling().getReference() instanceof TGComponent) {
o = ((TGComponent)(tmap.getTMLModeling().getReference())).getTDiagramPanel().tp; o = ((TGComponent)(tmap.getTMLModeling().getReference())).getTDiagramPanel().tp;
...@@ -118,9 +116,9 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -118,9 +116,9 @@ public class SecurityGenerationForTMAP implements Runnable {
return; return;
} }
avatar2proverif = new AVATAR2ProVerif(avatarspec); AVATAR2ProVerif avatar2proverif = new AVATAR2ProVerif(avatarspec);
try { try {
ProVerifSpec proverif = avatar2proverif.generateProVerif(true, true, 3, true, true); avatar2proverif.generateProVerif(true, true, 3, true, true);
//warnings = avatar2proverif.getWarnings(); //warnings = avatar2proverif.getWarnings();
if (!avatar2proverif.saveInFile("pvspec")) { if (!avatar2proverif.saveInFile("pvspec")) {
...@@ -146,7 +144,7 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -146,7 +144,7 @@ public class SecurityGenerationForTMAP implements Runnable {
Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authenticityResults = pvoa.getAuthenticityResults(); Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authenticityResults = pvoa.getAuthenticityResults();
for (TMLChannel ch : tmap.getTMLModeling().getSecChannelMap().keySet()) { for (TMLChannel ch : tmap.getTMLModeling().getSecChannelMap().keySet()) {
if (ch.isCheckConfChannel()) { if (ch.isCheckConfChannel()) {
List<Integer> confStatus = new ArrayList<Integer>(); List<Integer> confStatus = new ArrayList<>();
for (AvatarPragma pragma : tmap.getTMLModeling().getSecChannelMap().get(ch)) { for (AvatarPragma pragma : tmap.getTMLModeling().getSecChannelMap().get(ch)) {
if (pragma instanceof AvatarPragmaSecret) { if (pragma instanceof AvatarPragmaSecret) {
AvatarPragmaSecret pragmaSecret = (AvatarPragmaSecret) pragma; AvatarPragmaSecret pragmaSecret = (AvatarPragmaSecret) pragma;
...@@ -176,8 +174,8 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -176,8 +174,8 @@ public class SecurityGenerationForTMAP implements Runnable {
} }
} }
if (ch.isCheckAuthChannel()) { if (ch.isCheckAuthChannel()) {
List<Integer> weakAuthStatus = new ArrayList<Integer>(); List<Integer> weakAuthStatus = new ArrayList<>();
List<Integer> strongAuthStatus = new ArrayList<Integer>(); List<Integer> strongAuthStatus = new ArrayList<>();
for (AvatarPragma pragma : tmap.getTMLModeling().getSecChannelMap().get(ch)) { for (AvatarPragma pragma : tmap.getTMLModeling().getSecChannelMap().get(ch)) {
if (pragma instanceof AvatarPragmaAuthenticity) { if (pragma instanceof AvatarPragmaAuthenticity) {
AvatarPragmaAuthenticity pragmaAuth = (AvatarPragmaAuthenticity) pragma; AvatarPragmaAuthenticity pragmaAuth = (AvatarPragmaAuthenticity) pragma;
...@@ -232,8 +230,7 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -232,8 +230,7 @@ public class SecurityGenerationForTMAP implements Runnable {
} }
} catch (Exception e) { } catch (Exception e) {
System.out.println("SECGEN EXCEPTION " + e); TraceManager.addDev("SECGEN EXCEPTION " + e);
} }
} }
...@@ -244,39 +241,16 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -244,39 +241,16 @@ public class SecurityGenerationForTMAP implements Runnable {
t.join(); t.join();
} catch (Exception e) { } catch (Exception e) {
TraceManager.addDev("SECGEN. Error in Security Generation Thread"); TraceManager.addDev("SECGEN. Error in Security Generation Thread");
System.out.println("SECGEN. Error in Security Generation Thread");
} }
return tmap; return tmap;
} }
public boolean portInTask(TMLTask task, TMLChannel ch) {
TMLActivity adTask = task.getActivityDiagram();
for (TMLActivityElement elem : adTask.getElements()) {
if (elem instanceof TMLWriteChannel) {
TMLWriteChannel writeChannel = (TMLWriteChannel) elem;
for (int i = 0; i < writeChannel.getNbOfChannels(); i++) {
if (writeChannel.getChannel(i).equals(ch)) {
return true;
}
}
} else if (elem instanceof TMLReadChannel) {
TMLReadChannel readChannel = (TMLReadChannel) elem;
for (int i = 0; i < readChannel.getNbOfChannels(); i++) {
if (readChannel.getChannel(i).equals(ch)) {
return true;
}
}
}
}
return false;
}
public void run() { public void run() {
TMLModeling<?> tmlmodel = tmap.getTMLModeling(); TMLModeling<?> tmlmodel = tmap.getTMLModeling();
//Proverif Analysis channels //Proverif Analysis channels
List<TMLChannel> nonConfChans = new ArrayList<TMLChannel>(); List<TMLChannel> nonConfChans = new ArrayList<>();
List<TMLChannel> nonWeakAuthChans = new ArrayList<TMLChannel>(); List<TMLChannel> nonWeakAuthChans = new ArrayList<>();
List<TMLChannel> nonStrongAuthChans = new ArrayList<TMLChannel>(); List<TMLChannel> nonStrongAuthChans = new ArrayList<>();
List<TMLChannel> channels = tmlmodel.getChannels(); List<TMLChannel> channels = tmlmodel.getChannels();
for (TMLChannel channel : channels) { for (TMLChannel channel : channels) {
...@@ -310,22 +284,22 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -310,22 +284,22 @@ public class SecurityGenerationForTMAP implements Runnable {
//With the proverif results, check which channels need to be secured //With the proverif results, check which channels need to be secured
HashSet<TMLChannel> chAddCSA = new HashSet<TMLChannel>(); HashSet<TMLChannel> chAddCSA = new HashSet<>();
HashSet<TMLChannel> chAddCWA = new HashSet<TMLChannel>(); HashSet<TMLChannel> chAddCWA = new HashSet<>();
HashSet<TMLChannel> chAddSA = new HashSet<TMLChannel>(); HashSet<TMLChannel> chAddSA = new HashSet<>();
HashSet<TMLChannel> chAddWA = new HashSet<TMLChannel>(); HashSet<TMLChannel> chAddWA = new HashSet<>();
HashSet<TMLChannel> chAddC = new HashSet<TMLChannel>(); HashSet<TMLChannel> chAddC = new HashSet<>();
for (TMLChannel chan : tmlmodel.getChannels()) { for (TMLChannel chan : tmlmodel.getChannels()) {
boolean nonConf = nonConfChans.contains(chan); boolean nonConf = nonConfChans.contains(chan);
boolean nonWeakAuth = nonWeakAuthChans.contains(chan); boolean nonWeakAuth = nonWeakAuthChans.contains(chan);
boolean nonStrongAuth = nonStrongAuthChans.contains(chan); boolean nonStrongAuth = nonStrongAuthChans.contains(chan);
// add Confidentiality and Strong Authenticity // add Confidentiality and Strong Authenticity
if (chan.isSecurityGoalConf() && nonConf && chan.isSecurityGoalStrongAuth() && nonStrongAuth) { if (chan.isSecurityGoalConf() && chan.isSecurityGoalStrongAuth() && (nonStrongAuth || nonConf)) {
chAddCSA.add(chan); chAddCSA.add(chan);
} }
// add Confidentiality and Weak Authenticity // add Confidentiality and Weak Authenticity
else if (chan.isSecurityGoalConf() && nonConf && chan.isSecurityGoalWeakAuth() && nonWeakAuth) { else if (chan.isSecurityGoalConf() && chan.isSecurityGoalWeakAuth() && (nonWeakAuth || nonConf)) {
chAddCWA.add(chan); chAddCWA.add(chan);
} }
// add Strong Authenticity // add Strong Authenticity
...@@ -355,80 +329,54 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -355,80 +329,54 @@ public class SecurityGenerationForTMAP implements Runnable {
SecurityPattern secPattern = new SecurityPattern(secPatternName, SecurityPattern.SYMMETRIC_ENC_PATTERN, overhead, "", SecurityPattern secPattern = new SecurityPattern(secPatternName, SecurityPattern.SYMMETRIC_ENC_PATTERN, overhead, "",
encComp, decComp, spNonce.getName(), "", ""); encComp, decComp, spNonce.getName(), "", "");
channelSecMap.put(ch, secPattern); HandleSecurityGoalsForChannels(tmlmodel, ch, secPattern, !nonceChannelExist, spNonce, chNonce);
tmlmodel.addSecurityPattern(secPattern); }
List<TMLWriteChannel> listWr = WriteOperatorsOfChannel(ch.getOriginTask(), ch); HashSet<TMLChannel> chAddCAndCWA = new HashSet<>(chAddCWA);
List<TMLReadChannel> listRd = ReadOperatorsOfChannel(ch.getDestinationTask(), ch); chAddCAndCWA.addAll(chAddC);
if (taskAndItsHSMMap.containsKey(ch.getOriginTask())) {
TMLTask hsmTask = taskAndItsHSMMap.get(ch.getOriginTask());
TMLChannel chToHSM = FindOrCreateChannelToHSM(hsmTask, ch.getOriginTask(), ch);
TMLChannel chFromHSM = FindOrCreateChannelFromHSM(hsmTask, ch.getOriginTask(), ch);
addToSecurityTaskMap(hsmTask, secPattern);
if (!nonceChannelExist) {
TMLActivityElement NonceBranch = addNonceExchangeBranchHSM(hsmTask, channelNonceToHsmMap.get(chNonce), spNonce, false);
taskHSMBranchesMap.get(hsmTask).add(NonceBranch);
nonceCommunicationWithHsmAD(ch.getOriginTask(), spNonce, channelNonceToHsmMap.get(chNonce), hsmTaskRequestMap.get(hsmTask),
taskHSMBranchesMap.get(hsmTask).size() - 1, true, chNonce, ch.getOriginTask().getActivityDiagram().getFirst());
}
try {
TMLActivityElement branch = addBranchHSM(hsmTask, chToHSM, chFromHSM, secPattern, true);
taskHSMBranchesMap.get(hsmTask).add(branch);
} catch (TMLCheckingError e) {
throw new RuntimeException(e);
}
for (TMLWriteChannel wr : listWr) { for (TMLChannel ch : chAddCAndCWA) {
communicationWithHSMAD(ch.getOriginTask(), wr, secPattern, chToHSM, chFromHSM, hsmTaskRequestMap.get(hsmTask), taskHSMBranchesMap.get(hsmTask).size()-1); String secPatternNameInit = "se_" + ch.getChannelName();
} String secPatternName = secPatternNameInit;
} else { int index = 0;
addToSecurityTaskMap(ch.getOriginTask(), secPattern); while (tmap.getSecurityPatternByName(secPatternName) != null) {
try { secPatternName = secPatternNameInit + index;
addEncryptionAD(ch.getOriginTask(), listWr, secPattern); index ++;
} catch (TMLCheckingError e) {
throw new RuntimeException(e);
}
if (!nonceChannelExist) {
addNonceReceiveAD(ch.getOriginTask(), chNonce, spNonce, ch.getOriginTask().getActivityDiagram().getFirst());
}
} }
if (taskAndItsHSMMap.containsKey(ch.getDestinationTask())) { SecurityPattern secPattern = new SecurityPattern(secPatternName, SecurityPattern.SYMMETRIC_ENC_PATTERN, overhead, "",
TMLTask hsmTask = taskAndItsHSMMap.get(ch.getDestinationTask()); encComp, decComp, "", "", "");
TMLChannel chToHSM = FindOrCreateChannelToHSM(hsmTask, ch.getDestinationTask(), ch); HandleSecurityGoalsForChannels(tmlmodel, ch, secPattern, false, null, null);
TMLChannel chFromHSM = FindOrCreateChannelFromHSM(hsmTask, ch.getDestinationTask(), ch); }
addToSecurityTaskMap(hsmTask, secPattern);
if (!nonceChannelExist) {
TMLActivityElement NonceBranch = addNonceExchangeBranchHSM(hsmTask, channelNonceFromHsmMap.get(chNonce), spNonce, true);
taskHSMBranchesMap.get(hsmTask).add(NonceBranch);
nonceCommunicationWithHsmAD(ch.getDestinationTask(), spNonce, channelNonceFromHsmMap.get(chNonce), hsmTaskRequestMap.get(hsmTask),
taskHSMBranchesMap.get(hsmTask).size() - 1, false, chNonce, ch.getDestinationTask().getActivityDiagram().getFirst());
}
try {
TMLActivityElement branch = addBranchHSM(hsmTask, chToHSM, chFromHSM, secPattern, false);
taskHSMBranchesMap.get(hsmTask).add(branch);
} catch (TMLCheckingError e) {
throw new RuntimeException(e);
}
for (TMLReadChannel rd : listRd) { for (TMLChannel ch : chAddSA) {
communicationWithHSMAD(ch.getDestinationTask(), rd, secPattern, chToHSM, chFromHSM, hsmTaskRequestMap.get(hsmTask), taskHSMBranchesMap.get(hsmTask).size()-1); SecurityPattern spNonce = FindOrCreateNonceSecurityPattern(ch.getOriginTask(), ch.getDestinationTask());
} boolean nonceChannelExist = nonceChannelIsCreated(ch.getDestinationTask(), ch.getOriginTask());
} else { TMLChannel chNonce = FindOrCreateNonceChannel(ch.getDestinationTask(), ch.getOriginTask());
try { String secPatternNameInit = "mac_" + ch.getChannelName();
addDecryptionAD(ch.getDestinationTask(), listRd, secPattern); String secPatternName = secPatternNameInit;
} catch (TMLCheckingError e) { int index = 0;
throw new RuntimeException(e); while (tmap.getSecurityPatternByName(secPatternName) != null) {
} secPatternName = secPatternNameInit + index;
if (!nonceChannelExist) { index ++;
addNonceSendAD(ch.getDestinationTask(), chNonce, spNonce, ch.getDestinationTask().getActivityDiagram().getFirst());
}
addToSecurityTaskMap(ch.getDestinationTask(), secPattern);
} }
for (HwCommunicationNode commNode :tmap.getAllCommunicationNodesOfChannel(ch)) {
if (!tmap.isCommNodeMappedOn(chNonce, commNode)) { SecurityPattern secPattern = new SecurityPattern(secPatternName, SecurityPattern.MAC_PATTERN, overhead, "",
tmap.addCommToHwCommNode(chNonce, commNode); encComp, decComp, spNonce.getName(), "", "");
} HandleSecurityGoalsForChannels(tmlmodel, ch, secPattern, !nonceChannelExist, spNonce, chNonce);
}
for (TMLChannel ch : chAddWA) {
String secPatternNameInit = "mac_" + ch.getChannelName();
String secPatternName = secPatternNameInit;
int index = 0;
while (tmap.getSecurityPatternByName(secPatternName) != null) {
secPatternName = secPatternNameInit + index;
index ++;
} }
SecurityPattern secPattern = new SecurityPattern(secPatternName, SecurityPattern.MAC_PATTERN, overhead, "",
encComp, decComp, "", "", "");
HandleSecurityGoalsForChannels(tmlmodel, ch, secPattern, false, null, null);
} }
for (TMLTask hsmTask : taskHSMBranchesMap.keySet()) { for (TMLTask hsmTask : taskHSMBranchesMap.keySet()) {
...@@ -441,6 +389,87 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -441,6 +389,87 @@ public class SecurityGenerationForTMAP implements Runnable {
} }
} }
private void HandleSecurityGoalsForChannels(TMLModeling<?> tmlmodel, TMLChannel ch, SecurityPattern secPattern, boolean nonceGenerationNeeded,
SecurityPattern spNonce, TMLChannel chNonce) {
tmlmodel.addSecurityPattern(secPattern);
List<TMLWriteChannel> listWr = WriteOperatorsOfChannel(ch.getOriginTask(), ch);
List<TMLReadChannel> listRd = ReadOperatorsOfChannel(ch.getDestinationTask(), ch);
if (taskAndItsHSMMap.containsKey(ch.getOriginTask())) {
TMLTask hsmTask = taskAndItsHSMMap.get(ch.getOriginTask());
TMLChannel chToHSM = FindOrCreateChannelToHSM(hsmTask, ch.getOriginTask(), ch);
TMLChannel chFromHSM = FindOrCreateChannelFromHSM(hsmTask, ch.getOriginTask(), ch);
addToSecurityTaskMap(hsmTask, secPattern);
if (nonceGenerationNeeded) {
TMLActivityElement NonceBranch = addNonceExchangeBranchHSM(hsmTask, channelNonceToHsmMap.get(chNonce), spNonce, false);
taskHSMBranchesMap.get(hsmTask).add(NonceBranch);
nonceCommunicationWithHsmAD(ch.getOriginTask(), spNonce, channelNonceToHsmMap.get(chNonce), hsmTaskRequestMap.get(hsmTask),
taskHSMBranchesMap.get(hsmTask).size() - 1, true, chNonce, ch.getOriginTask().getActivityDiagram().getFirst());
}
try {
TMLActivityElement branch = addBranchHSM(hsmTask, chToHSM, chFromHSM, secPattern, true);
taskHSMBranchesMap.get(hsmTask).add(branch);
} catch (TMLCheckingError e) {
throw new RuntimeException(e);
}
for (TMLWriteChannel wr : listWr) {
communicationWithHSMAD(ch.getOriginTask(), wr, secPattern, chToHSM, chFromHSM, hsmTaskRequestMap.get(hsmTask),
taskHSMBranchesMap.get(hsmTask).size()-1);
}
} else {
addToSecurityTaskMap(ch.getOriginTask(), secPattern);
try {
addEncryptionAD(ch.getOriginTask(), listWr, secPattern);
} catch (TMLCheckingError e) {
throw new RuntimeException(e);
}
if (nonceGenerationNeeded) {
addNonceReceiveAD(ch.getOriginTask(), chNonce, spNonce, ch.getOriginTask().getActivityDiagram().getFirst());
}
}
if (taskAndItsHSMMap.containsKey(ch.getDestinationTask())) {
TMLTask hsmTask = taskAndItsHSMMap.get(ch.getDestinationTask());
TMLChannel chToHSM = FindOrCreateChannelToHSM(hsmTask, ch.getDestinationTask(), ch);
TMLChannel chFromHSM = FindOrCreateChannelFromHSM(hsmTask, ch.getDestinationTask(), ch);
addToSecurityTaskMap(hsmTask, secPattern);
if (nonceGenerationNeeded) {
TMLActivityElement NonceBranch = addNonceExchangeBranchHSM(hsmTask, channelNonceFromHsmMap.get(chNonce), spNonce, true);
taskHSMBranchesMap.get(hsmTask).add(NonceBranch);
nonceCommunicationWithHsmAD(ch.getDestinationTask(), spNonce, channelNonceFromHsmMap.get(chNonce), hsmTaskRequestMap.get(hsmTask),
taskHSMBranchesMap.get(hsmTask).size() - 1, false, chNonce, ch.getDestinationTask().getActivityDiagram().getFirst());
}
try {
TMLActivityElement branch = addBranchHSM(hsmTask, chToHSM, chFromHSM, secPattern, false);
taskHSMBranchesMap.get(hsmTask).add(branch);
} catch (TMLCheckingError e) {
throw new RuntimeException(e);
}
for (TMLReadChannel rd : listRd) {
communicationWithHSMAD(ch.getDestinationTask(), rd, secPattern, chToHSM, chFromHSM, hsmTaskRequestMap.get(hsmTask),
taskHSMBranchesMap.get(hsmTask).size()-1);
}
} else {
try {
addDecryptionAD(ch.getDestinationTask(), listRd, secPattern);
} catch (TMLCheckingError e) {
throw new RuntimeException(e);
}
if (nonceGenerationNeeded) {
addNonceSendAD(ch.getDestinationTask(), chNonce, spNonce, ch.getDestinationTask().getActivityDiagram().getFirst());
}
addToSecurityTaskMap(ch.getDestinationTask(), secPattern);
}
if (nonceGenerationNeeded) {
for (HwCommunicationNode commNode : tmap.getAllCommunicationNodesOfChannel(ch)) {
if (!tmap.isCommNodeMappedOn(chNonce, commNode)) {
tmap.addCommToHwCommNode(chNonce, commNode);
}
}
}
}
private void initHSMTaskDiagram(TMLTask task) { private void initHSMTaskDiagram(TMLTask task) {
String hsmTaskNameInit = appName + "__" + "HSM_" + task.getTaskName(); String hsmTaskNameInit = appName + "__" + "HSM_" + task.getTaskName();
int index = 0; int index = 0;
...@@ -470,7 +499,7 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -470,7 +499,7 @@ public class SecurityGenerationForTMAP implements Runnable {
request.addParam(new TMLType(TMLType.NATURAL)); request.addParam(new TMLType(TMLType.NATURAL));
tmap.getTMLModeling().addRequest(request); tmap.getTMLModeling().addRequest(request);
hsmTaskRequestMap.put(hsm, request); hsmTaskRequestMap.put(hsm, request);
taskHSMBranchesMap.put(hsm, new ArrayList<TMLActivityElement>()); taskHSMBranchesMap.put(hsm, new ArrayList<>());
initHSMArchDiagram(hsm, task); initHSMArchDiagram(hsm, task);
} }
...@@ -517,7 +546,7 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -517,7 +546,7 @@ public class SecurityGenerationForTMAP implements Runnable {
private void initHSMArchDiagram(TMLTask hsmTask, TMLTask task) { private void initHSMArchDiagram(TMLTask hsmTask, TMLTask task) {
TMLArchitecture arch = tmap.getArch(); TMLArchitecture arch = tmap.getArch();
List<HwCommunicationNode> communicationNodesOfHSM = new ArrayList<HwCommunicationNode>(); List<HwCommunicationNode> communicationNodesOfHSM = new ArrayList<>();
//Find the CPU where the task is mapped to //Find the CPU where the task is mapped to
HwExecutionNode cpuTask = tmap.getHwNodeOf(task); HwExecutionNode cpuTask = tmap.getHwNodeOf(task);
...@@ -586,7 +615,8 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -586,7 +615,8 @@ public class SecurityGenerationForTMAP implements Runnable {
taskHSMCommunicationNodesMap.put(hsmTask, communicationNodesOfHSM); taskHSMCommunicationNodesMap.put(hsmTask, communicationNodesOfHSM);
} }
private TMLActivityElement addBranchHSM(TMLTask hsmTask, TMLChannel dataCh, TMLChannel retrieveDataCh, SecurityPattern sp, boolean isEncryption) throws TMLCheckingError { private TMLActivityElement addBranchHSM(TMLTask hsmTask, TMLChannel dataCh, TMLChannel retrieveDataCh, SecurityPattern sp,
boolean isEncryption) throws TMLCheckingError {
TMLActivity hsmTaskAD = hsmTask.getActivityDiagram(); TMLActivity hsmTaskAD = hsmTask.getActivityDiagram();
TMLReadChannel rd = new TMLReadChannel(dataCh.getChannelName(), hsmTaskAD.getReferenceObject()); TMLReadChannel rd = new TMLReadChannel(dataCh.getChannelName(), hsmTaskAD.getReferenceObject());
rd.addChannel(dataCh); rd.addChannel(dataCh);
...@@ -657,34 +687,6 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -657,34 +687,6 @@ public class SecurityGenerationForTMAP implements Runnable {
} }
} }
/*private TMLActivityElement addNonceExchangeHSM(TMLTask hsmTask, TMLChannel nonceCh, SecurityPattern sp, boolean isNonceSender,
TMLActivityElement headerElement) {
TMLActivity hsmTaskAD = hsmTask.getActivityDiagram();
if (isNonceSender) {
TMLExecC exec = new TMLExecC(sp.getName(), hsmTaskAD.getReferenceObject());
exec.setSecurityPattern(sp);
exec.setAction(Integer.toString(sp.getEncTime()));
hsmTaskAD.addElement(exec);
headerElement.addNext(exec);
TMLWriteChannel wr = new TMLWriteChannel(nonceCh.getChannelName(), hsmTaskAD.getReferenceObject());
wr.addChannel(nonceCh);
hsmTaskAD.addElement(wr);
wr.setNbOfSamples("1");
wr.setSecurityPattern(sp);
exec.addNext(wr);
return wr;
} else {
TMLReadChannel rd = new TMLReadChannel(nonceCh.getChannelName(), hsmTaskAD.getReferenceObject());
rd.addChannel(nonceCh);
rd.setSecurityPattern(sp);
rd.setNbOfSamples("1");
hsmTaskAD.addElement(rd);
headerElement.addNext(rd);
return rd;
}
}*/
private void communicationWithHSMAD(TMLTask task, TMLActivityElementChannel comm, SecurityPattern sp, TMLChannel dataCh, private void communicationWithHSMAD(TMLTask task, TMLActivityElementChannel comm, SecurityPattern sp, TMLChannel dataCh,
TMLChannel retrieveDataCh, TMLRequest request, int indexRequest) { TMLChannel retrieveDataCh, TMLRequest request, int indexRequest) {
TMLActivity taskAD = task.getActivityDiagram(); TMLActivity taskAD = task.getActivityDiagram();
...@@ -846,7 +848,7 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -846,7 +848,7 @@ public class SecurityGenerationForTMAP implements Runnable {
} }
private List<TMLReadChannel> ReadOperatorsOfChannel(TMLTask task, TMLChannel ch) { private List<TMLReadChannel> ReadOperatorsOfChannel(TMLTask task, TMLChannel ch) {
List<TMLReadChannel> elems = new ArrayList<TMLReadChannel>(); List<TMLReadChannel> elems = new ArrayList<>();
for (TMLActivityElement elem : task.getActivityDiagram().getElements()) { for (TMLActivityElement elem : task.getActivityDiagram().getElements()) {
if (elem instanceof TMLReadChannel) { if (elem instanceof TMLReadChannel) {
TMLReadChannel rc = (TMLReadChannel) elem; TMLReadChannel rc = (TMLReadChannel) elem;
...@@ -861,7 +863,7 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -861,7 +863,7 @@ public class SecurityGenerationForTMAP implements Runnable {
} }
private List<TMLWriteChannel> WriteOperatorsOfChannel(TMLTask task, TMLChannel ch) { private List<TMLWriteChannel> WriteOperatorsOfChannel(TMLTask task, TMLChannel ch) {
List<TMLWriteChannel> elems = new ArrayList<TMLWriteChannel>(); List<TMLWriteChannel> elems = new ArrayList<>();
for (TMLActivityElement elem : task.getActivityDiagram().getElements()) { for (TMLActivityElement elem : task.getActivityDiagram().getElements()) {
if (elem instanceof TMLWriteChannel) { if (elem instanceof TMLWriteChannel) {
TMLWriteChannel wc = (TMLWriteChannel) elem; TMLWriteChannel wc = (TMLWriteChannel) elem;
...@@ -888,7 +890,8 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -888,7 +890,8 @@ public class SecurityGenerationForTMAP implements Runnable {
if (tasksNonceSPMap.containsKey(taskPair)) { if (tasksNonceSPMap.containsKey(taskPair)) {
return tasksNonceSPMap.get(taskPair); return tasksNonceSPMap.get(taskPair);
} }
SecurityPattern secPatternNonce = new SecurityPattern("nonce_" + destinationTaskInit.getTaskName() + "_" + originTaskInit.getTaskName(), SecurityPattern.NONCE_PATTERN, overhead, "", encComp, decComp, "", "", ""); SecurityPattern secPatternNonce = new SecurityPattern("nonce_" + destinationTaskInit.getTaskName() + "_" + originTaskInit.getTaskName(),
SecurityPattern.NONCE_PATTERN, overhead, "", encComp, decComp, "", "", "");
tasksNonceSPMap.put(taskPair, secPatternNonce); tasksNonceSPMap.put(taskPair, secPatternNonce);
tmap.getTMLModeling().addSecurityPattern(secPatternNonce); tmap.getTMLModeling().addSecurityPattern(secPatternNonce);
return secPatternNonce; return secPatternNonce;
...@@ -1013,7 +1016,7 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -1013,7 +1016,7 @@ public class SecurityGenerationForTMAP implements Runnable {
tmlmodel.getSecurityTaskMap().get(sec).add(task); tmlmodel.getSecurityTaskMap().get(sec).add(task);
} }
} else { } else {
List<TMLTask> listTask = new ArrayList<TMLTask>(); List<TMLTask> listTask = new ArrayList<>();
listTask.add(task); listTask.add(task);
tmlmodel.getSecurityTaskMap().put(sec, listTask); tmlmodel.getSecurityTaskMap().put(sec, listTask);
} }
...@@ -1021,7 +1024,7 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -1021,7 +1024,7 @@ public class SecurityGenerationForTMAP implements Runnable {
public TMLMapping<?> autoMapKeys() { public TMLMapping<?> autoMapKeys() {
if (tmap == null) { if (tmap == null) {
return tmap; return null;
} }
//Find all Security Patterns, if they don't have an associated memory at encrypt and decrypt, tmap them //Find all Security Patterns, if they don't have an associated memory at encrypt and decrypt, tmap them
TMLModeling<?> tmlm = tmap.getTMLModeling(); TMLModeling<?> tmlm = tmap.getTMLModeling();
...@@ -1029,7 +1032,8 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -1029,7 +1032,8 @@ public class SecurityGenerationForTMAP implements Runnable {
return tmap; return tmap;
} }
for (SecurityPattern sp : tmlm.getSecurityTaskMap().keySet()) { for (SecurityPattern sp : tmlm.getSecurityTaskMap().keySet()) {
if (sp.getType().equals(SecurityPattern.SYMMETRIC_ENC_PATTERN) || sp.getType().equals(SecurityPattern.MAC_PATTERN) || sp.getType().equals(SecurityPattern.ASYMMETRIC_ENC_PATTERN)) { if (sp.getType().equals(SecurityPattern.SYMMETRIC_ENC_PATTERN) || sp.getType().equals(SecurityPattern.MAC_PATTERN) ||
sp.getType().equals(SecurityPattern.ASYMMETRIC_ENC_PATTERN)) {
for (TMLTask t : tmlm.getSecurityTaskMap().get(sp)) { for (TMLTask t : tmlm.getSecurityTaskMap().get(sp)) {
HwExecutionNode node1 = tmap.getHwNodeOf(t); HwExecutionNode node1 = tmap.getHwNodeOf(t);
boolean taskMappedToCPU = false; boolean taskMappedToCPU = false;
...@@ -1046,7 +1050,6 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -1046,7 +1050,6 @@ public class SecurityGenerationForTMAP implements Runnable {
HwBus curBus = link.bus; HwBus curBus = link.bus;
boolean keyFound = false; boolean keyFound = false;
HwMemory memNodeToMap = null; HwMemory memNodeToMap = null;
outer:
for (HwLink linkBus : tmap.getArch().getHwLinks()) { for (HwLink linkBus : tmap.getArch().getHwLinks()) {
if (linkBus.bus == curBus) { if (linkBus.bus == curBus) {
if (linkBus.hwnode instanceof HwMemory) { if (linkBus.hwnode instanceof HwMemory) {
...@@ -1055,7 +1058,7 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -1055,7 +1058,7 @@ public class SecurityGenerationForTMAP implements Runnable {
if (keys.contains(sp)) { if (keys.contains(sp)) {
keyFound = true; keyFound = true;
keyMappedtoMem = true; keyMappedtoMem = true;
break outer; break;
} }
} }
} }
...@@ -1064,7 +1067,6 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -1064,7 +1067,6 @@ public class SecurityGenerationForTMAP implements Runnable {
if (memNodeToMap != null) { if (memNodeToMap != null) {
TraceManager.addDev("Adding " + sp.getName() + " key to " + memNodeToMap.getName()); TraceManager.addDev("Adding " + sp.getName() + " key to " + memNodeToMap.getName());
tmap.addSecurityPattern(memNodeToMap, sp); tmap.addSecurityPattern(memNodeToMap, sp);
keyMappedtoMem = true;
} else { } else {
HwMemory newHwMemory = new HwMemory(cpuNode.getName() + "KeysMemory"); HwMemory newHwMemory = new HwMemory(cpuNode.getName() + "KeysMemory");
TraceManager.addDev("Creating new memory: " + newHwMemory.getName()); TraceManager.addDev("Creating new memory: " + newHwMemory.getName());
...@@ -1076,8 +1078,8 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -1076,8 +1078,8 @@ public class SecurityGenerationForTMAP implements Runnable {
tmap.getArch().getHwLinks().add(linkNewMemWithBus); tmap.getArch().getHwLinks().add(linkNewMemWithBus);
tmap.addSecurityPattern(newHwMemory, sp); tmap.addSecurityPattern(newHwMemory, sp);
TraceManager.addDev("Adding " + sp.getName() + " key to " + newHwMemory.getName()); TraceManager.addDev("Adding " + sp.getName() + " key to " + newHwMemory.getName());
keyMappedtoMem = true;
} }
keyMappedtoMem = true;
} }
} }
} }
...@@ -1105,7 +1107,6 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -1105,7 +1107,6 @@ public class SecurityGenerationForTMAP implements Runnable {
tmap.addSecurityPattern(memNodeToMap, sp); tmap.addSecurityPattern(memNodeToMap, sp);
TraceManager.addDev("Adding " + sp.getName() + " key to " + memNodeToMap.getName()); TraceManager.addDev("Adding " + sp.getName() + " key to " + memNodeToMap.getName());
keyMappedtoMem = true;
//Connect Bus and Memory //Connect Bus and Memory
HwLink newLinkBusMemory = new HwLink("Link_"+newPrivateBus.getName() + "_" + memNodeToMap.getName()); HwLink newLinkBusMemory = new HwLink("Link_"+newPrivateBus.getName() + "_" + memNodeToMap.getName());
...@@ -1153,36 +1154,4 @@ public class SecurityGenerationForTMAP implements Runnable { ...@@ -1153,36 +1154,4 @@ public class SecurityGenerationForTMAP implements Runnable {
return tmap; return tmap;
} }
class HSMChannel {
public static final int SENC = 0;
public static final int NONCE_ENC = 1;
public static final int MAC = 2;
public static final int DEC = 3;
public static final int AENC = 4;
public static final int NONCE = 5;
public TMLChannel channel;
public TMLTask task;
public int secType;
public String nonceName = "";
public HSMChannel(TMLChannel n, TMLTask t, int type) {
channel = n;
task = t;
secType = type;
}
}
class ChannelData {
public String name;
public boolean isOrigin;
public boolean isChan;
public ChannelData(String n, boolean orig, boolean isCh) {
name = n;
isOrigin = orig;
isChan = isCh;
}
}
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment