移动计算系统信息流安全

摘要：

程序信息流安全是信息安全的一个重要研究方向.基于类型的静态分析可以保证程序信息流安全.与单进程系统相比,移动计算系统中数据通讯的存在使得程序信息流安全保护更加困难.Cornell大学的Zdancewic对函数式语言λsec的单进程程序信息流安全进行了研究.本文在其工作的基础上,根据移动计算系统的结构特征,通过对函数式语言λsec进行扩充,加入通讯原语,将其扩展成移动计算语言MobileML,并针对一个简单的移动计算模型,给出了描述程序信息流安全的无干扰性定义,设计了相应的信息流类型系统,用以静态检查保证MobileML语言程序信息流安全.

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

所属期刊栏目：27

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

资助基金：中国科学院资助项目60473068

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

页数：共6页

页码：1455-1460