R2U2: monitoring and diagnosis of security threats for unmanned aerial systems

Adapteva: The parallella board, https://www.parallella.org/board

Ahmed A, Lisitsa A, Dixon C (2013) Testid: a high performance temporal intrusion detection system. In: ICIMP 2013, The eighth international conference on internet monitoring and protection, pp 20–26

Ardupilot.com: APM:Plane, Open source fixed-wing aircraft UAV, http://plane.ardupilot.com

Bartocci E, Grosu R, Karmarkar A, Smolka SA, Stoller SD, Zadok E, Seyster J (2013) Adaptive runtime verification. In: Proc RV 2012, LNCS, vol 7687. Springer. doi: 10.1007/978-3-642-35632-2_18

Bilge L, Dumitras T (2012) Before we knew it: An empirical study of zero-day attacks in the real world. In: Proceedings of the 2012 ACM conference on computer and communications security. pp 833–844. CCS ’12, ACM, New York, NY, USA, doi: 10.1145/2382196.2382284

Bushnell D, Denney E, Enomoto F, Pai G, Schumann J (2013) Preliminary recommendations for the collection, storage, and analysis of UAS safety data. Technical Report NASA/TM-2013-216624, NASA Ames Research Center

Chavira M, Darwiche A (2005) Compiling Bayesian networks with local structure. In: Proceedings of the 19th international joint conference on artificial intelligence (IJCAI), pp 1306–1312

Christian Science Monitor: RQ-170 GPS Spoofing (2011), http://www.csmonitor.com/World/Middle-East/2011/1215/Exclusive-Iran-hijacked-US-drone-says-Iranian-engineer-Video

Donzé A, Maler O, Bartocci E, Nickovic D, Grosu R, Smolka S (2012) On temporal logic and signal processing. In: Proc ATVA 2012, LNCS, vol 7561. Springer. doi: 10.1007/978-3-642-33386-6_9

Fisher K (2014) Using formal methods to enable more secure vehicles: DARPA’s HACMS program. In: Proceedings of the 19th ACM SIGPLAN international conference on functional programming. pp 1–1. ICFP ’14, ACM, New York, NY, USA, doi: 10.1145/2628136.2628165

GAO (2015) Air traffic control: FAA needs a more comprehensive approach to address cybersecurity as agency transitions to nextgen. Tech. Rep. GAO-15-370, United States Government Accountability Office (04 2015), http://www.gao.gov/assets/670/669627.pdf

Geist J, Rozier KY, Schumann J (2014) Runtime observer pairs and bayesian network reasoners on-board FPGAs: Flight-certifiable system health management for embedded systems. In: Proceedings of Runtime verification - 5th international conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Springer, pp 215–230. doi: 10.1007/978-3-319-11164-3_18

Heffernan D, Macnamee C, Fogarty P (2014) Runtime verification monitoring for automotive embedded systems using the iso 26262 functional safety standard as a guide for the definition of the monitored properties. IET Softw 8(5):193–203

Humphreys T (2012) Statement on the vulnerability of civil unmanned aerial vehicles and other systems to civil GPS spoofing. University of Texas at Austin (July 18, 2012)

Jafarnia-Jahromi A, Broumandan A, Nielsen J, Lachapelle G (2012) GPS vulnerability to spoofing threats and a review of antispoofing techniques. Int J Navig Obs 2012:12702. doi: 10.1155/2012/127072

Jaksic S, Bartocci E, Grosu R, Kloibhofer R, Nguyen T, Nickovic D (2015) From signal temporal logic to FPGA monitors. In: 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp 218–227

Javaid AY, Sun W, Devabhaktuni VK, Alam M (2012) Cyber security threat analysis and modeling of an unmanned aerial vehicle system. In: Proceedings of international conference on technologies for Homeland security (HST), 2012 IEEE, pp 585–590

JSBSim: JSBSim - open source flight dynamics model, http://jsbsim.sourceforge.net

Kalajdzic K, Bartocci E, Smolka SA, Stoller SD, Grosu R (2013) Runtime verification with particle filtering. In: Proc RV 2013, LNCS, vol 8174. Springer, pp 149–166

Kerns AJ, Shepard DP, Bhatti JA, Humphreys TE (2014) Unmanned aircraft capture and control via GPS spoofing. J Field Robot 31(4):617–636

Kim A, Wampler B, Goppert J, Hwang I, Aldridge H (2012) Cyber attack vulnerabilities analysis for unmanned aerial vehicles. In: Proceedings of Infotech@Aerospace 2012. doi: 10.2514/6.2012-2438

Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-time Syst 2(4):255–299

Kwon C, Liu W, Hwang I (2013) Security analysis for cyber-physical systems against stealthy deception attacks. In: 2013 American control conference, pp 3344–3349

Lu H, Forin A (2007) The design and implementation of P2V, an architecture for zero-overhead online verification of software programs. Tech. Rep. MSR-TR-2007-99, Microsoft Research, http://research.microsoft.com/apps/pubs/default.aspx?id=70470

Magiera J, Katulski R (2015) Detection and mitigation of GPS spoofing based on antenna array processing. J Appl Res Technol 13(1): 45–57, http://www.sciencedirect.com/science/article/pii/S1665642315300043

Maler O, Nickovic D, Pnueli A (2008) Checking temporal properties of discrete, timed and continuous behaviors. In: Pillars of Computer Science, LNCS, vol 4800. Springer, pp 475–505. doi: 10.1007/978-3-540-78127-1_26

MAVProxy: A UAV ground station software package for mavlink based systems, http://tridge.github.io/MAVProxy

McMilin E, De Lorenzo DS, Walter T, Lee TH, Enge P (2014) Single antenna GPS spoof detection that is simple, static, instantaneous and backwards compatible for aerial applications. In: Proceedings of the 27th international technical meeting of the satellite division of the institute of navigation (ION GNSS+ 2014), Tampa, FL. pp 2233–2242

