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/398Bug in guard with else2024-01-25T11:16:38ZJawher JerrayBug in guard with else# Summary
The syntax checker does not detect incorrect use of "else" guard and returns an exception when a state has a single next with an "else" in the guard of the transition.
# Example Project
In attach 3 Avatar examples where the ...# Summary
The syntax checker does not detect incorrect use of "else" guard and returns an exception when a state has a single next with an "else" in the guard of the transition.
# Example Project
In attach 3 Avatar examples where the Else guard is used incorrectly.
[bug-guardElse-in-avatar.xml](/uploads/c167b5fe269acbb665c61c5fa837576b/bug-guardElse-in-avatar.xml)
# What is the current bug behavior?
(What actually happens)
In the first avatar design, it returns an exception 'NullPointerException'.
For the second model, the syntax analysis is successful however there are two transitions with an "else" in guard.
For the third model, the syntax analysis is successful however an element that has a single next with an "else" in the guard of the transition.
# What is the expected correct behavior?
The syntax checker is expected to return an error for all 3 examples.
# Possible fixes
I created a branch called "fix-avatar-guardElse" that solve this bug, where the "else" guard is allowed to be used at most once and only for states/operators that have more than one next element.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/390Misleading error when ProVerif fails to execute2023-11-09T11:59:23ZMarvin HäuserMisleading error when ProVerif fails to execute# Summary
When ProVerif fails to execute, the "Security verification with ProVerif" dialog reports the error "ERROR: no properties to prove".
# Steps to reproduce
Attempt to start the security verification of a valid project but an in...# Summary
When ProVerif fails to execute, the "Security verification with ProVerif" dialog reports the error "ERROR: no properties to prove".
# Steps to reproduce
Attempt to start the security verification of a valid project but an incorrect ProVerif path.
# Example Project
Any project from the in-built repository from the "security" category.
# What is the current bug behavior?
The error is misleading and may suggest an issue with the model. The logs do indicate the correct error that the execution of ProVerif failed.
# What is the expected correct behavior?
The error should precisely state the source of the error and/or refer to the corresponding log file.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/389Question about properties in requirements diagrams2023-10-06T15:45:23ZDominique BlouinQuestion about properties in requirements diagramsHello
I'm not sure how to use the property blocks in TTool, do you have any resources available that explain how to use it correctly?
I'm already familiar with the requirements themselves, but not how the properties relate to them.
Be...Hello
I'm not sure how to use the property blocks in TTool, do you have any resources available that explain how to use it correctly?
I'm already familiar with the requirements themselves, but not how the properties relate to them.
Best regards
Maisa<br/> Submitted by external user maisa.cietto@usp.brhttps://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/387Certification requirement type2023-09-18T12:31:53ZDominique BlouinCertification requirement typeBonjour!
My name is Maisa and I'm using TTool to model certification requirements for an aircraft system.
However, TTool doesn't provide this requirement type.
It would be very nice to have this type available, if possible.
Cordially,...Bonjour!
My name is Maisa and I'm using TTool to model certification requirements for an aircraft system.
However, TTool doesn't provide this requirement type.
It would be very nice to have this type available, if possible.
Cordially,
Maisa Cietto<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/385Remove errors messages printed in the console by IBSStdParser2023-06-20T09:17:50ZLudovic ApvrilleRemove errors messages printed in the console by IBSStdParserExample of message to be removed:
Syntax error
instead expected token classes are [MINUS, NOT, LPAR, INT, BOOL]
Couldn't repair and continue parseExample of message to be removed:
Syntax error
instead expected token classes are [MINUS, NOT, LPAR, INT, BOOL]
Couldn't repair and continue parseSophie CoudertSophie Couderthttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/384Avatar block diagram: checking of donnected signakls fails: red triangle is d...2023-03-27T11:25:01ZLudovic ApvrilleAvatar block diagram: checking of donnected signakls fails: red triangle is displayed even if signals are correctly connectedhttps://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/382Adding documentation to RG window2023-03-16T13:10:19ZLudovic ApvrilleAdding documentation to RG windowAnd test if traces in graph format are correct.And test if traces in graph format are correct.