Time-sensitive Information Flow Control in Timed Event-B

Research output: Contribution to conferencePaper

111 Downloads (Pure)

Abstract

Protecting confidential data in today’s computing environments is an important problem. Information flow control can help to avoid information leakage and violations introduced by executing the software applications. In software development cycle, it is important to handle security related issues from the beginning specifications at the level of abstract. Mu [1] investigated the problem of preserving information flow security in the Event-B specification models. A typed Event- B model was presented to enforce information flow security and to prevent direct flows introduced by the system. However, in practice, timing behaviours of programs can also introduce a covert flow. The problem of run-time flow monitoring and controlling must also be addressed. This paper investigates information flow control in the Event-B specification language with timing constructs. We present a timed Event-B system by introducing timers and relevant time constraints into the system events. We suggest a time-sensitive flow security condition for the timed Event-B systems, and present a type system to close the covert channels of timing flows for the system by ensuring the security condition. We then investigate how to refine timed events during the stepwise refinement modelling to satisfy the security condition.
Original languageEnglish
Publication statusPublished - 13 Sep 2017
Event11th Theoretical Aspects of Software Engineering Conference - Nice, France
Duration: 13 Sep 201715 Sep 2017

Conference

Conference11th Theoretical Aspects of Software Engineering Conference
Abbreviated titleTASE 2017
CountryFrance
CityNice
Period13/09/1715/09/17

Fingerprint Dive into the research topics of 'Time-sensitive Information Flow Control in Timed Event-B'. Together they form a unique fingerprint.

  • Cite this

    Mu, C., & Qin, S. (2017). Time-sensitive Information Flow Control in Timed Event-B. Paper presented at 11th Theoretical Aspects of Software Engineering Conference, Nice, France.