Security and Safety Threat Detection Method for Unmanned Aerial System Based on Runtime Verification
Author:
Affiliation:

Fund Project:

National Key Research and Development Program of China (2017YFB1001802); National Program on Key Basic Research Project (973) (2014CB340703); National Natural Science Foundation of China (61690203, 61532007)

  • Article
  • | |
  • Metrics
  • |
  • Reference [38]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    The defects of the software and hardware in unmanned aerial system and external malicious attack pose a great threat to the security and safety of UAS.Due to the complex running environment of UAS,many factors are difficult to predict accurately in the development process.Therefore,it is of great significance to adopt an effective runtime security and safety guarantee mechanism.This paper proposes a UAS security and safety threat detection method based on runtime verification.Firstly,after analyzing a variety of security and safety threats that UAS may encounter,the paper defines the threats in discrete-time MTL and presents the corresponding UAS-DL language to describe the security and safety monitoring specification.Then an automatic generation algorithm of security and safety threat monitor is introduced based on the alternating automaton,and security and safety monitoring of multi-UAS is implemented by parameterization method.In order to improve the accuracy of the detection,the method of combining runtime verification with Bayesian network inference is also studied.The experiment is carried out with the actual UAS development simulation platform Ardupilot,and monitors are deployed on the field-programmable gate array (FPGA) hardware independently to avoid excessive usage of UAS computing resources.Experimental results show that the proposed method can effectively detect the security and safety threats of UAS.

    Reference
    [1] Schumann J, Moosbrugger P, Rozier KY. Monitoring and diagnosis of security threats for unmanned aerial systems. In:Proc. of the Runtime Verification. 2015. 233-249.
    [2] Aiello AM, Berryman JF, Grohs JR, Schierman JD. Run-Time assurance for advanced flight-critical control systems. In:Proc. of the AIAA Guidance, Nav. and Control Conf. AIAA, 2010.
    [3] Basin D, Klaedtke F, Zălinescu E. Algorithms for monitoring real-time properties. In:Proc. of the Int'l Conf. on Runtime Verification. Berlin, Heidelberg:Springer-Verlag, 2011. 260-275.[doi:10.1007/978-3-642-29860-8_20]
    [4] Divakaran S, D'Souza D. Conflict-Tolerant real-time specifications in metric temporal logic. In:Proc. of the 17th Int'l Symp. on Temporal Representation and Reasoning (TIME). IEEE, 2010. 35-42.[doi:10.1109/TIME.2010.23]
    [5] Maler O, Nickovic D, Pnueli A. Checking temporal properties of discrete, timed and continuous behaviors. In:Proc. of the Pillars of Computer Science. Berlin, Heidelberg:Springer-Verlag, 2008. 475-505.[doi:10.1007/978-3-540-78127-1_26]
    [6] Basin D, Klaedtke F, Müller S, Pfitzmann B. Runtime monitoring of metric first-order temporal properties. In:Proc. of the LIPIcs-Leibniz Int'l Conf. on Informatics, Vol.2. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2008. 49-60.
    [7] Backasch R, Hochberger C, Weiss A, Leucker M, Lasslop R. Runtime verification for multicore SoC with high-quality trace data. ACM Trans. on Design Automation of Electronic Systems (TODAES), 2013,18(2):18:1-18:26.[doi:10.1145/2442087.2442089]
    [8] Reinbacher T, Rozier KY, Schumann J. Temporal-Logic based runtime observer pairs for system health management of real-time systems. In:Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg:Springer-Verlag, 2014. 357-372.[doi:10.1007/978-3-642-54862-8_24]
    [9] Kiczales G, Lamping J, Mendhekar A, Maeda C, Lopes C, Loingtier J, Irwin J. Aspect-Oriented programming. In:Proc. of the ECOOP'97-Object-Oriented Programming. 1997. 220-242.
    [10] Kiczales G, Hilsdale E, Hugunin J, Kersten M, Palm J, Griswold W. An overview of AspectJ. In:Proc. of the European Conf. on Object-Oriented Programming. Berlin, Heidelberg:Springer-Verlag, 2001. 327-354.[doi:10.1007/3-540-45337-7_18]
    [11] Spinczyk O, Gal A, Schröder-Preikschat W. AspectC++:An aspect-oriented extension to the C++ programming language. In:Proc. of the 40h Int'l Conf. on Tools Pacific:Objects for Internet, Mobile and Embedded Applications. Australian Computer Society, Inc., 2002. 53-60.
    [12] Coady Y, Kiczales G, Feeley M, Smolyn G. Using AspectC to improve the modularity of path-specific customization in operating system code. Proc. of the ACM SIGSOFT Software Engineering Notes, 2001,26(5):88-98.[doi:10.1145/503271.503223]
    [13] Mitsch S, Platzer A. ModelPlex:Verified runtime validation of verified cyber-physical system models. In:Proc. of the Runtime Verification. 2014. 199-214.
    [14] Fraigniaud P, Rajsbaum S, Travers C. On the number of opinions needed for fault-tolerant run-time monitoring in distributed systems. In:Proc. of the Runtime Verification. 2014. 92-107.
    [15] Pedro AM, Pereira1 D, Pinho LM, Pinto JS. Monitoring for a decidable fragment of MTL-∫. In:Proc. of the Runtime Verification. 2015. 169-184.[doi:10.1007/978-3-319-23820-3_11]
    [16] Kane1 A, Chowdhury O, Datta A, Koopman P. A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In:Proc. of the Runtime Verification. 2015. 102-117.[doi:10.1007/978-3-319-23820-3_7]
    [17] Kim A, Wampler B, Goppert J, Hwang I, Aldridge H. Cyber attack vulnerabilities analysis for unmanned aerial vehicles. In:Proc. of the Infotech@Aerospace. 2012.[doi:10.2514/6.2012-2438]
    [18] Leucker M, Schallhart C. A brief account of runtime verification. Journal of Logic and Algebraic Programming, 2009,78(5):293-303.[doi:10.1016/j.jlap.2008.08.004]
    [19] Allan C, Avgustinov P, Christensen AS, Hendren L, Kuzins S, Lhoták O, Moor O, Sereni D, Sittampalam G, Tibble J. Adding trace matching with free variables to AspectJ. In:Proc. of the 20th Annual ACM SIGPLAN Conf. on Object Oriented Programming Systems, Languages, and Applications (OOPSLA 2005). New York, 2005. 345-364.[doi:10.1145/1103845.1094839]
    [20] Chen F, Jin D, Meredith P, Rosu G. Monitoring oriented programming-A project overview. In:Proc. of the 4th Int'l Conf. on Intelligent Computing and Information Systems (ICICIS 2009). 2009. 72-77.
    [21] Colombo C, Pace GJ, Schneider G. LARVA-Safer monitoring of real-time Java programs (tool paper). In:Proc. of the 7th IEEE Int'l Conf. on Software Engineering and Formal Methods (SEFM). 2009. 33-37.[doi:10.1109/SEFM.2009.13]
    [22] Pnueli A. The temporal logic of programs. In:Proc. of the 18th IEEE Symp. on Foundation of Computer Science (FOCS'77). Washington, 1977. 46-57.[doi:10.1109/SFCS.1977.32]
    [23] Subramanyam R, Krishnan MS. Empirical analysis of CK metrics for object-oriented design complexity:Implications for software defects. IEEE Trans. on Software Engineering, 2003,29(4):297-310.[doi:10.1109/TSE.2003.1191795]
    [24] Gabbay D, Pnueli A, Shelah S, Stavi J. On the temporal analysis of fairness. In:Proc. of the 7th ACM Symp. on Principles of Programming Languages (POPL 2080). Washington, 1980. 163-173.[doi:10.1145/567446.567462]
    [25] Gastin P, Oddoux D. Fast LTL to Büchi automata translation. In:Proc. of the Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg:Springer-Verlag, 2001. 53-65.[doi:10.1007/3-540-44585-4_6]
    [26] Muller D, Schupp PE. Alternating automata on infinite objects, determinacy and Rabin's theorem. In:Proc. of the LITP Spring School on Theoretical Computer Science. Berlin, Heidelberg:Springer-Verlag, 1984. 99-107.
    [27] Kupferman O, Vardi M. Weak alternating automata are not that weak. In:Proc. of the 5th Israeli Symp. on Theory of Computing and Systems (ISTCS'97). IEEE, 1997. 147-158.[doi:10.1109/ISTCS.1997.595167]
    [28] Chen F, Rou G. Parametric trace slicing and monitoring. In:Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg:Springer-Verlag, 2009. 246-261.[doi:10.1007/978-3-642-00768-2_23]
    [29] Bauer A, Küster JC, Vegliach G. The ins and outs of first-order runtime verification. Formal Methods in System Design, 2015, 46(3):286-316.[doi:10.1007/s10703-015-0227-2]
    [30] Medhat R, Joshi Y, Bonakdarpour B, Fischmeister S. Parallelized runtime verification of first-order LTL specifications. Technical Report, CS-2014-11, University of Waterloo, 2014.
    [31] Reger G, Rydeheard D. From first-order temporal logic to parametric trace slicing. In:Proc. of the Runtime Verification. Springer Int'l Publishing, 2015. 216-232.[doi:10.1007/978-3-319-23820-3_14]
    [32] PEARL J. Fusion, propagation, and structuring in belief networks. Artificial Intelligence, 1986,29(3):241-288.[doi:10.1016/0004-3702(86)90072-X]
    [33] Spirtes P, Glymou RC, Scheines R. Causality from Probability. Technical Report, CMU-LCL-89-3, CMU-PHIL-12, Carnegie Mellon University, 1989.
    [34] Xie XC, Geng Z, Zhao Q. Decomposition of structural learning about directed acyclic graphs. Artificial Intelligence, 2006,170(4):422-439.[doi:10.1016/j.artint.2005.12.004]
    [35] http://reasoning.cs.ucla.edu/samiam/index.php
    [36] http://ardupilot.org/
    [37] Geist J, Rozier KY, Schumann J. Runtime observer pairs and Bayesian network reasoners on-board FPGAs:Flight-Certifiable system health management for embedded systems. In:Proc. of the RV 2014. 2014. 215-230.[doi:10.1007/978-3-319-11164-3_18]
    [38] Mirkovic J, Reiher P. A taxonomy of DDoS attack and DDoS defense mechanisms. ACM SIGCOMM Computer Communications Review, 2004,34(2):39-53.[doi:10.1145/997150.997156]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

杨栋,史浩,董威,刘宗林,周戈.基于运行时验证的无人飞行系统安全威胁检测方法.软件学报,2018,29(5):1360-1378

Copy
Share
Article Metrics
  • Abstract:4081
  • PDF: 7206
  • HTML: 3833
  • Cited by: 0
History
  • Received:July 10,2017
  • Revised:August 29,2017
  • Adopted:November 21,2017
  • Online: January 09,2018
You are the first2032491Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063