摘要
程序信息流安全是信息安全的一个重要研究方向.基于类型的静态分析可以保证程序信息流安全.与单进程系统相比,移动计算系统中数据通讯的存在使得程序信息流安全保护更加困难.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.
出处
《小型微型计算机系统》
CSCD
北大核心
2006年第8期1455-1460,共6页
Journal of Chinese Computer Systems
基金
国家自然科学基金项目(60473068)资助
关键词
程序信息流安全
无干扰性
形式语义
类型系统
子定型
information flow security
noninterference
formal semantics
type system
subtyping
