Verifying data secure flow in AUTOSAR models

This paper presents an approach for enhancing the design phase of AUTOSAR models when security annotations are required. The approach is based on information flow analysis and abstract interpretation. The analysis evaluates the correctness of the model by assessing if the flow of data is secure with respect to causal data dependencies within the model. To find these dependencies an exhaustive search through the model would be required. Abstract interpretation is used as a trade-off between the precision and complexity of the analysis. The approach also provides annotated models without oversizing the set of annotations.