Security Types for Synchronous Data Flow Systems

Synchronous reactive data flow is a paradigm that provides a high-level abstract programming model for embedded and cyber-physical systems, including the locally synchronous components of IoT systems. Security in such systems is severely compromised due to low-level programming, ill-defined interfaces and inattention to security classification of data. By incorporating a Denning-style lattice-based secure information flow framework into a synchronous reactive data flow language, we provide a framework in which correct-and-secure-by-construction implementations for such systems can be specified and derived. In particular, we propose an extension of the Lustre programming framework with a security type system. We prove the soundness of our type system with respect to the co-inductive operational semantics of Lustre by showing that well-typed programs exhibit non-interference.