Hybrid, Dynamic Logic for Hybrid Systems Information Flow

Secure information flow is an important part of ensuring the security and privacy of any computer system. Information flow is little-studied in the context of cyber-physical systems. In this work, I introduce the first notion of information flow that accounts for hybrid (i.e. mixed discrete and continuous) dynamics that arise in CPS.

I introduce a logic, dHL, which can be used to state and verify information flow properties for hybrid-dynamic systems (as well as other hyper-properties). The dHL logic is a dynamic logic based on differential dynamic logic and additional incorporates features from hybrid logic enabling it to represent program states explicitly, simplifying hyperproperty reasoning. This is the first logic I know of which uses hybrid operators to express hyperproperties.

The dHL logic has been used to model and verify a smart grid model based on the FREEDM microgrid. Our analysis reveals and ultimately resolves a bug in the model.