TTool issueshttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues2024-03-04T13:57:04Zhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/401Penalties in simulation prevents formal verification2024-03-04T13:57:04ZLudovic ApvrillePenalties in simulation prevents formal verificationBut formal verification icon is still enabled, and formal explo fails -> no info to usersBut formal verification icon is still enabled, and formal explo fails -> no info to usershttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/400Infinite loop on dtree.forceUpdate() in tests2024-02-03T18:30:41ZGuillaume BlancInfinite loop on dtree.forceUpdate() in tests# Summary
When running a test with AbstractUITest, sometimes (randomly), when the function mainGUI.checkModelingSynthax() is called, the dtree.forceUpdate() method blocks indefinitely the execution.
# Steps to reproduce
Run ui.Avatar...# Summary
When running a test with AbstractUITest, sometimes (randomly), when the function mainGUI.checkModelingSynthax() is called, the dtree.forceUpdate() method blocks indefinitely the execution.
# Steps to reproduce
Run ui.AvatarSecurityTests with `mainGUI.checkModelingSyntax(true, true);` instead of `mainGUI.checkModelingSyntax(true, false);` at line 91.
# Relevant logs and/or screenshots
Sometimes, this error is thrown:
```
java.lang.NullPointerException
at java.desktop/javax.swing.JLabel.setIcon(JLabel.java:398)
at java.desktop/javax.swing.tree.DefaultTreeCellRenderer.getTreeCellRendererComponent(DefaultTreeCellRenderer.java:543)
at ui.tree.DiagramTreeRenderer.getTreeCellRendererComponent(DiagramTreeRenderer.java:110)
at java.desktop/javax.swing.plaf.basic.BasicTreeUI$NodeDimensionsHandler.getNodeDimensions(BasicTreeUI.java:3155)
at java.desktop/javax.swing.tree.AbstractLayoutCache.getNodeDimensions(AbstractLayoutCache.java:493)
at java.desktop/javax.swing.tree.VariableHeightLayoutCache$TreeStateNode.updatePreferredSize(VariableHeightLayoutCache.java:1344)
at java.desktop/javax.swing.tree.VariableHeightLayoutCache$TreeStateNode.expand(VariableHeightLayoutCache.java:1465)
at java.desktop/javax.swing.tree.VariableHeightLayoutCache$TreeStateNode.expand(VariableHeightLayoutCache.java:1272)
at java.desktop/javax.swing.tree.VariableHeightLayoutCache.rebuild(VariableHeightLayoutCache.java:728)
at java.desktop/javax.swing.tree.VariableHeightLayoutCache.setModel(VariableHeightLayoutCache.java:111)
at java.desktop/javax.swing.plaf.basic.BasicTreeUI.setModel(BasicTreeUI.java:495)
at java.desktop/javax.swing.plaf.basic.BasicTreeUI$Handler.propertyChange(BasicTreeUI.java:3820)
at java.desktop/java.beans.PropertyChangeSupport.fire(PropertyChangeSupport.java:341)
at java.desktop/java.beans.PropertyChangeSupport.firePropertyChange(PropertyChangeSupport.java:333)
at java.desktop/java.beans.PropertyChangeSupport.firePropertyChange(PropertyChangeSupport.java:266)
at java.desktop/java.awt.Component.firePropertyChange(Component.java:8731)
at java.desktop/javax.swing.JTree.setModel(JTree.java:893)
at ui.tree.JDiagramTree.forceUpdate(JDiagramTree.java:158)
at ui.MainGUI.checkModelingSyntax(MainGUI.java:4505)
at ui.MainGUI.checkModelingSyntax(MainGUI.java:3858)
at ui.AvatarSecurityTests.runTest(AvatarSecurityTests.java:91)
at ui.AvatarSecurityTests.testAvatarSecurityModel(AvatarSecurityTests.java:78)
```
# Possible fixes
We tried to add some delay after loading the model.
The current fix is to remove the forceUpdate() call.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/399ProVerifCodeDirectory path not updated when a new model/project is opened.2024-01-30T16:48:12ZPierre DontenvilleProVerifCodeDirectory path not updated when a new model/project is opened.# Summary
When we want to do a security verification with ProVerif, the ProVerifCodeDirectory path is only updated once even after opening different model or project.
# Steps to reproduce
- Open a security model from the TTOOL reposit...# Summary
When we want to do a security verification with ProVerif, the ProVerifCodeDirectory path is only updated once even after opening different model or project.
# Steps to reproduce
- Open a security model from the TTOOL repository.
- Click on "Synthax analysis" then on "Check Syntax".
- Click on "Security verification (ProVerif)".
- Observe the ProVerifCodeDirectory path in the "Generate ProVerif code in:".
It should be like "TTool/modeling/<model_name>/proverif/"
- Open an other security model from the TTOOL repository.
- Click on "Synthax analysis" then on "Check Syntax".
- Click on "Security verification (ProVerif)".
- Observe the ProVerifCodeDirectory path in the "Generate ProVerif code in:".
It shouldn't have changed : "TTool/modeling/<previous_model_name>/proverif/", instead of being : "TTool/modeling/<new_model_name>/proverif/"
# What is the current bug behavior?
When opening two projects from TTOOL repository (previous and new), the second ProVerifCodeDirectory path is :
"TTool/modeling/<previous_model_name>/proverif/"
# What is the expected correct behavior?
It should be "TTool/modeling/<new_model_name>/proverif/"https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/397Proverif proof on state reachability: new information is fed back for "cannot...2023-12-19T20:01:51ZLudovic ApvrilleProverif proof on state reachability: new information is fed back for "cannot be proved"https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/396Needed functions for security models2023-12-17T16:12:09ZGuillaume BlancNeeded functions for security modelsTo model DiffieHellman-active.pv from Proverif examples, two functions are missing.
First, there is:
```
const g: bitstring.
fun exp(bitstring, bitstring): bitstring.
equation forall x: bitstring, y: bitstring; exp(exp(g, x), y) = exp(e...To model DiffieHellman-active.pv from Proverif examples, two functions are missing.
First, there is:
```
const g: bitstring.
fun exp(bitstring, bitstring): bitstring.
equation forall x: bitstring, y: bitstring; exp(exp(g, x), y) = exp(exp(g, y), x).
```
It is still possible to replace it with `DH(pk(x),y) = DH(pk(y),x)`.
And then there is also:
```
reduc forall m: bitstring, k: bitstring; checksign(sign(m,k), pk(k)) = m.
```https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/395Generated Proverif specification can't be equivalent to an example model2023-12-12T17:38:02ZGuillaume BlancGenerated Proverif specification can't be equivalent to an example modelThe targeted model is "pineedham-shr-orig4-comp.pi".
Here are the impactful differences between the pvspec and the example:
"param keyCompromise = strict." can't be added.
It ensures compromised sessions end before non-compromised ones...The targeted model is "pineedham-shr-orig4-comp.pi".
Here are the impactful differences between the pvspec and the example:
"param keyCompromise = strict." can't be added.
It ensures compromised sessions end before non-compromised ones start.
The getKey function should be private.
Keys that are generated by a process should be instantiated in Process___0 instead of Process___start.
For instance, in the example, "new k" should be in S___0 instead of S___start.
The same thing applies to keys that are passed as a parameter.
Instantiating a key in the init process, then passing it to ___start, and then exchanging it in a channel to ___0 is not equivalent to passing the key directly to ___0.
Finally, removing all ___start processes completely allows to have the expected results.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/394Proverif specification execution fails if typed Pi calculus isn't used2023-12-12T10:02:02ZGuillaume BlancProverif specification execution fails if typed Pi calculus isn't used# Summary
The execution of proverif returns an error if the "Generate typed Pi calculus" isn't checked.
# Steps to reproduce
- Open any security model
- Click on Synthax analysis
- Click on Security Analysis (proverif)
- Uncheck Gener...# Summary
The execution of proverif returns an error if the "Generate typed Pi calculus" isn't checked.
# Steps to reproduce
- Open any security model
- Click on Synthax analysis
- Click on Security Analysis (proverif)
- Uncheck Generate typed Pi calculus
- Execute the verification
# What is the current bug behavior?
The result of the verification is 'Synthax error.: File "../proverif/pvspec", line 4, characters 1-3'
# What is the expected correct behavior?
The same result as if the checkbox was checked should be output.
# Possible fixes
The source of the issue is that the generator outputs "set abbreviateDerivation = false." instead of "param abbreviateDerivation = false." as it should be in Pi.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/393Proverif specification generation fails when using Timer type in messages2023-12-07T15:20:50ZLudovic ApvrilleProverif specification generation fails when using Timer type in messagesSo types in functions are not checked for before proverif generation (e.g., syntax checking)So types in functions are not checked for before proverif generation (e.g., syntax checking)https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/392Z3 DSE crashes on SmartCardProtocol2023-11-07T23:16:21ZMarvin HäuserZ3 DSE crashes on SmartCardProtocol# Summary
Performing Z3 DSE on the SmartCardProtocol project from the in-built repository crashes.
# Steps to reproduce
1. Load the SmartCardProtocol from the in-built repository.
2. Switch to Mapping1 and start Z3 DSE.
# What is th...# Summary
Performing Z3 DSE on the SmartCardProtocol project from the in-built repository crashes.
# Steps to reproduce
1. Load the SmartCardProtocol from the in-built repository.
2. Switch to Mapping1 and start Z3 DSE.
# What is the current bug behavior?
The process fails with the following error:
```
ERROR: Z3 Unknown Exception: Cannot invoke "tmltranslator.TMLTask.getOperation()" because "tmlTask" is null
```
# What is the expected correct behavior?
The process completes successfully, e.g.:
```
Optimized mapping found
The optimal mapping solution is:
(1) Spatial mapping of tasks:
TASK --> PLATFORM NODE
AppC__InterfaceDevice --> cpu0
AppC__SmartCard --> cpu0
AppC__TCPIP --> cpu0
AppC__Application --> cpu0
AppC__Timer --> cpu0
(2) Temporal mapping of tasks:
cpu0 : AppC__Timer at 0 ; AppC__Application at 1 ;
(3) Spatial mapping of channels onto controllers:
Channel(InterfaceDevice,SmartCard) --> cpu0
Channel(SmartCard,TCPIP) --> cpu0
Channel(SmartCard,InterfaceDevice) --> cpu0
Channel(TCPIP,TCPIP) --> cpu0
Channel(TCPIP,Application) --> cpu0
Channel(TCPIP,SmartCard) --> cpu0
Channel(Application,TCPIP) --> cpu0
```
# Possible fixes
The issue is masked or possibly resolved by rolling back the following change:
https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/107/diffs#75d2c997b1d082b003e6aa869cae021c48149d03_108_105
The change is undocumented and the intention is not obvious.
# Relevant logs and/or screenshots
Debugging the code check above with a "task name | writers.Empty() | readers.Empty()" scheme yields:
```
[tmltranslator.dsez3engine.InputInstance] AppC__Timer true true
[tmltranslator.dsez3engine.InputInstance] AppC__InterfaceDevice false false
[tmltranslator.dsez3engine.InputInstance] AppC__TCPIP false false
[tmltranslator.dsez3engine.InputInstance] fAppC__Application false true
[tmltranslator.dsez3engine.InputInstance] AppC__SmartCard false false
```
Thus, ``AppC__Timer`` is not picked as final task with the change from the MR, but is picked prior.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/391JDK 17: Migrate from Nashorn JS engine2023-11-10T18:24:49ZMarvin HäuserJDK 17: Migrate from Nashorn JS engineJDK 17 removed the Nashorn JavaScript engine [1]. This breaks DSE, which expects a JavaScript engine to be registered out-of-the-box. The most commonly accepted alternative to the removed Nashorn engine appears to be Graal.JS, with a mig...JDK 17 removed the Nashorn JavaScript engine [1]. This breaks DSE, which expects a JavaScript engine to be registered out-of-the-box. The most commonly accepted alternative to the removed Nashorn engine appears to be Graal.JS, with a migration guide readily available [2]. As ScriptEngine is not extensively used, the code changes required a fairly minimal to ship and consume Graal.JS along TTool. However, there are complicated considerations regarding combining it with GraalVM to improve performance:
* Optimal configuration requires experimental features to be enabled and module path upgrades [3].
* In a quick and dirty integration test, their class path isolation feature malfunctioned for unknown reasons.
[1] https://openjdk.org/jeps/372
[2] https://www.graalvm.org/latest/reference-manual/js/NashornMigrationGuide/
[3] https://www.graalvm.org/22.1/reference-manual/js/RunOnJDK/#graalvm-javascript-on-jdk-11https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/388Question: Does TTool support the Requirements Interchange Format?2023-09-21T06:29:54ZDominique BlouinQuestion: Does TTool support the Requirements Interchange Format?Hello
Does TTool support the Requirements Interchange Format (ReqIF), proposed by OMG (https://www.omg.org/reqif/)?
Best regards
Maisa
<br/> Submitted by external user maisa.cietto@usp.brHello
Does TTool support the Requirements Interchange Format (ReqIF), proposed by OMG (https://www.omg.org/reqif/)?
Best regards
Maisa
<br/> Submitted by external user maisa.cietto@usp.brhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/386Compilation error after generating Diplodocus Simulation Code2023-07-21T10:06:08ZJawher JerrayCompilation error after generating Diplodocus Simulation Code# Summary
In some cases, when the sending task's CPU, the receiving task's CPU and the channel's memory are linked to different buses, this can produce an error when compiling the generated Diplodocus simulation code.
# Example Projec...# Summary
In some cases, when the sending task's CPU, the receiving task's CPU and the channel's memory are linked to different buses, this can produce an error when compiling the generated Diplodocus simulation code.
# Example Project
Here an example that produces a compilation error in the generating Diplodocus Simulation Code.
[routingPathBug.xml](/uploads/3d090c85a4965a2609fde317b1ca972f/routingPathBug.xml)
# What is the current bug behavior?
In the generated simulation code (appmodel.cpp) and when creating a channel, its Bus masters array may contain undeclared elements.
it is normal that these bus masters are not declared because they do not exist in the architecture.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/383Avatar: authorizing constant attributes2023-03-28T11:55:12ZLudovic ApvrilleAvatar: authorizing constant attributesHaving constant attributes would help the syntax checking of Avatar models.Having constant attributes would help the syntax checking of Avatar models.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/380Using security proof from the command line (TMLMapping)2023-02-28T11:29:09ZLudovic ApvrilleUsing security proof from the command line (TMLMapping)For this, we would need to add security aspects to TML, and parse them back, and allow security verification from CLIFor this, we would need to add security aspects to TML, and parse them back, and allow security verification from CLIhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/373Reset number of samples in a channel with wic command2022-09-09T11:56:08ZJawher JerrayReset number of samples in a channel with wic commandWe can reset the number of samples in a channel using the wic command by putting 0 as # of samples.
We probably could mention this feature in the wic command help.We can reset the number of samples in a channel using the wic command by putting 0 as # of samples.
We probably could mention this feature in the wic command help.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/370Adding help for ports of diplodocus component2022-08-04T12:34:41ZLudovic ApvrilleAdding help for ports of diplodocus componentWe have to explain in particular the capacity and width of channelWe have to explain in particular the capacity and width of channelhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/366Reachability graph: info on values when using complex types2022-07-20T12:14:59ZLudovic ApvrilleReachability graph: info on values when using complex typesValues are simply concatenated e.g. 02 when it should be "0,2"Values are simply concatenated e.g. 02 when it should be "0,2"https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/365New avatar safety property: investigate FIFO size2022-07-20T12:11:37ZLudovic ApvrilleNew avatar safety property: investigate FIFO sizeThat would be great if we could use the FIFO size in Avatar safety property, e.g. A<>FIFO.size<10That would be great if we could use the FIFO size in Avatar safety property, e.g. A<>FIFO.size<10https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/363English menus not displayed correctly in a Windows 10 set in chinese2022-05-19T15:54:54ZLudovic ApvrilleEnglish menus not displayed correctly in a Windows 10 set in chinese![image1](/uploads/f562078163d86f570e7575ef5b7ba43c/image1.png)
![image2](/uploads/3da39d38a8154a2bca4b8d83c14294c1/image2.png)![image1](/uploads/f562078163d86f570e7575ef5b7ba43c/image1.png)
![image2](/uploads/3da39d38a8154a2bca4b8d83c14294c1/image2.png)https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/361Avatar-to-proverif generates an unvalid proverif specification because invali...2022-05-02T16:02:52ZLudovic ApvrilleAvatar-to-proverif generates an unvalid proverif specification because invalid guards for proverif are not detectedFor instance, (a==b) != false generates a faulty proverif specificationFor instance, (a==b) != false generates a faulty proverif specification