基于细粒度信息流分析的高可靠系统安全验证方法研究

项目名称： 基于细粒度信息流分析的高可靠系统安全验证方法研究

项目编号： No.61303224

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 胡伟

作者单位： 西北工业大学

项目金额： 26万元

中文摘要： 高可靠系统设计是一个代价极高的过程。其主要难点在于安全属性的形式化验证。然而，现有的基于语言、过程代数和网络的安全验证方法大多针对较高的抽象层次，无法检测到硬件中的时间隐通道，也无法捕捉由软硬件交互所引发的不确定性系统行为。本项目从信息流安全角度研究高可靠系统的安全验证问题，通过构建底层硬件精确的信息流数学模型来对系统的安全属性进行验证。项目研究电路层面上的细粒度信息流分析方法，采用数学手段为底层硬件构建精确的信息流模型，从硬件电路抽象层次捕捉硬件中全部的逻辑信息流，尤其是硬件相关时间隐通道所引发的有害信息流；研究上层安全属性的映射及验证方法，在给定的信息流安全策略下基于底层硬件的信息流度量能力实现系统关键安全属性的形式化验证，通过捕捉安全域之间的有害信息流动在设计阶段即检测系统中潜在的安全漏洞,包扩硬件相关的时间隐通道，并可向上层提供信息流度量能力，为高可靠系统软硬件安全验证提供支撑。

中文关键词： 高可靠系统；安全验证；形式化方法；信息流分析；无干扰

英文摘要： Designing high-assurance systems is a costly endeavor.The main difficulty lies in formal verification of critical security properties.However, existing language, process algebra and network based methods target too high a level of abstraction to detect hardware-specific timing channels or to capture underministic system behaviors caused by hardware-software interference. This project addresses the high-assurance system security verification problem from the perspective of information flow security.It aims to formally verify security properties through the construction of precise mathematic information flow model for the underlying hardware. To ahieve such a goal, this project studies circuit level fine granularity information flow analysis method. It uses mathematic approaches to formulate information flow model for the underlying hardware to capture all digital information flows, especially harmful flows of information resulting from hardware-specific timing channels. Further, this project studies information security property mapping and verification methods. Critical security properties are formally verified with support of information flow measurement capability from the underlying hardware under specific information flow security policies; potential security vulnerabilities, including hardware-specific timi

英文关键词： High-assurance System；Security Verification；Formal Method；Information Flow Analysis；Non-interference