Normalising Lustre Preserves Security

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. The main result is the preservation of security types by the normalisation transformations. The soundness of our security typing rules is shown by establishing that well-security-typed programs are non-interfering, via a reduction to type-preservation (here), semantics-preservation (Bourke et al.) and our previous result of non-interference for NLUSTRE.