（计算机软件与理论专业论文）基于语言的程序信息流安全.pdf

中国科学技术大学博士学位论文 摘要 摘要 随着i n t e m e t 的不断发展 人们越来越多地从网上下载并使用程序 程序信 息流安全问题越来越重要 程序信息流安全阀题是指程序能否保护重要数据的机 密性和完整性 数据机密性的保护是指程序不让窃密者通过其所能得到的输出数 据等信息来获取或推断程序中的机密数据 如用户密码 数据完整性的保护是指 程序不让窃密者通过调整给程序的输入数据等方式来篡改程序中的机密数据 本 文研究使用基于语言的技术来保护程序信息滤安全 鉴于保护数据机密性的方法 也可用于保护数据完整性 所以本文的程序信息流安全研究以数据机密性的保护 为研究对象 为了保护重要数据的机密性 机密性的安全策略通常要求程序具有 如下的安全性质 高安全级别的输入数据的变化不会影响低安全级别输出数据的 变化 文献中将这种安全陛质称作无干扰性 本文综合叙述了己有的基于编程语言的软件安全研究 带证明的代码口c c 和类型化汇编语言 t a l 两种方法针对的安全策略都是最基本的安全策略如内存 安全 控制流安全和栈安全 信息流安全编程语言则实施信息流安全策略 它扩 大了所描述的类型安全 使其包含无干扰性 本文首先考虑一个简单的移动计算模型 以此为基础 着重考虑了代码移动 对程序信息流安全的影响 确定相应的安全策略 在c o m e l l 大学z d a n c e 姒c 的工 作 函数式语言九 的单进程程序信息流安全 的基础上 根据移动计算系统的 结构特征 通过对函数式语言丸 进行扩充 加入通讯原语 将其扩展成移动计 算语言m o b i l e m l 设计了相应的信息流类型系统 用以类型检查保证m o b i i e m l 语言程序信息流安全 鉴于实际使用的分布式移动计算系统中的主机数目通常多于两个 进程会根 据需要自动创建 我们研究了多进程分布式计算系统中进程之间的通讯对系统信 息流安全的影响 通过对m o b i l e m l 语言进行扩充 加入进程产生表达式 将其 扩展成分布式移动计算语言c o n c u r m l 并设计了两级信息流类型系统 基于源 语言的类型检查和基于进程演算的类型检查 保证进程之间的通讯不会导致信息 泄密 基于类型的分析虽然是检查程序信息流安全的一种有效方法 但过于保守 本文也尝试将传统的数据流分析方法用于单进程程序信息流安全的检查 即利用 数据流分析来跟踪程序数据间的安全依赖关系 达到检查程序信息流安全的目的 竺曼坠童堡奎奁兰堡圭兰堡篁兰 垫茎 和基于类型的方法相比 数据流分析方法能更加精确地分析程序 具有更大的宽 容性 关键词 信息流安全 信息流安全编程语言 无干扰性 形式语义 类型系统 类型安全 静态分析 数据流分析 一 i i 耋曼型茎苎奎奎薹堡圭兰堡鎏圣 丝 竺 a b s t r a c t w i t ht h ec o n t i n u o u s d e v e l o p m e n to fi n t e m e t s o m e u n t m s t e dc o d e sa r e d o w n l o a d e df r o mt h en e t w o r kf o rl o c a la p p l i c a t i o n w h i c hm a k e si te s s e n t i a lt op r o t e c t d a t ac o n f i d e n t i a l i t ya n di n t e g r i t y s t a n d a r ds e c u r i t ym e c h a n i s m ss u c ha sa c c e s sc o n t r o l a n de n c r y p t i o nd on o tp r o v i d eas u b s t a n t i a la s s u r a n c et h a tt h ee n d t o e n db e h a v i o ro fa c o m p u t i n gs y s t e ms a t i s f i e si m p o r t a n ts e c u r i t y p o l i c i e s s u c ha sc o n f i d e n t i a l i t y a n e n d t o e n dc o n f i d e n t i a l i t yp o l i c yc a l l e dn o n i n t e r f e r e n c em i g h ta s s e r tt h a ts e c r e ti n p u t d a t ac a nn o tb ei n f e r r e db ya na t t a c k e rt h r o u g ht h ea t t a c k e r so b s e r v a t i o n so fs y s t e m o u t p u t t h i sp o l i c yr e g u l a t e si n f o r m a t i o nf l o w t h i st h e s i si n v e s t i g a t e sl a n g u a g e b a s e d m e t h o dt oe n s u r ei n f o r m a t i o nf l o ws e c u r i t yo f p r o g r a m s t h i st h e s i sd e s c r i b e st h es t a t eo fa r to fl a n g u a g e b a s e dr e s e a r c h e so ns o f t w a r e s a f e t y p c c p r o o fc a r r y i n gc o d e a n dt a l t y p e da s s e m b l yl a n g u a g e c h e c kw h e t h e rt h e c o d eo b e y sb a s i cs a f e t y e g c o n t r o l f l o ws a f e t y m e m o r ys a f e t y a n ds t a c ks a f e t y s e c u r i t y t y p e dp r o g r a m m i n gl a n g u a g e su s es t a t i ct y p i n gt oe n f o r c ei n f o r m a t i o n f l o w s e c u r i t yp o l i c i e s m o b i l ec o m p u t a t i o ns y s t e mi n v o l v e sc o m m u n i c a t i o n w h i c hm a k e se n s u r i n g s e c u r i t ym o r ed i f f i c u l t b a s e do nt h ez d a n c e w i c sw o r k t h i st h e s i si n t r o d u c e sam o b i l e c o d el a n g u a g ec a l l e dm o b i l e m lw h c i hc o m b i n e s 九 w i t hc o n s t r u c t sf o rt r a n s m i t t i n g a n dr e c e i v i n gv a l u e so nc h a n n e l sa c r o s sr e m o t es i t e s a n dd e v e l o p sat y p es y s t e mt o e n s u r ei n f o r m a t i o nf l o ws e c u r i t yf o rs i m p l em o b i l ec o m p u t a t i o ns y s t e m t h et h e s i sa l s oe x t e n d sm o b i l e m lw i t hs p a w no p e r a t o rw h i c ha l l o w sd y n a m i c p r o c e s sc r e a t i o n t h u st h ee x t e n d e dl a n g u a g ec a l l e dc o n c u r m lp r o v i d e sf a r i l yg e n e r a l s u p p o r tf o rc o n c u r r e n c y at y p es y s t e md e s i g n e d h e r ei st of a c t o rt h ei n f o r m a t i o n s e c u r i t ya n a l y s i si n t ot w op i e c e s i tc a ne n s u r es e c u r i t y f o rc o m m u n i c a t i o nb e t w e e n p r o c e s s e s t y p e b a s e da n a l y s e sc a nb eu s e dt oc h e c ki n f o r m a t i o nf l o ws e c u r i t yo fp r o g r a m s b u tt h e ya r eo v e r l yc o n s e r v a t i v e t h i st h e s i sa p p l i e ss t a n d a r dt e c h n i q u eo fd a t af l o w a n a l y s i st oc h e c ki n f o r m a t i o nf l o ws e c u r i t yo fs e q u e n t i a lp r o g r a m s i no r d e rt om a k et h e c h e c k i n gm o r ea c c u r a t e i tc a ns t a t i c a l l yd e t e r m i n eh o w ap r o g r a m so u t p u t sa r er e l a t e d t oi t si n p u t s i e h o wt h ef o r m e rd e p e n d d i r e c t l yo ri n d i r e c t l y o nt h el a t t e r c o m p a r e d u i w i t ht y p e b a s e da n a l y s e s t h em e t h o dd e s c r i b e di nt h i st h e s i si sm o r en a t u r a la n d1 e s s r e s t r i c t i v e k e y w o r d i n f o r m a t i o nf l o w se c u f i t y s e c u r i t y t y p e dp r o g r a m m i n gl a n g u a g e s n o n i n t e r f e r e n c e f o r m a ls e m a n t i c s t y p es y s t e m t y p es a f e t y s t a t i ca n a l y s i s d a t af l o w a n a l y s i s i v 中圆科学技术大学博士学位论文 第1 章绪论 自 a 自 e 耸i i t e 1 2 j e e j 鼍t j t e e 自 t 自e 目 e j t t 自e 自 一 1 1 研究背景 第1 章绪论 计算机技术的发展进步是一把双刃剑 一方面它使信息的处理 传播更加迅 速 方便 另一方面也使信息的安全性匾临更严峻的考验 数据的完整性 机密 性等性质不再仅是军用计算系统的安全要求 而是i n t e r n e t 上日益增长的企业 个人用户的需求 信息安全问题的研究已成为当今计算机科学领域所面对的挑战 之一 1 1 1 信息安全 什么是信息安全 归纳起来 从信息的安全特性角度看 最基本的要保证以 下几点 简称为c i a t l 2 1 机密性 c o n f i d e n t i a l i t y 信息不泄露给非授权用户 实体或进程 或供 其利用的特性 对抗对手的被动攻击 保证信息不泄露给未授权的人 2 完整性 i n t e g r i t y 数据未经授权不能进行改变的特性 即信息在存储或 传输过程中保持不被修改 不被破坏和丢失的特性 对抗对手主动攻击 防止信 息被未经授权的篡改 3 g 用性 a v a i l a b i l i t y 可被授权实体访问并按需求使用的特性 即当需 要时能否存取所需的信息 例如网络环境下拒绝服务 破坏网络和有关系统的正 常运行等都属于对可用性的攻击 保证信息及信息系统确实为授权使用者所用 1 1 2 程序信息流安全 程序信息流安全问题是指程序能否保护重要数据的机密性和完整性 3 l 数据 机密性的保护是指程序不让窃密者通过其所能得到的输出数据等信息来获取或推 断程序中的机密数据 如用户密码 数据完整性的保护是指程序不让窃密者通过 调整给程序的输入数据等方式来篡改程序中的机密数据 程序信息流安全韵研究 主要是寻找 些方法来判断程序是否能保护重要数据的机密性和完整性 鉴于保 护数据机密性的方法也可用于保护数据完整性 所以目前程序信息流安全的研究 普遍以数据机密性的保护为研究对象 下面给出一个程序信息流安全的例子 例如 某公司开发的股票投资分析软件由客户端程序和服务器端程序组成 客户端程序在你个人计算机上运行 服务器端程序在该公司的服务器上运行 根 三星型兰彗奎查兰堡圭兰堡鎏兰董 耋篁鎏 图1 1 程序信息流安全的例子 据应用需要 客户端程序会接收服务器端程序发送的移动代码 将其放到你个人 计算机上运行 接收的移动代码会读取你计算机上的私有信息 以便根据你的情 况给出投资建议 它运行时也会通过网络传回一些信息 用于改进该软件 如果 该投资分析软件编写不当或恶意窃取 那么该公司利用传回的信息窃取你的私有 信息 如何确保软件不会泄露用户的私有信息 这是典型的程序信息流安全问题 1 1 3 隐蔽通道 隐蔽通道1 4 是一种能够从高敏感级向低敏感级发送信息的机制 这样信息可 以通过隐蔽通道不经意地泄漏给非授权用户 系统中的每个信息比特只要可以由 一个进程修改 而由另 个进程直接或间接地读取 就形成了一个潜在的信息通 道 根据信息的获取方式 隐蔽通道分成两种类型 一类是隐蔽存储通道 即当 一个高安全级别进程对某客体进行写操作 另一个低安全级别进程可以观察到写 的结果 另一类是隐蔽时间通道 即 个高安全级别进程对系统性能产生影响 而这种影响由另一个低安全级别进程监测并由如实时实钟这样的事件坐标测量 系统中使用的程序可能存在大量的隐蔽通道 这是因为低级别用户 窃密者 通常都是低级别用户 通过对程序源码分析等方法来了解程序数据间的相互关系 并试图根据其对程序运行行为的观察 推断商安全级别数据的有关信息 几个简 单的例子如下 本文均用h 代表高安全级别变量 l 代表低安全级别变量 1 显式存储通道可能引起的泄密 例1 1 赋值l h 窃密者可以通过l 直接获得高安全级别数据h 2 隐式存储通道也可能引起泄密 它和程序控制结构有关 例1 2 分支i f h t h e n l 1e l s e l 0 在该段程序中 尽管独立看两个对i 的 赋值都没有问题 但是它们执行与否取决于h 因此窃密者同样可以通过l 推断 出有关h 的信息 3 隐蔽时间通道可能引起的泄密 中国科学技术大学博士学位论文第1 章绪论 例1 3i f h 0t h e nd e l a y 1 0 0 该段程序表示当h 大于0 时 程序运行延时 1 0 0 秒 窃密者可以通过测量程序运行时间的长短来推断有关h 的信息 4 程序终止与否可能导致泄密 它也属于隐蔽时间通道 例1 4i f h 0t h e nl o o p 该程序表示当h 大于0 时 程序陷入死循环 窃密 者可以根据程序是否终止来推断有关h 的信息 还有一些其它形式会引起程序泄密 举例如下 5 别名可能导致泄密 例1 5r t r u e o r t r u e l l e tx i fht h e n r e l s er i n x 2 f a l s e i f rt h e n h 值是f a l s e e l s e h 值是t r u e 该程序描述的是可变存储单元的共享造成的别名泄密 其中r 和r 表示两个 低级别存储单元 它们被赋值低级别数据t r u e 根据h 值的不同 x 可能是r 或 者1 f 的别名 随后x 被赋值低级别数据f a l s e 这样 判断r 存储值是否发生变化 就能推断有关h 的信息 6 系统的概率行为可能导致泄密 例1 6h h m o d2 1 h 口o5 1 0 口o5 l 1 其中运算 2 05 表示一种概率 为0 5 的行为选择 例如l 0 口o5 l 1 表示进程分别以0 5 的概率执行l 0 或l 1 如果我们假设窃密者只是能了解程序的所有可能结果 那么他无法推断有关h 的信息 但是如果窃密者能了解程序的所有可能结果发生的概率 那么他就可以 根据程序执行结果的发生概率来推断有关h 的信息 1 2 传统方法 传统的解决安全问题的方法包括访问控制 代码检测以及加解密方法等 访问控 i z 5 6 1 可能是软件系统中最广泛使用的安全机制 它指控制系统中的主 体 如进程 对系统中的客体 如文件 目录等 的访m 如读 写和执行等 用户只能根据自己的权限大小来访问系统资源 不得越权访问 在概念上系统的主体对客体的存取权限由一个访m 矩阵来表示 访问矩阵的 行和列分别是系统中所有的主体和客体 矩阵中的每一项表示某主体对某客体的 访问方式 读 写和执行 访m 矩阵在系统中常采用存取控制表 a c l 能力 表或其他适合稀疏矩阵的数据结构存储 巾周科学技术尤学博士学位论文第1 套绪论 例1 3i f h 0 t h e nd e l a y 1 0 0 该段程序表示当h 大于0 时 程序运行延时 1 0 0 秒 窃密者可以通过测量程序运行时间的长短来推断有关h 的信息 4 程序终止与否可能导致泄密 它也属于隐蔽时间通道 例1 4i f h 0t h e nl o o p 该程序表示当h 大于0 时 程序陷入死循环 窃密 者可以根据程序是否终止来推断有关h 的信息 还有一些其它形式会引起程序泄密 举例如下 5 别名可能导致泄密 例1 5r t m e r t r u e l l e tx i fht h e nr e l s eri n x f a l s e i f rt h e n 一 h 值是f a l s e e l s e h 值是t r u e 该程序描述的是可变存储单元的共享造成的别名泄密 其中r 和r 表示两个 低级别存储单元 它们被赋值低级别数据t r u e 根据h 值的不同 x 可能是r 或 者r f 的别名 随后x 被赋值低级别数据f a l s e 这样 判断r 存储值是否发生变化 就能推断有关h 的信息 6 系统的概率行为可能导致泄密 例1 6h h r o o d2 1 h 口o5 1 0 口o5 l 1 其中运算口o5 表示一种概率 为0 5 的行为选择 例如l 0 口o5 l 1 表示进程分别以0 5 的概率执行i 0 或1 1 如果我们假设窃密者只是能了解程序的所有可能结果 那么他无法推断有关h 的信息 但是如果窃密者能了解程序的所有可能结果发生的概率 那么他就可咀 根据程序执行结果的发生概率来推断有关h 的信息 1 2 传统方法 传统的解决安全问题的方法包括访问控制 代码检测以及加解密方法等 访问控制 5 6 1 可能是软件系统中最广泛使用的安全机制 它指控制系统中的主 体 如进程 对系统中的客体 如文件 目录等 的访问 如读 写和执行等 用户只能根据自己的权限大小来访问系统资源 不得越权访问 在概念上系统的主体对客体的存取权限由一个访问矩阵来表示 访问矩阵的 行和列分别是系统中所有的主体和客体 矩阵中的每一项表示某主体对某客体的 访问方式 读 写和执行 访问矩阵在系统中常采用存取控制表 a c l 能力 表或其他适合稀疏矩阵的数据结构存储 表或其他适合稀疏矩阵的数据结构存储 中国科学技术大学博士学位论文第1 章绪论 建立在访问矩阵之上的自主访问控制 d a c 使一个客体的拥有者能自由地 决定其他主体对此客体的访问权限 因此它不能约束访问权的扩散而导致的信息 泄露 强制访问控制 m a c 策略通过把所有的主体和客体加上安全性标记 1 a b e l 从而把系统中的主体和客体进行分级 一个主体对客体的存取 只能根据他们的 安全标记所确定的安全级别和事先规定的规则进行 访问控制一般应用于文件和进程等大的客体 这样访问控制只能构建租颗粒 度控制的安全系统 其次 访问控制机制的最终安全依赖于主体 它不能有效地 处理隐蔽通道问题 代码检测是指对机器码进行修改使关键操作可以在执行时被监视 它使用如 下策略 1 若原代码没有违背安全策略 修改后代码的函数行为与原代码的一 致 2 如果原代码违背了安全策略 修改后代码运行时将检测到对安全策略的违 背 让系统截获控制权并终止该错误进程 或者阻止该违背在系统其它部分产生 不良后果 但是 对任意代码通过代码检测方式强加安全策略 代价将非常高 在每个 敏感操作之前都必须执行运行时检查 会使得运行时开销过大 对程序进行分析 后可以删除一些不必要的检查 但是这种分析的代价也不 j 还会增加装入代码 时的开销 此外 即使是最优秀的分析技术也是不完善的 因为安全性质通常是 不可判定的 加解密方法 7 1 是指在数据传输过程中对数据进行加密 在接收时对其进行解 密 从而防止数据豹泄露 但是 当前加密协议的安全性依赖于一些尚未证明的 复杂性理论的假设 另外 加解密方法只能保证重要数据在传输过程中不会泄密 一旦接收方收到数据并且解密后 它就无法保证接收方对数据的处理过程中不产 生泄密 1 3 基于语言的安全 s c h n e i d e 产 1 舛将基于语言的安全定义为使用基于编程语言的理论和实现的 技术 包括语义 类型 优化和验证等 来解决安全问题 这个方向包括了许多 领域的技术 基于语言的安全的大规模应用首例也许是j a v a l l l l 语言 j a v a 语言的精心设计 使得j a v a 程序很稳键 另外j a v a 包含一种基于语言的机制来阻挡恶意的小应用 程序 j a v a 运行环境包括一个字节码检验器 它除了检查字节码的完整性外 还 对字节码进行数据流分析 检查操作码及其操作数是否有效等 由此来保证内存 安全 控制流安全和类型安全等基本性质 同时它也包括一个可信的安全管理器 用来执行如受限的磁盘i o 之类的较高级安全策略 j a v a 编译器产生独立于平台的字节码 它在执行之前由接收方检验 然后被 j a v a 虚拟机解释执行 或者被进一步编译成本地的机器指令 j a v a 的早期版本包括大量的安全漏洞 l 例如 j d k l 1 4 类型系统中有一个 缺陷 在小应用程序的控制下可以创建一个只被部分实例化的类装载器 小应用 程序就可以使用这个类装载器来装入一个恶意的安全管理器 使接收方允许磁盘 访问 从而破坏接收方的数据 这些问题的出现都是因为目前j a v a 缺乏一个足够完备的语义模型 j a v a 并没 有形式规范 它的规范只是非形式的描述 致力于改善这种现状的研究成果已经 出现 例如 对于前面所说的部分实例化问题 s t e p h e nn f r e u n d l l 3 1 提供了一个 针对对象初始化的类型系统 给每个新分配但没有初始化的对象指派特殊的类型 当对象被初始化后 该对象的类型修改为对象的实例化类型 这样 通过静态检 查 可以发现引用未初始化对象的情况 从而报告安全错误 这种方法与s u n 公 司后来提出的修改版本略有不同 但有同样的效果 j o h n c m i t c h e l l 和s t e p h e n n f r e u n d 提出了一种比较完善的j a v a 类型系统 包括了j a v a 字节码语言的大部分 有类 接口 方法 构造函数 异常以及字节码子例程等 为开发字节码语言以 及j a v a 虚拟机验证器的形式规范奠定了基础 但是j a v a 有一个很大的缺点 由 j a v a 编译器产生的独立于机器的字节码不够低级 在下载之后需要j v m 解释或 者由j i t 编译器编译成机器指令 这两种方法都造成运行的时间开销较高 1 3 2p r o o fc a r r y i n gc o d e 卡内基梅隆大学的n e c u l a 和l e e t 4 1 5 1 6 提出了一种新的方法来保护主机免遭 恶意代码的攻击 这种方法称为携带证明代码 p c c p r o o f c a r r y i n gc o d e p c c 能 保证主机自动确定其它系统提供的程序代码是否安全地安装并执行 它是指允许 安全条件形式证明在代码运行前产生和验证的一种方法 其关键思想在于代码发 送方创建一个形式化的 安全证明 来证实代码是否遵照预先定义的安全条件 然后 代码接收方使用一个简单快速的证明验证器来检查证明过程是否正确 从 而判断代码是否可以安全执行 在p c c 框架中代码产生方和代码消费方共同协商了安全策略 即给出了安全 中国科学技术大学博士学位论文 第1 章绪论 代码的规范 代码产生方通过验证编译器 c e r t i f y i n gc o m p i l e r 将源语言编译为 带有循环不变式注释的目标代码 产生循环不变式是一件困难的事情 但是由于 在n e c u l a 的p c c 实现中安全策略较为简单 验证编译器能够通过源程序的类型 信息自动产生循环不变式 除了目标代码之外 代码产生方还需要产生移动代码 满足安全策略的证明 证明产生的过程和扩展静态检查中类似 验证条件产生器 产生验证条件 然后用自动定理证明器产生证明 代码消费方在同时接收到带注释的目标码和证明之后 使用同样的验证条件 产生器产生验证条件 但是代码消费方并不产生证明 而是检查附带证明是否正 确 证明检查过程可以看作一个类型检查过程 它将检查证明中的每一步推断是 逻辑中的公理或是推断规则的一个实例 因为验证条件是通过对目标码进行符号 计算产生的 所以所检查的确实是实际代码满足安全策略的证明 这可以防止恶 意的代码通过携带一个合法的证明来破坏主机 p c c 框架具有通用性 能够用来确保包括内存安全 类型安全以及资源限制 在内的各种安全性质 p c c 还是一种有效的移动代码传递协议 代码产生方承担 了对代码安全性质的繁复的证明工作 而代码消费方只需承担少量且能够启动完 成的检查工作 1 3 3t y p e da s s e m b l yl a n g u a g e t a l 类型化的汇编语言 t a l 1 7 1 8 1 9 是一种基于语言的系统 在编译强类型语 言的程序时 程序中的类型信息通过一系列的转换依附在目标代码之中 产生 种带类型注解的目标代码 同时 必须有一个类型检查器对这种目标代码进行静 态检查 判断目标代码的语义与施加的类型限制是否一致来决定目标代码是否安 全 t a l 的理想目标是提供一种低级的 静态的类型化目标语言 使之比j a v a 字节码更加适合于支持众多的源语言以及大量的优化 最初 t a l 是通过对一种类m l 的多态类型抽象语言进行一系列变换丙得到 的结果 这些变换被称为保类型变换 最终形成的t a l 是基于传统的i n t e l 体系 结构的汇编语言 但是 t a l 的静态类型系统加强了高级的语言抽象 铡如闭包 元组以及用户自定义的抽象数据类型等 r a l 的类型系统保证类型正确的程序不 会违反这些抽象 而且 t a l 的类型系统不会阻碍如寄存器分配 指令选取和指 令调度之类的低级优化 产生早期t a l 版本的变换中包括了后续传递语义 c p s 变换 c p s 使用堆分 塞里型耋薹娄盔兰堡圭兰堡鎏耋堡 塞篁丝 配的活动记录取代栈分配的活动记录 堆分配与传统的栈分配的实现相比有不少 优点 易于实现一些控制原语如异常 一阶后续等 a p p e l 和邵中 2 0 指出堆分配 可以节省空间 因为它更容易共享环境 堆分配有统一的内存管理机制 垃圾回 收 来分配和释放各种对象 包括活动记录 但是有两个重要的因素使得提供对 栈的支持很有必要 基于栈的活动记录所占用空间比基于堆的活动记录要小 许 多芯片的体系结构设计要求应用程序使用基于栈的方法 例如 奔腾p r o 芯片内 部有一个用来预测过程返回地址的内部栈 它来源于使用标准控制栈的调用 返回 原语 因此 t a l 的后续版本添加了栈 它的文法请参见 1 7 n e a lg l e w 和g r e gm o r r i s e t t 2 1 1 指出将t a l 扩展成m t a l m o d u l at a l 并在 每个目标文件的开始处添加引入和导出接口 使得连接时的类型检查与目标文件 自身的类型检查分离开来 如果检查得出各个文件的接口是良类型的 则可以保 证目标代码在连接时的良类型性质 目前 t a l 已实现的版本叫做t a l x 8 6 软件 包 它定义了类似于c 的高级语言p o p c o r n 1 3 4 信息流安全编程语言 基于编程语言表示和检查安全属性能够有效地帮助写出安全程序a 这个方向 包括了许多领域的技术 其中最主要的是基于安全语言的方法 一个安全的语言 保证了用它写出的语言的执行无误 安全语言通常具有特定形式的规范 以及根 据规范制定的程序检查器 在现代编程语言中基于类型系统来构造安全语言是一 种重要的手段 类型系统排除了一个运行时的错误集合 通过类型检查的程序将 不会出现这个集合中的错误 类型方法具有坚实的理论基础和实用而有效的检查 手段 它弓l 起了越来越多的关注 传统的类型系统的表达能力较弱 不能够满足 描述一些程序安全性质的要求 近年来基于类型方法的热点研究围绕着设计能够 表示更加丰富程序安全性质的类型系统来展开 例如通用的高阶类型化中问语言 f l i n t 2 2 1 基于依赖类型的命令式语言x a n a d l 1 2 3 以及对传统类型系统进行类型细 化 t y p er e f i n e m e n t 的研究 2 自二十世纪九十年代以来 信息流安全编程语言 2 5 1 该语言能保证用它写出 的程序是信息流安全的 的研究一直成为国际上的研究热点n 经过近十几年的发 展 这方面的研究已经取得了相当多的成果 程序信息流安全的静态分析方法 2 6 由d e n n i n g 最早提出 他的基本思想是用 完全格模型来描述程序数据的安全级别 通过语法制导的静态翻译 确保一安全 级别的输入端 变量或进程的信息只会流向同级别或更高级别的输出端 变量或 皇里型耋茎查奎兰堡圭耋簦篁塞 薹 耋塑兰 进程 例如 如果变量石的安全级别是点 那么变量y 到x 的赋值的语义动作是 判断关系上迎是否由格隐含 该方法不足之处在于缺少形式化的可靠性证明 d e n n i sv o l p a n o 和g e o f f r e ys m i t h 在d e n n i n g 工作的基础上 给出了第一个基 于类型的程序信息流安全分析方法 2 7 2 s j 研究的语言是简单的w h i l e 命令式编程 语言 它包括赋值语句和简单的控制语句 变量存储的值是整数值 他们解决的 是隐蔽存储通道引起的泄密 所设计的信息流类型系统独立于普通类型系统 变 量类型反映该变量的安全级别 表达式类型是表达式所含变量安全级别的最小上 界 语句类型记录语句中被赋值变量的安全级别最小值 鉴于该语言具有的控制 结构比较简单 仅有条件语句和w h i l e 循环语句 类型规则要求判断表达式的类 型和分支语句 或循环体语句 的类型一致 由于类型系统是由一组定型公理和 规则构成的形式化系统 因此可形式化证明信息流类型系统接受的程序是信息流 安全的 c o m e l l 大学的j i f j a v a i n f o r m a t i o nf l o w 2 9 3 0 3 1 1 以整个j a v a 语言为研究对 象 包括对象 异常和参数化类等 n f 的信息流类型系统是对j a v a 普通类型系 统的扩展 普通类型上增加安全级别标识 它使用一个安全级别标记p c 来记录 表达式所在控制结构反映出的安全级剐 防止表达式计算过程中产生的副作用 例 如赋值和异常抛出 导致泄密 此外 j i f 使用的是分散标识格模型 d e c e n t r a l i z e d l a b e lm o d e l 跟普通格安全模型相比 能更好她支持不信任用户之间的信息共享 并且在 定的安全条件下 允许降密动作 d e c l a s s i f y 发生 j i f 表达能力强 几 乎包括所有j a v a 语言特征 这使得它能应用于实际工程 但另一方面复杂的语 言特征使得类型系统可靠性 保证程序信息流安全 难以形式化验证 p o t t i e r 和s i m o n e r 设计的信息流安全语言 3 2 1 是一个值调用的九语言 称作c o r e m l 所含的语言特征包括l e t 多态 积 p r o d u c t s 和 s u m s 引用 异常和 普通简单操作 他们最大的贡献是巧妙地证明了c o r em l 语言程序是信息流安全 的 具体的做法是 首先定义一个非标准扩充语言 c o r em l 语言是其子集 它 允许显式地推断程序表达式两次计算过程中的相同点和不同点 其次 设计该扩 充语言的类型系统 证明其具有主体归约属性 s u b j e c tr e d u c t i o np r o p e r t y 最后 把c o r e m l 语言的信息流安全证明转化成该扩充语言的主体归约属性 类型安全 属性的一种 的结论 基于编程语言语义的信息流安全描述程序闻的行为等价关系 可用互模性 b i s i m u l a t i o n 定义 基于抽象状态机的信息流安全是对系统迹进行分析 它们是 不同抽象层次上的信息流安全定义 h e i k om a n t e l 祁a n d r e is a b e l f e l d 3 3 3 4 1 把两者 璧坠兰塞当奎兰曼圭兰堡鎏兰釜 兰堑篁 联系到一起 他们以一个简单多进程编程语言为例 先将该语言保证的程序信息 流安全属性转化成一个抽象状态机层次上定义的安全规范 通过对转换可靠性和 完备性的证明 说明了这两个方面定义的信息流安全是等价的 目前 基于语言的程序信息流安全研究主要围绕着下列四个方面开展 1 车 富信息流安全语言的表达能力 2 并发系统信息流安全的保护 3 基于语言的隐蔽 通道分析 4 提出更加灵活的程序信息流安全策略 1 3 5p c c 和t a l 对信息流安全编程语言的影响 尽管前面介绍的带证明的代码 p c c 和类型化汇编语言 t a l 两种方法针对 的安全策略都是最基本的安全策略 内存安全 控制流安全和栈安全 但是这些 方法使用的技术可借鉴用于程序信息流安全的保护 p c c 是将h o a r e 逻辑用于汇编语言安全性质的验证 目前h o m e 逻辑已经可 以用于对程序信息流安全性质的验证口5 1 逻辑方法和类型方法同根同源 类型理 论即是构造逻辑的一种 逻辑方法和类型方法同根同源 类型理论即是构造逻辑 的一种 c u r r y h o w a r d 同构 c u r r y h o w a r di s o m o i p h i s m0 1 c o r r e s p o n d e n c e 更揭 示了类型系统和逻辑之间的对应和类似 命题即是类型 p r o p o s i t i o n sa st y p e s 这种对应使这两个方向上的研究能够互相启发 t a l 是一个在汇编语言层次上的类型化语言 使褥类型在编译中不仅能够引 导编译过程 还能够用于安全性质的推理 而目前信息流安全编程语言大多都是 高级语言 在编译的过程中类型检查器对源程序进行了类型检查之后 在代码优 化和翻译到机器代码的过程中 这些类型信息大多被抛弃 信息流安全属性在翻 译的过程中并不能被保证 如果使用t a l 技术 设计汇编语言层次上的信息流安 全编程语言 那么信息流安全信息被保持到低级代码中 此举降低程序验证层次 减小系统的需信任计算基础 1 4 本文概述 信息流安全编程语言使用静态信息流类型检查 能保证通过类型检查的程序 是信息流安全的 这样 程序信息流安全的证明是自动完成 并且类型系统能较 好地支持模块性和高阶语言特征 这些优点使得类型检查成为保证程序信息流安 全的重要方法 垦型兰螫娄查耋曼圭兰堡篁圭篁 塞彗鎏 1 4 1 研究工作 目前 信息流安全编程语言大多都是单进程 线程 编程语言 适用于单个 主机系统 随着网络技术的发展 分布式移动计算系统的应用越发广泛 这些系 统具有分布性 移动性和不确定性等特征 这给程序信息流安全的保护带来了诸 多困难 分布式移动计算系统的信息流安全属于系统级安全 它不仅要确保系统 中的每个组件是信息流安全的 而且还要保证组件之间的通讯不会破坏信息流安 全 本文工作着重考虑了这一问题 鉴于分布式移动计算系统中影响信息流安全的因素太多 我们首先考虑一个 简单的移动计算模型 以此为基础 着重考虑了代码移动对程序信息流安全的影 响 确定相应的安全策略 在c o m e l l 大学z d a n c e w i c 的工作 函数式语言九 的 单进程程序信息流安全 的基础上 2 根据移动计算系统的结构特征 通过对函 数式语言k 进行扩充 加入通讯原语 将其扩展成移动计算语言m o b i l e m l 设 计了相应的信息流类型系统 用以类型检查保证m o b i l e m l 语言程序信息流安全 随后 针对分布式移动计算系统中多个进程的特点 我们研究了进程之间的 通讯对信息流安全的影响 通过增加进程产生表达式 m o b i l e m l 扩充成为 c o n c u r m l 语言 设计了两级信息流类型系统 基于源语言的类型检查和基于进 程演算的类型检查 保证进程之间的通讯不会导致信息泄密 最后 我们也尝试将传统的数据流分析方法用于单进程程序信息流安全的检 查 即利用数据流分析来跟踪程序数据间的安全依赖关系 达到检查程序信息流 安全的目的 和基于类型的方法相比 数据流分析方法能更加精确地分析程序 具有更大的宽容性 1 4 2 特色和贡献 本文分别綦于三种不同的机器模型 单进程计算模型 简单的移动计算模型 和分布式移动计算模型 用数据流分析或类型系统的方法 进行了程序信息流安 全的研究 它具有如下所述的特色和贡献 1 在一种最简单的移动计算模型上 根据移动计算系统的结构特征 将函数 式语言九 扩展成移动计算语言m o b i l e m l 给出描述m o b i l e m l 程序信息流安全 的无干扰性定义 设计了相应的信息流类型系统 以支持用静态检查方式来保证 m o b i l e m l 程序的信息流安全 2 在 种简单的分布式移动计算模型上 研究多进程分布式计算系统中进程 之间的通讯对系统信息流安全的影晌 通过在m o b i l e m l 语言中加入进程产生表 中国科学技术犬学博士学位论文第1 章绪论 达式 将其扩展成分布式移动计算语言c o n c u r m l 并设计了两级信息流类型系 统 基于m o b i l e m l 语言的类型检查和基于进程演算的类型检查 使得在完成普 通类型检查的同时 可以保证进程之间的通讯不会导致信息泄密 c o n c u r m l 语言能很好地支持分布式移动计算环境 允许任意进程并发 支持 同步通讯及相应的进程同步 信道和函数作为第一类值 能很好地模拟网络连接 的动态性和代码的移动性 3 对于单进程计算模型 基于w h i l e 语言 提出一种信息流安全的数据流分 析算法 并证明了该算法的可靠性 和基于类型系统的方法相比 数据流分析方 法具有较大的宽容性 1 4 3 章节安排 文章的剩下章节将做如下安排 论文的第二章将描述信息流安全模型 以及 说明信息流安全编程语言设计的一般方法 第三章将针对一个简单的移动计算模 型设计保证程序信息流安全的移动计算编程语言m o b i l e m l 给出包括语法 动 态语义 静态语义的形式描述 第四章从简单移动系统环境转移到多进程分布式 环境 编程语言c o n c u r m l 相应地增加了进程产生表达式 设计了相应的类型系 统 保证进程间通讯不会导致泄密 第五章将介绍如何用传统的数据流分析方法 来保证单进程程序信息流安全 最后在第六章将给出对本文工作的总结 中国科学技术大学博士学位论文 第2 章信息流安全模型 第2 章信息流安全模型 六十年代末期 计算机系统的安全漏洞就已经为人们所认识 开始了对信息 的安全性的研究 进入九十年代 计算机的性能得到了成百上千倍的提高 应用 的范围扩大 并以通信网络把各个孤立的单机系统联系起来相互通信和共享资源 计算机信息的安全问题也日益严峻 为此开发出了各种各样的信息安全技术 在 研究中人们发现 不存在一个绝对安全的系统 一个系统的安全总有这样或那样 的漏洞 设计一个安全系统的关键是要对系统的安全需求 以及如何设计和实现 安全控制有一个清晰的 全面的理解和描述 也就是说 要提出并实现一定的安 全策略 根据对系统的安全性要求的高低 可以采用不同形式的模型 对于一个中等 安全程度而言 可以采用一个自然语言描述的安全模型 而对于高安全等级的系 统 般要采用形式数学方法来对精确的安全定义进行建模 数学模型 形式化 描述和验证技术