Abstract
Hybrid systems are integrations of discrete computation and continuous physical evolution. The physical components of such systems introduce safety requirements, the achievement of which asks for the correct monitoring and control from the discrete controllers. However, due to denial-of-service security attack, the expected information from the controllers is not received and as a consequence the physical systems may fail to behave as expected. This paper proposes a formal framework for expressing denial-of-service security attack in hybrid systems. As a virtue, a physical system is able to plan for reasonable behavior in case the ideal control fails due to unreliable communication, in such a way that the safety of the system upon denial-of-service is still guaranteed. In the context of the modeling language, we develop an inference system for verifying safety of hybrid systems, without putting any assumptions on how the environments behave. Based on the inference system, we implement an interactive theorem prover and have applied it to check an example taken from train control system.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993)
Alur, R., Dang, T., Ivancic, F.: Predicate abstraction for reachability analysis of hybrid systems. ACM Transactions on Embedded Computing Systems 5(1), 152–199 (2006)
Asarin, E., Bournez, O., Dang, T., Maler, O.: Approximate reachability analysis of piecewise-linear dynamical systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 20–31. Springer, Heidelberg (2000)
Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14(4), 583–604 (2003)
He, J.: From CSP to hybrid systems. In: A Classical Mind, pp. 171–189. Prentice Hall International (UK) Ltd. (1994)
Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996, pp. 278–292 (1996)
Lafferrierre, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. Journal of Symbolic Computation 11, 1–23 (2001)
Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1–15. Springer, Heidelberg (2010)
Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT 2011, pp. 97–106. ACM (2011)
Lynch, N., Segala, R., Vaandrager, F., Weinberg, H.: Hybrid I/O automata. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 496–510. Springer, Heidelberg (1996)
Manna, Z., Pnueli, A.: Verifying hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 4–35. Springer, Heidelberg (1993)
Nielson, H.R., Nielson, F.: Probabilistic analysis of the quality calculus. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 258–272. Springer, Heidelberg (2013)
Nielson, H.R., Nielson, F., Vigo, R.: A calculus for quality. In: Păsăreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 188–204. Springer, Heidelberg (2013)
Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. and Comput. 20(1), 309–352 (2010)
Platzer, A., Quesel, J.: European Train Control System: A case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 246–265. Springer, Heidelberg (2009)
Wang, S., Nielson, F., Riis Nielson, H.R.: A framework for hybrid systems with denial-of-service security attack. Technical Report ISCAS-SKLCS-14-06, Institute of Software, Chinese Academy of Sciences (2014)
Zhan, N., Wang, S., Zhao, H.: Formal modelling, analysis and verification of hybrid systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Unifying Theories of Programming and Formal Engineering Methods. LNCS, vol. 8050, pp. 207–281. Springer, Heidelberg (2013)
Zhou, C., Hansen, M.R.: Duration Calculus — A Formal Approach to Real-Time Systems. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)
Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Zhou, C., Wang, J., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 511–530. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Wang, S., Nielson, F., Nielson, H.R. (2014). Denial-of-Service Security Attack in the Continuous-Time World. In: Ábrahám, E., Palamidessi, C. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2014. Lecture Notes in Computer Science, vol 8461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-43613-4_10
Download citation
DOI: https://doi.org/10.1007/978-3-662-43613-4_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-43612-7
Online ISBN: 978-3-662-43613-4
eBook Packages: Computer ScienceComputer Science (R0)