This paper presents a method to check data secure flow in security annotated AUTOSAR models. The approach is based on information flow analysis and abstract interpretation. The analysis computes the lowest security level of data sent on a communication, according to the annotations in the model and the code of runnables. An abstract interpreter executes runnables on abstract domains that abstract from real values and consider only data dependency levels. Data secure flow is verified if data sent on a communication always satisfy the security annotation in the model. The work has been developed in the EU project Safure, where modeling extensions to AUTOSAR have been proposed to improve security in automotive communications.
Verifying Data Secure Flow in AUTOSAR Models by Static Analysis
Cinzia Bernardeschi
;Gianluca Dini;Maurizio Palmieri
2017-01-01
Abstract
This paper presents a method to check data secure flow in security annotated AUTOSAR models. The approach is based on information flow analysis and abstract interpretation. The analysis computes the lowest security level of data sent on a communication, according to the annotations in the model and the code of runnables. An abstract interpreter executes runnables on abstract domains that abstract from real values and consider only data dependency levels. Data secure flow is verified if data sent on a communication always satisfy the security annotation in the model. The work has been developed in the EU project Safure, where modeling extensions to AUTOSAR have been proposed to improve security in automotive communications.File | Dimensione | Formato | |
---|---|---|---|
ForSE_2017_15_CR.pdf
accesso aperto
Descrizione: camera ready
Tipologia:
Documento in Pre-print
Licenza:
Creative commons
Dimensione
315.15 kB
Formato
Adobe PDF
|
315.15 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.