Mengshoel OJ, Chavira M, Cascio K, Poll S, Darwiche A, Uckun S (2010) Probabilistic model-based diagnosis: an electrical power system case study. IEEE Trans Syst Man Cyberne Part A Syst Hum 40(5):874–885

Meredith PO, Jin D, Griffith D, Chen F, Roşu G (2012) An overview of the MOP runtime verification framework. Int J Softw Tools Technol Transf 14(3):249–289

Musliner D, Hendler J, Agrawala AK, Durfee E, Strosnider JK, Paul CJ (1995) The challenges of real-time AI. IEEE Computer 28, 58–66. http://citeseer.comp.nus.edu.sg/article/musliner95challenges.html

Naldurg P, Sen K, Thati P (2004) A temporal logic based framework for intrusion detection. In: FORTE, LNCS, vol. 3235, Springer, pp 359–376

Olivain J, Goubault-Larrecq J (2005) The orchids intrusion detection tool. In: CAV, LNCS, vol. 3576, Springer, pp 286–290

Pearl J (1985) A constraint propagation approach to probabilistic reasoning. In: UAI, AUAI Press, pp 31–42

Pellizzoni R, Meredith P, Caccamo M, Rosu G (2008) Hardware runtime monitoring for dependable COTS-based real-time embedded systems. In: RTSS 2008, IEEE, pp 481–491

Perry S (2015) Subcommittee hearing: Unmanned aerial system threats: exploring security implications and mitigation technologies. Committee on homeland security, http://homeland.house.gov/hearing/subcommittee-hearing-unmanned-aerial-system-threats-exploring-security-implications-and

Pike L, Goodloe A, Morisset R, Niller S (2010) Copilot: a hard real-time runtime monitor. In: Proc RV 2010, LNCS, vol 6418, Springer, pp 345–359

Psiaki ML, Humphreys TE (2016) GNSS spoofing and detection. Proc IEEE 104(6):1258–1270

Reinbacher T, Geist J, Moosbrugger P, Horauer M, Steininger A (2012) Parallel runtime verification of temporal properties for embedded software. In: MESA, pp 224–231

Reinbacher T (2013) Analysis of embedded real-time systems at runtime. Ph.D. thesis, Technische Universität Wien, Austria

Reinbacher T, Brauer J, Horauer M, Steininger A, Kowalewski S (2014) Runtime verification of microcontroller binary code. Sci Comput Program 80:109–129. doi: 10.1016/j.scico.2012.10.015

Reinbacher T, Rozier KY, Schumann J (2014) Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Tools and algorithms for the construction and analysis of systems - 20th international conference, TACAS 2014, Grenoble, France, LNCS, vol 8413, pp 357–372. Springer. doi: 10.1007/978-3-642-54862-8_24

Schumann J, Mbaya T, Mengshoel OJ, Pipatsrisawat K, Srivastava A, Choi A, Darwiche A (2013) Software health management with Bayesian networks. In: Innovations in System and Software Engineering, vol 9. Springer, pp 271–292

Schumann J, Moosbrugger P, Rozier KY (2015) R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. In: Proc RV 2015, LNCS, vol 9333. Springer, Cham. pp 233–249. doi: 10.1007/978-3-319-23820-3_15

Schumann J, Roychoudhury I, Kulkarni C (2015) Diagnostic reasoning using prognostic information for unmanned aerial systems. In: Proceedings of the 2015 annual conference of the prognostics and health management society (PHM2015)

Schumann J, Rozier KY, Reinbacher T, Mengshoel OJ, Mbaya T, Ippolito C (2013) Towards real-time, on-board, hardware-supported sensor and software health management for unmanned aerial systems. In: Proceedings of the 2013 annual conference of the prognostics and health management society (PHM2013)

Schumann J, Rozier KY, Reinbacher T, Mengshoel OJ, Mbaya T, Ippolito C (2015) Towards real-time, on-board, hardware-supported sensor and software health management for unmanned aerial systems. Int J Progn Health Manag 6(21):1–27

Selyunin K, Nguyen T, Bartocci E, Nickovic D, Grosu R (2016) Monitoring of MTL specifications with IBM’s spiking-neuron model. In: 2016 Design, automation test in europe conference exhibition (DATE), pp 924–929

Selyunin K, Nguyen T, Bartocci E, Grosu R (2016) Applying runtime monitoring for automotive electronic development. In: Proc RV 2016, LNCS, vol 10012. Springer, pp 462–469. doi: 10.1007/978-3-319-46982-9_30

Shachtman N, Axe D Most U.S. drones openly broadcast secret video feeds. Wired (10 2012), http://www.wired.com/2012/10/hack-proof-drone/

Shepard DP, Bhatti JA, Humphreys TE (2012) Drone hack. GPS World 23(8):30–33

Stoller SD, Bartocci E, Seyster J, Grosu R, Havelund K, Smolka SA, Zadok E (2012) Runtime verification with state estimation. In: Proc RV 2011, LNCS, vol 7186. Springer, pp 193–207. doi: 10.1007/978-3-642-29860-8_15

Todman T, Stilkerich S, Luk W (2015) In-circuit temporal monitors for runtime verification of reconfigurable designs. In: Proceedings of the 52nd annual design automation conference. pp 50:1–50:6. DAC ’15, ACM, New York, NY, USA, doi: 10.1145/2744769.2744856

U.S. Air Force: Aircraft Accident Investigation: RQ-1L, S/N 96-3023. AIB Class A Aerospace mishaps (September 2000), http://usaf.aib.law.af.mil/ExecSum2000/RQ-1L_Nellis_14Sep00.pdf