The approach

The approach

Methodology

The FORESEEN methodology is based on the following steps:

1. simulation of an autonomous system of vehicles by means of co-simulation and collection of simulation traces;
2. generation of formal models for each trace in terms of a process algebra language;
3. detection of attacks by means of model checking technique;
4. identification of trace segments characteristic of attacks, and of their formal model (as process algebra expressions or temporal logic formulae);
5. using abstract interpretation techniques to quantify the robustness of the analysis.

Steps (2)-(5) are the formal methods-based part of our methodology and can be repeated until the required level of robustness is reached. In the following image is presented a schematic representation of the proposed approach.

FORESEEN methodology schema

Model Based Attack Injection

Once the CPS model has been generated, we proceed to the identification of the safety-critical physical devices, namely sensors and
actuators, which are directly responsible for the vehicle control. Then we are able to design attack scenarios, and run the
co-simulation in case of attacks. In particular:

• data alteration attacks ranging from temporary to permanent and periodic data alterations are considered
• the attack injection is implemented by modelling the effect of the attack in the system.

Trace Data Collection

Once the attack has been implemented and added to the co-simulation, a set of run with and without the attacks are executed. The data related to the state evolution of the system, which are called traces, are collected. Given the complexity and width of the search space, we adopt an incremental approach, by first producing traces where simple attacks are injected and subsequently create more and more complex attack scenarios. This approach allows us to generate traces in more controlled environment, while at the same time helping the building and validation of formal models.

Model Checking

After the generation of the formal models and the definition of the attack properties, the properties are verified on the driving system models, as shown in the figure below. This is accomplished by using a formal verification environment, that acts as a classificator.