Secure Composition in Synchronous Dataflow 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 extend the Lustre programming framework with a security type system. The work is currently being formalized in Coq over Vèlus development.
Madhukar Yerraguntla, Sanjiva Prasad, Subodh Sharma