Detecting security leaks in hybrid systems with information flow analysis
Detecting security leaks in hybrid systems with information flow analysis
复制标题
DOI：
10.1145/3359986.3361212
复制
发表时间：
2019-10
期刊：
影响因子：
--
通讯作者：
L. V. Nguyen;G. Mohan;James Weimer;O. Sokolsky;Insup Lee;R. Alur
中科院分区：
文献类型：
--
作者：
L. V. Nguyen;G. Mohan;James Weimer;O. Sokolsky;Insup Lee;R. Alur
信息流分析是一种有效的方法来检查有用的安全属性，如秘密信息是否会泄漏给对手。尽管在编程语言领域得到了广泛的研究，但基于信息流的安全分析在网络物理系统（CPS）领域还没有得到广泛的研究。CPS对传统的基于类型的技术提出了有趣的挑战，因为它们对混合的离散-连续行为进行建模，并且通常表示为状态机的组合。在本文中，我们提出了一个轻量级的静态分析方法，使CPS模型的信息安全属性。我们介绍了一套安全规则的混合自动机，其特点是不干涉的财产。基于这些规则，我们提出了一种算法，产生的安全约束之间的每个子组件的混合自动机，然后将这些约束转换成一个有向依赖图搜索非干扰违规。所提出的算法可以直接应用于自动机的并行合成，而不诉诸模型扁平化技术。我们的静态检查器工作在Simulink/Stateflow格式建模的混合系统上，并决定模型是否满足用户为每个变量提供的安全注释的非干扰性。此外，我们的方法还可以推断变量的安全标签，允许设计人员验证部分安全注释的正确性。我们展示了两个案例研究的潜在好处，所提出的方法。
Information flow analysis is an effective way to check useful security properties, such as whether secret information can leak to adversaries. Despite being widely investigated in the realm of programming languages, information-flow-based security analysis has not been widely studied in the domain of cyber-physical systems (CPS). CPS provide interesting challenges to traditional type-based techniques, as they model mixed discrete-continuous behaviors and are usually expressed as a composition of state machines. In this paper, we propose a lightweight static analysis methodology that enables information security properties for CPS models. We introduce a set of security rules for hybrid automata that characterizes the property of non-interference. Based on those rules, we propose an algorithm that generates security constraints between each sub-component of hybrid automata, and then transforms these constraints into a directed dependency graph to search for non-interference violations. The proposed algorithm can be applied directly to parallel compositions of automata without resorting to model-flattening techniques. Our static checker works on hybrid systems modeled in Simulink/Stateflow format and decides whether or not the model satisfies non-interference given a user-provided security annotation for each variable. Moreover, our approach can also infer the security labels of variables, allowing a designer to verify the correctness of partial security annotations. We demonstrate the potential benefits of the proposed methodology on two case studies.