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.
翻译:同步反应数据流语言 LUSTRE 是一种表达式语言, 配有一套用于模拟、 模拟和检查多种安全临界系统的成套工具。 正式认证的 LUSTRE 编译中的一个关键中间步骤是将LUSTRE 转换为一种“ 正常的LUSTRE ” ( NLUSTRE ) 的子语言。 最近, 我们为 NLUSTRE 提出了一个简单的 Denning 式的基于 lattice 的安全信息流类型系统, 并且通过建立安全型程序在共导流语义方面没有相互影响, 证明了它的正确性。 在本文中, 我们为不受限制的 LUSTRE 提出了一个类似的安全型号系统, 并展示了Bourke 等人的语义- 保留从 LUSTRE 到 NLUSTRE 的正常化变换。 一个新颖的办法是使用完善的安全型安全型系统来调用。 主要结果是通过常规转换来保护安全型号的安全型号。 我们的安全打字规则的正确性输入系统, 显示我们的安全性输入规则的正确性, 通过以前的安全性类型不互换, 通过以前的变变换, 安全型程序, 和变换, 安全性, 变换, 安全性, 变换, 的, 安全性, 变换为以前的变换, 变换。