|
|
软件学报 2014
一种面向非干扰的线程程序逻辑DOI: 10.13328/j.cnki.jos.004429, PP. 1143-1153 Abstract: 目前，针对线程信息流的验证研究主要着重于时间信道.然而，由于线程程序中线程控制原语存在函数副作用，对此类原语的不恰当调用亦可引起非法信息流，有意或无意地破坏程序的非干扰属性.因此，提出以验证线程程序信息流为目的依赖逻辑，其可表达线程程序的数据流、控制流以及线程控制函数的副作用，推理程序变量和线程标识符之间的依赖关系，进而判定是否存在高机密性变量对低机密性变量的干扰.
|
