%0 Journal Article
%T 一种面向非干扰的线程程序逻辑
%A 李沁？
%A 曾庆凯？
%A 袁志祥？
%J 软件学报
%P 1143-1153
%D 2014
%R 10.13328/j.cnki.jos.004429
%X 目前，针对线程信息流的验证研究主要着重于时间信道.然而，由于线程程序中线程控制原语存在函数副作用，对此类原语的不恰当调用亦可引起非法信息流，有意或无意地破坏程序的非干扰属性.因此，提出以验证线程程序信息流为目的依赖逻辑，其可表达线程程序的数据流、控制流以及线程控制函数的副作用，推理程序变量和线程标识符之间的依赖关系，进而判定是否存在高机密性变量对低机密性变量的干扰.
%K 非干扰
%K 动态作用域线程
%K 公理语义
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4429&flag=1