Verifying data secure flow in AUTOSAR models

Abstract

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.

APPENDIX A

• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 

This section reports the abstract rules for the instructions. In the rules we use the following notations:

• i is the bb of the CFG to which the instruction belongs.

• lvar is used for local variables, gvar for global variables, P for sender-receiver ports, arg& denotes arguments passed by reference, ptr is used for pointers and array for arrays.

• f() is used for functions, including runnables.

• $Scope({\mathtt {bb}}_i)$ is a function that returns the set of blocks in the scope of the conditional instruction in $\texttt {bb}_i$.

• $A [{\delta } / {x}]$ is a global context equal to A except for the variable x that is assigned $\delta$. Similarly, for other elements in the global context.

• $Q(M [{\delta } / {x}])$ is a local context equal to Q except for the variable x in memory M that is assigned $\delta$.

• $Q(Env [{\delta } / {Env}])$ is a local context equal to Q except for the environment that is assigned $\delta$.

Some rules regarding global variables are omitted, because they can easily be derived from the corresponding rule of local variable using the global context in place of the local memory. We note that, the level of variables and function’s parameters, return and environment, in the global context file A never decreases. For example, if x is in the global context, the assignment of an expression to x updates the level of x to the lub between the current level and the level of the expression. If x is in the local memory the assignment of an expression to x sets the level of x to level of the expression.

When the abstract interpreter finds a function call it applies the three invoke rules in sequence:

• the first updates the global context with the levels of the actual parameters

• the second updates the variables passed by reference with the level in the global context

• the third evaluates the expression of the return of the function using the level in the global context

When the abstract interpreter finds an assignment to a sender/receiver port, which corresponds to a send operation, the abstract rule updates both the value of the sender port and the value of the receiver port in the global context A, using the set of links L.

When the abstract interpreter finds an assignment to a client/server port, this is transformed into a call to the runnable implementing the service. This rule is similar to a function call and it not shown in the figure.