Using Assurance Cases and Boolean Logic Driven Markov Processes to Formalise Cyber Security Concerns for Safety-Critical Interaction with Global Navigation Satellite Systems Electronic Communications of the EASST Volume 45 (2011) Proceedings of the Fourth International Workshop on Formal Methods for Interactive Systems (FMIS 2011) Using Assurance Cases and Boolean Logic Driven Markov Processes to Formalise Cyber Security Concerns for Safety-Critical Interaction with Global Navigation Satellite Systems Chris W. Johnson 18 pages Guest Editors: Judy Bowen, Steve Reeves Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST Using Assurance Cases and Boolean Logic Driven Markov Processes to Formalise Cyber Security Concerns for Safety-Critical Interaction with Global Navigation Satellite Systems Chris W. Johnson School of Computing Science, University of Glasgow, Glasgow, UK, G12 8RZ. Johnson@dcs.gla.ac.uk http://www.dcs.gla.ac.uk/∼johnson Abstract: Satellite-based location and timing systems support a wide range of mass market applications, typically using the GPS infrastructure. Until recently, these ap- plications 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 organisa- tions including the UK Ministry of Defence, have raised concerns about our in- creasing 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 ap- plications 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. Keywords: Safety Cases, Boolean Logic Driven Markov Processes, Cyber Security, Global Navigation Satellite Systems 1 Introduction This paper considers security and safety concerns for the users of Global Navigation Satellite Systems (GNSS). Our concern is partly justified because there is a growing dependency on timing and location information provided by these applications. This creates significant vul- nerabilities for many different infrastructures across Europe and North America [Roy11]. First generation GNSS architectures, such as GPS and GLONASS, suffer from a number of errors. Some of these problems stem from satellite geometry. If all the satellites are closely grouped together then the benefits of differential signal processing will be reduced. This tends to act as a multiplier for errors induced from other sources. For instance, gravitational forces create subtle 1 / 18 Volume 45 (2011) mailto:Johnson@dcs.gla.ac.uk http://www.dcs.gla.ac.uk/~johnson Assurance Cases and BDMP Models for Safety and Security in GNSS changes in the orbit of the satellites within a GNSS constellation. Further problems arise from multipath effects. The signals arriving at a receiver are often reflected from large structures in- cluding buildings. This creates inaccuracies of up to 75 meters in urban environments because the reflected signal will take longer to arrive than a direct transmission. Further problems stem from ionospheric effects. Radio waves can be considered to travel at the speed of light in outer space. However, the ionizing effects of solar radiation form layers that refract electromagnetic waves from satellite transmissions. Most end users do not correct for unforeseen changes such as variations introduced by strong solar winds. These errors and the lack of suitable correction mechanisms help to explain why first gen- eration GNSS architectures have not been widely integrated into safety-related systems [BO07, JY11]. For example, the International Civil Aviation Organization (ICAO) Required Naviga- tion Performance provides minimum performance criteria for the use of these architectures in a range of applications. These criteria are expressed in terms of Accuracy- how correct is the air- crafts position estimate; Integrity- the largest aircraft position error can reach without detection; Availability- how often can the aircraft use the systems with the desired accuracy and integrity; Continuity - the probability that an operation once commenced can be completed and Time to Alert the maximum interval before a performance issue is detected. Satellite Based Augmentation Systems (SBAS) address these limitations and are intended to support Safety of Life (SoL) applications. These architectures include the North American Wide Area Augmentation System (WAAS) and the Asian Multi-functional Satellite Augmenta- tion System (MSAS) as well as the European Geostationary Navigation Overlay Service (EG- NOS). These systems use a number of ground reference stations, to compare known information about the time and their location with the signals received from the satellites to compute dif- ferential corrections and integrity data for each monitored satellite. This information is collated by a smaller number of master stations that then broadcast deviation corrections using a second network of geostationary satellites. The corrections can then be applied to location information derived from the GPS or GLONASS networks. Europe has just certified the EGNOS GNSS for Safety of Life (SoL) applications, including approaches to aircraft runways. Further applications are proposed, for example in railway signalling, where exact information about the speed and position of trains can be used to ensure adequate separation without locking sections of track, as in conventional approaches. The EGNOS infrastructure uses redundancy to address many of these concerns in SoL ap- plications. For instance, each of the four master stations rotates from being the Master to a Hot-Back-Up and then to be a Cold-Back-Up. The complexity of the underlying design created a host of human factors concerns. In particular, configuration and maintenance posed particular challenges given the potential consequences of errors by the systems engineering teams. The design of this infrastructure was, therefore, guided by the assumption that no single operator error would lead to a loss of integrity. This has significant implications in terms of the security assessments in later sections; it is less clear whether this level of protection might also be offered against deliberate attacks. The complex and critical nature of satellite based augmentation systems also justifies the use of formal analysis techniques. Numerous mathematical studies were made of the underlying algorithms to establish the correctness of the relationships between the signals received by the ground reference stations and the differential corrections as well as the reliability information Proc. FMIS 2011 2 / 18 ECEASST broadcast to the eventual end users. However, the reliability analysis was driven by semi-formal techniques based on Failure Modes, Effects and Critical Analysis. The results from these studies were supported by operational observations of test applications to provide evidence that helped to demonstrate conformance with the requirements listed above. The following pages argue that complex interactions between safety and security concerns justify the use of more formal techniques to support the future development of next generation GNSS. A further motivation for the use of mathematical reasoning is that safety and security require- ments extend beyond the underlying SBAS to include the interactive applications that rely on these infrastructures. This extends formal analysis in novel ways; most formal approaches tend to focus on an individual level of abstraction. In contrast, many SBAS applications also employ Receiver Autonomous Integrity Monitoring (RAIM) to detect potential faults in the underlying GNSS measurements. Additional signals, for instance from other satellites arrays, are used to confirm the fixes derived from the underlying SBAS. RAIM services offer significant benefits to end users. For instance, they can be used during critical phases of flight, such as an approach, when the pilot needs to be informed of such inaccuracies as soon as possible. As we shall see, formal analysis can be used to verify that RAIM warnings support SBAS data during critical operations. However, mathematical verification techniques must also be extended to consider a host of human factors issues. For instance, it is unclear whether end users must understand the underlying reasons why their systems indicate the need to perform a go around when RAIM alerts identify potential inaccuracies in GNSS data. 2 Security Threats to GNSS Infrastructures Most of the design concerns that motivated the development of SBAS focussed on safety rather than security requirements. The existing infrastructures remain vulnerable to a range of attacks. An early warning was provided by an approach into New Jersey during December 1997. The crew of a Continental trans-Atlantic flight lost all GPS signals; jeopardising confidence in an array of on-board systems. It was initially believed that this had been caused by an intentional jamming attack. It later turned out to have been the unintended result of a US military test. A 200-kilometer interference zone was created by a GPS antenna with a 5-watt signal, stepping through frequencies. The UK Ministry of Defence (MOD) illustrated the potential threat for maritime navigation [GWWB09]. A medium powered jamming device generated noise over a pre-defined area of the UK coastline. This study clearly illustrated the impact that the threats to GNSS integrity can have upon the end users of these infrastructures. Particular problems were identified for crews using integrated bridge systems. This technology brings together navigation tools with autopilot control so that a jammed GPS signal could lead to a significant deviation without warning. Even if an alert was issued there are significant barriers to identifying the correct position given the consequent loss of situation awareness. The crews in this trial were all aware that the GPS signals would be jammed. However, multiple simultaneous alarms rapidly increased the crews workload as they cross-checked navigational information. The impact for on-board systems was compounded by the impact of jamming for shore-based services. Numerous errors began to undermine the Vessel Traffic Services that provide an overview of coastal areas. Some of the 3 / 18 Volume 45 (2011) Assurance Cases and BDMP Models for Safety and Security in GNSS data returned by vessels was based on incorrect GPS fixes that contradicted radar sources. Many of the vulnerabilities associated with convention GNSS architectures stem from the relatively weak signals that are used. A common analogy is to compare GPS output to using the power of a car headlight across one third of the Earths surface at more than 20,000km. Most western military organisations can interrupt GNSS signals; simulation software enables planners to identify the optimal allocation and distribution of jamming systems. The military development of satellite navigation jamming devices has been mirrored by the increasing availability of hand held systems that cost little more than $100 and have a range of several kilometres. These portable technologies can be used in a range of criminal activities for instance, to disrupt the signals to GPS tracking devices that would otherwise report the location of a stolen vehicle or shipment. It is illegal to offer these devices for sale within the European Union. This is because they cannot comply with the existing Electro-Magnetic Compatibility (EMC) directives; the prohibition was not primarily intended to protect GNSS services. Within the UK, national legislation prevents the operation of a jammer but it is not illegal to own such a device [Roy11]. Further threats illustrate the relationship between underlying systems vulnerabilities and the usability of safety-critical SBAS applications. First generation GNSS infrastructures provide little support for users trying to authenticate signals. This makes it possible to spoof location information through the broadcast of fake GNSS-like signals or the rebroadcast of valid GNSS signals. Signal simulation software can be used to recreate the anticipated GPS signals for a given route using a particular set of waypoints and timing intervals. Coupled with a spoofing transmitter, these simulators can fool the user into thinking that they are following a specified route. The problems of designing the simulator and then integrating it with effective, mobile jamming technologies have created significant barriers to their application for criminal ends. However, these are likely to be eroded in coming years and the potential threats cannot be dis- counted. The criminal motivation is proportionate to the diversification of GNSS applications including route monitoring for toll and insurance pricing. Some of these concerns are being addressed through technological innovation. For instance, spoofing will become far more difficult once Galileo begins to provide encrypted signals for use in safety-related applications. Other threats continue to affect future GNSS architectures. As mentioned, the design of the EGNOS and Galileo ground based systems focused on meeting ac- curacy, integrity, availability, continuity and time to alert requirements. Software and hardware teams were focused on a series of feared events and failure modes. Algorithmic barriers and standard operating practices, including maintenance procedures, were then created to address these concerns. Deliberate attacks were not part of this analysis. In consequence, a number of low level vulnerabilities may persist. Fortunately, the defences that were created in response to safety concerns also provide protection against potential security threats. The same CRC and error checking techniques that help to identify potential failure modes can also identify a range of attacks. There remains some concern as to whether these defences would offer sufficient pro- tection against insider threats. For instance, most SBAS infrastructures rely on configuration files that enable operators to respond to the failure of particular components. This increases con- fidence in meeting the safety requirements, cited above. However it also creates opportunities for malicious reconfiguration. Similarly, GNSS infrastructures are typically designed to operate autonomously for short periods of time. Elements of the infrastructure can also be commanded from more than one ground station. This creates a concern that external agents or insiders could Proc. FMIS 2011 4 / 18 ECEASST spoof legitimate commands or gain temporary control of the infrastructures. This might sound relatively far-fetched. However, the investment in relatively simple attack modes such as those used by STUXNET provides a warning of future vulnerabilities as more and more national infras- tructures rely on satellite based navigation and timing information. These potential threats also reinforced the point that security concerns extend beyond the scope of an initial safety analysis into the entire operational life cycle of GNSS architectures through development to deployment and maintenance. A recent report from the UK Royal Academy of Engineering [Roy11] argued that 6% of GDP in Western Countries depends on GNSS technology. It went on to criticise the lack of backup technologies. At a national level, agencies should monitor and report on disruption to GNSS signals. At an international level, greater attention should be paid to the vulnerabilities that over- reliance on this technology is creating in the financial markets. Managerial and operational staff should prepare for GNSS outages from ten minutes to a month. The RAE team also argued that GNSS vulnerabilities should be explicitly included in the risk assessments that support crit- ical infrastructures. The limited scope of the RAE report did not, however, identify formal or semi-formal techniques that might support such analyses. In contrast, the following paragraphs identify a range of tools that might increase the resilience of safety-related SBAS applications. 3 High-Level Structures: Semi-Formal Dependability Cases The safety of Satellite Based Augmentation Systems (SBAS) depends on many different forms of evidence, including but not limited to risk assessments, architectural descriptions, develop- ment standards, test data, independent audits etc. In previous work, we have described how semi-formal argumentation techniques help to structure these different sources of evidence. In particular, Johnson and Atencia Yepez [JY11] use this approach to reason about the impact of security threats for the users of safety-critical GNSS applications. In this approach, the edges of a graph denote that evidence supports a particular goal. These diagrams support discussion be- tween stakeholders who often have very different viewpoints on the validity of particular safety or security arguments. For instance, the Goal Structuring Notation (GSN) uses a goal or claim to represent an assertion that can be assessed as either true or false [KW04]. A developer might assert that RAIMs techniques are acceptably safe during low probability continuity failures. A solution can be used to present the evidence that supports a goal or strategy. This is important be- cause it provides a link between the high level argument structure embedded within GSN and the more detailed documentation provided by specific development techniques such as Fault Trees, FMECA, Formal methods etc. Figure 1 shows how GSN can be used to argue that an SBAS is acceptable safe. This top level goal can be broken down into sub-claims. In this case, G2 focuses on eliminating or mitigating the hazards that might undermine the ICAO performance requirements in terms of accuracy, in- tegrity, continuity and availability. G3 focuses on the need to operate the SBAS according to the identified Standard Operating Procedures (SOPs). These goals are placed within the context of specification and requirements documents including EC Reg 550/2004, EGN SDD SoL etc. Ev- idence that these sub goals have been addressed can be derived from a range of tests initially on limited geographical areas and subsequently by more sustained monitoring of ground stations. 5 / 18 Volume 45 (2011) Assurance Cases and BDMP Models for Safety and Security in GNSS Figure 1: Initial GSN for Satellite Based Augmentation Systems (SBAS) Proc. FMIS 2011 6 / 18 ECEASST The EGNOS End to End Simulator (EETES) also provides evidence of robustness against accu- racy concerns. Solution S4 also shows how evidence from formal analysis techniques, including model checking, can be integrated into the safety arguments within a GSN. The semi-formal, safety case structures used to support EGNOS certification for SoL appli- cations are significantly more complex than that illustrated in Figure 1. A modular approach was, therefore, developed to structure arguments that addressed low level infrastructure concerns through to usability issues [JY10]. Part A of the safety case explains why the system has been designed, developed and deployed in a manner compliant to ICAO Standards and Recommended Practices (SARPS). This was coordinated by the European Commission with support from the European Space Agency as the lead body in the initial design of the EGNOS architecture. In contrast, Part B argues that the SBAS will be operated and maintained to meet the ICAO SARPs by the commercial European Satellite Services Provider (ESSP). Additional safety cases are then required for each of the end-user applications that are built on top of the SBAS SoL architecture. Goodenough, Lipson and Weinstock [GLW06] have used GSN to analyse security concerns. In this case, the top level goal demonstrated that the system was acceptably secure. Their ap- proach focussed on relatively low-level threats to software systems; structuring evidence that an implementation will not be vulnerable to buffer overflow attacks. The arguments still relied upon a range of human factors claims. For instance, programmers must be trained to avoid vul- nerabilities in their code. Competent programmers must also be used to review the software. Goodenough, Lipson and Weinstocks work is particular relevant for this workshop; their assur- ance cases also integrated evidence from mathematically based tools for static code analysis. It is possible to identify a number of different ways in which semi-formal argumentation techniques might integrate security AND safety concerns for interactive systems: • Integration within a single dependability argument. Under this approach, the top level goal would be to demonstrate the dependability of a complex system. A first sub-goal would present the arguments that any implement was acceptably safe. A second sub-goal would then structure the evidence showing that the system was acceptably secure. This approach raises a number of concerns in particular, it is difficult to show that some security evidence has implications for systems safety and vice versa. • Integration of safety concerns into security assurance cases. This approach would begin by constructing the security arguments pioneered by Goodenough, Lipson and Weinstock [GLW06]. Additional nodes might then be introduced into the diagram to distinguish evidence or arguments about security concerns that might undermine the safety of any implementation. This approach suffers from a range of practical problems for example, it is possible to identify potential safety concerns with every threat or vulnerability. However, there are additional safety hazards that would not be represented in the combined diagram because they are not strictly related to the original security assurance case. • Integration of security threats into safety cases. We have chosen to adopt a third approach. This begins by developing a conventional safety case, such as that illustrated in Figure 1. The second stage is to use conventional forms of threat and vulnerability analysis to iden- tify security concerns that were not identified during the previous step. Additional evi- dence must then be introduced into the hybrod structure to document any additional miti- 7 / 18 Volume 45 (2011) Assurance Cases and BDMP Models for Safety and Security in GNSS G1: EGNOS SBAS is acceptably safe C1: SBAS performance requirements identified in EGNOS Service Defi nition Document – Open Service, Ref : EGN-SDD OS V1.1 – 30th October 2009 and ICAO Annex10 Vol I (Radio Navigation Aids) – 6th Ed July 2006 ver. 85, EC Reg 550/2004 S1: Initial tests on limited geographical areas G2: all identified hazards with accuracy, integrity, continuity and availability have been eliminated or mitigated to an acceptable level. C2: Hazards and ‘feared events’ identified according to the EGNOS end-to- end validation programme G3: SBAS operations conducted according to agreed SOPs. C3: EGNOS Safety of Life Service Definition Document European Commission, DG Enterprise and Industry Ref : EGN- SDD SoL, V1.0 also RTCA/DO-229D G4: Hazards to accuracy have been mitigated. G8: Probability of deterministic failure < 10{-5) per service hour G9: Probability of random stochastic failure < 10{-5) per service hour G10: SBAS ops will be conducted following practices in European Cooperation for Space Standardization; Space Engineering –Verification; ECSS-E-10-02A; 17 November 1998. G11: SBAS ops meet detailed requirements in Single European Sky Certification of ESSP S4: Fault tree for EGNOS components S5: Evidence of Conformance from Audit eg French NSA for EC, July 2010. S6: Process evidence from ESSP teams S2: Real-time monitoring of Signal-in-Space data CE1: Excessive multipath at RIMS level jeopardizes continuity S3: Simulator data eg EGNOS End to End Simulator (EETES) G7: Hazards to, continuity have been mitigated. G5: Hazards to integrity have been mitigated. G6: Hazards to availability have been mitigated. SC1: Localized jamming of GPS or spoofing invisible to ground stations . SC2: Concerns over insider threat to EGNOS ground stations. Figure 2: Integrating Security Threats to GNSS Architectures within GSN Safety Arguments gation that must be introduced to address these security concerns beyond those that were already considered as part of an initial safety assessment. Figure 2 shows how safety and security arguments can be integrated into a single graphical struc- ture [JY11]. The augmented assurance case identifies two safety concerns. The first uses the UK MOD studies to provide evidence that localised disturbances to GPS or GLONASS signals would not be visible to an EGNOS ground station. The threats posed from such interference can be mit- igated through the application of the RAIMs techniques mentioned in previous sections of this paper. However, the representation of security and safety arguments within an integrated GSN helps to document the importance of these approaches for the dependability of future applica- tions. Figure 2 also includes a second set of security concerns based around the potential insider threat to GNSS infrastructures. These are rarely modelled within simulation environments; how- ever, coordinated attacks by individuals who are familiar with the ground architecture of an SBAS system would undermine many of the defences that are intended to mitigate the impact of individual human errors. Previous paragraphs have shown how semi-formal assurance cases can be used to represent and reason about the interaction between security and safety concerns in complex, interactive systems. These graphical structures collate the many diverse forms of evidence, including formal analysis, that support dependability arguments. They are particularly appropriate for SBAS and GNSS applications where the quality of end-user interaction is determined by the interaction of Proc. FMIS 2011 8 / 18 ECEASST multiple infrastructures each supported by the cooperation of many different commercial and regulatory organisations. A number of caveats can be raised about the use of the hybrid technique, illustrated in Fig- ure 2. For instance, the EGNOS safety case is divided into different parts addressing the design, implementation and operation of the underlying infrastructures. Further components have been developed to demonstrate that particular applications are acceptably safe. It remains to be seen whether it is possible to trace the impact of particular threats and vulnerabilities across these different boundaries to identify the impact that particular cyber attacks might have upon the end users of GNSS data. Further limitations stem from the qualitative and semi-formal nature of most safety cases. This limits the inferences that can be drawn about the potential impact of safety hazards and security threats. In order to look for more quantitative support, we must look more closely at the techniques that can be used to obtain the evidence, which is documented in the nodes of an assurance case. 4 Lower-Level Analysis: Boolean Driven Markov Processes (BDMP) Safety argumentation techniques, such as the GSN used in Figures 1 and 2, provide a graphical means of integrating evidence from formal analysis with the products from other safety-related software engineering processes that are required by most development standards and by regu- latory agencies. This is important because formal methods are not sufficient in themselves to support the design, implementation and operation of most complex GNSS applications; they must be augmented by risk analysis techniques, by functional testing and usability studies, by environmental and observational data etc. This section goes on to look at one formal approach that can be used to consider both safety and security requirements, while reinforcing these initial links between complementary development techniques. Boolean Driven Markov Processes (BDMPs) have strong similarities to more conventional fault trees that have been supported the development of many different safety-related interfaces. Bouissou and Bon [BB03] provide an overview of the approach and explain one important dif- ference with the BDMP semantics. Boolean Driven Markov Processes extend conventional Fault Trees with triggers that are represented by dotted arrows similar to the priority AND gates that have been integrated into some Fault Trees. The target of the arrow is activated if the source state occurs. These relationships between the leaf nodes in the BDMP can be formalised within Markov Processes, the use of Boolean logic embedded in the tree notation also helps to reduce the potential state space explosion associated with conventional Markov Processes in applica- tions as complex as the GNSS described in this paper. Figure 3 introduces the annotations that provide a bridge between the fault tree components and the underlying Markov Processes [BB03]. Figure 4 goes on to apply the approach to model N-2 safety-related failures involving GNSS implementations. Each of the diagrams illustrates how multiple independent failures can undermine the confidence and situation awareness of end- users by interrupting the provision of navigation and timing information. In Figure 4 a) there is a probability that the RAIMs secondary system will fail to provide a correct location when it is needed following the loss of a primary SBAS fix. In contrast, Figure 4 b) considers the situation in which the RAIMs fault may occur before the loss of SBAS; this might happen during a fail 9 / 18 Volume 45 (2011) Assurance Cases and BDMP Models for Safety and Security in GNSS Figure 3: BDMP Annotations following Bouissou and Bon (2003) silent problem or as a result of incorrect configuration, maintenance etc. Figure 4 c) illustrates how these two different scenarios can be combined within the same BDMP model. Piètre-Cambaciédiès and Bouissou, [PB10b] have recently extended Boolean Driven Markov Processes to represent and reason about security threats for complex systems. This approach borrows many of the concepts that have been embedded with the attack trees that are themselves based on concepts from Fault Tree notations. As before, the intention is to associate Markov Processes with the leaf nodes of the tree structures. These leaves are used to represent the actions of potential attackers; they capture important state changes that describe whether an attack has been executed or not, whether it can be detected or not once it has begun and so forth. The Markov processes describe the probability of that node being true; this creates the opportunity to develop an executable semantics from the notation in which a state transition in the underlying process will trigger the leaf node to become true. Figure 5 summarises the security extensions to the BDMP modelling language. Piètre-Cambaciédiès and Bouissou [PB10a] provide a more complete introduction to the syn- tax and semantics of this integrated approach to security and safety modelling. However, the language continues to be refined as further applications test the expressive completeness of the annotations illustrated in Figure 3 and 5. Figure 6 builds on this previous work and applies the security extensions to represent a malicious attack on an SBAS infrastructure. In this case, the attacker acts to disable a RAIM implementation before undermining the GNSS infrastructure. Any attack on the SBAS would have little impact if the receiver autonomous monitoring systems could detect and respond to the failure. Figure 6 illustrates an important strength of the BDMP approach. The probability of an attack on both the RAIM and SBAS implementation might be very low. However, the UK government has recently acknowledged that greater consideration needs to be paid to what are known as N-2 vulnerabilities. These characterise low probability, high consequence failures of multiple infrastructures where there may be hidden interdependencies for instance, the insider threat Proc. FMIS 2011 10 / 18 ECEASST Loss of navigation and timing data. AND Active Failure Failure on Demand Loss of SBAS corrections On-demand failure of RAIMs A: Initial failure, compounded by failure on demand Loss of navigation and timing data. PAND Active Failure Loss of SBAS corrections Loss of RAIMs secondary source B: Initial failure, followed by secondary failure Active Failure Loss of navigation and timing data. PAND Active Failure Loss of SBAS corrections Loss of RAIMs secondary source Active Failure OR AND Failure on Demand On-demand failure of RAIMs secondary source C: Composite model of N-2 Failure Scenarios Figure 4: BDMP Modelling of Primary and Backup Systems 11 / 18 Volume 45 (2011) Assurance Cases and BDMP Models for Safety and Security in GNSS Figure 5: BDMP Security Annotations following Piètre-Cambaciédiès and Bouissou, (2010) from a common infrastructure provider (software or hardware) cannot be discounted for both RAIMs and SBAS technologies. Figure 7 extends the BDMP approach to consider a hybrid vulnerability in which external attacks exploit wider failures in a national critical infrastructure. In diagram A, the attacker waits until there is a failure in the RAIM infrastructure before mounting an attack on the SBAS infrastructure. This does not seem a plausible scenario given that the attacker would need to know that the failure had occurred and that the users of an SBAS application would continue operation without the support of the RAIM implementation before they launched their attack. This formalisation is important because it provides the basis for discounting certain lines of attack providing this decision can be validated by a broad range of stakeholders. In contrast, diagram B models a scenario in which the attacker disables the RAIM implementation and allows the system to continue operating until there is a subsequent fault in the SBAS application. Again the plausibility of the attack mode might be questioned; however, this scenario describes the insertion of a latent threat that has significant potential to compromise the safety and security of many complex systems. Figure 8 builds on the BDMP extensions to construct a model that integrates accidental faults with malicious attacks on both the RAIMs and SBAS infrastructures. As can be seen, the RAIMs for an end-user application might be disabled either through a fault or through an attack. This would lead to a loss of navigation and timing information if it were followed by the failure of an SBAS infrastructure either through an attack or fault. The same consequences would arise if the loss of the SBAS were to be followed by a failure on demand for the RAIM implementation. The links between BDMP diagrams and fault trees enable the use of minimal cut set al- gorithms to identify the different scenarios that might compromise the operation of complex, safety-critical systems. Integrated diagrams, such as that illustrated by Figure 8, can be also drive the quantitative analysis of attack and failure scenarios using the underlying Markov Pro- cesses that support each of the lead nodes. Their analysis is intended to derive the probability of an undesired event within a given period of time or the mean time in which this event will oc- cur. Piètre-Cambaciédiès and Bouissou [PB10b] show how these models can be used to suggest Proc. FMIS 2011 12 / 18 ECEASST Loss of navigation and timing data. AND Malicious attack on SBAS infrastructure Malicious attack on RAIMs secondary source Figure 6: BDMP Modelling of Primary and Backup Systems 13 / 18 Volume 45 (2011) Assurance Cases and BDMP Models for Safety and Security in GNSS Loss of navigation and timing data. AND Malicious attack on SBAS infrastructure Loss of RAIMs secondary source Active Failure Loss of navigation and timing data. PAND Loss of SBAS corrections Malicious attack on RAIMs secondary source B: Malicious attack, followed by secondary failure Active Failure A: Initial failure, followed by malicious attack Figure 7: BDMP Hybrid Modelling of Security Attacks and Accidental Vulnerabilities Loss of navigation and timing data. PAND OR AND OR OR Failure on Demand Active Failure Active Failure Loss of RAIMs secondary source Malicious attack on RAIMs secondary source Malicious attack on SBAS infrastructure Loss of SBAS corrections On-demand failure of RAIMs secondary source RAIMs disabled SBAS disabled Figure 8: BDMP Integrated Modelling of Security Attacks and Accidental Vulnerabilities Proc. FMIS 2011 14 / 18 ECEASST potential vulnerabilities in these integrated models. Their work focuses on the quantitative anal- ysis of pollution incidents. However, their results can be extended to our case study. In systems whose mission time is short it is better to conduct a malicious attack on both infrastructures even though the probability of success might be relatively small. The probability of detection is also constrained by the limited time exposure. Over longer periods of operation, or if an attack takes longer to mount, it is better for the attacker to use a hybrid approach. For example, malicious code might be inserted into a RAIMs implementation and triggered during accidental problems in the operation or configuration of a GNSS. This attack strategy could be reversed if there was a higher probability of detection associated with the RAIMs compared to the SBAS infrastructure. In either case, the relatively low probability of detection for malicious code inserted by an insider remains a significant concern across most critical infrastructures. In order to support this quantitative, integrated use of BDMP for security and safety assess- ments we must define values for in-operation (λ ) and on-demand failures (γ ). It is also important to model the probability that an attack action will be successful (β ). The probability of active failure for the SBAS in Figure 8 can be derived from existing safety case evidence, mentioned previously. The probability of the active loss and the on-demand failure of RAIMs implementa- tions can be derived from application specific safety assessments, e.g. supporting ICAO Required Navigation Performance criteria. However, the remaining values are less clear cut. How can one assess the probability of a successful attack on a RAIMs implementation or an SBAS infras- tructure? It is for this reason that we have not attempted to calculate the derived values from the Markov Processes; there are further concerns over attempts to accurately assess the existing vulnerabilities of a critical component of European infrastructures. Some national agencies have argued that the managers of key systems must act as though state sponsored cyber attacks have a probability of one. In other words, the design, management and operation of critical systems must be guided by the assumption that they will be the target of external agencies. This simpli- fies some aspects of the quantitative assessments, security analysts can focus on the probability of detection before any intrusion has the potential to affect the end users of the underlying in- frastructure. The hybrid BDMP analysis in Figure 8 provides a framework for this more detailed work. 5 Conclusions Previous generations of Global Navigation Satellite Systems could not be used for safety-related applications. Ionospheric interference and multipath signals combined to create problems of accuracy, integrity, availability and continuity. The underlying architectures provided no guar- antees about the time taken to alert the end users to potential problems. These issues have all recently been addressed through the development of Safety of Life extensions for Satellite Based Augmentation Systems. In consequence, the European Commission has supported the certifi- cation of these infrastructures for applications ranging from precision approaches to runways through to advanced railway signalling systems. Similar provisions have been made for the use of the North American North American Wide Area Augmentation System (WAAS) and the Asian Multi-functional Satellite Augmentation System (MSAS). A range of tools and techniques have been used to support the development and operation of 15 / 18 Volume 45 (2011) Assurance Cases and BDMP Models for Safety and Security in GNSS SBAS infrastructures. These include conventional risk assessment methods, such as HAZOPS and FMECA. They also include a range of empirical tests both on the ground and space based components. Formal analysis has been applied to represent and reason about the algorithms used to calculate necessary corrections to the GPS and GLONASS signals. Usability tests have also supported the systems engineering and configuration tools used in the operation of SBAS infrastructures. Graphical argumentation techniques have been used to gather this evidence into a coherent structure that demonstrates augmentation infrastructures are acceptably safe within a range of different contexts. At the same time that satellite based augmentation systems have been approved for location and timing information in safety-critical interfaces, a range of organisations including the US Department of Defense and UK Ministry of Defence; have raised concerns about increasing civil vulnerability to attacks on the underlying infrastructures. These vulnerabilities are compounded by a range of human factors concerns; the more that end users begin to rely on navigation and timing infrastructures then the greater the consequences will be for any interruption to those ser- vices. Previous studies by the MoD and by the FAA have shown that crews suffer a significant loss of situation awareness when there is any interruption to GNSS infrastructures. The integra- tion of navigation and timing data into a wide range of applications also undermines operators confidence in a host of interactive systems, not simply those that report on their present location. For example, studies of GNSS jamming have shown that relatively cheap devices undermine a host of maritime bridge information systems and shore based traffic monitoring applications. Further concerns arise because it is unclear how to represent and reason about the safety con- cerns that are created by the diverse security threats to GNSS architectures, including spoofing and the insider threat to both space and ground based systems. Such security concerns invalidate many of the assumptions that support the provision of critical services. One approach would be to extend the application of argumentation techniques such as GSN from safety-related applica- tions to represent security argumentation. Several examples have been developed to show how this can be done for a range of software applications. However, this suffers from a number of limitations. In particular, it can be difficult to represent and reason about the impact that security threats might have upon underlying safety arguments. We have, therefore, extended previous approaches to show how security threats might be used to challenge the evidence that supports arguments about GNSS Safety of Life applications. The intention is to provide an integrated, risk-based approach to the identification of attack scenarios that can help assess the resilience of safety cases to security threats across the life cycle extending from design to maintenance and operation. The integration of security concerns into safety cases helps to sketch the potential conse- quences of a malicious attack on an underlying SBAS. A key benefit is that the safety case provides a means of collating the diverse sources of evidence from design, testing and analysis summarised above. However, this evidence must be derived using other tools and techniques. It is for this reason that this paper has also presented a means of analysing the more detailed in- teractions between the security and safety of GNSS. In particular, we have shown how Boolean Driven Markov Processes help to avoid some of the state explosion limitations of conventional Markov techniques using extensions to the well-known Fault Tree notation. An important ben- efit of this approach is that it has already been developed to consider attacks on safety-related applications. However, it has not previously been applied to consider failure modes and security Proc. FMIS 2011 16 / 18 ECEASST threats to critical infrastructures, such as the SBAS described in this paper. Much remains to be done. In particular, the quantitative application of the Markov processes relies upon estimates of the likelihood of successful attacks on elements of the SBAS infras- tructure. This, in turn, must be validated by expert judgement across a range of stakeholders including the designers and operators of the infrastructure components, the end users of the GNSS applications as well as national intelligence agencies similar to the UK Centre for the Protection of National Infrastructure. The elicitation of these estimates reinforces the close inte- gration between human factors and formal analysis that is a recurring theme in this work and in any study to address the interactions between security and safety. Acknowledgements: The work described in the paper has been supported by the UK Engi- neering and Physical Sciences Research Council grant EP/I004289/1. Special thanks are due to Amaya Atencia Yepez, GMV who provided valuable comments on an early draft of this paper any remaining errors remain those of the author. Bibliography [BB03] M. Bouissou, J.-L. Bon. A New Formalism that Combines the Advantages of Fault Trees and Markov Models: Boolean Logic Driven Markov Processes. Reliability Engineering and System Safety journal 82(2):149–163, 2003. [BO07] U. Bhatti, W. Ochieng. Failure Modes And Models For Integrated GPS/INS Sys- tems. The Journal of Navigation 60(2):327348, 2007. [GLW06] J. Goodenough, H. Lipson, C. Weinstock. Arguing Security - Creating Security Assurance Cases. Technical report Technical report DAP/SSH/091, Software En- gineering Institute, Carnegie Mellon University, Pittsburg, USA, 2006. [GWWB09] A. Grant, P. Williams, N. Ward, S. Basker. GPS Jamming and the Impact on Mar- itime Navigation. The Journal of Navigation 62(2):173–187, 2009. [JY10] C. Johnson, A. A. Yepez. Safety Cases for Global Navigation Satellite Systems Safety of Life (SoL) Applications. In Lacoste-Francis (ed.), Proceedings of the Fourth International Association for the Advancement of Space Safety, Huntsville Alabama,. NASA/ESA, ESTEC, Noordwijk, The Netherlands, 2010. ISBN 978- 92-9221-244-5, ESA Technical report SP-680. [JY11] C. Johnson, A. A. Yepez. Mapping the Impact of Security Threats on Safety- Critical Global Navigation Satellite Systems. In To Appear in the Proceedings of the 29th International Systems Safety Society Conference, Las Vegas, USA. August 2011. [KW04] T. P. Kelly, R. A. Weaver. The Goal Structuring Notation - A Safety Argument Notation. In Proceedings of the Dependable Systems and Networks 2004 Workshop on Assurance Cases. July 2004. 17 / 18 Volume 45 (2011) Assurance Cases and BDMP Models for Safety and Security in GNSS [PB10a] L. Piètre-Cambaciédiès, M. Bouissou. Attack and Defence Dynamic Modelling with BDMP (Boolean logic Driven Markov Processes). In Proceedings of the 5th International Conference on Mathematical Methods, Models and Architectures for Computer Network Security. Volume LNCS 6258, pp. 86–101. St Petersburg, Rus- sia, September 2010. [PB10b] L. Piètre-Cambaciédièss, M. Bouissou. Modelling Safety and Security Interdepen- dencies with BDMP (Boolean logic Driven Markov Processes). In IEEE Interna- tional Conference on Systems Man and Cybernetics (SMC). P. 2852 2861. 10-13 Oct 2010. [Roy11] Royal Academy of Engineering. Global Navigation Space Systems (GNSS): Re- liance and Vulnerabilities. Technical report, Royal Academy of Engineering, Lon- don, UK, 2011. Proc. FMIS 2011 18 / 18 Introduction Security Threats to GNSS Infrastructures High-Level Structures: Semi-Formal Dependability Cases Lower-Level Analysis: Boolean Driven Markov Processes (BDMP) Conclusions