移动计算系统信息流安全

作     者：黄海军 陈意云 HUANG Hai-jun;Chen Yi-yun

作者机构：中国科技大学计算机系 中国科学院软件研究所计算机科学实验室北京100080 

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

出 版 物：《小型微型计算机系统》 (Journal of Chinese Computer Systems)

年 卷 期：2006年第27卷第8期

页      码：1455-1460页

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

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

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1000-1220.2006.08.010

馆 藏 号：203178211...