The IoT Modeling Language
The IoT modeling language is a formal language for specifying and enforcing security in IoT systems. It is developped in TAMIS team, at INRIA Rennes.
We will guide on how to use our framework with an example, a Smart Hospital system. First you have to download the resources folder. Inside you will find:
- The IoT model and its attack tree
In resources/smartHospital there are two versions of a Smart Hospital hospital50.iot and hospital100.iot. The attack tree is modeled in a file attack.json.
- The transpiler from IoT to BIP. Available as a jar, called transpiler.jar. To run it, write
where the first argument is the path to the IoT model and the second argument is the path to the attack tree.
This command generates the following files:
java -jar transpiler.jar smartHospital/hospital50.iot smartHospital/attack.json
For conveniency, the files generated from the SmartHospital examples are available in resources/smartHospital_bip/.
- compile_model.sh is a script that runs BIP on the generated model;
- iot_model.bip, monitor.bip and model_monitor.bip are the generated BIP files.
The source code of the transpiler is also available.
- The auxiliary files for running BIP The script compile_model.sh as well as the files medjack_types.c, medjack_types.h are necessary for compiling the BIP files into an executable. However BIP is not available as a jar, so you need to install it and set up its environment variables. There are several steps to follow:
You can now run the script
in the resources/smartHospital_bip/ folders to generate the two executables, called system50 and system100.
- The Plasma model checker Is available in the folder ressources/plasmalab-1.4.5-SNAPSHOT. You have to copy here the two files system50 and system100. You can then either run Plasma once, for example using the Monte Carlo method with 1000 samples:
or you can generate a set of results using the script experiements_server.sh. Be careful if using the script as the results are large and importance splitting uses a lot of memory. It risks to trigger a Java Garbage Collector expection.
launch -m model50:bip -r mc:bltl -a montecarlo -A"Total samples"=1000 >> results50