移动计算系统信息流安全  

Information Flow Security for Mobile Computation System

作　　者：黄海军[1] 陈意云[1,2] 

机构地区：[1]中国科技大学计算机系 [2]中国科学院软件研究所计算机科学实验室,北京100080

出　　处：《小型微型计算机系统》2006年第8期1455-1460,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(60473068)资助

摘　　要：程序信息流安全是信息安全的一个重要研究方向.基于类型的静态分析可以保证程序信息流安全.与单进程系统相比,移动计算系统中数据通讯的存在使得程序信息流安全保护更加困难.Cornell大学的Zdancewic对函数式语言λsec的单进程程序信息流安全进行了研究.本文在其工作的基础上,根据移动计算系统的结构特征,通过对函数式语言λsec进行扩充,加入通讯原语,将其扩展成移动计算语言MobileML,并针对一个简单的移动计算模型,给出了描述程序信息流安全的无干扰性定义,设计了相应的信息流类型系统,用以静态检查保证MobileML语言程序信息流安全.Ensuring information flow security of programs is an important research direction of information security. Typebased analyses can be used to ensure information flow security of programs. Mobile computation system involves communication, which makes ensuring security more difficult. Based on the Zdancewic＇s work, this paper extends λsec with constructs for transmitting and receiving values on channels across remote sites, and develops a type system to ensure information flow security for simple mobile computation system.

关 键 词：程序信息流安全 无干扰性 形式语义 类型系统 子定型 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]