Time-sensitive information flow control in timed event-B

Chunyan Mu, Shengchao Qin

Research output: Chapter in Book/Report/Conference proceedingPublished conference contribution


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 publicationIEEE 2017 11th International Symposium on Theoretical Aspects of Software Engineering (TASE)
EditorsFrédéric Mallet, Min Zhang, Eric Madelaine
PublisherIEEE Computer Society
Number of pages8
Publication statusPublished - 2017

Bibliographical note

2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)


Dive into the research topics of 'Time-sensitive information flow control in timed event-B'. Together they form a unique fingerprint.

Cite this