Innovative Project: Vehicle to Anything (V2X)

The V2X part of our innovative project is used to exchange messages between a master and slave vehicle. These messages are standardized and are more detailed in the project tab of my portfolio. 

No security is set up on the MQTT server used to carry the V2X messages. The only attempt is the authentication by username / password but which is only a facade security because the communication channel is not encrypted.

In concrete terms, anyone who knows the public IP address of our server can easily intercept the messages and especially the connection identifiers exchanged during the connection establishment phase, as shown in the image below. 

Here, we use the Wireshark utility which allows us to observe the packets exchanged on an interface. We can see the name of the client who sent it, the username and especially the password. We can also see directly the IP address of origin of the message. Finally, all the topics subscribed by the master car are visible on the capture.

In addition to the connection data exchanged, a person able to read all the frames exchanged on the network can also have access to the content of the entire message. On the picture below, we can see who the message comes from (90.55.195.18) which was our master's IP, the publication topic (platooning/cam/master_car) and the content of the message which is in JSON format.

Anyone with this information can compromise confidentiality, availability and integrity. 

For confidentiality, the messages are in clear with information allowing to locate the vehicle with an extreme precision. We are talking here about a few centimeters of precision.

For availability, we can imagine an attacker who saturates the MQTT server or even one of the vehicles with a very large quantity of messages.

For integrity, an attacker can do IP Spoofing and modify the information sent without too much difficulty. We can imagine a man-in-the-middle attack, where a malicious person could send false information to hijack the vehicles or even control them.

Finally, we could reinforce the security of the exchanges by integrating the encryption of the channel with TLS. This is a feature that the MQTT protocol offers natively. However, TLS does not guarantee the security because only the message is encrypted but at the end we can see the message if we have access to one of the components.

ProVerif

ProVerif is an automatic symbolic protocol verifier. It supports a wide range of cryptographic primitives, defined by rewrite rules or by equations. It can prove various security properties: secrecy, authentication, and process equivalences, for an unbounded message space and an unbounded number of sessions. It takes as input a description of the protocol to verify in a dialect of the applied pi calculus, an extension of the pi calculus with cryptography. It automatically translates this protocol description into Horn clauses and determines whether the desired security properties hold by resolution on these clauses. (Source)

Here, we ask ProVerif if the attacker can have access to the GPS coordinates, if he can know the decryption key " K " and if he can make an injection. 

Here is the result after running ProVerif. The summary of the verification shows us that the attacker cannot have access to the GPS coordinates, cannot know the decryption key "K" and cannot perform an injection.