-
题名利用特征配置的SLIM安全性验证方法
被引量：3
- 1
-
-
作者
李宙洲
魏欧
黄鸣宇
-
机构
南京航空航天大学计算机科学与技术学院
-
出处
《小型微型计算机系统》
CSCD
北大核心
2017年第10期2346-2351,共6页
-
基金
国家"九七三"重点基础研究发展计划项目(2014CB744904)资助
国家自然科学基金项目(61170043)资助
航空科学基金项目(20155552047)资助
-
文摘
安全关键系统的愈发复杂,使得系统的安全性和开发成本面临着越来越大的挑战.由ESA赞助的COMPASS项目,使用SLIM对诸如航天器系统这样的安全关键系统进行建模,不仅可以描述系统标定的软硬件行为,还可以描述系统的概率性故障、故障对系统的影响和系统恢复.本文从软件产品线角度提出一个新颖的、针对SLIM扩展模型的验证方法—将软件产品线中产品的可变性引入安全性验证过程,将系统中的故障看作系统中可以进行配置的特征,直观、清楚地刻画了安全分析中系统的结构和行为.使用成熟的SLIM语言建立安全关键系统的扩展模型,将SLIM扩展模型中的故障作为特征、完成扩展模型到fPromela模型的转换;利用软件产品线模型检测工具SNIP对转换得到的f Promela模型进行检测,找出造成系统失效的故障,完成对SLIM扩展模型的安全性验证工作.根据模型转换的规则,设计并实现了转换工具S2F.同时,结合COMPASS给定的标准案例—数据采集系统进行实例分析.
-
关键词
安全关键系统
SLIM语言
F
Promela语言
安全性验证
模型检测
-
Keywords
safety-critical system
SLIM
fPromela modelling language
safety verification
model checking
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名概率模型检测的网络传播干预策略
被引量：1
- 2
-
-
作者
李宙洲
魏欧
郭宗豪
余鹏
韩兰胜
-
机构
南京航空航天大学计算机科学与技术学院
华中科技大学计算机科学与技术学院
-
出处
《小型微型计算机系统》
CSCD
北大核心
2017年第6期1175-1180,共6页
-
基金
国家"九七三"重点基础研究发展计划项目(2014CB744904)资助
国家自然(61170043
61272033)资助
-
文摘
网络普遍存在于自然界和人类社会中,计算机病毒、传染疾病、森林火灾以及社会流言等在网络中的传播给经济、社会带来巨大挑战.寻找有效的干预策略实现对网络传播的控制是一个重要的研究问题.根据传播过程的内在规律,引入了概率网络传播模型,将干预目标描述为相应的概率时序逻辑属性,提出了概率情况下的网络传播干预策略问题;进一步,以离散的邮件病毒传播模型为研究对象,重点分析了安装防护,定期防护两种防护措施,给出了相应的干预策略分析问题;并且,采用概率模型检测工具PRISM,结合近似模型检测方法,进行了实验分析.
-
关键词
概率模型检测
网络传播干预策略
近似模型检测方法
形式化方法
-
Keywords
probabilistic model checking
network propagation intervention
approximate probabilistic model checking
formal methods
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名基于自适应的软件定义安全架构
被引量：1
- 3
-
-
作者
陶云祥
李宙洲
-
机构
中移(苏州)软件技术有限公司
-
出处
《电信工程技术与标准化》
2019年第6期66-71,共6页
-
文摘
随着云计算的快速发展,传统固定边界和设备的安全手段,在云安全时代出现了技术上的不适应以及疲于奔命的运维现象。软件定义适用于解决云计算中面临的系统性问题。软件定义安全有轻量、易部署、高兼容、可编排的特点,结合Gartner提出的自适应安全架构的思想,设计了可以自适应的软件定义安全的架构。该架构可以分为管理编排层、控制层、业务层和物理层,以松耦合的模块结合形式,开放标准对外接口,兼容新技术的使用和对接,实现虚拟安全网元自动可编排的自适应安全闭环。
-
关键词
自适应
云安全
软件定义安全
-
Keywords
adaptive
cloud security
software defined security
-
分类号
TN918
[电子电信—通信与信息系统]
-
