Using Assurance Cases and Boolean Logic Driven Markov Processes to Formalise Cyber Security Concerns for Safety-Critical Interaction with Global Navigation Satellite Systems

Abstract

Satellite-based location and timing systems support a wide range of mass market applications, typically using the GPS infrastructure. Until recently, these applications could not be used within safety-critical interfaces. Limits to the accuracy, availability, integrity and continuity of the space-based signals prevented regulatory agencies from certifying their use. Over the last three months, however, the latest generation of augmented Global Navigation Satellite Systems (GNSS) have been approved for use in safety-related applications. They use a range of techniques to overcome the limitations of previous infrastructures. This means that they can be used as primary navigation tools in a wide range of interactive systems, including aircraft cockpits, railway signalling tools etc. Unfortunately, a range of organisations including the UK Ministry of Defence, have raised concerns about our increasing vulnerability to attacks on these satellite based architectures. These threats are compounded by the difficulty of representing and reasoning about the impact of jamming, spoofing and insider threats for the end-users of safety-critical systems. A sudden loss of navigational support can undermine users confidence in complex applications and pose a significant threat to distributed situation awareness. We show how formal reasoning techniques can be used to identify the safety and security concerns that jeopardise interaction with future generations of Global Navigation Satellite Systems applications.