TTool merge requestshttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests2024-03-27T09:28:56Zhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/485Avatar security tests2024-03-27T09:28:56ZJawher JerrayAvatar security testsAdd Avatar and Diplodocus Security tests
Fix bugs in TMLTextSpecification and TML2AvatarAdd Avatar and Diplodocus Security tests
Fix bugs in TMLTextSpecification and TML2Avatarhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/484CAPEC Tracer Functionality2024-03-22T16:44:04ZAlan Birchler De AllendeCAPEC Tracer FunctionalityIntegrated the CAPEC tracing functionality into TTool's AI GUI window. To use this functionality, Python 3 needs to be installed. Then, run the following commands on your terminal: "pip install --user -r <path_to_your_ttool_installation>...Integrated the CAPEC tracing functionality into TTool's AI GUI window. To use this functionality, Python 3 needs to be installed. Then, run the following commands on your terminal: "pip install --user -r <path_to_your_ttool_installation>/src/main/resources/capec_tracer/requirements_capec_tracer.txt" and "python3 -m spacy download en_core_web_sm". You should see the CAPEC tracer option at the bottom of the list of available AI chat options.Ludovic ApvrilleLudovic Apvrillehttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/483Security results in Diplodocus2024-03-15T14:30:46ZJawher JerraySecurity results in Diplodocus- Improve the display of security results in Diplodocus.
- Show all Proverif traces for each channel (conf and auth).
- Show ProVerif traces for a specific operator in the activity diagram (conf and auth).
- Upgrade the translation from ...- Improve the display of security results in Diplodocus.
- Show all Proverif traces for each channel (conf and auth).
- Show ProVerif traces for a specific operator in the activity diagram (conf and auth).
- Upgrade the translation from TML to Avatar.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/482Backtrace Confidentiality in AD2024-02-28T08:57:28ZJawher JerrayBacktrace Confidentiality in ADDisplay confidentiality result for each write channel in activity diagramsDisplay confidentiality result for each write channel in activity diagramshttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/481new presentation for SecurityPattern2024-02-09T18:19:32ZJawher Jerraynew presentation for SecurityPatternhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/480fix a bug in backtracing Auth in AD2024-01-24T09:31:50ZJawher Jerrayfix a bug in backtracing Auth in ADFix a bug in clearing the previous backtracing of Authenticity in Activity Diagrams before each security verificationFix a bug in clearing the previous backtracing of Authenticity in Activity Diagrams before each security verificationhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/479fix a bug in Avatar when handling an Else guard2024-01-16T08:36:43ZJawher Jerrayfix a bug in Avatar when handling an Else guardTo solve Issue #398To solve Issue #398https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/478Adding a compiler for JURASSIC AMULET2023-11-29T18:06:21ZBastien SultanAdding a compiler for JURASSIC AMULETAdding a compiler for JURASSIC AMULET, including a new package tmltranslator.mutations.Adding a compiler for JURASSIC AMULET, including a new package tmltranslator.mutations.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/477[WIP] simulation code generation fixes2023-11-29T14:36:15ZMarvin Häuser[WIP] simulation code generation fixesRunning DSE on "SmartCardProtocol" currently crashes all simulation binaries on AARCH64 macOS with Xcode Clang. I identified multiple culprits, such as undefined behaviour when traversing a variadic argument list, or dereferencing a NULL...Running DSE on "SmartCardProtocol" currently crashes all simulation binaries on AARCH64 macOS with Xcode Clang. I identified multiple culprits, such as undefined behaviour when traversing a variadic argument list, or dereferencing a NULL pointer. To further harden the code against such bugs, I propose enabling the typical "extra" warnings, as well as making most warnings fatal. This already uncovered further issues, such as uninitialized return values. Please refer for the individual commits for details.
This remains a WIP draft for three reasons:
- There are open questions for commits marked as [WIP]:
- https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/commit/6f1d3dd6e69e742daab3d0c7eaaf8f58ac461c81: This is supposed to be NULL in real-world runs?
- https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/commit/9f51e068890eedc5ed978295a29f1c9895ba7def: The types for these are unsigned, so the condition is always true. Is it realistic for the subtraction done at initialization to underflow and must this be detected instead? Should the code maybe use overflow-safe arithmetics?
- https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/commit/f62c886cd9fc34abfda76ebe66cb29c957335177: I took best guesses here at what is intended to fall through and what might be a bug, but I have no definite answers.
- I tested the changes only with "SmartCardProtocol", other code generation samples may emit errors.
- Project-specific code used by end-user projects may start emitting errors as well. Maybe this should be suppressible via an environment variable or some custom Makefile with a property? I am not sure which route to take.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/476Pattern generation2023-11-15T17:23:37ZJawher JerrayPattern generation* Add comments in script files that test pattern handling.
* Execute command line that contains a comment.
* Fix typos in the description of some pattern handling commands.* Add comments in script files that test pattern handling.
* Execute command line that contains a comment.
* Fix typos in the description of some pattern handling commands.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/475Pattern generation2023-11-15T13:25:34ZJawher JerrayPattern generation* Fix indentation problems.
* Remove drawTMLAndTMAPSpecification() method + add new parameter for suffix in drawTMLSpecification() and drawTMAPSpecification() methods.* Fix indentation problems.
* Remove drawTMLAndTMAPSpecification() method + add new parameter for suffix in drawTMLSpecification() and drawTMAPSpecification() methods.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/474JNA: Update to 5.13.0 for ARM compatibility v22023-11-20T08:01:13ZMarvin HäuserJNA: Update to 5.13.0 for ARM compatibility v2Currently, terminal support is broken on macOS and Linux on AARCH64, because JNA 3.3.0 does not support this architecture. Update the library to the latest version, which supports AARCH64 and enables terminal support.
Tested to enable t...Currently, terminal support is broken on macOS and Linux on AARCH64, because JNA 3.3.0 does not support this architecture. Update the library to the latest version, which supports AARCH64 and enables terminal support.
Tested to enable terminal support on AARCH64 macOS with JDK 21 and Linux with JDK 11. Tested on AARCH64 Windows with JDK 21 to not cause regressions (terminal support is equally broken before and after the change).
V2: Fix deprecation and other warnings introduced by updating JNA. This may make the code incompatible with previous versions of the library.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/473Revert "Merge branch 'jna_update' into 'master'"2023-11-14T16:57:24ZLudovic ApvrilleRevert "Merge branch 'jna_update' into 'master'"This reverts merge request !471This reverts merge request !471https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/472Pattern handling2023-11-15T09:54:21ZJawher JerrayPattern handlingAdd pattern handling using CLI or graphical interface
+ add tests for the CLI commands.Add pattern handling using CLI or graphical interface
+ add tests for the CLI commands.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/471JNA: Update to 5.13.0 for ARM compatibility2023-11-14T16:31:56ZMarvin HäuserJNA: Update to 5.13.0 for ARM compatibilityCurrently, terminal support is broken on macOS and Linux on AARCH64,
because JNA 3.3.0 does not support this architecture. Update the library
to the latest version, which supports AARCH64 and enables terminal
support.
Tested to enable t...Currently, terminal support is broken on macOS and Linux on AARCH64,
because JNA 3.3.0 does not support this architecture. Update the library
to the latest version, which supports AARCH64 and enables terminal
support.
Tested to enable terminal support on AARCH64 macOS with JDK 21 and Linux with JDK 11. Tested on AARCH64 Windows with JDK 21 to not cause regressions (terminal support is equally broken before and after the change).https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/470Improving AImulet module2023-08-30T11:24:16ZBastien SultanImproving AImulet modulehttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/469Improving AIMULET and adding a test on AvatarSpecification cloning2023-08-03T11:39:36ZBastien SultanImproving AIMULET and adding a test on AvatarSpecification cloninghttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/468Adding semantic feedback to AIMULET2023-07-31T11:23:31ZBastien SultanAdding semantic feedback to AIMULEThttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/467fix a bug in Diplodocus code generator2023-07-26T10:41:39ZJawher Jerrayfix a bug in Diplodocus code generatorFix a bug in the search for the path between the CPU of the sending task and the CPU of the receiving task while passing through the memory of the channel.Fix a bug in the search for the path between the CPU of the sending task and the CPU of the receiving task while passing through the memory of the channel.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/466Update: auto mapping keys + pvspec generation + random sequence translation2023-07-19T14:46:49ZJawher JerrayUpdate: auto mapping keys + pvspec generation + random sequence translation- Fix bracketing in pvspec generation
- Update random sequence translation from TML to Avatar
- Update auto mapping keys
- Change type of some variables from HashMap to LinkedHashMap to maintain order- Fix bracketing in pvspec generation
- Update random sequence translation from TML to Avatar
- Update auto mapping keys
- Change type of some variables from HashMap to LinkedHashMap to maintain order