Analysis of Protocols for High-assurance Networks

• Aim: The project aims to provide authentication and reliable communication protocols for unmanned aerial vehicles (UAVs). It covers both internal communication within the UAV and external communication between a ground station and the vehicle. To show feasability of the approach, the project aims at building a research demo vehicle, which is a modified quadcopter.
• Context: This project deals with the communication aspects of the SMACCM project @ Data61, which is part of DARPA's HACMS program for high-assurance cyber-military systems.
• Approach: External communication must be resistant against common attacks, such as replay, eavesdropping or pretending to be another party. A necessary requirement therefore is authentication (and often encryption). Since there already exist good solutions for authentication and encryption for communication protocols, we use off-the shelf solutions whenever possible. However, due to hard- and software requirements, these solutions sometimes need adaptation. We follow the same approach with regard to reliability.

Activities

• External Communication between the ground station and the air vehicle is a simple one-to-one communication. Since the communication is wireless, in order to ensure that the messages received by the UAV indeed stem from the ground station, and vice versa, the messages should be encrypted and the sender should be authenticated. Moreover, the protocol needs to ensure reliable delivery of messages, in spite of possible message loss due to unreliable channels or sabotage by an attacker. Most of these issues can be considered part of the "secure data link"-challenge.
  A solution considered for the research demo vehicle is the combination of MavLink and HMAC. MavLink is an existing lightweight, header-only message marshalling library for micro air vehicles, such as the demo vehicle; it forms the (insecure) basis for message sending. HMAC (keyed-hash message authentication code) is an off-the-shelf mechanism for message authentication, when combined with any cryptographic hash function such as MD5 or SHA. The purpose is to demonstrate how a previously insecure link can be secured.
  For real UAVs MavLink can easily be replaced by any other link-layer protocol.
  As soon as secure communication is guaranteed, we plan to design (integrate) higher-layer protocols, which handle requirements such as reliable packet delivery.
• Internal Communication in vehicles is often based on a CAN bus for controller area networks (ISO 11898-1:2003). The aim is to analyse and formalise internal communication protocols to form a reliable basis for communication between the components of the UAV. As for the external protocol, the CAN bus protocol needs to ensure reliable delivery of messages, in spite of possible message loss due to unreliable channels or sabotage by an attacker. A problem with CAN bus is that packet pay load is limited to 8 bytes only; this is not sufficient when sending flight control messages or encrypted data. As a consequence we design a fragmentation and reassembly protocol which runs on top of the CAN bus to handle messages with larger pay load. Additionally, security can be improved for wired communication by adding hardware bridges.

 

Publications

 

2017

Rob van Glabbeek and Peter Hoefner Split, send, reassemble: A formal specification of a CAN bus protocol stack 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), pp. 14-52, Uppsala, Sweden, April, 2017

 

Reports

		Robert van Glabbeek and Final verification of network protocol November 2016
		Robert van Glabbeek and Peter Höfner SMACCM Milestone Report: Preliminary trusted gateway implementation February 2016
		Robert van Glabbeek and Peter Höfner SMACCM Milestone Report: Preliminary verification of network protocol November 2015
		Robert van Glabbeek and Peter Höfner SMACCM Milestone Report: Formal specification of protocols for internal high-assurance network July 2015
		Robert van Glabbeek, and Peter Höfner SMACCM Milestone Report: Preliminary formal specification of protocols for internal high-assurance network October 2014
		Robert van Glabbeek, Peter Höfner and Gerwin Klein with contributions by Thomas M. DuBuisson, Galois Inc SMACCM Milestone Report: Network protocol analysis January 2014
		Robert van Glabbeek, Peter Höfner and Gerwin Klein SMACCM Milestone Report: Preliminary network protocol analysis April 2013