基于精化的可信执行环境内存隔离机制验证

可信执行环境(trusted execution environment, TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其安全性不能保证,可能造成存储在安全内存中的敏感数据泄露.为验证TEE内存隔离机制的安全性,针对基于ARM TrustZone技术构建的TEE,提出一种基于精化的可信执行环境内存隔离机制安全性验证方法.建立抽象模型和具体模型,并定义两种模型之间的精化关系,在证明精化关系成立和抽象模型满足信息流安全性的前提下,验证具体模型的信息流安全性.具体模型建模了TEE内存隔离机制的关键硬件和软件,包括TrustZone地址空间控制器、MMU和TrustZone monitor等,在定理证明器Isabelle/HOL中,验证了该模型满足无干扰、无泄露、无影响等信息流安全属性.     

Decomposition in Real-Time Safety-Critical Systems

Existing formal techniques for the development of software for use in safety-critical systems do not adequately address non-functional system requirements such as those involving timing. In this paper we describe a formal development method in which specifications may be decomposed into unexceptional programs whilst preserving the functional and timing requirements of the specification. We illustrate the method with a speed monitoring example.     

基于信号稀疏特性和核函数的非线性盲信号分离算法

文章结合核函数,把基于信号稀疏特性的线性盲分离方法应用于非线性混叠情况而给出了一种非线性混叠信号盲分离算法。该算法首先将混叠信号映射到高维核特征空间,其次,在核特征空间中构造一组正交基,通过这组正交基将高维核特征空间的信号映射到这组正交基张成的参数空间中,从而把非线性混叠信号盲分离问题转化为参数空间的线性混叠信号盲分离问题。最后,在参数空间中,应用基于信号稀疏特性的线性盲分离方法对信号进行分离。该算法收敛精度较高,稳定性好。仿真结果表明该算法是有效的,具有良好的分离性能。     

操作系统内核权能访问控制的形式验证

操作系统内核是构建安全攸关系统软件的基础. 任何计算机系统的正确运行都依赖于底层操作系统实现的正确性,因此,对操作系统内核进行形式验证是很迫切的需求.然而,操作系统中存在的多任务并发、数据共享和竞争等行为,给操作系统内核的验证带来很大的挑战.近年来,基于定理证明的方法广泛用于操作系统各功能模块的形式验证,并取得多个成功应用.微内核操作系统权能访问控制模块提供基于权能的细粒度访问控制,旨在防止未经授权的用户访问系统内核资源和服务.在权能访问控制模块实现中,所有任务的权能空间构成多个树结构,同时每个任务权能节点包含多种嵌套的复杂数据结构,以及权能函数中广泛存在的对权能结构的访问、修改、(递归)删除等操作,使得它的形式验证与操作系统其他功能模块相比更加困难.本文将以并发精化程序逻辑CSL-R为基础,通过证明权能应用程序接口函数(API函数)和其抽象规范之间的精化关系,来验证航天嵌入式领域某微内核操作系统权能访问控制的功能正确性.我们首先对权能数据结构进行形式建模,并在此基础上定义全局不变式来保持权能空间的一致性;然后定义反映功能正确性需求的内核函数的前后条件规范和API函数的抽象规范;最终验证了权能API函数C代码实现和抽象规范之间的精化关系.以上所有的定义和验证均在Coq定理证明器中完成.我们在验证过程中发现了实现的错误,并得到了微内核操作系统设计方的确认和修改.     

An Experiment with Reactive Data-flow Tasking in Active Robot Vision

This paper presents an experiment with the synchronous approach to reactive systems programming, and particularly the Signal language, applied to a significant problem in robot vision: active visual reconstruction. This application consists of the specification of a system dealing with various domains such as robot control, computer vision and transitions between different modes of control. It illustrates the adequacy in such domains of Signal, a data flow programming language and environment. The programming environment features tools for formal specification, analysis, consistency checking and code generation. Signal and its language-level extension for task preemption SignalGTi are used at the different levels of the application: data-flow function for the camera motion control (visual servoing), reconstruction method (in parallel to visual servoing, involving the dynamical processes), and reconstruction of complex scenes (with transitions between several robotics tasks). The combination of these levels constitutes a hybrid behavior with (sampled) continuous control and discrete transitions. These techniques are validated experimentally by an implementation on a robotic cell. © 1997 by John Wiley & Sons, Ltd.     

用数据流分析方法检查程序信息流安全

程序信息流安全是信息安全的一个重要研究方向.基于类型的分析虽然是检查程序信息流安全的一种有效方法,但过于保守.本文尝试将传统的数据流分析方法用于程序信息流安全的检查,即利用数据流分析来跟踪程序数据间的安全依赖关系,达到检查程序信息流安全的目的.和基于类型的方法相比,数据流分析方法能更加精确地分析程序,具有更大的宽容性.最后,本文对数据流分析方法的可靠性进行了证明.     

用XML数据岛创建上下文菜单

XML数据岛通过特定的标签把 XML数据直接嵌入到 HTML文档中 ,采用数据岛作为交互手段 ,不仅可以使数据具备一定的语义信息 ,同时还能保持 HTML原有的特色 ,如利用用户端脚本程序实现动态信息交换等。给出了通过 XML的数据岛来快速创建自定义的上下文菜单     

Deriving parallel computations from functional specifications: A seismic example on a hypercube

Three algorithms developed for a seismic model illustrate that, when the target hardware has many processing elements, functional programs can exhibit better performance than programs developed with conventional techniques. This stands in contrast to the widely held belief that functional programs necessarily pay in poor performance for their advantages in conciseness and likelihood of correctness. Two of the algorithms evolved from an analysis of the seismic model with the goal of finding parts of the computation that could proceed in parallel. The first algorithm has a low communication to computation ratio. The second and third algorithms have higher ratios trading communication time for computation time. The third algorithm was derived from a presentation of the input/output relationship of the model expressed as a composition of mathematical functions. This algorithm exhibited substantially better performance than either of the others. The algorithm achieves its good performance by setting up a producer-consumer pipeline between simultaneously operating portions of the computation. This pipeline balances computation and interprocessor communication more effectively than the other two algorithms.     

Linux内核中一种高精度定时器的设计与实现

CGL(Carrier Grade Linux)是由开源组织(OSDL,Open Source Development Lab)发起的、专门针对电信级服务的Lin-ux。CGL在标准Linux的基础上,增加了一组为适应电信运营环境而设计的特性。某些电信应用对实时性有较高要求,普通Linux在实时性方面和电信平台的要求之间还存在一定的差距。为增强系统的软实时能力,CGL要求提供一种精度在0.1毫秒以上高精度定时器(high-resolution timer)。首先介绍Linux内核2.6.x中时钟与定时器的情况,然后详细阐述这种符合POSIX1003.1b API标准的高精度定时器的设计与实现,最后总结该定时器的性能并得出结论。     

XML技术在高速数据访问接口中的应用

IEC61970标准给出了高速数据访问(HSDA)的组件接口规范(CIS),但在数据格式实现上没有给出具体规定,因此,不同厂商自定义数据格式,造成数据格式不统一、各种应用系统之间存在异构性的问题。针对该问题,文章提出了利用可扩展标记语言(XML)技术的解决方案,主要介绍了如何在HSDA中应用XML技术实现统一的数据格式的方法。     

A Case Study on Applying a Tool for Automated System Analysis Based on Modular Specifications Written in TRIO

An effective means for analyzing and reasoning on software systems is to use formal specifications to simulate their execution. The simulation traces can be used for specification testing and reused for functional testing of the system later in the development process. It is widely acknowledged that, to deal with the complexity of industrial-size systems, specifications must be structured into modules providing abstraction mechanisms and clear interfaces. In our past work, we defined and implemented a method for simulating specifications written in the TRIO temporal logic language, and applied it to functional testing of time-critical industrial systems. In the present paper, we report on a case study with a tool that analyzes TRIO specifications by taking advantage of their modular structure, so as to overcome the well-known state-explosion problem and make the proposed method really scalable. We discuss the fundamental operations and the algorithms on which the tool is based. Then, we illustrate its use in a realistic case study, inspired from an industrial application. Finally, we comment on the overall results in terms of usability of the tool and effectiveness of the approach, and we outline future improvements.     

出具证明编译器中代码优化与程序规范转换

出具证明编译器在软件安全研究得到越来越多的关注,是程序验证研究的一个重要方向.但目前关于出具证明编译器的研究主要是在程序逻辑设计和定理自动化证明方面,很少关注编译优化对规范的影响.而编译优化是决定出具证明编译器是否能走向应用的关键因素之一.通过研究数据流优化的基本行为,提出利用数据流分析结果来变换规范的方法,以使原规范的约束准确而充分地施加于优化后的代码,并实现了一个包含多种优化和相应规范转换的编译器原型系统,展示了方法的可行性.     

基于Delphi的多功能电表人机界面的数据处理

Delphi是当今数据库应用软件开发的主流工具,介绍了基于Delphi语言设计的多功能电表的人机界面的数据处理,包括数据的采集和存储.简单概述了Delphi的特点与结构,并详细论述了符合645电能表规约的串口通讯的程序编写和基于Access数据库的数据存储.     

Traffic routing in a computer network

This paper presents a technique for tuning Decnet networks so as to minimize the average end-to-end packet delay for the entire network. It represent an adaptation of theoretical work on network flows to the realistic case of Decnet. Using this technique to configure hypothetical networks, it then discusses the behaviour of the Decnet routing algorithm with respect to network size, topological connectivity and traffic configuration.     

涉密信息网络安全防护问题的研究

随着计算机网络的飞速发展,网络安全已成为国家信息安全战略的重要组成部分,其中涉密信息网络安全防护问题显得格外重要。在物理隔离的条件下建立涉密专网,并借鉴相关网络建设的成功经验,提出制度管理、数据备份和保护、安全审计等多种技术手段,对涉密信息进行更加严密的安全防护,避免涉密信息的泄露。     

基于层次分析的客服中心实时数据流自动监测方法

为了提高客服中心的智能管理和信息调度能力,结合大数据分析方法进行客服中心实时数据监测和自动采集设计。提出一种基于模糊规则特征量挖掘和层次分析聚类的客服中心实时数据流自动监测方法。建立客服中心的网格分布结构模型并进行客服中心实时数据流监测统计特征分析,进行客服中心实时监测数据属性集的向量量化特征分解,对客服中心实时数据采用信息融合和模糊层析性分析方法实现信息融合,进行关联数据自适应特征提取,挖掘客服中心实时监测数据信息流的正相关性特征量。在层次性聚类算法基础上采用自回归分析进行客服中心实时数据流的模糊聚类和信息预测,提高客服中心实时数据监测的准确性,同时降低了客服服务中心数据流监测的风险。仿真结果表明,采用该方法进行客服中心实时数据监测的聚类性较高,预测性较好,能降低数据聚类的误分率,提高了客服中心实时数据监测能力。     

内网安全信息防泄漏系统的开发与实现

主要研究在Windows系统内核模式中开发过滤驱动,以实现文件透明加解密功能并实现了对内网安全中信息防泄漏系统的设计。系统对网络安全域内所有计算机上的重要信息的存储和传输实施访问控制、数据保护和日志记录,提供集中管理控制机制、安全策略生命周期管理方法和审计分析报告,防止内部网络重要信息被泄漏和破坏。     

流数据处理在住房公积金信息数据库中的应用研究

攫取流数据处理在住房公积金信息数据库之中的应用为主要研究对象,旨在对住房公积金信息数据库之中所出现的时间窗口瓶颈加以缓解.