微内核中断机制的形式化设计与验证.doc

第４０ 卷 第３ 期 ２０１３ 年３ 月 计 算 机 科 学 Ｖｏｌ．４０ Ｎｏ．３ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ Ｍａｒ２０１３ 微内核中断机制的形式化设计与验证 李康杰 钱振江 黄 皓 （南京大学软件新技术国家重点实验室 南京２１００４６） （南京大学计算机科学与技术系 南京２１００４６） 摘 要 操作系统的正 确性和安全 性很难用定 量的方法进行描述。 形式化 方法是操作系统设计和验证领域公 认的标 准方法。 以操作系统对象语义模型（ＯＳＯＳＭ）为基础，采用形式化 方法对微内核架 构 的 中 断 机 制 进 行 了 设 计 和 验 证， 在自行开发的安全 可信操作系统 ＶＴＯＳ 上加以实现，采用Ｉｓａｂｅｌｌｅ／ＨＯＬ 对设计过程 进行了形式化 描述，对 ＶＴＯＳ 中 断机制的完整性进行了验证，这对操作系统的形式化 设计和验证工作起 到了一定 的借鉴意义。 关键词 形式化 设计，形式化 验证，微内核，中断，完整性 中图法分类号 文献标识码 ＴＰ３１６ Ａ ＦｏｒｍａｌＤｅｓｉｇｎａｎｄＶｅｒｉｆｉｃａｔｉｏｎｏｆＩｎｔｅｒｒｕｐｔＭｅｃｈａｎｉｓｍ Ｂａｓｅｄｏｎ Ｍｉｃｒｏｋｅｒｎｅｌ ＬＩＫａｎｇ－ｊｉｅ ＱＩＡＮ Ｚｈｅｎ－ｊｉａｎｇ ＨＵＡＮＧ Ｈａｏ （ＳｔａｔｅＫｅｙＬａｂｏｒａｔｏｒｙｆｏｒＮｏｖｅｌＳｏｆｔｗａｒｅＴｅｃｈｎｏｌｏｇｙ，Ｎａｎｊｉｎｇ Ｕｎｉｖｅｒｓｉｔｙ，Ｎａｎｊｉｎｇ２１００４６，Ｃｈｉｎａ） （ＤｅｐａｒｔｍｅｎｔｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅａｎｄＴｅｃｈｎｏｌｏｇｙ，Ｎａｎｊｉｎｇ Ｕｎｉｖｅｒｓｉｔｙ，Ｎａｎｊｉｎｇ２１００４６，Ｃｈｉｎａ） Ａｂｓｔｒａｃｔ Ｉｔｉｓｄｉｆｆｉｃｕｌｔｔｏｄｅｓｃｒｉｂｅｔｈｅｃｏｒｒｅｃｔｎｅｓｓａｎｄｓｅｃｕｒｉｔｙｏｆｔｈｅｏｐｅｒａｔｅｓｙｓｔｅｍ （ＯＳ）ｂｙｑｕａｎｔｉｔａｔｉｖｅａｎａｌｙｓｉｓ． ＦｏｒｍａｌｍｅｔｈｏｄｉｓｔｈｅａｃｋｎｏｗｌｅｄｇｅｄｓｔａｎｄａｒｄｏｎｅｉｎｄｅｓｉｇｎａｎｄｖｅｒｉｆｉｃａｔｉｏｎｆｏｒＯＳ．Ｂａｓｅｄｏｎｔｈｅｏｐｅｒａｔｅｓｙｓｔｅｍ ｏｂｊｅｃｔ ｓｅｍａｎｔｉｃｓｍｏｄｅｌ（ＯＳＯＳＭ），ｗｅｄｅｓｉｇｎｅｄａｎｄｖｅｒｉｆｉｅｄｔｈｅｉｎｔｅｒｒｕｐｔｉｏｎｍｅｃｈａｎｉｓｍｏｆｍｉｃｒｏｋｅｒｎｅｌａｒｃｈｉｔｅｃｔｕｒｅｕｓｉｎｇｆｏｒ－ ｍａｌｍｅｔｈｏｄ，ｗｈｉｃｈｗａｓｒｅａｌｉｚｅｄｏｎｏｕｒｓｅｌｆ－ｉｍｐｌｅｍｅｎｔｅｄｖｅｒｉｆｉｅｄｔｒｕｓｔｅｄｏｐｅｒａｔｅｓｙｓｔｅｍ （ＶＴＯＳ）．Ｍｅａｎｗｈｉｌｅ，ｗｅｕｓｅｄ ｔｈｅｔｈｅｏｒｅｍ ｐｒｏｖｅｒＩｓａｂｅｌｌｅ／ＨＯＬｔｏｆｏｒｍａｌｌｙｄｅｓｃｒｉｂｅｔｈｅｄｅｓｉｇｎｐｒｏｃｅｓｓ，ａｎｄｖｅｒｉｆｙｔｈｅｉｎｔｅｇｒａｌｉｔｙｏｆｔｈｅｉｎｔｅｒｒｕｐｔｉｏｎ ｍｅｃｈａｎｉｓｍｏｆＶＴＯＳ．ＯｕｒｒｅｓｅａｒｃｈｐｌａｙｓｃｅｒｔａｉｎｒｅｆｅｒｅｎｔｉａｌｓｉｇｎｉｆｉｃａｎｃｅｏｎｆｏｒｍａｌｄｅｓｉｇｎａｎｄｖｅｒｉｆｉｃａｔｉｏｎｏｆＯＳ． Ｋｅｙｗｏｒｄｓ Ｆｏｒｍａｌｄｅｓｉｇｎ，Ｆｏｒｍａｌｖｅｒｉｆｉｃａｔｉｏｎ，Ｍｉｃｒｏｋｅｒｎｅｌ，Ｉｎｔｅｒｒｕｐｔ，Ｉｎｔｅｇｒｉｔｙ 在 ＯＳ 的设计过程中就采用严格的形式化方法来对 系 统 的设计进行描述，使形式化的设计和验证相结合，基于这样的 设计 思 路，设 计 并 实 现 了 ＶＴＯＳ（Ｖｅｒｉｆｉｅｄ Ｔｒｕｓｔｅｄ Ｏｐｅｒａｔｉｎｇ Ｓｙｓｔｅｍ）。ＶＴＯＳ 是按照预定的安全目标而实现的微内核架 构 ＯＳ，并采用Ｉｓａｂｅｌｌｅ／ＨＯＬ［７］定理证明工具对其设计和实现 进行了一致性验证，因此 ＶＴＯＳ 达到了一定的安全等级。 引言 １ 操作系统（ＯｐｅｒａｔｉｎｇＳｙｓｔｅｍ，ＯＳ）是其他计算机软件的 基础，具有高安全性和高可靠性的要求。 形 式 化 方 法 是 验 证 ＯＳ 正确性和安全性的公认方法，因此将形式化方法与 ＯＳ 的 设计以及实现结合是非常必要的，这样可以最大限度地保证 ＯＳ 的正确性。 近年 来 国 内 外 不少学者在这些方面做了很多工 作。 ＮＩＣＴＡ 机构的 ＫｌｅｉｎＧ．博士带领的研究小组对ｓｅＬ４ 进行了 形式化的验证［１］，系统按照访问控制模型、高 层 设 计、低 层 设 计和系统代码实现层等层次来进行划分，目的在于通过验证 各个层 次 之 间 的 一 致 性 来 说 明 系 统 的 正 确 性。Ｙａｌｅ 大 学 ｓｈａｏ带领的 Ｆｌｉｎｔ项目 组［２］采用自行开发的 ＶｅｒｉＭＬ 语 言 和 λＨＯＬｉｎｄ逻辑系统设计［３］和 开