The Model-Learning-Checking (shortened MLC) approach combines model-learning to generate formal models of IoT systems and model-checking to evaluate whether security properties hold on these models. In this work, we have chosen to limit the scope of our work to IoT devices, gateways and client applications seen as black boxes. We assume that each device or gateway is physically secured and that we only have access to the network and user interfaces.
The MLC approach consists of:
a Model-Learning-Checking solution to help audit the security of IoT systems. We use the Labelled Transition System (LTS) to express the behaviours of every component of an IoT system. We also express the security measures proposed by the ENISA organisation with linear temporal logic (LTL) formula composed of propositions or predicates. Our approach verifies whether these measures are correctly implemented in an IoT system and returns counterexamples when issues are detected. The former may be used to interpret the results and derive treatments;
a technique to help auditors instantiate LTL formula with fewer efforts. This technique completes the LTS transitions by injecting predicates found in the LTL formula. It is manifest that some expert knowledge is still required to analyse the LTSs. We propose to capture this knowledge into an expert system made up of rules in order to automate the injection and to save time by reusing the expert knowledge encoded in inference rules;
We performed an evaluation on three IoT use-cases given below.
Inference rules for Drools : Rules
Property types : link