马文辉+郭云川+张会兵

摘要：无干扰是安全信息流的一个重要需求，安全多执行（SME）是实施无干扰的一种重要方式。本文通过实例指出了反应系统中SME模型在并发调度下可能违背运行无干扰特性，分析了导致这种情况的原因，提出了相应的解决方案。

关键词：无干扰；安全多执行；反应系统

中图分类号：TP311.1

文献标识码：A

DOI：10.3969/jissti.1003-6970.2015.06.015

本文著录格式：马文辉，郭云川，张会兵，等，安全多执行机制的无干扰性研究[J].软件，2015，36（6）：83-87

ResearchonFacial-IightingNormalizationMethods

MAWen-hui1，GUOYun_chuan2，ZHANGHui-bing3

[Abstract]：SecureMulti-Execution（SME）isanimportantapproachforenforcingnon-interference，whichisacriticalrequirementinthefieldofsecureinformationflow.Inthispaper，RS-SMEsupportingasynchronousI/O，isanalyzed.TheresultshowsthatRS-SMEviolatesnon-interferencewhenexecutedinaconcurrentenvironment.Thereasonanditscorrespondingsolutionareproposed.

[Keywords]：Non-interference；Securemulti-execution；Reactivesystem

0引言

信息流（InformationFlow）控制通过规定系统中不同客体间的信息流动关系来保证信息的合法流动，同传统方法相比，信息流控制不仅可以约束信息的显式流动，而且可以控制信息的隐式流动（实际上信息流中显式流动为隐式流动的一个实例），从而防止相互影响而带来的非法信息流，在信息安全领域中信息流控制是一种较为基础的方法。信息流控制的目标为：防止攻击者通过分析观测某种（些）操作而导致的系统上下文环境改变来推断信息，其核心技术手段是增加不确定性。如攻击者Bob希望获取Alice的信息，但受访问策略等的约束，Bob不能直接读取Alice的信息，在这种情况下Bob可通过观测Alice的操作对上下文环境的改变来推断Alice相关信息，其防护方法是增加Alice操作的不确定性。

无干扰是保障信息流安全的基本方式，目前有三种基本机制：限制计算[1]、缓解（Mitigation）[2]及安全多执行（SecureMulti-Execution，SME）机制[3]。限制计算是通过对计算进行某种方式的约束（如约束程序语言中的条件及循环语句），从而避免泄露信息；与限制方式不同，缓解方式的基本假设是现实系统中完全避免信息泄露是不可能的，只要信息泄露量（或泄露带宽）在容许范围内即可。在这两种机制中，限制计算提供了无干扰性质，但由于对计算进行了约束，因此其表达能力受到限制；虽然缓解方式未约束计算行为，但其允许信息泄漏，因此，不是真正意义上无干扰。针对这两种方式的不足，2010年研究者提出了一种全新的保障无干扰机制SME[3]，其核心思想是每个安全级主体均调度执行程序，不同安全级执行时保证只能接收同等或低安全级的输入，并在同等安全级输出。该方式的主要优点是任意程序（包括不满足无干扰的程序）均能以无干扰方式执行，同时不改变无干扰程序的行为。

由于SME的内在优点使得研究者围绕SME在安全策略、安全语言及安全实施等方面展开了众多研究，代表性的工作包括：在安全策略方面，针对[3]的全序执行策略，[4]指出该策略只能保障可比较级上的弱无干扰，对于不可比较级不能保障任何无干扰，并提出了格模式执行策略，该策略能够保障可比较标签上的强无干扰及不可比较级上的弱无干扰。在安全语言方面，[5]借鉴SME在动态信息流环境中针对JavaScript引入方面值（FacetedValue），利用单进程模拟高低安全级的多执行，该方法保证最小开销，同时不依赖以前动态方式的阻塞执行，以此获得无干扰性质。在安全实施方面，[6]首次设计了针对Haskell语言的SME库核。[8，9]扩展了概率.时间进程代数，设计时间.概率无干扰的一致性建模方法，并以此为基础给出了度量方法[10，11]给出了面向机密性和完整性的融合模型。

