基于IsabelleHOL的安全操作系统形式化验证方法.pdf

计 算 机 与 现 代 化 2017年第 4期 JISUANJIYUXIANDAIHUA 总第260期 文章编号：1006-2475(2017)04-0099-06 基于 Isabelle／HOL的安全操作系统形式化验证方法 郭 毅，杨维永，刘 苇 (南京南瑞信息通信科技有限公司，江苏 南京 210003) 摘要：操作系统作为信息时代的基石，其安全性不言而喻。常规的软件测试方法不足以保障操作系统的安全性，需使用 更为严格的基于数理逻辑的形式化验证方法。本文提 出一种软件形式化验证的新思路：通过在 Isabelle中构造模拟运行 环境 ，使汇编代码运行其中，并记录系统状态的变化，最终根据程序运行前后 系统状 态的变化情况判断程序的正确性和 安全性。重点介绍了顺序、分支和循环等3种程序结构的证明方法，并通过一个程序实例证明，得到在任意前提条件下 程序执行前后 系统状态的变化情况。 关键词：安全操作系统；形式化验证 ；Isabelle／HOL；霍尔逻辑 中图分类号：TP309．2 文献标识码：A doi：10．3969／j．issn．1006-2475．2017．04．0020 FormalVerificationMethodofSecureOperatingSystem BasedonIsabelle／HOL GU0Yi，YANGW ei-yong，LIU Wei (NARIInformation＆CommunicationTechnologyCo．Ltd．，Naming210003，China) Abstract：Astheeornerstoneoftheinformationage，theimportanceofoperatingsystem securityisserf-evident．Conventional methodsofsoftwaretestingarenotenoughtoguaranteethesafetyoftheoperatingsystem ，SOweneedtousemorerigorousfomr al verificationmethodsbasedonmathematicallogic．Thispaperputsforwardanew ideaofofmr al verificationofsoftware：construc— ringasimulationrunningenvironmentinIsabelle，andrunningtheassemblycodeinit，recordingthechangesofthesystem state， andfinallyaccordingtothechangesofsystem statebeforeandafterrunoftheprogram ，detemr iningthecorrectnessandsafetyof theprorgam．Itemphaticallyintroducestheprovemethodofsequential，conditionalanditerativesturcture，usesthem ontoa sma pleprorgam ，andgetsthestatechangesunderanypreconditions． Keywords：secureoperatingsystem；ofmr alverification；Isabelle／HOL；Horaelogic 已有的操作系统形式化验证项 目有 seL4 、Ver． 0 引 言 isoft 和 Flint 等。本文提出一种全新的软件形式 如今，软件已充斥人类生活的方方面面，随之而 化验证方法，其理论依据为霍尔逻辑。为降低引入人 来的是大量的软件安全 问题。作为最核心的基础软 为错误的风险，选择使用辅助定理证明工具