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.

Hybrid-Logical Constructs Enable Information Flow Proofs

Related Publication(s)

Brandon Bohrer and André Platzer.
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow.
Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science,
LICS 2018, Oxford, UK, July 9-12, 2018, ACM, 2018. © The authors.
To appear. preprint