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 may be specified and derived. In particular, we propose an extension of the LUSTRE programming framework with a security type inference system. The novelty of our type system lies in a symbolic formulation of constraints over security type variables, in particular the treatment of node calls, which allows us to reason about secure flow with respect to any security class lattice.
The main theorem is the soundness of our type system with respect to the co-inductive operational semantics of LUSTRE, which we prove by showing that well- typed programs exhibit noninterference. Rather than tackle the full language, we first prove the noninterference result for a well-behaved sub-language called “Normalised LUSTRE” (NLUSTRE), for which our type system is far simpler. We then show that Bourke et al.’s semantics-preserving “normalisation” transformations from LUSTRE to NLUSTRE are security-preserving as well. This preservation of security types by the normalisation transformations is a property akin to “subject reduction” but at the level of compiler transformations. The main result that well-security-typed LUSTRE programs are noninterfering follows from a reduction to our earlier result of noninterference for NLUSTRE via the semantics preservation (of Bourke et al.) and type preservation results.
Joint work with Rathnakar Madhukar Yerraguntla and Subodh Vishnu Sharma. Parts of this work appeared in MEMOCODE 2020 (best paper), ICTAC 2021, and their integration and extension is on arXiv.
Sanjiva Prasad is a Professor and former Head of the Department of Computer Science and Engineering (2018-2021) and also the Amar Nath and Shashi Khosla School of Information Technology (2011-20015) at the Indian Institute of Technology Delhi. His research interests include formal methods, programming languages and their semantics, security of information flow and networks, and medical applications of computing. He has written several conference and journal papers in these areas, served on the technical programme committees of several international conferences, and delivered seminar talks at leading universities across the world. He is currently Editor-in-Chief of ACM Books (based in New York), and Chair of the executive committee of the Association for Logic in India.
Prof. Prasad is currently Head of IIT Delhi’s School of Public Policy. His research interests in this area concern issues regarding data and computation, and their confidentiality and integrity, in particular health-related data systems. He is also interested in issues of higher education, pedagogical processes and affordable access to educational materials.
Prior to working at IIT Delhi, Prof. Prasad worked on program verification at Odyssey Research Associates in Ithaca, USA from 1990-1992, and then at the European Computer-Industry Research Center (ECRC GmbH) in Munich, Germany from 1992-1994 on the Facile project which was based on his dissertation. He was a visiting Lektor at BRICS, Aarhus University from 1998 to 1999. His PhD is from Stony Brook University, New York, and he earned a BTech in Computer Science and Engineering from the Indian Institute of Technology Kanpur in 1985.