diff --git a/doc/SysMLSec/fig/fv3_t2.svg b/doc/SysMLSec/fig/fv3_t2.svg index 9385028551db1e37be15ca0ea53efbd4e2e9abe2..e8c5d55ac92950aff563aa339de12943928afd0b 100644 --- a/doc/SysMLSec/fig/fv3_t2.svg +++ b/doc/SysMLSec/fig/fv3_t2.svg @@ -12,7 +12,7 @@ height="256" viewbox="377 53 79 253" id="svg6998" - inkscape:version="0.48.5 r10040" + inkscape:version="0.48.4 r9939" sodipodi:docname="fv3_t2.svg"> <metadata id="metadata7080"> @@ -36,16 +36,16 @@ guidetolerance="10" inkscape:pageopacity="0" inkscape:pageshadow="2" - inkscape:window-width="640" - inkscape:window-height="480" + inkscape:window-width="2048" + inkscape:window-height="1086" id="namedview7076" showgrid="false" - inkscape:zoom="0.71710526" - inkscape:cx="228" - inkscape:cy="153" - inkscape:window-x="771" - inkscape:window-y="537" - inkscape:window-maximized="0" + inkscape:zoom="2.868421" + inkscape:cx="-150.43595" + inkscape:cy="106.22785" + inkscape:window-x="0" + inkscape:window-y="27" + inkscape:window-maximized="1" inkscape:current-layer="svg6998" /> <line x1="36.091743" @@ -308,4 +308,10 @@ y="148.3945" style="font-size:12px;font-family:SansSerif" id="text7074">sec:Cipherdata</text> + <path + style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" + d="m 32.802637,138.38934 c 9.46153,-1.13712 9.728644,19.92324 0.753685,19.73573" + id="path3019" + inkscape:connector-curvature="0" + sodipodi:nodetypes="cc" /> </svg> diff --git a/doc/SysMLSec/sysmlsec_documentation.tex b/doc/SysMLSec/sysmlsec_documentation.tex index dfc4be00557efecf9a70110940ecc7853abdd1dd..94cd00bacf9c266df061b42e038e2b532b9a3802 100644 --- a/doc/SysMLSec/sysmlsec_documentation.tex +++ b/doc/SysMLSec/sysmlsec_documentation.tex @@ -126,7 +126,7 @@ Editor} & \textbf{Year} \subsection{Summary} -This document describes how to use SysML-Sec using simple examples\footnote{This document has been started in the scope of the AQUAS european project}. In particular, it covers requirements, attack trees, HW/SW partitioning and software design. +This document describes how to use SysML-Sec using simple examples\footnote{This document has been started in the scope of the AQUAS european project}. In particular, it covers requirements, attack trees, HW/SW partitioning and software design. \newpage @@ -136,7 +136,7 @@ At first, if not already configured\footnote{You version of TTool should be alre \begin{verbatim} TTool/bin/config.xml \end{verbatim} -Open your configuration file, and set the following lines accordingly with your TTool and ProVerif installation: +Open your configuration file, and add the following lines accordingly with your TTool and ProVerif installation: \begin{itemize} \item Directory in which formal specifications for security proofs are generated: \begin{verbatim} @@ -151,7 +151,7 @@ Open your configuration file, and set the following lines accordingly with your <ProVerifVerifierHost data="localhost" /> \end{verbatim} \end{itemize} -We also assume that the DIPLODOCUS simulator correctly works. +We also assume that the DIPLODOCUS simulator works correctly. \subsection{External tools} @@ -159,7 +159,7 @@ The configuration for the DIPLODOCUS simulator assumes that a \textbf{C compile \newpage \section{Getting started with a toy example}\label{sec:example} -This very first example explains how to use the main capabilities of SysML-Sec +This very first example explains how to use the main capabilities of SysML-Sec. \subsection{Getting the example} Be sure to get the latest version of TTool including the remote loading of models (March 2018 and after). Do: File, Open from TTool repository, and select "SysMLSecTutorial.xml". @@ -172,13 +172,13 @@ The first tab of the model presents an overview of the SysML-Sec methodology (se \centering \includegraphics[width=0.99\textwidth]{build/method-svg.pdf} -\caption{The first diagram represents the method of SysML-Sec. Each stage of the method is represented by a rectangle that contains a link to all diagrams of the corresponding stage} \label{fig:method} +\caption{The first diagram represents the SysML-Sec method. Each stage of the method is represented by a rectangle that contains a link to all diagrams of the corresponding stage} \label{fig:method} \end{figure*} \subsection{Security requirements} -Security requirements are captured with a SysML requirement diagrams that is extended in the following way: +Security requirements are captured with a SysML requirement diagram that is extended in the following ways: \begin{enumerate} -\item Requirements can be tagged as "Functional", "Non Functional", "Privacy", "Confidentiality", "Non Repudiation", "Controlled Access", "Availability", "Immunity", "Data Origin Authenticity", "Freshness", "Business", "StakeHolder Need", "Other" +\item Requirements can be tagged as "Functional", "Non Functional", "Privacy", "Confidentiality", "Non Repudiation", "Controlled Access", "Availability", "Immunity", "Data Origin Authenticity", "Freshness", "Business", "Stakeholder Need", "Other" \item Requirements have a \textbf{risk} attribute (low, medium, high). \item Property blocks can be added in order to reference a given property. Then, a "satisfy" link can be drawn between a Property and a Requirement. \end{enumerate} @@ -192,7 +192,7 @@ The requirement diagram of Figure \ref{fig:req1} shows a confidentiality require \end{figure*} \subsection{Functional Model (version 1)} -The functional model is build upon the merge of a SysML Block Definition Diagram and a SysML Internal Block Diagram, see Figure \ref{fig:fv1}. The functional view contains two blocks : T1 and T2. The functional behavior of T1 and T2 is captured with Activity diagrams, as displayed on the left and right of Figure \ref{fig:fv1}. Basically, T1 write one data sample, and T2 reads one data sample. +The functional model is built upon the merge of a SysML Block Definition Diagram and a SysML Internal Block Diagram, see Figure \ref{fig:fv1}. The functional view contains two blocks : T1 and T2. The functional behavior of T1 and T2 is captured with Activity diagrams, as displayed on the left and right of Figure \ref{fig:fv1}. Basically, T1 writes one data sample, and T2 reads one data sample. \begin{figure*}[htbp] @@ -224,7 +224,7 @@ A simple architecture model and mapping is shown in Figure \ref{fig:mapping1}. T \end{figure*} \subsection{Attack Tree Model} -We can now capture potential attacks on this system in an attack tree model. SysML doesn't propose any way to capture fault or attack trees. TTool proposes to rely on SysML parametric diagrams in order to capture attacks (or faults). +We can now capture potential attacks on this system in an attack tree model. However, SysML doesn't propose any way to capture fault or attack trees. TTool thus proposes relying on SysML parametric diagrams in order to capture attacks (or faults). \begin{figure*}[htbp] \centering @@ -232,24 +232,24 @@ We can now capture potential attacks on this system in an attack tree model. Sys \caption{Attack Tree Model} \label{fig:attacktree} \end{figure*} -The attack tree of Figure \ref{fig:attacktree} contains a root attack: "RetrieveConfidentialData". This root attack is possible if and only if the attack first connects on the bus (let's call this attack $att_1$), and then reads (and interpret) a data on the bus ($att_2$). Making either $att_1$ or $att_2$ not possible in our system would suffice to ensure that the root attack is not possible. This is obvious in our attack tree, but this is not always the case. Thus, TTool proposes a way to investigate if a given attack is still possible in the system directly from attack trees. Let's try together: +The attack tree of Figure \ref{fig:attacktree} contains a root attack: "RetrieveConfidentialData". This root attack is possible if and only if the attacker first connects to the bus (let's call this attack $att_1$), and then reads (and interprets) a data on the bus ($att_2$). Making either $att_1$ or $att_2$ not possible in our system would be sufficient to ensure that the root attack is not possible. This is obvious in our attack tree, but this is not always the case, such as for larger systems with complex logical combinations of attack steps. Thus, TTool proposes a way to investigate if a given attack is still possible in the system directly from attack trees. Let's try together: \begin{enumerate} -\item Make a right click on the root attack, and click on "Select for Reachability/Liveness". -\item. Let's now see if the root attack is reachable. For this, check the syntax of the diagram, and click on the "Safety verification (internal tool)" icon. Then, select "Reachability of selected states" and click on start. Close the window. You diagram should be annotated with a green "R", as shown on Figure \ref{fig:attacktree_verif1}. -\item Let's make $att_1$ or $att_2$ not feasible. For this, you can make a right click on e.g. $att_1$ and select "Disable". If an attack is disabled, it probably means that a countermeasure has been used. Thus, countermeasure blocks can be linked to attacks. In the case of $ att_1$, the countermeasure is to make the bus private (e.g., make it internal to a chip if the attacker has no way to investigate a bus within a chip). For $att_2$, a common countermeasure is to use security protocols relying on ciphering algorithms. For now, we assume that only $att_1$ is disabled. Make the verification process. After this verification process, you should obtain a red "R", meaning that the root attack is no more feasible (see Figure \ref{fig:attacktree_verif2}) +\item Right click on the root attack, and click on "Select for Reachability/Liveness". +\item Let's now see if the root attack is reachable. For this, check the syntax of the diagram, and click on the "Safety verification (internal tool)" icon. Then, select "Reachability of selected states" and click on start. Close the window. You diagram should be annotated with a green "R", as shown on Figure \ref{fig:attacktree_verif1}. +\item Let's make $att_1$ or $att_2$ not feasible. For this, you can right click on e.g. $att_1$ and select "Disable". If an attack is disabled, it probably means that a countermeasure has been used. Thus, countermeasure blocks can be linked to attacks. In the case of $ att_1$, the countermeasure is to make the bus private (e.g., make it internal to a chip if the attacker has no way to investigate a bus within a chip). For $att_2$, a common countermeasure is to use security protocols relying on ciphering algorithms. For now, we assume that only $att_1$ is disabled. Run the verification process again. After this verification process, you should obtain a red "R", meaning that the root attack is no longer feasible (see Figure \ref{fig:attacktree_verif2}) \end{enumerate} \begin{figure*}[htbp] \centering \includegraphics[width=0.8\textwidth]{fig/attacktree_verif1.png} -\caption{Attack Tree Model after formal verification} \label{fig:attacktree_verif1} +\caption{Attack Tree Model after formal verification with no attack steps disabled} \label{fig:attacktree_verif1} \end{figure*} \begin{figure*}[htbp] \centering \includegraphics[width=0.8\textwidth]{fig/attacktree_verif2.png} -\caption{Attack Tree Model after formal verification} \label{fig:attacktree_verif2} +\caption{Attack Tree Model after formal verification with attack steps disabled by countermeasures} \label{fig:attacktree_verif2} \end{figure*} \subsection{Implementing security countermeasures} @@ -263,10 +263,10 @@ Before implementing security countermeasures in the mapping model, this document \item The result of the verification is displayed in the lower part of Figure \ref{fig:proverif1}. There are two results: \begin{itemize} \item The $comm$ channel is NOT confidential, which proves that the confidentiality requirement is NOT satisfied -\item The read and write actions in T2 and T1 are reachable. This result is important in the case the property is satisfied. Indeed, if none of these actions were reachable, the channel would be confidential since there would be no exchange of data in this channel +\item The read and write actions in T2 and T1 are reachable. This result is important in the case the property is satisfied. Indeed, if none of these actions were reachable, the channel would be confidential since there would be no exchange of data on this channel. \end{itemize} -\item Since $comm$ is not confidential, TTool can draw an attack trace that shows how the attacker manages to retrieve the data. Make a right click on the non satisfied authenticity, and select "show trace" (see Figure \ref{fig:trace1}). This (obvious) trace explains that T1 directly send a data to the attacker since T1 writes the data on a public bus. -\item The functional view is annotated with the verification results, as shown on Figure \ref{fig:fv1results} +\item Since $comm$ is not confidential, TTool can draw an attack trace that shows how the attacker manages to retrieve the data. Right click on the non satisfied authenticity, and select "show trace" (see Figure \ref{fig:trace1}). This (obvious) trace explains that T1 directly send a data to the attacker since T1 writes the data on a public bus. +\item The functional view is annotated with the verification results, as shown on Figure \ref{fig:fv1results}. \end{enumerate} \begin{figure*}[htbp] @@ -293,16 +293,16 @@ Before implementing security countermeasures in the mapping model, this document \subsubsection{Countermeasure 1: Secure Bus} As seen before, a first countermeasure is to use a secure bus, which is called "private" in TTool. Thus, the bus in the second mapping (called "SecureArchitectureWithNonSecureFV") is private. You can see this with the green shield icon on the bus. A double-click on this bus makes it possible to change this parameter (public, private). -Try to make the security verification of this second system. You should observe that the confidentiality property is now verified. +Try to run the security verification of this second system. You should observe that the confidentiality property is now verified. \begin{figure*}[htbp] \centering \includegraphics[width=0.6\textwidth]{build/mapping2-svg} -\caption{Secure Architecture thanks to a private bus} \label{fig:mapping2} +\caption{Secure Architecture due to a private bus} \label{fig:mapping2} \end{figure*} \subsubsection{Countermeasure 2: Secure Functions} -A second countermeasure consists in adding security mechanisms to the two functions T1 and T2. TTool offers cryptographic configurations to add security mechanisms to the behaviour of blocks. Basically, a cryptographic configuration specifies the type of security mechanism (symmetric cipher, hash, key manipulation, nonce, etc.) and its performance impact in terms of complexity operations by sample. +A second countermeasure consists in adding security mechanisms to the two functions T1 and T2. TTool offers cryptographic configurations to add security mechanisms to the behaviour of blocks (See our Modelsward 2017 paper). Basically, a cryptographic configuration specifies the type of security mechanism (symmetric cipher, hash, key manipulation, nonce, etc.) and its performance impact in terms of complexity operations by sample. The modified activity diagrams of T1 and T2 are given in Figure \ref{fig:fv3}. Note that only the activity diagrams have been modified with regards to previous version. @@ -314,12 +314,12 @@ The modified activity diagrams of T1 and T2 are given in Figure \ref{fig:fv3}. N \caption{Functional view updated with cryptographic configurations} \label{fig:fv3} \end{figure*} -If you double-click on the SE operator of T1, the following windows should open (see Figure \ref{fig:ccdialog}). This dialog window contains the following field: +If you double-click on the SE operator of T1, the following windows should open (see Figure \ref{fig:ccdialog}). This dialog window contains the following fields: \begin{itemize} \item \textbf{Name} of the configuration. This name is useful to reference a given cryptographic configuration when writing/reading data. For instance, the write operator on $comm$ in T1 uses the Cipherdata cryptographic configuration. \item The \textbf{type} of the cryptographic configuration: Symmetric, Asymmetric, MAC, Hash, Nonce, Advanced. In our case, a symmetric encryption is selected. \item The \textbf{complexity}, in terms of integer operations, of the selected operation -\item The use of \textbf{cryptographic material}: keys, nonces and precise algorithms (AES, etc.) +\item The use of \textbf{cryptographic material}: keys, nonces and precise algorithm (AES, etc.) \end{itemize} @@ -354,14 +354,14 @@ Without taking into account penalties of the hardware platform (e.g. cache miss, \end{figure*} \subsection{Designing security protocols} -During the HW/SW partitioning stage, security mechanisms have been modeled at a high level of abstraction, mostly for placing them correctly in the system, and evaluating their impact on the system performance. During the software design stage, security protocols can be designed in a more precise way. +During the HW/SW partitioning stage, security mechanisms have been modeled at a high level of abstraction, mostly to place them correctly in the system, and to evaluate their impact on the system performance. During the software design stage, security protocols can be designed in a more precise way. -A design contains a block diagram (see Figure \ref{fig:design}) as well as a state machine for each regular block (see Figure \ref{fig:design_t}). +A software design contains a block diagram (see Figure \ref{fig:design}) as well as a state machine for each task block (see Figure \ref{fig:design_t}). -The block diagram contains a main block ("System") with two sub blocks ("T1" and "T2"). Two other blocks "Key" and "Messages" are used to define custom data types. T1 and T2 are cryptoblocks, i.e. they define default cryptographic methods e.g. encrypt, decrypt, hash, mac, message manipulation (concat, cut), etc. Last, a pragma operators: +The block diagram contains a main block ("System") with two sub blocks ("T1" and "T2"). These tasks correspond to the same tasks modeled in the HW/SW Partitioning phase at a higher level of abstraction. Two other blocks "Key" and "Messages" are used to define custom data types. T1 and T2 are cryptoblocks, i.e. they define default cryptographic methods e.g. encrypt, decrypt, hash, mac, message manipulation (concat, cut), etc. Last, a pragma: \begin{itemize} \item links cryptographic keys of T1 and T2. This key "sk" is system-wide, which means that it is shared once for all protocol sessions. -\item gives a security property: the value of the attribute "secretData" of "T1" must remain confidential. +\item gives a security property to check: the value of the attribute "secretData" of "T1" must remain confidential. \end{itemize} diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java index 8f6efb92ac2ea586dc938c41987754fea095dd68..cc1754a0407b7a6f9f83d296de23c7ca9e855ea7 100755 --- a/src/main/java/ui/GTURTLEModeling.java +++ b/src/main/java/ui/GTURTLEModeling.java @@ -748,6 +748,7 @@ public class GTURTLEModeling { TMLArchitecture archi = map.getArch(); TURTLEPanel tmlap = map.getCorrespondanceList().getTG(archi.getFirstCPU()).getTDiagramPanel().tp; TMLActivityDiagramPanel firewallADP = null; + TMLComponentDesignPanel tcp = tmlcdp; TMLComponentTaskDiagramPanel tcdp = tmlcdp.tmlctdp; if (TraceManager.devPolicy == TraceManager.TO_CONSOLE) { MainGUI gui = tmlcdp.getMainGUI(); @@ -758,7 +759,7 @@ public class GTURTLEModeling { int ind = gui.tabs.indexOf(tmlcdp); String tabName = gui.getTitleAt(tmlcdp); gui.cloneRenameTab(ind, "firewallDesign"); - // TMLComponentDesignPanel tcp = (TMLComponentDesignPanel) gui.tabs.get(gui.tabs.size()-1); + tcp = (TMLComponentDesignPanel) gui.tabs.get(gui.tabs.size()-1); newarch.renameMapping(tabName, tabName + "_firewallDesign"); } @@ -768,31 +769,32 @@ public class GTURTLEModeling { TMLADStartState adStart = null; TMLADForEverLoop adLoop = null; TMLADChoice adChoice = null; + TMLADChoice adChoice2 = null; TMLADReadChannel adRC = null; TMLADExecI exec = null; TMLADWriteChannel adWC = null; TMLADStopState adStop = null; - + TMLADStopState adStop2= null; int links = map.getArch().getLinkByHwNode(firewallNode).size(); TraceManager.addDev("Links " + links); HwCPU cpu = new HwCPU(firewallNode.getName()); map.getTMLArchitecture().replaceFirewall(firewallNode, cpu); - for (int link = 0; link < links / 2; link++) { + // for (int link = 0; link < links / 2; link++) { HashMap<TMLChannel, TMLChannel> inChans = new HashMap<TMLChannel, TMLChannel>(); HashMap<TMLChannel, TMLChannel> outChans = new HashMap<TMLChannel, TMLChannel>(); if (TraceManager.devPolicy == TraceManager.TO_CONSOLE) { - firewallComp = new TMLCPrimitiveComponent(0, 0, tmlcdp.tmlctdp.getMinX(), tmlcdp.tmlctdp.getMaxX(), tmlcdp.tmlctdp.getMinY(), tmlcdp.tmlctdp.getMaxY(), false, null, tmlcdp.tmlctdp); - tmlcdp.tmlctdp.addComponent(firewallComp, 0, 0, false, true); - firewallComp.setValueWithChange(firewallNode.getName() + link); - firewallADP = tmlcdp.getTMLActivityDiagramPanel(firewallNode.getName() + link); + firewallComp = new TMLCPrimitiveComponent(tmlcdp.tmlctdp.getMaxX()-100, tmlcdp.tmlctdp.getMaxY()-100, tmlcdp.tmlctdp.getMinX(), tmlcdp.tmlctdp.getMaxX(), tmlcdp.tmlctdp.getMinY(), tmlcdp.tmlctdp.getMaxY(), false, null, tcp.tmlctdp); + tcp.tmlctdp.addComponent(firewallComp, 0, 0, false, true); + firewallComp.setValueWithChange(firewallNode.getName()); + firewallADP = tcp.getTMLActivityDiagramPanel(firewallNode.getName()); } List<TMLChannel> channelsCopy = tmlm.getChannels(); List<TMLChannel> toAdd = new ArrayList<TMLChannel>(); - TMLTask firewall = new TMLTask("TASK__" + firewallNode.getName() + "_" + link, firewallComp, firewallADP); + TMLTask firewall = new TMLTask("TASK__" + firewallNode.getName(), firewallComp, firewallADP); tmlm.addTask(firewall); @@ -805,7 +807,7 @@ public class GTURTLEModeling { TMLTask dest = chan.getDestinationTask(); TMLPort origPort = chan.getOriginPort(); TMLPort destPort = chan.getDestinationPort(); - TMLChannel wr = new TMLChannel(chan.getName() + "_firewallIn" + link, chan.getReferenceObject()); + TMLChannel wr = new TMLChannel(chan.getName() + "_firewallIn", chan.getReferenceObject()); //Specify new channel attributes wr.setSize(chan.getSize()); wr.setMax(chan.getMax()); @@ -813,7 +815,7 @@ public class GTURTLEModeling { wr.setType(TMLChannel.BRBW); wr.setPriority(chan.getPriority()); wr.setTasks(orig, firewall); - TMLChannel rd = new TMLChannel(chan.getName() + "_firewallOut" + link, chan.getReferenceObject()); + TMLChannel rd = new TMLChannel(chan.getName() + "_firewallOut", chan.getReferenceObject()); rd.setTasks(firewall, dest); rd.setSize(chan.getSize()); rd.setMax(chan.getMax()); @@ -849,47 +851,63 @@ public class GTURTLEModeling { tmp = new TGConnectorTMLAD(adChoice.getX(), adChoice.getY(), firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP, adLoop.getTGConnectingPointAtIndex(1), adChoice.getTGConnectingPointAtIndex(0), new Vector<Point>()); firewallADP.addComponent(tmp, adChoice.getX(), adChoice.getY(), false, true); for (TMLChannel chan : inChans.keySet()) { + TMLChannel newChan = inChans.get(chan); - TMLCChannelOutPort originPort = new TMLCChannelOutPort(0, 0, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, null, tcdp); - TMLCChannelOutPort destPort = new TMLCChannelOutPort(0, 0, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, null, tcdp); - for (TGComponent tg : tcdp.getComponentList()) { + TMLCChannelOutPort originPort = new TMLCChannelOutPort(0, 0, tcp.tmlctdp.getMinX(), tcp.tmlctdp.getMaxX(), tcp.tmlctdp.getMinY(), tcp.tmlctdp.getMaxX(), true, null, tcp.tmlctdp); + TMLCChannelOutPort destPort = new TMLCChannelOutPort(0, 0, tcp.tmlctdp.getMinX(), tcp.tmlctdp.getMaxX(), tcp.tmlctdp.getMinY(), tcp.tmlctdp.getMaxX(), true, null, tcp.tmlctdp); + for (TGComponent tg : tcp.tmlctdp.getComponentList()) { if (tg instanceof TMLCPrimitiveComponent) { if (tg.getValue().equals(newChan.getOriginTask().getName().split("__")[1])) { - originPort = new TMLCChannelOutPort(tg.getX(), tg.getY(), tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, tg, tcdp); + System.out.println(newChan.getName() + " " + tg.getValue()); + originPort = new TMLCChannelOutPort(tg.getX(), tg.getY(), tcp.tmlctdp.getMinX(), tcp.tmlctdp.getMaxX(), tcp.tmlctdp.getMinY(), tcp.tmlctdp.getMaxX(), true, tg, tcp.tmlctdp); originPort.commName = newChan.getName(); - tcdp.addComponent(originPort, tg.getX(), tg.getY(), true, true); + tcp.tmlctdp.addComponent(originPort, tg.getX(), tg.getY(), true, true); } else if (tg.getValue().equals(firewallNode.getName())) { - destPort = new TMLCChannelOutPort(tg.getX(), tg.getY(), tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, tg, tcdp); + System.out.println(newChan.getName() + tg.getValue()); + destPort = new TMLCChannelOutPort(tg.getX(), tg.getY(), tcp.tmlctdp.getMinX(), tcp.tmlctdp.getMaxX(), tcp.tmlctdp.getMinY(), tcp.tmlctdp.getMaxX(), true, tg, tcp.tmlctdp); destPort.isOrigin = false; destPort.commName = newChan.getName(); - tcdp.addComponent(destPort, tg.getX(), tg.getY(), true, true); + tcp.tmlctdp.addComponent(destPort, tg.getX(), tg.getY(), true, true); } } } - TMLCPortConnector conn = new TMLCPortConnector(0, 0, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, null, tcdp, originPort.getTGConnectingPointAtIndex(0), destPort.getTGConnectingPointAtIndex(0), new Vector<Point>()); - tcdp.addComponent(conn, 0, 0, false, true); - + System.out.println("Ports " + originPort + " " + destPort); + TMLCPortConnector conn = new TMLCPortConnector(0, 0, tcp.tmlctdp.getMinX(), tcp.tmlctdp.getMaxX(), tcp.tmlctdp.getMinY(), tcp.tmlctdp.getMaxX(), true, null, tcp.tmlctdp, originPort.getTGConnectingPointAtIndex(0), destPort.getTGConnectingPointAtIndex(0), new Vector<Point>()); + tcp.tmlctdp.addComponent(conn, 0, 0, false, true); + + + originPort = new TMLCChannelOutPort(0, 0, tcp.tmlctdp.getMinX(), tcp.tmlctdp.getMaxX(), tcp.tmlctdp.getMinY(), tcp.tmlctdp.getMaxX(), true, null, tcp.tmlctdp); + destPort = new TMLCChannelOutPort(0, 0, tcp.tmlctdp.getMinX(), tcp.tmlctdp.getMaxX(), tcp.tmlctdp.getMinY(), tcp.tmlctdp.getMaxX(), true, null, tcp.tmlctdp); + TMLChannel wrChan = outChans.get(chan); - for (TGComponent tg : tcdp.getComponentList()) { + for (TGComponent tg : tcp.tmlctdp.getComponentList()) { if (tg instanceof TMLCPrimitiveComponent) { if (tg.getValue().equals(firewallNode.getName())) { - originPort = new TMLCChannelOutPort(tg.getX(), tg.getY(), tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, tg, tcdp); + System.out.println(newChan.getName() + tg.getValue()); + originPort = new TMLCChannelOutPort(tg.getX(), tg.getY(), tcp.tmlctdp.getMinX(), tcp.tmlctdp.getMaxX(), tcp.tmlctdp.getMinY(), tcp.tmlctdp.getMaxX(), true, tg, tcp.tmlctdp); originPort.commName = wrChan.getName(); - tcdp.addComponent(originPort, tg.getX(), tg.getY(), true, true); + tcp.tmlctdp.addComponent(originPort, tg.getX(), tg.getY(), true, true); } else if (tg.getValue().equals(wrChan.getDestinationTask().getName().split("__")[1])) { - destPort = new TMLCChannelOutPort(tg.getX(), tg.getY(), tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, tg, tcdp); + System.out.println(wrChan.getName() + " "+ tg.getValue()); + destPort = new TMLCChannelOutPort(tg.getX(), tg.getY(), tcp.tmlctdp.getMinX(), tcp.tmlctdp.getMaxX(), tcp.tmlctdp.getMinY(), tcp.tmlctdp.getMaxX(), true, tg, tcp.tmlctdp); destPort.isOrigin = false; destPort.commName = wrChan.getName(); - tcdp.addComponent(destPort, tg.getX(), tg.getY(), true, true); + tcp.tmlctdp.addComponent(destPort, tg.getX(), tg.getY(), true, true); } } } - conn = new TMLCPortConnector(0, 0, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxX(), true, null, tcdp, originPort.getTGConnectingPointAtIndex(0), destPort.getTGConnectingPointAtIndex(0), new Vector<Point>()); - tcdp.addComponent(conn, 0, 0, false, true); + + System.out.println("Ports " + originPort + " " + destPort); + conn = new TMLCPortConnector(0, 0, tcp.tmlctdp.getMinX(), tcp.tmlctdp.getMaxX(), tcp.tmlctdp.getMinY(), tcp.tmlctdp.getMaxX(), true, null, tcp.tmlctdp, originPort.getTGConnectingPointAtIndex(0), destPort.getTGConnectingPointAtIndex(0), new Vector<Point>()); + tcp.tmlctdp.addComponent(conn, 0, 0, false, true); + } int xpos = 200; int i = 1; for (TMLChannel chan : inChans.keySet()) { + if (i>3){ + break; + } TMLChannel newChan = inChans.get(chan); adRC = new TMLADReadChannel(xpos, 350, firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP); adRC.setChannelName(newChan.getName()); @@ -904,37 +922,48 @@ public class GTURTLEModeling { exec = new TMLADExecI(xpos, 400, firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP); exec.setDelayValue(Integer.toString(firewallNode.latency)); - firewallADP.addComponent(exec, 400, 200, false, true); + firewallADP.addComponent(exec, xpos, 400, false, true); tmp = new TGConnectorTMLAD(exec.getX(), exec.getY(), firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP, adRC.getTGConnectingPointAtIndex(1), exec.getTGConnectingPointAtIndex(0), new Vector<Point>()); firewallADP.addComponent(tmp, exec.getX(), exec.getY(), false, true); + + + + + adChoice2 = new TMLADChoice(xpos, 500, firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP); + firewallADP.addComponent(adChoice2, 500, 300, false, true); + + tmp = new TGConnectorTMLAD(exec.getX(), exec.getY(), firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP, exec.getTGConnectingPointAtIndex(1), adChoice2.getTGConnectingPointAtIndex(0), new Vector<Point>()); + firewallADP.addComponent(tmp, exec.getX(), exec.getY(), false, true); + - if (channelAllowed(map, chan)) { + // if (channelAllowed(map, chan)) { TMLChannel wrChan = outChans.get(chan); - adWC = new TMLADWriteChannel(xpos, 400, firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP); + adWC = new TMLADWriteChannel(xpos, 600, firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP); adWC.setChannelName(wrChan.getName()); - adWC.setSamples("1"); - firewallADP.addComponent(adWC, xpos, 400, false, true); + adWC.setSamples("1"); + firewallADP.addComponent(adWC, xpos, 600, false, true); - tmp = new TGConnectorTMLAD(exec.getX(), exec.getY(), firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP, exec.getTGConnectingPointAtIndex(1), adWC.getTGConnectingPointAtIndex(0), new Vector<Point>()); + + tmp = new TGConnectorTMLAD(exec.getX(), exec.getY(), firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP, adChoice2.getTGConnectingPointAtIndex(1), adWC.getTGConnectingPointAtIndex(0), new Vector<Point>()); firewallADP.addComponent(tmp, exec.getX(), exec.getY(), false, true); - adStop = new TMLADStopState(xpos, 500, firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP); - firewallADP.addComponent(adStop, xpos, 500, false, true); + adStop = new TMLADStopState(xpos, 650, firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP); + firewallADP.addComponent(adStop, xpos, 650, false, true); tmp = new TGConnectorTMLAD(adStop.getX(), adStop.getY(), firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP, adWC.getTGConnectingPointAtIndex(1), adStop.getTGConnectingPointAtIndex(0), new Vector<Point>()); firewallADP.addComponent(tmp, adStop.getX(), adStop.getY(), false, true); - } else { - adStop = new TMLADStopState(xpos, 500, firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP); - firewallADP.addComponent(adStop, xpos, 500, false, true); + // } else { + adStop2 = new TMLADStopState(xpos, 650, firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP); + firewallADP.addComponent(adStop2, xpos, 650, false, true); - tmp = new TGConnectorTMLAD(adStop.getX(), adStop.getY(), firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP, exec.getTGConnectingPointAtIndex(1), adStop.getTGConnectingPointAtIndex(0), new Vector<Point>()); + tmp = new TGConnectorTMLAD(adStop.getX(), adStop.getY(), firewallADP.getMinX(), firewallADP.getMaxX(), firewallADP.getMinY(), firewallADP.getMaxY(), false, null, firewallADP, adChoice2.getTGConnectingPointAtIndex(2), adStop2.getTGConnectingPointAtIndex(0), new Vector<Point>()); firewallADP.addComponent(tmp, adStop.getX(), adStop.getY(), false, true); - } + // } xpos += 100; i++; } - } + // } TMLStartState start = new TMLStartState("start", adStart); act.setFirst(start); @@ -1097,8 +1126,8 @@ public class GTURTLEModeling { for (String cpuName : selectedCpuTasks.keySet()) { Map<String, HSMChannel> hsmChannels = new HashMap<String, HSMChannel>(); TMLCPrimitiveComponent hsm = new TMLCPrimitiveComponent(0, 500, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxY(), false, null, tcdp); - TAttribute isEnc = new TAttribute(2, "isEnc", "true", 4); - hsm.getAttributeList().add(isEnc); + //TAttribute isEnc = new TAttribute(2, "isEnc", "true", 4); + //hsm.getAttributeList().add(isEnc); tcdp.addComponent(hsm, 0, 500, false, true); hsm.setValueWithChange("HSM_" + cpuName); //Find all associated components @@ -1139,8 +1168,8 @@ public class GTURTLEModeling { TMLActivityDiagramPanel tad = t.getTMLActivityDiagramPanel(compName); Set<TGComponent> channelInstances = new HashSet<TGComponent>(); Set<TGComponent> secOperators = new HashSet<TGComponent>(); - isEnc = new TAttribute(2, "isEnc", "true", 4); - comp.getAttributeList().add(isEnc); + // isEnc = new TAttribute(2, "isEnc", "true", 4); + //comp.getAttributeList().add(isEnc); //Find all unsecured channels //For previously secured channels, relocate encryption to the hsm @@ -1248,7 +1277,7 @@ public class GTURTLEModeling { if (!hsmChan.isChan) { originPort.typep = 2; destPort.typep = 2; - originPort.setParam(0, new TType(2)); + // originPort.setParam(0, new TType(2)); } destPort.isOrigin = !hsmChan.isOrigin; @@ -1289,12 +1318,11 @@ public class GTURTLEModeling { fromStart = tad.findTGConnectorEndingAt(chan.getTGConnectingPointAtIndex(0)); TGConnectingPoint point = fromStart.getTGConnectingPointP2(); - //set isEnc to true int yShift = 50; TMLADSendRequest req = new TMLADSendRequest(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad); req.setRequestName("startHSM_" + cpuName); - req.setParam(0, "isEnc"); + // req.setParam(0, "isEnc"); tad.addComponent(req, xpos, ypos + yShift, false, true); fromStart.setP2(req.getTGConnectingPointAtIndex(0)); @@ -1374,10 +1402,10 @@ public class GTURTLEModeling { //Set isEnc to false int yShift = 50; - TMLADActionState act = new TMLADActionState(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad); - act.setValue("isEnc=false"); - tad.addComponent(act, xpos, ypos + yShift, false, true); - fromStart.setP2(act.getTGConnectingPointAtIndex(0)); + // TMLADActionState act = new TMLADActionState(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad); + // act.setValue("isEnc=false"); + // tad.addComponent(act, xpos, ypos + yShift, false, true); + //fromStart.setP2(act.getTGConnectingPointAtIndex(0)); //Add send request operator @@ -1385,16 +1413,16 @@ public class GTURTLEModeling { yShift += 50; TMLADSendRequest req = new TMLADSendRequest(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad); req.setRequestName("startHSM_" + cpuName); - req.setParam(0, "isEnc"); + // req.setParam(0, "isEnc"); req.makeValue(); tad.addComponent(req, xpos, ypos + yShift, false, true); //Add connection - fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>()); - fromStart.setP1(act.getTGConnectingPointAtIndex(1)); + // fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>()); + // fromStart.setP1(act.getTGConnectingPointAtIndex(1)); fromStart.setP2(req.getTGConnectingPointAtIndex(0)); - tad.addComponent(fromStart, xpos, ypos, false, true); + // tad.addComponent(fromStart, xpos, ypos, false, true); yShift += 50; @@ -1437,7 +1465,7 @@ public class GTURTLEModeling { //Shift components down to make room for the added ones, and add security contexts to write channels for (TGComponent tg : tad.getComponentList()) { - if (tg.getY() >= ypos && tg != wr && tg != req && tg != rd && tg != chan && tg != act) { + if (tg.getY() >= ypos && tg != wr && tg != req && tg != rd && tg != chan) { tg.setCd(tg.getX(), tg.getY() + yShift); } } @@ -1461,7 +1489,7 @@ public class GTURTLEModeling { fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>()); - TMLADReadRequestArg req = new TMLADReadRequestArg(300, 100, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad); +/* TMLADReadRequestArg req = new TMLADReadRequestArg(300, 100, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad); tad.addComponent(req, 300, 100, false, true); req.setParam(0, "isEnc"); req.makeValue(); @@ -1471,14 +1499,14 @@ public class GTURTLEModeling { fromStart.setP2(req.getTGConnectingPointAtIndex(0)); tad.addComponent(fromStart, 300, 200, false, true); - +*/ TMLADChoice choice = new TMLADChoice(300, 200, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad); tad.addComponent(choice, 300, 200, false, true); //Connect readrequest and choice fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>()); - fromStart.setP1(req.getTGConnectingPointAtIndex(1)); + fromStart.setP1(start.getTGConnectingPointAtIndex(0)); fromStart.setP2(choice.getTGConnectingPointAtIndex(0)); tad.addComponent(fromStart, 300, 200, false, true); @@ -1567,6 +1595,17 @@ public class GTURTLEModeling { fromStart.setP1(enc.getTGConnectingPointAtIndex(1)); fromStart.setP2(wr.getTGConnectingPointAtIndex(0)); tad.addComponent(fromStart, 300, 200, false, true); + + //Add Stop + TMLADStopState stop = new TMLADStopState(xc, 600, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad); + tad.addComponent(stop, xc, 700, false, true); + + + //Connext stop and write channel + fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>()); + fromStart.setP1(wr.getTGConnectingPointAtIndex(1)); + fromStart.setP2(stop.getTGConnectingPointAtIndex(0)); + tad.addComponent(fromStart, 300, 200, false, true); } xc += 300; @@ -1640,6 +1679,17 @@ public class GTURTLEModeling { fromStart.setP1(enc.getTGConnectingPointAtIndex(1)); fromStart.setP2(wr.getTGConnectingPointAtIndex(0)); tad.addComponent(fromStart, 300, 200, false, true); + + //Add Stop + TMLADStopState stop = new TMLADStopState(xc, 600, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad); + tad.addComponent(stop, xc, 700, false, true); + + + //Connext stop and write channel + fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>()); + fromStart.setP1(wr.getTGConnectingPointAtIndex(1)); + fromStart.setP2(stop.getTGConnectingPointAtIndex(0)); + tad.addComponent(fromStart, 300, 200, false, true); } diff --git a/src/main/java/ui/tmldd/TMLArchiFirewallNode.java b/src/main/java/ui/tmldd/TMLArchiFirewallNode.java index af33ff900df90590f4ccb26a7924947c6dc7c3b6..78d15efd187731e3d520e8bc70e4e89caf66c322 100644 --- a/src/main/java/ui/tmldd/TMLArchiFirewallNode.java +++ b/src/main/java/ui/tmldd/TMLArchiFirewallNode.java @@ -67,7 +67,7 @@ public class TMLArchiFirewallNode extends TMLArchiCommunicationNode implements S private int derivationy = 3; private String stereotype = "FIREWALL"; private ArrayList<String> rules = new ArrayList<String>(); - private int latency = 0; + private int latency = 10; public TMLArchiFirewallNode(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) { super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp); diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java index 96070236842347a28e23b054ac85b9cbf23239fa..836f53590fac5a22c6ec2b1c701f17f432014861 100644 --- a/src/main/java/ui/window/JDialogProverifVerification.java +++ b/src/main/java/ui/window/JDialogProverifVerification.java @@ -141,8 +141,8 @@ public class JDialogProverifVerification extends JDialog implements ActionListen //security generation buttons ButtonGroup secGroup; - protected JCheckBox autoSec, autoConf, autoWeakAuth, autoStrongAuth, autoMapKeys, custom, addHSM; - + protected JCheckBox autoConf, autoWeakAuth, autoStrongAuth, custom; + protected JRadioButton autoSec, autoMapKeys, addHSM; protected JTextField encTime, decTime, secOverhead; protected JComboBox<String> addtoCPU; @@ -279,12 +279,13 @@ public class JDialogProverifVerification extends JDialog implements ActionListen c01.gridheight = 1; //genJava.addActionListener(this); - secGroup = new ButtonGroup(); - autoSec = new JCheckBox("Add security"); - jp02.add(autoSec, c01); - autoSec.addActionListener(this); - secGroup.add(autoSec); - autoConf = new JCheckBox("Add security (Confidentiality)"); + + secGroup=new ButtonGroup(); + autoSec= new JRadioButton("Add security"); + jp02.add(autoSec, c01); + autoSec.addActionListener(this); + secGroup.add(autoSec); + autoConf= new JCheckBox("Add security (Confidentiality)"); jp02.add(autoConf, c01); autoConf.setEnabled(false); autoConf.addActionListener(this); @@ -296,25 +297,27 @@ public class JDialogProverifVerification extends JDialog implements ActionListen autoStrongAuth = new JCheckBox("Add security (Strong Authenticity)"); autoStrongAuth.setEnabled(false); jp02.add(autoStrongAuth, c01); - autoStrongAuth.addActionListener(this); - autoMapKeys = new JCheckBox("Add Keys"); - autoMapKeys.addActionListener(this); + + autoStrongAuth.addActionListener(this); + autoMapKeys= new JRadioButton("Add Keys"); + autoMapKeys.addActionListener(this); jp02.add(autoMapKeys, c01); - secGroup.add(autoMapKeys); - addHSM = new JCheckBox("Add HSM"); - jp02.add(addHSM, c01); - addHSM.addActionListener(this); - secGroup.add(addHSM); - jp02.add(new JLabel("Add HSM to component:"), c01); - listIgnored = new JList<String>(ignoredTasks); - - - listPanel = new JPanel(); - GridBagConstraints c02 = new GridBagConstraints(); - c02.gridwidth = 1; - c02.gridheight = 1; - c02.fill = GridBagConstraints.BOTH; - listIgnored.setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION); + secGroup.add(autoMapKeys); + addHSM = new JRadioButton("Add HSM"); + jp02.add(addHSM,c01); + addHSM.addActionListener(this); + secGroup.add(addHSM); + jp02.add(new JLabel("Add HSM to component:"),c01); + listIgnored = new JList<String>(ignoredTasks); + + + listPanel = new JPanel(); + GridBagConstraints c02 = new GridBagConstraints(); + c02.gridwidth=1; + c02.gridheight=1; + c02.fill= GridBagConstraints.BOTH; + listIgnored.setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION ); + listIgnored.addListSelectionListener(this); JScrollPane scrollPane1 = new JScrollPane(listIgnored); scrollPane1.setPreferredSize(new Dimension(250, 200));