| 一种面向非干扰的线程程序逻辑 |
| |
| 引用本文： | 李沁,曾庆凯,袁志祥. 一种面向非干扰的线程程序逻辑[J]. 软件学报, 2014, 25(6): 1143-1153 |
| |
| 作者姓名： | 李沁 曾庆凯 袁志祥 |
| |
| 作者单位： | 安徽工业大学计算机学院, 安徽马鞍山 243032;计算机软件新技术国家重点实验室南京大学, 江苏南京 210023;南京大学计算机科学与技术系, 江苏南京 210023;安徽工业大学计算机学院, 安徽马鞍山 243032 |
| |
| 基金项目： | 国家自然科学基金（61170070，90818022，61321491）；国家科技支撑计划（2012BAK26B01）；国家高技术研究发展计划（863）（2011AA1A202） |
| |
| 摘 要： | 目前，针对线程信息流的验证研究主要着重于时间信道.然而，由于线程程序中线程控制原语存在函数副作用，对此类原语的不恰当调用亦可引起非法信息流，有意或无意地破坏程序的非干扰属性.因此，提出以验证线程程序信息流为目的依赖逻辑，其可表达线程程序的数据流、控制流以及线程控制函数的副作用，推理程序变量和线程标识符之间的依赖关系，进而判定是否存在高机密性变量对低机密性变量的干扰.
|
| 关 键 词： | 非干扰 动态作用域线程 公理语义 |
| 收稿时间： | 2012-10-31 |
| 修稿时间： | 2012-10-31 |
Logic of Multi-Threaded Programs for Non-Interference |
| |
| LI Qin,ZENG Qing-Kai and YUAN Zhi-Xiang. Logic of Multi-Threaded Programs for Non-Interference[J]. Journal of Software, 2014, 25(6): 1143-1153 |
| |
| Authors: | LI Qin ZENG Qing-Kai YUAN Zhi-Xiang |
| |
| Affiliation: | 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;School of Computer, Anhui University of Technology, Maanshan 243032, China |
| |
| Abstract: | |
| |
| Keywords: | non-interference dynamic scoping multi-threaded program axiomatic semantic |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
