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 的正常化变换。 一个新颖的办法是使用完善的安全型安全型系统来调用。 主要结果是通过常规转换来保护安全型号的安全型号。 我们的安全打字规则的正确性输入系统, 显示我们的安全性输入规则的正确性, 通过以前的安全性类型不互换, 通过以前的变变换, 安全型程序, 和变换, 安全性, 变换, 安全性, 变换, 的, 安全性, 变换为以前的变换, 变换。

0
下载
关闭预览

相关内容

《计算机信息》杂志发表高质量的论文,扩大了运筹学和计算的范围,寻求有关理论、方法、实验、系统和应用方面的原创研究论文、新颖的调查和教程论文,以及描述新的和有用的软件工具的论文。官网链接:https://pubsonline.informs.org/journal/ijoc
专知会员服务
123+阅读 · 2020年9月8日
知识图谱推理,50页ppt,Salesforce首席科学家Richard Socher
专知会员服务
105+阅读 · 2020年6月10日
商业数据分析,39页ppt
专知会员服务
159+阅读 · 2020年6月2日
开源书:PyTorch深度学习起步
专知会员服务
50+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
Facebook: 会话机器人最新进展
AINLP
7+阅读 · 2019年9月9日
计算机类 | 低难度国际会议信息6条
Call4Papers
6+阅读 · 2019年4月28日
计算机 | USENIX Security 2020等国际会议信息5条
Call4Papers
7+阅读 · 2019年4月25日
神器Cobalt Strike3.13破解版
黑白之道
12+阅读 · 2019年3月1日
【TED】生命中的每一年的智慧
英语演讲视频每日一推
9+阅读 · 2019年1月29日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
人工智能 | COLT 2019等国际会议信息9条
Call4Papers
6+阅读 · 2018年9月21日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
计算机视觉近一年进展综述
机器学习研究会
9+阅读 · 2017年11月25日
Dissimilarity Mixture Autoencoder for Deep Clustering
Arxiv
0+阅读 · 2021年7月14日
Arxiv
0+阅读 · 2021年7月14日
Arxiv
0+阅读 · 2021年7月13日
Arxiv
7+阅读 · 2018年3月19日
VIP会员
相关VIP内容
专知会员服务
123+阅读 · 2020年9月8日
知识图谱推理,50页ppt,Salesforce首席科学家Richard Socher
专知会员服务
105+阅读 · 2020年6月10日
商业数据分析,39页ppt
专知会员服务
159+阅读 · 2020年6月2日
开源书:PyTorch深度学习起步
专知会员服务
50+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
相关资讯
Facebook: 会话机器人最新进展
AINLP
7+阅读 · 2019年9月9日
计算机类 | 低难度国际会议信息6条
Call4Papers
6+阅读 · 2019年4月28日
计算机 | USENIX Security 2020等国际会议信息5条
Call4Papers
7+阅读 · 2019年4月25日
神器Cobalt Strike3.13破解版
黑白之道
12+阅读 · 2019年3月1日
【TED】生命中的每一年的智慧
英语演讲视频每日一推
9+阅读 · 2019年1月29日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
人工智能 | COLT 2019等国际会议信息9条
Call4Papers
6+阅读 · 2018年9月21日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
计算机视觉近一年进展综述
机器学习研究会
9+阅读 · 2017年11月25日
Top
微信扫码咨询专知VIP会员