微内核操作系统互斥量模块功能正确性的形式化验证

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误,因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中,互斥量可协调多任务对资源的访问,是一种常用的任务同步方式,其功能正确性对于保障多任务应用的正确性十分关键.基于定理证明方法,在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模,给出其接口函数的形式化规范,并实现这些接口函数的功能正确性验证.

可信执行环境软件侧信道攻击研究综述

为保护计算设备中安全敏感程序运行环境的安全,研究人员提出了可信执行环境(TEE)技术,通过对硬件和软件进行隔离为安全敏感程序提供一个与通用计算环境隔离的安全运行环境.侧信道攻击从传统的需要昂贵设备发展到现在仅基于微体系结构状态就能通过软件方式获取机密信息的访问模式,从而进一步推测出机密信息.TEE架构仅提供隔离机制,无法抵抗这类新出现的软件侧信道攻击.深入调研了ARM TrustZone、Intel SGX和AMD SEV这3种TEE架构的软件侧信道攻击及相应防御措施,并探讨其攻击和防御机制的发展趋势.首先,介绍了ARM TrustZone、Intel SGX和AMD SEV的基本原理,并详细阐述了软件侧信道攻击的定义以及缓存侧信道攻击的分类、方法和步骤;之后从处理器指令执行的角度,提出一种TEE攻击面分类方法,利用该方法对TEE软件侧信道攻击进行分类,并阐述了软件侧信道攻击与其他攻击相结合的组合攻击;然后详细讨论TEE软件侧信道攻击的威胁模型;最后全面总结业界对TEE软件侧信道攻击的防御措施,并从攻击和防御两方面探讨TEE软件侧信道攻击未来的研究趋势.

大叶芥菜绿色高效栽培技术

栽培技术不够统一、生产管理水平偏低成为制约甘肃省陇南市大叶芥菜产业发展的主要因素,当地通过对大叶芥菜生产的各个技术环节进行不断优化,使大叶芥菜商品率达到95%以上,每667 m^(2)经济效益提高25%以上。大叶芥菜(Brassica juncea var.rugosa Bailey)又名大叶青菜,属十字花科芸薹属一年生草本植物,包括叶用芥、茎用芥、根用芥、薹用芥等不同类型(刘佩瑛,1996;吕家龙,2001)。

TrustZone中断隔离机制的形式化验证

TrustZone技术通过对硬件进行安全扩展,为软件提供了相互隔离的可信执行环境和通用执行环境.中断隔离机制是TrustZone的关键隔离机制,确保安全中断和非安全中断分别在可信执行环境和通用执行环境中被处理,该机制不正确可能导致安全中断被通用执行环境处理,从而影响可信执行环境的安全性.本文提出ARMv8 TrustZone架构中断隔离机制的形式化验证方法,在定理证明器Isabelle/HOL中建立包含中断隔离机制关键软硬件的形式化模型,该模型为状态迁移系统,包括中断处理程序、TrustZone Monitor、中断控制器等组件;在证明模型满足正确性的基础上,通过展开定理验证无干扰、无泄露、无影响等信息流安全属性,结果表明TrustZone中断隔离机制满足信息流安全属性,在中断处理过程中不存在隐蔽的信息流通道.

基于函数式语义的循环和递归程序结构通用证明技术

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.

XDSL技术群与矿井远程通讯的研究

全面分析了矿井环境的特殊性,为了克服光纤传输方式的缺点和采用视频电缆传输方式的不足,解决在矿井条件下实现安全、高速通讯这个难题,建议在矿井通讯中引入基于普通双绞线的宽带通信技术——xDSL 技术。在介绍了 xDSL 技术群的特点及其基本原理的基础上,结合正在研发的远程视频监控系统和矿井移动通讯系统的实际情况,提出了已经初步研发成功的基于 ADSL 和 HDSL技术的系统级应用模型,最后,给出了将 ADSL 技术和 HDSL 技术应用于矿井通讯的改造方案。实践证明:在现行条件下,基于普通双绞线的 xDSL 技术群是矿井通讯更为现实、可行的传输方式。

