摘要：同时多线程(simultaneous multi-threading,SMT)技术是提升线程级并行度的重要微架构优化技术之一,SMT技术能够在1个物理核上实现2个逻辑核,提升处理器的整体性能.然而,以共享执行端口为代表的SMT环境下特有的时间侧信道安全问题也陆续出现.提出了一种基于动态资源使用策略的SMT环境下执行端口时间侧信道攻击防护方法,基于SMT技术对数据结构资源的不同处理方式设计动态策略调整算法,通过改进处理器端口绑定及调度选择算法以防护SMT环境下执行端口时间侧信道攻击.防护设计实现了端口冲突矩阵、分支过滤器和动态资源使用策略修改器3个组件,该方法在防护有效性上可以达到关闭SMT技术的防护效果且性能开销大大降低,同时硬件开销可控,具有较高的应用价值.

摘要：介绍了一种研究系统特权安全问题的方法.由于其特有的迁移系统安全状态的能力,使得分析及保护系统特权都很困难,因此,传统访问控制研究中所采用的技术无法复制到该领域.在访问控制空间理论下,检查了系统特权的来源问题及其特点,从而将系统规则划分为约束规则与执行规则两类,分别描述授权的限制与效果.进一步对规则逻辑形式进行推导,发现特权操作问的特殊授权关系以及相关属性,并设计了一种快速构造授权推导图的算法.在此基础上,分析隐式授权安全问题可能存在的滥用特权威胁.最后对POSIX(portable operating system interface)标准的权能机制进行形式化描述,计算并构造其授权推导图.对标准设计中存在的滥用威胁提供了对策,有效地实现了与最小特权原则的一致性.

摘要：体系结构设计在软件开发过程中扮演着重要角色.工程中常用图形语言为软件体系结构建模,它们有直观、半形式化的优点;但是语义不够精确,难以对它们表示的模型进行分析,在这方面,形式化方法可与之互补.但在工程使用中仅用形式化语言建模又不太现实,所以如何结合二者之长以提高软件的可靠性已成为工业界和学术界共同关心的问题.提出了双重软件体系结构描述框架XYZ/ADL:支持工程中软件体系结构的基本概念,前端用一般的体系结构框图作为结构描述,用UML活动图、状态图作为抽象行为表示;后端用既可表示系统动态语义又可表示系统静态语义的时序逻辑语言XYZ/E作为一致的语义基础.前端的图形语言便于软件工程师的交流和使用,后端的形式语言是进一步的形式化分析验证的基础.

摘要：安全性和灵活性是各种改进的BLP模型追求的目标.如何在保持安全性的前提下增加BLP模型的灵活性,一直是安全操作系统研究人员研究的重点.安全模型是系统设计的基础,如果在系统中实现了不安全的“安全模型”,其后果是严重的.结合多级安全(MLS)的核心思想,通过实例列举的方式深入分析了两个改进的BLP模型——DBLP(dynamic BLP)和SLCF(security label common framework).尽管这两个模型都提出了在系统运行时动态地调整主体安全级的规则,但是分析表明,它们还是不安全的.在这两个模型的规则控制下,特洛伊木马可以通过显式地读和写操作将高安全等级的信息泄漏给低安全等级的主体,从而违反了多级安全(MLS)策略.研究结果为人们避免选用不安全的模型提供了有意义的理论支持.

摘要：为了满足应用程序的多样化需求,异构多核处理器出现并逐渐进入市场,其中的处理核心(core)具有不同的微架构或者指令集架构(ISA),为应用提供多样化特性支持,比如指令级并行(ILP)、内存级并行(MLP),这些核心协同工作满足整个计算系统的优化目标,比如高性能、低功耗或者良好的能效.然而,目前主流的调度技术主要是针对传统同构处理器架构设计,没有考虑异构硬件能力的差异性.在异构多核处理器环境下,调度技术如何感知硬件的异构特性,为不同类型的应用程序提供更加合适和匹配的硬件资源,这是值得探索的问题.对近年来在该研究领域的成果进行了综述研究,特别是在性能非对称多核处理器架构下,异构调度技术面临的优化目标、分析模型、调度决策和算法评估等主要问题进行了分析和描述,并依次对相关技术进行了系统的总结,最后从软硬件融合的角度对今后的研究工作进行了展望.

