Denial-of-Service Security Attack in the Continuous-Time World

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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.
Original languageEnglish
Title of host publicationFormal Techniques for Distributed Objects, Components, and Systems. Proceedings
EditorsErika Ábrahám, Catuscia Palamidessi
PublisherSpringer
Publication date2014
Pages149-165
ISBN (Print)978-3-662-43612-7
ISBN (Electronic)978-3-662-43613-4
DOIs
Publication statusPublished - 2014
Event34th IFIP WG 6.1 International Conference, FORTE 2014 - Berlin, Germany
Duration: 3 Jun 20145 Jun 2014

Conference

Conference34th IFIP WG 6.1 International Conference, FORTE 2014
CountryGermany
CityBerlin
Period03/06/201405/06/2014
SeriesLecture Notes in Computer Science
Volume8461
ISSN0302-9743

Keywords

  • Hybrid systems
  • Denial-of-service
  • Safety verification
  • Inference system

Fingerprint Dive into the research topics of 'Denial-of-Service Security Attack in the Continuous-Time World'. Together they form a unique fingerprint.

Cite this