Normalising Lustre Preserves Security
Sanjiva Prasad, R. Madhukar Yerraguntla

TL;DR
This paper demonstrates that security properties are preserved during the normalization process from LUSTRE to NLUSTRE, ensuring secure information flow in safety-critical system modeling.
Contribution
It extends a security type system from NLUSTRE to unrestricted LUSTRE and proves that normalization transformations preserve security types.
Findings
Security types are preserved during normalization.
Well-security-typed programs are non-interfering.
Normalization transformations are security-preserving.
Abstract
The synchronous reactive data flow language LUSTRE is an expressive language, equipped with a suite of tools for modelling, simulating and model-checking a wide variety of safety-critical systems. A critical intermediate step in the formally certified compilation of LUSTRE involves translation to a well-behaved sub-language called "Normalised LUSTRE" (NLUSTRE). Recently, we proposed a simple Denning-style lattice-based secure information flow type system for NLUSTRE, and proved its soundness by establishing that security-typed programs are non-interfering with respect to the co-inductive stream semantics. In this paper, we propose a similar security type system for unrestricted LUSTRE, and show that Bourke et al.'s semantics-preserving normalisation transformations from LUSTRE to NLUSTRE are security-preserving as well. A novelty is the use of refinement security types for node calls.…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