摘要：近年来,在移动计算环境中,异构多核处理器已经逐渐成为主流.与传统同构的处理器设计相比,此类异构多核处理器以更低的功耗成本满足设备的计算需求.但是异构环境下CPU核之间的微架构差异,也为操作系统中的一些基本方法提出了新的挑战.面向性能非对称异构多核环境下调度的负载均衡问题,从系统层面提出了一种负载均衡机制S-Bridge,可以减少处理器微架构差异以及任务执行需求差异对传统负载均衡带来的影响.S-Bridge的主要贡献是从系统层提供了通用的、适配异构性的负载均衡相关接口,使任意调度器都能方便地与异构多核处理器系统进行适配.基于CFS和HMP调度器在ARM平台上进行实验,同时在X86平台上进行S-Bridge通用性的验证,结果表明:S-Bridge可以支持不同真实平台和内核版本的快速实现,平均性能提升超过15%,部分情况下可达65%.

摘要：改善单调速率（rate monotonic，简称RM）可调度性判定算法的效率，是过去40年计算机实时臣统设计的重要问题。最近，研究人员把可调度性判定问题扩展到了更一般的优化设计问题，即，如何调节在区间可选择情况下的任务运行时间，使得：（1）系统RM可调度；（2）系统的某个性能（如CPU利用率）达到最优。在已有的求解实时系统RM优化设计问题的方法中，都是先把原问题建模成广义约束优化问题，然后再对广义约束优化问题进行求解，但现有方法的求解速度较慢，任务数较多时不再适用。提出一种求解优化问题的方法——基于树状的线性规划搜（1inear programming search，简称LPS）方法。该方法先将实时系统RM优化设计问题建模成广义约束优化问题，再将其分拆成若干线性规划子问题，然后构造线性规划搜索树，利用剪枝搜索算法求解部分线性规划子问题，最后得到优化解。实验结果表明：LPS方法相比于已有的方法能够节省20％～70％的求解时间，任务数越多，节省时间越多。该研究成果可以与计算机可满足性模定理（satisfiability modulo theories，简称SMT）领域的多个研究热点问题联系起来，并可望改善SMT问题的求解效率。

摘要：进程重放用于程序调试,无法重现系统全部状态,难以分析错误根源.而系统级重放复杂且难于实现,尚无模型分析方法提供理论指导,确保重放执行与记录执行等价.为了使执行重放系统适用于系统调试,建立虚拟机指令执行模型,提出了虚拟机执行重放的定义,给出并证明了成功重放的充分条件.根据该充分条件,设计实现了基于Xen的虚拟机重放系统***讨论了Xen DomU中不确定事件的种类,给出各类事件的重放方法以及时间点的匹配算法.CASMotion成功实现了不确定事件的准确重放,实验结果表明其具有较低的性能损失.

摘要：发现被移动对象频繁造访的热门区域是从轨迹数据库中挖掘运动模式的重要前提,而合理约束热门区域的大小是提高轨迹模式的精确表达能力的关键.研究如何从轨迹数据库找出热门区域及如何限制其大小.定义了带有覆盖范围约束的热门区域,并采用过滤-精炼策略发现热门区域.在过滤阶段,设计了一种基于网格的密集区域发现近似算法以提高发现效率;在精炼阶段,提出了基于趋势和差异性的度量指标,实现了对应区域重构算法及重构参数启发性选择算法,保证了从密集区域中有效提取出符合覆盖范围约束的热门区域.在真实数据集上验证了该工作的有效性.

摘要：基于现有协议自动生成方法无法直接用于公平交换协议,我们对Clark-Jacob方法进行了扩展,针对公平交换协议的设计空间特征,获得公平性判定模型,模型引入通信信道类型编码,并将主体拥有集合和主体信念集合相分离来完成协议生成过程中消息的衍生和目标的判定,指出公平性包含的局部目标和全局目标,利用基于适应度函数的遗传优化算法,对用二进制表示的协议空间进行优化搜索,获得满足目标的协议,并通过实例说明文中方法的可行性.