###
Journal of Software:2014.25(6):1143-1153

一种面向非干扰的线程程序逻辑
李沁,曾庆凯,袁志祥
(安徽工业大学计算机学院, 安徽马鞍山 243032;计算机软件新技术国家重点实验室南京大学, 江苏南京 210023;南京大学计算机科学与技术系, 江苏南京 210023)
Logic of Multi-Threaded Programs for Non-Interference
LI Qin,ZENG Qing-Kai,YUAN Zhi-Xiang
(School of Computer, Anhui University of Technology, Maanshan 243032, China;State Key Laboratory for Novel Software Technology Nanjing University, Nanjing 210023, China;Department of Computer Science and Technology, Nanjing University, Nanjing 210023, China)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 1955   Download 1966
Received:October 31, 2012    Revised:October 31, 2012
> 中文摘要: 目前,针对线程信息流的验证研究主要着重于时间信道.然而,由于线程程序中线程控制原语存在函数副作用,对此类原语的不恰当调用亦可引起非法信息流,有意或无意地破坏程序的非干扰属性.因此,提出以验证线程程序信息流为目的依赖逻辑,其可表达线程程序的数据流、控制流以及线程控制函数的副作用,推理程序变量和线程标识符之间的依赖关系,进而判定是否存在高机密性变量对低机密性变量的干扰.
Abstract:Existing work on the verification of information flow in threads mainly focuses on timing channels. However, this paper shows that system calls, such as‘fork’ or ‘join’ with side effects, can also be used to create covert channels intentionally or accidentally. The study results in a dependency logic for verifying information flow in multi-threaded programs where improper calls over thread controlling primitives with side effects could incur illegal information flow. The logic can express the data flow, control flow and the side effects of thread-controlling system calls, and can reason about the dependency relationship among variables and thread identities, to determine whether secret variables interfere with public ones in multi-threaded programs.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61170070,90818022,61321491);国家科技支撑计划(2012BAK26B01);国家高技术研究发展计划(863)(2011AA1A202) 国家自然科学基金(61170070,90818022,61321491);国家科技支撑计划(2012BAK26B01);国家高技术研究发展计划(863)(2011AA1A202)
Foundation items:
Reference text:

李沁,曾庆凯,袁志祥.一种面向非干扰的线程程序逻辑.软件学报,2014,25(6):1143-1153

LI Qin,ZENG Qing-Kai,YUAN Zhi-Xiang.Logic of Multi-Threaded Programs for Non-Interference.Journal of Software,2014,25(6):1143-1153