基于ARM的嵌入式WEB服务器研究

在各种基于客户机/服务器模式的Internet应用中,为了降低服务器的功耗、体积和成本,提出了采用嵌入式WEB服务器代替传统的PC机服务器的方法。介绍了基于ARM嵌入式的WEB服务器设计,分析了系统的硬件配置与软件实现,探讨了嵌入式操作系统的选择和HTTP服务器的工作流程,并进行了相应的实验。

经济型矿井远程网络摄像机系统

目前远程视频监控系统已经成为计算机监控系统的重要分支,同时也是人们研究的热点和难点之一。国内外现有的远程监控系统大多基于光纤,而光纤如果遇到机械冲击、碰撞等都会造成光缆断缆或断芯,光缆断裂后,很难快速修复,且修复设备复杂,普通用户根本无法进行焊接修复,再加上光端机价格较高,这些都限制了光纤远程监控系统的应用和普及。为了解决这个问题,人们找到了价格相对便宜、维护十分简单的极低比特率双绞线解决方案。文中分别以TI低成本DSP芯片F206和TI高性能DSP芯片C6711为例,介绍两种基于DSP芯片的极低码率双绞线网络摄像机系统,这是两套非常经济、实用且具有广播能力的远程矿井网络摄像机系统。

基于ARM的嵌入式系统实验研究

在嵌入式系统实验中,了解ARM的体系结构、熟悉嵌入式操作系统是关键,为了掌握常用外部设备接口驱动程序、接口应用程序的设计,培养学生的硬件、软件协同设计能力,实现对受教育者的分层次培养。本文在认真分析实验内容和实验效果的基础上,提出将实验划分为基础验证型、设计型、综合型和创新型四类,以适应不同层次学习者的学习需要。

基于嵌入式系统的智能教具研究

为了解决现有教具智能化程度低、系统尺寸庞大等问题,研究一种基于知识发现的智能教具系统,并探讨能够在小型嵌入式系统条件下实现知识发现的方法.为突破传统的数据拟合技术,提出采用正交多项式方法,为避免在盲目搜索时,出现组合爆炸,采用了人工智能启发式搜索函数,以减少搜索次数,提高知识发现的自动化程度.

基于视频图像处理的矿井轨道运输监测研究

针对轨道运输监测采用轨道电路和压力传感器因受环境条件影响,可靠性差、现场维护困难,提出采用视频图像处理方法,利用模式识别、最优阈值和几何相似理论,实现非接触式可视化远程监控与测量。现场实验表明,系统不仅能对矿井运输列车运动速度、方向、列车异常情况及载荷等数据进行有效监测,同时为地面监控中心提供监控数据和监控图像,可直接监测井下现场的安全、稳定状况。

特殊环境嵌入式智能监测平台研究

在野外露天或环境恶劣的监测现场,使用计算机和数据采集卡来实现监测任务是相当危险和不可靠的。针对监测环境中可能存在易燃易爆条件,湿度大,灰尘多,监测场所分散,距离较远等特殊问题,分析了特殊监测环境中的平台选择,讨论了监测平台的通信方式和监测数据的压缩编码标准,提出了建立特殊环境嵌入式智能监测平台的思想,介绍了智能监测平台的设计与实现。

基于DSP的视频图象处理系统实验研究

在DSP视频处理系统实验中,了解DSP的体系结构、熟悉集成开发实验环境是关键.为了掌握常用视频图象处理方法和DSP视频图象处理技术,培养学生的工程应用能力,以实现对学生的分层次培养.本文在认真分析实验内容和实验效果的基础上,提出将实验划分为基础验证型、设计型、综合型和创新型四类,以适应不同层次学习者的需要.

低噪音视频图象采集系统电源设计

