LUSTRE中的安全信息流分类
Secure Information Flow Typing in LUSTRE
摘要：
同步反应式数据流是一种为嵌入式和网络物理系统（包括物联网系统的本地同步组件）提供高级抽象编程模型的范例。由于低层次的编程、定义不明确的接口和不注意数据的安全分类，这些系统的安全性受到严重损害。通过将丹宁风格的基于格的安全信息流框架到一个同步反应数据流语言，我们提供了一个框架，在该框架中，正确和安全的建设实现这样的系统可以指定和派生。特别是，我们提出了一个安全类型系统的光泽编程框架的扩展。我们的类型系统的新颖之处在于在安全类型变量的约束，特别是节点调用的治疗，这使我们能够对任何安全类格的安全流的原因的象征性制定。的主要定理是我们的类型系统的健全性方面的共同归纳操作语义的光泽，我们证明了良好的类型的程序表现出不干扰。而不是处理完整的语言，我们首先证明了一个行为良好的子语言称为“规范化光泽”（NLustre），我们的类型系统要简单得多的非干扰结果。然后，我们表明，伯克等人。从Lustre到NLustre的语义保持“规范化”转换也是安全保持的。这种通过规范化转换对安全类型的保留是一种类似于“主题归约”的属性，但在编译器转换的级别上。的主要结果，良好的安全类型的光泽程序是不干扰以下从减少到我们早期的结果不干扰NLustre通过语义保存（Bourke等人）。和类型保存结果。
英文摘要：
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 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 non-interference. Rather than tackle the full language, we first prove the non-interference 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 non-interfering follows from a reduction to our earlier result of non-interference for NLustre via the semantics-preservation (of Bourke et al.) and type preservation results.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
