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.

Inria

Use it

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

    java -jar transpiler.jar smartHospital/hospital50.iot smartHospital/attack.json

    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:
    • 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.
    For conveniency, the files generated from the SmartHospital examples are available in resources/smartHospital_bip/.

    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:
    • check out the extended BIP code (to prepare a working distribution with the interactive extension)

      git clone -b staging https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/bip/compiler.git

    • generate BIP distribution: go under compiler/distribution and run

      ./single-archive-dist.sh

    • go under compiler/distribution/build/bip_full and run

      . ./setup.sh

      (Note: you need to do it in bash terminal; also this sets the environment variables, you need to run it every new session).

    You can now run the script

    ./compile_model

    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:

    launch -m model50:bip -r mc:bltl -a montecarlo -A"Total samples"=1000 >> results50

    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.

Docs

Our publications:

Useful links:

Contact us

 E-Mail us at: delphine.beaulaton [at] irisa.fr
ioana-domnina.cristescu [at] inria.fr
najah.ben-said [at] inria.fr

Powered by w3.css