视频图象采集系统的电源设计十分重要,如果电源电压的纹波稍大,将严重影响视频A/D芯片的正常工作,分离出的行同步信号也会发生跳变,这些都将使A/D芯片的精度下降,造成图象包含雪花、水印干扰,图象模糊不清。为解决这个问题,介绍一种低噪音的电源方案。实际使用表明:采用新的电源方案使整个系统的稳定性明显提高,且可推广到其它数据采集系统。

基于红外探测技术的嵌入式智能监测平台研究

在实际照度较低的环境中,可见光波段的CCD摄像机获取的图象模糊不清,影响监测精度。而采用散射光小,穿透能力强的红外CCD,则可以显著改善图象质量,从理论上分析了Rayleigh散射,Mie散射,无选择散射对监测的影响,讨论了红外波段CCD的反射系数、透射系数与波长的关系。实验表明:监测采用红外波段可显著提高空间分辨率、穿透性,且能有效抑制光线散射造成的影响。

专线MODEM在远程通信系统中的应用

目前远程视频监控系统已经成为计算机监控系统的重要分支。国内外现有的远程监控系统大多基于光纤,而光纤如果遇到机械冲击、碰撞等都会造成光缆断缆或断芯,光缆断裂后,很难快速修复,且修复设备复杂,普通用户根本无法进行焊接修复,再加上光端机价格较高,这些都限制了光纤远程监控系统的应用和普及。为此,人们找到了价格相对便宜、维护十分简单的极低比特率双绞线解决方案。文中以基于MODEM专线方式的远程视频监控系统为例,介绍经济、实用且具有广播能力的远程网络摄像机系统。

苛刻环境嵌入式智能监测平台研究

在煤矿井下、野外露天或环境恶劣的监测现场,使用计算机和数据采集卡来实现监测任务是相当危险和不可靠的。针对监测环境中可能存在易燃易爆条件、湿度大、灰尘多、监测场所分散、距离较远等特殊问题,分析了苛刻监测环境中的平台选择,讨论了监测平台的通信方式和监测数据的压缩编码标准,提出了建立苛刻环境嵌入式智能监测平台的思想,介绍了智能监测平台的设计与实现。

苛刻环境嵌入式智能监测平台

针对监测环境中可能存在易燃、易爆条件,湿度大,灰尘多,监测场所分散,距离较远等特殊问题,通过对比两种不同环境的特点,分析了两种监测环境的平台选择,讨论了苛刻环境监测平台的通信与编码标准,阐述了建立苛刻环境嵌入式智能监测平台的思想,介绍了智能监测平台的设计与实现.

红外波段矿井监测的分析与探讨

由于井下实际照度很低,采用可见光波段的普通CCD摄像机获取的图像质量直接影响监测系统精度,井下湿度大、粉尘多,普通CCD在这种环境中会很快发生“失明”。而采用散射光小,穿透能力强的红外波段,由于红外CCD正常工作时,其表面温度大约在60～85℃之间,远高于井下环境温度,能克服普通CCD的冷凝缺陷,井下的大量粉尘难附着在其表面,通过研究分析和大量的井下实验发现,井下监测采用红外波段可显著提高空间分辨率、穿透性,且能有效抑制光线散射造成的影响。论证了矿井监测系统采用红外探测的正确性与可行性。

格林定理的形式化及其初步应用

格林定理广泛应用于物理学、流体力学和化学等领域。通常使用传统的计算机仿真和数值计算方法构建基于格林定理的系统模型。然而,由于工具软件可能存在的系统缺陷导致模型出现偏差,从而使任务失败。为解决上述问题,采用基于高阶逻辑的形式化方法,在定理证明器HOL Light中实现了格林定理相关内容的高阶逻辑建模与验证。首先,对梯度、散度等基本概念和性质进行了形式化描述;其次,对格林定理及其性质进行了形式化建模与验证;最后,基于格林定理的形式化模型完成了地下水控制模型的高阶逻辑推导,进而确保系统模型的安全性。