中文摘要：

程序信息流安全是信息安全的一个重要研究方向．基于类型的静态分析可以保证程序信息流安全与单进程系统相比．移动计算系统中数据通讯的存在使得程序信息流安全保护更加困难．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.