From 11daa68f1d7e34810ddf9e9a29222c7bb6c20f1d Mon Sep 17 00:00:00 2001
From: jerray <jawher.jerray@eurecom.fr>
Date: Fri, 12 May 2023 15:18:03 +0200
Subject: [PATCH] Add confidentiality pragma only for channels with the option
check confidentiality
---
.../tmltranslator/toavatarsec/TML2Avatar.java | 19 ++++++++++++++++++-
1 file changed, 18 insertions(+), 1 deletion(-)
diff --git a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
index 5b24369897..54fd4ca8c9 100644
--- a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
@@ -1834,12 +1834,29 @@ public class TML2Avatar {
for (SecurityPattern secPattern : secPatterns) {
AvatarAttribute sec = block.getAvatarAttributeWithName(secPattern.name);
if (sec != null) {
+ boolean checkAuthSecPattern = false;
+ for (TMLChannel ch : tmlmodel.getChannels(task)) {
+ if (ch.hasOriginTask(task) && ch.isCheckConfChannel()) {
+ TraceManager.addDev("1842 ch.name= " + ch.getName());
+ for (TMLActivityElement actElem : task.getActivityDiagram().getElements()){
+ if (actElem instanceof TMLWriteChannel) {
+ TMLWriteChannel wc = (TMLWriteChannel) actElem;
+ if(wc.hasChannel(ch) && actElem.securityPattern.getName().equals(secPattern.getName())){
+ checkAuthSecPattern = true;
+ break;
+ }
+ }
+ }
+ }
+ }
//sec = new AvatarAttribute(secPattern.name, AvatarType.INTEGER, block, null);
//AvatarAttribute enc = new AvatarAttribute(secPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
// block.addAttribute(sec);
// block.addAttribute(enc);
//}
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality " + block.getName() + "." + secPattern.name, null, sec));
+ if (checkAuthSecPattern) {
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality " + block.getName() + "." + secPattern.name, null, sec));
+ }
}
}
--
GitLab