软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2014年
6期
1143-1153
,共11页
非干扰%动态作用域线程%公理语义
非榦擾%動態作用域線程%公理語義
비간우%동태작용역선정%공리어의
non-interference%dynamic scoping multi-threaded program%axiomatic semantic
目前,针对线程信息流的验证研究主要着重于时间信道。然而,由于线程程序中线程控制原语存在函数副作用,对此类原语的不恰当调用亦可引起非法信息流,有意或无意地破坏程序的非干扰属性。因此,提出以验证线程程序信息流为目的依赖逻辑,其可表达线程程序的数据流、控制流以及线程控制函数的副作用,推理程序变量和线程标识符之间的依赖关系,进而判定是否存在高机密性变量对低机密性变量的干扰。
目前,針對線程信息流的驗證研究主要著重于時間信道。然而,由于線程程序中線程控製原語存在函數副作用,對此類原語的不恰噹調用亦可引起非法信息流,有意或無意地破壞程序的非榦擾屬性。因此,提齣以驗證線程程序信息流為目的依賴邏輯,其可錶達線程程序的數據流、控製流以及線程控製函數的副作用,推理程序變量和線程標識符之間的依賴關繫,進而判定是否存在高機密性變量對低機密性變量的榦擾。
목전,침대선정신식류적험증연구주요착중우시간신도。연이,유우선정정서중선정공제원어존재함수부작용,대차류원어적불흡당조용역가인기비법신식류,유의혹무의지파배정서적비간우속성。인차,제출이험증선정정서신식류위목적의뢰라집,기가표체선정정서적수거류、공제류이급선정공제함수적부작용,추리정서변량화선정표식부지간적의뢰관계,진이판정시부존재고궤밀성변량대저궤밀성변량적간우。
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.