特别地，[7]在轻量级Firefox浏览器中实施了基于反应系统（ReactiveSystem，RS）的SME（称之为RS-SME），并替换和完善了SOP策略（SameOriginPolicy）。同[3，4]的I/O同步执行不同，‘71采用异步SME执行，由于取消了同步等待机制，因此其效率优于[3，4]。虽然[7]证明了多执行机制的无干扰性，但其关注的无干扰只涉及反应系统本身的输入与输出。本文通过分析指出：RS-SME的多执行机制在并发调度下会对运行环境（CPU及内存占用等）带来不可忽视的影响，从而导致违背运行无干扰（我们称之为运行无干扰），分析了出现了这种情况的原因，给出了相应的解决方案。

1RS-SME模型

RS-SME的总体思想如下：系统行为用反应系统来建模，每个反应系统中对每个输入都对应一个（系列）输出，在运行时每个安全级主体均执行反应系统中的相关变迁，其执行过程采用“封套（wrapper）”进行调度，以此保障只接受低于自身安全级的输入，执行相同安全的输出，进而提供无干扰性质，下面介绍与RS-SME相关的概念[7]。

定义.反应系统为五元组（ConsumerState，ProducerState，Input，Output，_÷），其中，ConsumerState为所有消费状态集合，ProducerState为所有生产状态集合，Input和Output分别为输入和输出×字母表。令State=ConsumerStateUProducerState，Act=InputUOutput，_÷[StatexActxState为带状态转移集（为了简洁，后文用带标签方式来表示），其约束为：

（1）对所有的C∈ConsumerState，若C与Q，则a∈Input，且Q∈ProducerState；

（2）对所有的P∈ProducerState，若P3Q，则a∈Output；

（3）对所有C∈ConsumerState及f∈Input，则存在P∈ProducerState使得C～P；

（4）对所有P∈ProducerState及o∈Output，则存在Q∈State使得P与Q。

约束（1）要求：对所有消费状态，如果在该状态接受一个动作之后转移到下一个状态，则该动作一定是一个输入动作，下～个状态一定是生产状态。约束（2）要求：对所有生产状态，如果在该状态接受一个动作之后转移到下一个状态，则该动作一定是一个输出动作。注意：同约束（1）相比，约束（2）中的下一个状态不一定要求是消费状态。约束（3）要求：对所有消费状态和所有输入，一定存在一个生产状态使得在该消费状态接收该输入之后转移到该生产状态。约束（4）要求：对所有生产状态和所有输出，一定存在一个状态（不一定要求是消费状态）使得在该生产状态输出之后转移到某个状态。

给定一个反应系统，其流（stream）定义为，其中，s∈Act。用I和0分别表示输入流和输出流，令Q（I）0表示在Q状态输入流I对应的输出流为0，其形式定义为：

为保障系统无干扰地执行，RS-SME提出了使用“封套”进行调度，封套是一个二元组（R，L），其中，R：￡：Sta，te，为从安全级到反应系统状态的映射，c为安全级集合，R（，）表示在安全级，上子执行的运行状态；三为处于生产状态所有子执行的调度表。若三=≯，（月，三）表示封套处于消费状态，否则处于生产状态。封套的初始状态为（月，咖，其中，对所有的l∈￡，R（，）是原反应系统的初始状态。封套的形式语义如图1所示。

其中，fbf：，4ct_÷￡为从输入、输出到安全级的映射，表示对反应系统的输入或输出的安全级，DROPc和DROPP中的‘表示不可见动作，如，内部动作。Upper：Act_÷2c定义为Upper：Act（a）=（t|t》lbl（a））。LOAD规则通过将低安全级输入自动传输到高安全级，从而阻对同一输出的多次执行。

2安全分析

RS-SME模型提供无干扰的核心规则包括两条：（1）通过LOAD规则保障仅当子程序的运行安全级大于等于输入安全级时，才能接收输入进而转移到后继状态，否则，子程序只能处于原状态；（2）通过DROPc和DROPP规则保障仅当子程序的运行安全级等于输出安全级时才能输出。在单核处理器中，封套只能通过分时复用CPU来执行子执行，在每个时间片内只能运行单个子程序，这使得不能通过区分子程序运行的数量来违反无干扰性。然而，在多核处理器中子程序可以同时运行，这使得可通过运行不同数量的子执行来区分信息，从而违反无干扰性，下面以实例来说明。

例.给定反应系统RSo，如图2所示，其中，ConsumerState={Co，Cl}，ProducerState={P}，Input={ai，a2，a3}，OutPut={b}，初始状态为Co。令Co=令={l1，l2，l3}，，并满足，1≤l2≤l3，lbl定义为f6，（a1）=l1bl，（a2）=f2、f6，（a3）=f3、l6l（6）=l2。

为了便于描述，将图2所示的反应系统RSo拆分为RSl-RS3，分别如图3图5所示，下面对封套的状态进行分析：

（1）依据封套的定义，RSl-RS3的初始状态均为（R，φ），其中，R（，1）=R（，2）=R（，3）=C0；

（2）初始状态下唯一能采用的规则是LOAD规则，依据LOAD规则，不同的输入导致封套的状态（R，L）不同，如下：（2.1）对于RS1，相应的状态迁移为：（2.2）对于RS2，相应的状态迁移为：

（2.3）对于RS3，相应的状态迁移为：，其中，

（3）在（2）中三种封套均处于生产状态，对于每种生产状态，不同的调度策略有不同的调度行为，假设调度策略采用文[4]的顺序策略Sequential-2，即，优先执行最低安全级，且在该执行终止之前不执行其它子执行，下面以RSi为例进行分析：

（3.1）在/l级执行时，由于f6，（6）≠，l，因此唯一能采用的规则为DROPc，此时，为不可见输m，相应的状态迁移为：（R'，l1：：{l2，l3））_÷（R''，{l2，l3））），其中，R''（l1）=C1、R''（l2）=R''（l3）=P.

（3.2）对于（R''，{l2，l3}），由于采用低安全级优先策略，即，l2安全级优先执行，同时由于，6，（6）=l2，因此，唯一能采用的规则为OUTc，输出b，相应的变迁为（R'l2：：{l3}）与（R'''，{l3}），其中，R'''（l1）=R'''（l2）=C1、R'''（l3）=P：

（3.3）对于（R'''，{l3}，由于lbl（b）≠l3，因此唯一能采用的规则为DROPC，此时，为不可见输出，相应的状态迁移为：（R'''，l3：：{}）→（R''''，{}）），其中，R''''（l1）=R''''（l2）=R''''（l3）=C1。

在RS1中，对于输入数据a1（安全级为，，）、输出数据b（安全级为，l2），运行级为l1的子程序可接收al但不能输出数据b；运行级为l2的子程序可接收a，、也能输出数据b；运行级为，，的子程序可接收a1、但不能输出数据b。

类似地，在RS2中，对于输入数据a2（安全级为l2））、输出数据6，运行级为，，的子程序不接收a2、也不能输出数据b；运行级为，l2的子程序接收a2、同时输出数据6；运行级为l3的子程序接收a2、但不能输出数据b。

在RS3中，对于输入数据a3（安全级为l3）、输出数据6，运行级为l1和l2的子程序不接收a3、也不能输出数据b；运行级为，l3的子程序接收a2、但不输出数据b。

从上面的分析可以看出；对于无干扰系统（RSi和RS2），SME不改变执行结果，对于违背无干扰的系统（RS3），在串行执行情况下可以无干扰方式执行。

上面的例子是串行方式中多次执行来保障无干扰，然而，子执行并发调度时可能导致违背无干扰性质。假定在共享内存的多核处理器中，相同处理器内核的安全级相同，不同处理器内核的安全级不同。在这种多执行方式下若采用异步调度策略，由于异步策略不等待其它子程序运行终止，因此，可能导致多个子执行并发运行。子执行并发的数量不同会对程序运行环境造成影响（如耗用不同的内存），这使得即使对于本身满足无干扰性质的程序也可能导致使得并发多执行机制不满足无干扰性质，我们称这种无干扰为运行无干扰，下面进行分析。

如图2所示，在RSo中由于对于任意安全级的输入（ai、a2和a3），总是输出b，即，输出的b不能用来确定具体输入，因此，RSo自身满足无干扰性质。然而在并发执行中对于不同输入相应后继状态可调度执行的子程序数量不同。假设RSo在四核处理器上运行，每个内核命名为corelcore4，其中，core1、core2和core3的安全级分别为l1，l2及l3，即，分别以l1、l2及l3的安全级来执行子执行，core4用作调度封套，即调度core1、core2和core3的执行。当输人a1（a1的安全级为l1）后，依据多执行中异步并发调度策略，core4将调度安全级高于l1的内核处理器执行RSo中P状态下的子执行，即core1、core2和core3将并发执行P状态下的子执行；类似地，当输人a2（a2的安全级为l2，）后，core4调度core2和core3并发执行P状态下的子执行；当输人a3（a3的安全级为l3）后，core4仅调度core3执行P状态下的子执行。若每个子执行占用相同的内存，则输入a1后内存占有量高于输入a2后内存占有量，输人a2后内存占有量高于输入a3后内存占有量，由此，通过观察内存的使用可获得高安全级的执行情况，因此，并发执行时不同输入可能导致子执行的执行数量不同，从而违背无干扰性质。

上述未能保障无干扰性质的根本原因是没有对并发子执行的数量进行约束，这导致安全级输入并发子执行的数量不同，从而可能违背无干扰性质。为了解决这个问题，一种方式是在任意时刻均使得并发子执行的数量相同，并分配相同的内存。当没有更多的子执行需要执行时，则执行空操作使得低安全级不可区分，以此保障无干扰性质。如，在RSo中输入a2后，通过core4，增加一个空子执行并分配相应的内存；输人a3后，通过core4，增加两个空子执行并分配相应的内存，这样使得低安全级不可区分高安全级的输入。

3结论

安全信息流是保障信息不被直接或间接泄露的一项关键需求，无干扰是安全信息流的一个重要指标。本文通过实例指出了RS-SME在并发调度下可能违背运行无干扰，分析了出现了这种情况的原因，指出了相应的解决方案。虽然SME在保障安全执行方面具有重大优势，但是这种安全多执行是非确定的并未考虑概率因素，然而很非确定执行下能保障无干扰，并不意味着在概率执行情况下也能保障无干扰，这使得需要进一步研究概率执行条下如何通过SME机制来保证无干扰。在未来我们将把安全多执行机制应用到复杂系统安全分析[12，13]中。

参考文献

[1]BartheG，RezkT，WarmierM.PreventingTimingLeaksthroughTransactionalBranchingInstructions[C].ElectronicNotesinTheoreticalComputerScience.2006，33—55.

[2]AskarovA，MyersAC，ZhangD.PredictiveBlack-BoxMitigationofTimingChannels[C].ACMConferenceonComputerandCommunicationsSecurity.2010，297-307.

[3]DevrieseD，PiessensF.NoninterferencethroughSecureMulti-Execution[C].IEEESymposiumonSecurityandPrivacy.2010，109-124.

[4]KashyapV，WiedermannB，HardekopfB.Timing-andTermination-SensitiveSecureInformationFlow：ExploringaNewApproach[C].IEEESymposiumonSecurityandPrivacy.2011，413-428.

[5]AustinTH，FlanaganC.MultipleFacetsforDynamicInformationFlow[C].ProceedingsoftheACMSymposiumonPrinciplesofProgrammingLanguages.2012，165-178.

[6]JaskelioffM，RussoA[C].SecureMulti-ExecutioninHaskell.ProceedingsofAndreiErshovInternationalConferenceonPerspectivesofSystemInformatics.2011.

[7]BielovaN，DevrieseD，MassacciF，PiessensF.ReactiveNon-InterferenceforaBrowserModel[C].InternationalConferenceonNetworkandSystemSecurity.2011，97-104.

[8]郭云川，周渊，丁丽，等.基于概率干扰的概率隐蔽通道仿真研究[J].通信学报，2009，30（2）：59-64.

[9]李超，殷丽华，郭云川.基于ptSPA的概率时间信息流安全属性分析[J].计算机研究与发展，2011，48（08）：1370-1380.

[10]SUNDonghong，GUOYunchuan，YINLihu，HUChangzhen.ComparisonofMeasuringInformationLeakageforFullyProbabilisticSystems[J].InternationalJournaloflnnovativeComputingInformationandControl.2012，8（1）：255-268.

[11]郭云川，方滨兴，殷丽华，等.一种面向移动计算的机密性与完整性模型[J].计算机学报，2013，36（7）：1424-1433.

[12]韩丹，郭燕慧，杨义先.复杂信息系统结构脆弱性分析方法研究[J].新型工业化，2012，2（10）：35-41.

[13]江连峰，赵佳宝.复杂事件处理技术及其应用综述[J].软件，2014，35（2）：188-192.