Time-sensitive Information Flow Control in Timed Event-B

Chunyan Mu, Shengchao Qin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

268 Downloads (Pure)


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
Title of host publication2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)
ISBN (Electronic)9781538619247
Publication statusPublished - 13 Sept 2017
Event11th Theoretical Aspects of Software Engineering Conference - Nice, France
Duration: 13 Sept 201715 Sept 2017


Conference11th Theoretical Aspects of Software Engineering Conference
Abbreviated titleTASE 2017


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

Cite this