Security-Minded Verification of Cooperative Awareness Messages

The process of identifying threats to systems via threat modelling is often kept separate from the process of formally proving correctness of systems. In this paper we present a hybrid approach to performing both methodologies simultaneously via an example case-study of Cooperative Awareness Messages used by Connected Vehicles. By using this hybrid approach security properties can be identified and formally verified.

Importance

Formal verification is commonly used in systems where a high level of assurance is needed about a system, often in terms of the safe operating of that system. For these systems, security assurances are also important but the process of formally verifying security properties is often a separate process. Combining these two approaches allows the same high level of assurance to be provided about specific security aspects of a system.

Perspectives

Identifying good security properties that are interesting enough for a meaningful formal verification is hard. For many security properties it may not make sense to verify them, for example, for a verification that a communication channel is encrypted including proofs about cryptographic primitives is excessive for high-level applications. But verifying that the protocol is https instead of http is too trivial to be a useful proof. This is why in this paper we tie the security properties back to a safety property of the system.

Additionally, the suitability of different formal verification techniques depends on the security property. For some security properties (availability from the perspective of generating messages) we were able to use model checking and theorem provers, however, this approach will not be suitable in all cases. We could not verify availability from the perspective of receiving a message using these techniques. This is because eventually the processing capacity of the device will be exceeded, so the availability property cannot hold in all situations. Instead, we used runtime verification to implement a monitor for the availability property from the perspective of receving messages.

So while important to provide strong guarantees about the system’s security, it can be challenging to implement useful verification of such properties. Finally, the threat modelling process will need to identify security properties of interest, so unknown threats will still not be considered in this security-minded verification approach.

Extends

This paper extends a previous shorter paper:
Marie Farrell, Matthew Bradbury, Michael Fisher, Louise A. Dennis, Clare Dixon, Hu Yuan, and Carsten Maple. Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages. In Peter Csaba Ölveczky and Gwen Salaün, editors, Software Engineering and Formal Methods, 471–490. Cham, 2019. Springer International Publishing. doi:10.1007/978-3-030-30446-1 25.