一种面向非干扰的线程程序逻辑*

• 作者: 曾庆凯 李沁 袁志祥
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 非干扰 动态作用域线程 公理语义
• 年，卷（期）: 2014,（6）
• 所属期刊栏目: 软件学报
• 页码范围: 1143-1153
• 页数: 11页
• 分类号: TP301
• 字数: 9352字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004429

摘要

目前，针对线程信息流的验证研究主要着重于时间信道。然而，由于线程程序中线程控制原语存在函数副作用，对此类原语的不恰当调用亦可引起非法信息流，有意或无意地破坏程序的非干扰属性。因此，提出以验证线程程序信息流为目的依赖逻辑，其可表达线程程序的数据流、控制流以及线程控制函数的副作用，推理程序变量和线程标识符之间的依赖关系，进而判定是否存在高机密性变量对低机密性变量的干扰。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	曾庆凯		58	555	13.0	21.0
3	袁志祥	安徽工业大学计算机学院	33	149	7.0	10.0
6	李沁	安徽工业大学计算机学院	4	4	1.0	2.0