一种面向非干扰的线程程序逻辑*

摘要：

目前，针对线程信息流的验证研究主要着重于时间信道。然而，由于线程程序中线程控制原语存在函数副作用，对此类原语的不恰当调用亦可引起非法信息流，有意或无意地破坏程序的非干扰属性。因此，提出以验证线程程序信息流为目的依赖逻辑，其可表达线程程序的数据流、控制流以及线程控制函数的副作用，推理程序变量和线程标识符之间的依赖关系，进而判定是否存在高机密性变量对低机密性变量的干扰。

关键词：非干扰、动态作用域线程、公理语义

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金61170070,90818022,61321491;国家科技支撑计划2012BAK26B01;国家高技术研究发展计划8632011AA1A202

在线出版日期：2014-08-23（万方平台首次上网日期，不代表论文的发表时间）

页数：共11页

页码：1143-1153