Time-sensitive information flow control in timed event-B

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.