From c219958d5bfae71adc63bd9a4956bdab4a1e4d04 Mon Sep 17 00:00:00 2001
From: dontenvi <pierre.dontenville@eurecom.fr>
Date: Wed, 13 Dec 2023 10:32:17 -0500
Subject: [PATCH] SampleAutoSec added
---
.../tmltranslator/DiplodocusSecurityTest.java | 4 +-
.../Models/AliceAndBobHW/SampleAutoSec/golden | 2 +
.../AliceAndBobHW/SampleAutoSec/spec.tarchi | 116 ++++++++++++++++++
.../AliceAndBobHW/SampleAutoSec/spec.tmap | 22 ++++
.../AliceAndBobHW/SampleAutoSec/spec.tml | 32 +++++
5 files changed, 174 insertions(+), 2 deletions(-)
create mode 100644 ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/golden
create mode 100644 ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/spec.tarchi
create mode 100644 ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/spec.tmap
create mode 100644 ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/spec.tml
diff --git a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
index 839897e775..04df99cb4d 100644
--- a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
+++ b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
@@ -68,8 +68,8 @@ public class DiplodocusSecurityTest extends AbstractTest {
@Parameterized.Parameters(name = "{index}: {0}")
public static Collection models(){
return Arrays.asList(new Object[][] {
- {"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac"))},
- {"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac"))},
+ {"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac", "SampleAutoSec"))},
+// {"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac"))},
// {"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac", "SampleAutoSec"))}
});
}
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/golden
new file mode 100644
index 0000000000..c2984028e5
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/golden
@@ -0,0 +1,2 @@
+Query not attacker(Alice___sampleAutoSec__comm_chData[!1 = v]) is false.
+Query inj-event(authenticity___Bob___comm_chData___aftersignalstate_sampleAutoSec_comm_sampleAutoSec_comm(dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_sampleAutoSec_comm_sampleAutoSec_comm(dummyM)) is false.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/spec.tarchi b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/spec.tarchi
new file mode 100644
index 0000000000..8013dbe04a
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/spec.tarchi
@@ -0,0 +1,116 @@
+// Master clock frequency - in MHz
+MASTERCLOCKFREQUENCY 200
+
+NODE BRIDGE BridgeAlice
+SET BridgeAlice bufferByteSize 4
+SET BridgeAlice clockDivider 1
+
+NODE BRIDGE BridgeBob
+SET BridgeBob bufferByteSize 4
+SET BridgeBob clockDivider 1
+
+NODE MEMORY ExternalMemory
+SET ExternalMemory byteDataSize 4
+SET ExternalMemory clockDivider 1
+
+NODE MEMORY MemoryAlice
+SET MemoryAlice byteDataSize 4
+SET MemoryAlice clockDivider 1
+
+NODE MEMORY MemoryBob
+SET MemoryBob byteDataSize 4
+SET MemoryBob clockDivider 1
+
+NODE BUS BusBob
+SET BusBob byteDataSize 4
+SET BusBob pipelineSize 1
+SET BusBob arbitration 0
+SET BusBob sliceTime 10000
+SET BusBob burstSize 100
+SET BusBob privacy private
+SET BusBob clockDivider 1
+
+NODE BUS BusAlice
+SET BusAlice byteDataSize 4
+SET BusAlice pipelineSize 1
+SET BusAlice arbitration 0
+SET BusAlice sliceTime 10000
+SET BusAlice burstSize 100
+SET BusAlice privacy private
+SET BusAlice clockDivider 1
+
+NODE BUS ExternalBus
+SET ExternalBus byteDataSize 4
+SET ExternalBus pipelineSize 1
+SET ExternalBus arbitration 0
+SET ExternalBus sliceTime 10000
+SET ExternalBus burstSize 100
+SET ExternalBus privacy public
+SET ExternalBus clockDivider 1
+
+NODE CPU CPUAlice
+SET CPUAlice nbOfCores 1
+SET CPUAlice byteDataSize 4
+SET CPUAlice pipelineSize 5
+SET CPUAlice goIdleTime 10
+SET CPUAlice maxConsecutiveIdleCycles 10
+SET CPUAlice taskSwitchingTime 20
+SET CPUAlice branchingPredictionPenalty 2
+SET CPUAlice cacheMiss 5
+SET CPUAlice schedulingPolicy 0
+SET CPUAlice sliceTime 10000
+SET CPUAlice execiTime 1
+SET CPUAlice execcTime 1
+SET CPUAlice clockDivider 1
+
+NODE CPU CPUBob
+SET CPUBob nbOfCores 1
+SET CPUBob byteDataSize 4
+SET CPUBob pipelineSize 5
+SET CPUBob goIdleTime 10
+SET CPUBob maxConsecutiveIdleCycles 10
+SET CPUBob taskSwitchingTime 20
+SET CPUBob branchingPredictionPenalty 2
+SET CPUBob cacheMiss 5
+SET CPUBob schedulingPolicy 0
+SET CPUBob sliceTime 10000
+SET CPUBob execiTime 1
+SET CPUBob execcTime 1
+SET CPUBob clockDivider 1
+
+NODE LINK link_CPUBob_to_BusBob
+SET link_CPUBob_to_BusBob node CPUBob
+SET link_CPUBob_to_BusBob bus BusBob
+SET link_CPUBob_to_BusBob priority 0
+NODE LINK link_CPUAlice_to_BusAlice
+SET link_CPUAlice_to_BusAlice node CPUAlice
+SET link_CPUAlice_to_BusAlice bus BusAlice
+SET link_CPUAlice_to_BusAlice priority 0
+NODE LINK link_BridgeBob_to_BusBob
+SET link_BridgeBob_to_BusBob node BridgeBob
+SET link_BridgeBob_to_BusBob bus BusBob
+SET link_BridgeBob_to_BusBob priority 0
+NODE LINK link_BridgeBob_to_ExternalBus
+SET link_BridgeBob_to_ExternalBus node BridgeBob
+SET link_BridgeBob_to_ExternalBus bus ExternalBus
+SET link_BridgeBob_to_ExternalBus priority 0
+NODE LINK link_BridgeAlice_to_ExternalBus
+SET link_BridgeAlice_to_ExternalBus node BridgeAlice
+SET link_BridgeAlice_to_ExternalBus bus ExternalBus
+SET link_BridgeAlice_to_ExternalBus priority 0
+NODE LINK link_BridgeAlice_to_BusAlice
+SET link_BridgeAlice_to_BusAlice node BridgeAlice
+SET link_BridgeAlice_to_BusAlice bus BusAlice
+SET link_BridgeAlice_to_BusAlice priority 0
+NODE LINK link_ExternalMemory_to_ExternalBus
+SET link_ExternalMemory_to_ExternalBus node ExternalMemory
+SET link_ExternalMemory_to_ExternalBus bus ExternalBus
+SET link_ExternalMemory_to_ExternalBus priority 0
+NODE LINK link_MemoryAlice_to_BusAlice
+SET link_MemoryAlice_to_BusAlice node MemoryAlice
+SET link_MemoryAlice_to_BusAlice bus BusAlice
+SET link_MemoryAlice_to_BusAlice priority 0
+NODE LINK link_MemoryBob_to_BusBob
+SET link_MemoryBob_to_BusBob node MemoryBob
+SET link_MemoryBob_to_BusBob bus BusBob
+SET link_MemoryBob_to_BusBob priority 0
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/spec.tmap b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/spec.tmap
new file mode 100644
index 0000000000..86da2e7721
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/spec.tmap
@@ -0,0 +1,22 @@
+TMLSPEC
+ #include "spec.tml"
+ENDTMLSPEC
+
+TMLARCHI
+ #include "spec.tarchi"
+ENDTMLARCHI
+
+TMLMAPPING
+ MAP CPUAlice sampleAutoSec__Alice
+ SET sampleAutoSec__Alice priority 0
+ MAP CPUBob sampleAutoSec__Bob
+ SET sampleAutoSec__Bob priority 0
+ MAP ExternalMemory sampleAutoSec__comm
+ SET sampleAutoSec__comm priority 0
+ MAP ExternalBus sampleAutoSec__comm
+ SET sampleAutoSec__comm priority 0
+ MAP BusAlice sampleAutoSec__comm
+ SET sampleAutoSec__comm priority 0
+ MAP BusBob sampleAutoSec__comm
+ SET sampleAutoSec__comm priority 0
+ENDTMLMAPPING
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/spec.tml b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/spec.tml
new file mode 100644
index 0000000000..9f93e4cd5d
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/spec.tml
@@ -0,0 +1,32 @@
+// TML Application - FORMAT 0.2
+// Application: /home/kali/Documents/Eurecom/SemesterProject/TTool/modeling/AliceAndBobHW.ttool/AliceAndBobHW.xml
+// Generated: Wed Dec 13 08:48:12 EST 2023
+
+// PRAGMAS
+
+// Channels
+CHANNEL sampleAutoSec__comm NBRNBW 4 OUT sampleAutoSec__Alice IN sampleAutoSec__Bob
+VCCHANNEL sampleAutoSec__comm 0
+CONFCHANNEL sampleAutoSec__comm
+AUTHCHANNEL sampleAutoSec__comm
+
+// Events
+
+// Requests
+
+TASK sampleAutoSec__Alice
+ TASKOP
+ //Local variables
+
+ //Behavior
+ WRITE sampleAutoSec__comm 1
+ENDTASK
+
+TASK sampleAutoSec__Bob
+ TASKOP
+ //Local variables
+
+ //Behavior
+ READ sampleAutoSec__comm 1
+ENDTASK
+
--
GitLab