# A Noninterference Model for Mobile OS Information Flow Control and Its Policy Verification

Authors: Zhanhui Yuan; Wenfa Li; Zhi Yang; Lei Sun; Xuehui Du; Hongqi Zhang
Journal: Security and Communication Networks
 (2021)

---

## Abstract

Mobile operating systems such as Android are facing serious security risk. First, they have a large number of users and store a large number of users’ private data, which have become major targets of network attack; second, their openness leads to high security risks; third, their coarse-grained static permission control mechanism leads to a large number of privacy leaks. Recent decentralized information flow control (DIFC) operating systems such as Asbestos, HiStar, and Flume dynamically adjust the label of each process. Asbestos contains inherent covert channels due to this implicit label adjustment. The others close these covert channels through the use of explicit label change, but this impedes communication and increases performance overhead. We present an enhanced implicit label change model (EILCM) for mobile operating systems that can close the known covert channel in these models with implicit label change and supports dynamic constraints on tags for separation of duty. We also formally analyze the reasons why EILCM can close the known covert channels and prove that abstract EILCM systems have the security property of noninterference with declassification by virtue of the model checker tool FDR. We also prove that the problem of EILCM policy verification is NP-complete and propose a backtrack-based search algorithm to solve the problem. Experiments are presented to show that the algorithm is effective.


---

## Body

## 1. Introduction

At present, mobile operating systems have a large number of users and are key targets of network attack. Their privacy security problem is very serious. In 2020, China Internet Security Center intercepted 332000 new malicious app samples related to privacy theft on mobile operating systems and monitored 1.12 billion malicious attacks with an average of 3.06 million attacks per day. The openness of the mobile operating system leads to high security risks. The characteristics of mobile system interacting with the outside from multiple channels make their vulnerabilities easier to be exposed and utilized. The quality and security of apps in online app stores (such as Google play) are uneven, and it is difficult to ensure that there are no Trojans and viruses implanted by hackers. Hackers can steal data by embedding spy programs into normal applications to obtain illegitimate benefits [1]. Mobile operating systems are facing more severe privacy and security challenges than traditional PC operating systems [2–4]. Most mobile systems adopt discretionary access control (DAC) as the security model, but the DAC policy cannot effectively express the information flow control [5], which makes it difficult to effectively prevent Trojan stealing secret data. Mobile operating systems need to implement mandatory access control [6]. The essence of mandatory access control is to prevent information in a secret domain from leaking out of the domain. However, for the mobile operating systems with diversified and dynamic interaction with the outside world, the static isolation and blocking method cannot effectively balance availability and security [7].Decentralized information flow control (DIFC) [8] addresses the weaknesses of earlier approaches to the protection of secrecy and integrity in an operating system containing applications with potential exploits or third-party components [9], even in situations of mutual distrust [7]. DIFC allows processes to control the flow of their information without imposing the rigid constraints of a traditional multilevel security system [10]. DIFC allows programs to craft their own MAC security schemes. Each user has the power to declassify his own data, but declassification does not leak other users’ data. Even if a process is compromised, it will not endanger the data security of others [11]. DIFC has been widely applied to the protection of operating systems [12–18], databases [19], programming languages [6, 20, 21], web applications [22], etc.Asbestos [16], HiStar [17], and Flume [18] are classical DIFC operating systems. Asbestos adopts a “taint-propagation” policy, wherein each process P has two labels, a send label PS and a receive label PR. PS represents the process’s current contamination, while PR represents the maximum contamination it is able to accept from others. P may send to Q if PS is not more than QR, once communication is tainted by P. Qs is the least upper bound on the two send labels.Despite its benefits, the Asbestos design contains inherent covert channels. Consider a contaminated processA attempting to communicate a bit of sensitive information to an uncontaminated process C. An attacker might construct two uncontaminated processes. These processes, B0 and B1, both repeatedly send heartbeat messages to C. If it wants to communicate the value i to C, A will send a message to the Bi. If Bi tries to receive it, it will be contaminated and become a tainted process. If C does not receive a heartbeat message from Bi in the next time slot, it knows that A has sent value i to it. Now C has the sensitive information, copied bit-for-bit from A. There are many deformations of the covert channel, and if this mechanism is used for integrity protection, this covert channel still exists. Such channels are inherent to any system in which a contaminated process can change the labels of a less contaminated process implicitly. Because Asbestos’s event process abstraction makes forking very fast, this channel on Asbestos can leak kilobits of data per second [18].HiStar is a successor system to Asbestos. It avoids these channels by requiring the processes to contaminate themselves.The HiStar thread actively changes its label before reading the contaminated data. Flume later adopted a similar strategy, but within a streamlined label system. However, compared with implicit label changes, explicit label changes mean that the processes become more involved in information flow control, which will result in poor communication if these processes cannot adjust their label in a timely manner. Moreover, this also introduces performance overhead due to the system calls relative to it.This paper presents a model for information flow control at the operating system level, called enhanced implicit label change model (EILCM), to solve the contradiction. This model uses Flume labels and capabilities in terms of their set operations based on type tags, a well-understood formalism to express the dynamic processes isolation which can effectively prevent Trojans and spyware attacks. Our model has the following characteristics: firstly, it allows implicit label change but tries to close the known covert channels; secondly, it solves the contradictions between users’ sharing of common software and authorization constraints for separation of duty or least privilege through mutually exclusive tag constraints; and thirdly, its rule covers more information flow types such as file operation and program execution in addition to inter-process communication (IPC). We do not introduce privilege transfer or delegation of authority, considering that it is difficult for most commercial DIFC programs to predict their future runtime environment or to know in what situation it does or does not transfer privilege. In that case, policy management tasks will be ultimately passed on from the DIFC program to the system administrators and users. In contrast, delegation of authority adds more uncontrollable factors.In order to prove that there are no covert channels in an EILCM system, we adopt an approach similar to that of Krohn et al. [18]. We describe the model specification using the communicating sequential processes (CSP) to clarify the formal semantics of information flow control behaviors of the EILCM system; then we prove that an abstract EILCM system has the security property of noninterference based on CSP formulas. Our methods and that of [18] have the following differences. (1) Our definition of noninterference with declassification uses a standard CSP-oriented specification. Therefore, our proof uses both automated and manual analysis, while Krohn and Tromer’s definition [18] is property-oriented specification, so its proof is completely manual. (2) Our model adopts the centralized control of information flow and captures more information flow types, while the Flume model of [18] adopts distributed control and concentrates on IPC control, resulting in distinct differences in their formal semantics.Another problem studied in this paper is the verification of EILCM policies. Because of the richness and complexity of label management, whether the label configurations completely and consistently express the high-level policies and goals is an important problem to verify. In the traditional one-way information flow model, policy verification is quite simple. However, in some flexible systems to control information flow, such as Vista, Asbestos, Flume, etc., policy verification problems are complex [23, 24] due to their introduction of declassification functions or transfer privilege functions. These functions diffuse the individual policies and obscure their combined effect. Misconfigurations may make processes lose due privileges or obtain unduly privileges via a privilege exploit attack. Policy analysis and verification are especially necessary for the large systems that have hundreds of processes or users and tens of thousands of resources.In sum, the novel contributions of this paper are as follows:(i)
InSection 2, we present an enhanced implicit label change model (EILCM) that can close the known covert channels in the existing implicit label change models for information flow control at the operating system level. Moreover, the EILCM introduces mutually exclusive tag constraints to solve the contradictions between users’ sharing of common software and authorization constraints for separation of duty or least privilege. Based on the ISO general access control framework, we also use the CSP language to describe the formal semantics of information flow control behaviors of EILCM systems, which lays the foundation for noninterference proofs.(ii)
InSection 3, we formally analyze the reason that EILCM can close the known covert channels. Further, through the model checker tool FDR, we prove that an abstract EILCM system has the security property of noninterference with declassification.(iii)
InSection 4, we prove that the problem of EILCM policy verification is an NP-complete problem. This conclusion reflects, to some extent, the computational complexity of the problem of Flume policy verification, due to their partial similarity. We also present a backtrack-based search algorithm to solve the problem. Experiments are presented to show that the algorithm is effective.We discuss related work inSection 5 and conclude in Section 6.


## 2. EILCM Descriptions

### 2.1. Informal Descriptions of EILCM

In an EILCM protection system, letO be the set of all objects (e.g., files) and U be the set of all subjects (e.g., processes). Let DS be the set of secrecy (export) protection tags, with each tag denoting a secrecy domain type. It is with its secrecy level containing the same tag x that a requestor can observe the information in an x-type secrecy domain. Correspondingly, let DI be the set of integrity (import) protection tags, with each tag denoting an integrity domain type. A requestor whose integrity level does not contain the same y cannot alter the information in a y-type integrity domain.Definition 1.
(label). For each object or subjectp∈O∪U, its label Lp is a triple Sp,Ip,Cp, where Lp⊆DS denotes its secrecy level, Ip⊆DI denotes its integrity level, and Cp⊆DS∪DI×+,− denotes its management capability for its own label.
Secrecy levels and integrity levels, respectively, form a lattice under the partial order of the set relation⊆, such that Sp≥Sq if and only if Sp⊇Sq, and Ip≥Iq if and only if Iq⊇Ip. In EILCM, information can flow from low secrecy-level and high integrity-level objects or subjects to high secrecy-level and low integrity-level objects or subjects.
A subjectp with d+∈Cp can add a tag d to its own Sp if d∈DS or to its own Ip if d∈DI, while with d−∈Cs, it can remove d from its own Sp or Ip. Generally speaking, for a secrecy tag d1, an untrustworthy process p with d1+∈Cp and d1−∉Cp can read a secret file f with Sf=d1 by raising its own to Sp∪d1 without the ability to reveal it. If d1−∈Cp, the system conservatively assumes that p has declassification ability and it does not propagate f’s data. If there are multiple tags in Sf, then p requires independent consent for each tag before reading f. Similarly, for a integrity tag d2, a system-level process q with d2−∈Cq and d2+∉Cq can receive network data by reducing its own Iq to Iq−d2; however, once it reads this unsafe data, it loses the ability to modify the system configurations. If d2+∈Cq, the system conservatively assumes q has decontamination ability and it can still modify the system configurations.
The subject’s capability is derived from the properties of the executable object where it was born, which is set by the authority administrator. We defineCo=φ, o∈O, which means that an object cannot change its level itself.
To simplify notation, a subjectp’s “add-tag” capability is given by Cp+=d|d+∈Cp, and its “remove-tag” capability is given by Cp−=d|d−∈Cp. The notation Cp±=d|d+∈Cp∧d−∈Cp represents p’s dual-privilege capability.Definition 2.
(constraints).R⊆2DS∪2DI is a set of mutually exclusive tag constraints with the property that for each d1,d2,…,dm∈R, the secrecy/integrity level X of any object or subject satisfies X∩d1,d2,…,dm<2, which we call “XsatR.”
We introduce mutually exclusive tag constraints to solve the contradictions between users’ sharing of common software and authorization constraints for separation of duty or least privilege.Example 1.
(secrecy/least privilege). Alice and Bob share the word-processing programw to, respectively, edit their private documents with their secrecy levels dsA and dsB. Then, w’s capability should involve dsA+ and dsB+ in order to read these documents. Assume that Alice executes w to generate a new process wA with dsA∈SwA using her shell process, and wA inherits w’s capability. In order to prevent Alice from reading Bob’s document by means of wA, wA should be deprived of dsB+ capability at that time, which means that the process should run with as few privileges as possible. We can solve this problem by defining constraint dsA,dsB∈R.Example 2.
(integrity/separation of duty). General information systems emphasize the separation of powers and do not allow any individual to have sufficient authority within the system to single handedly perpetrate fraud. The normal division of authority is into security management, system configurations, and audit management. Assume these management domains are denoted, respectively, by integrity tags ofdim, dic, and dia, and the domain administrators are used to using same program w to modify their domain information, which requires that w’s capability should contain dim, dic, and dia together. However, we need be assured that when it is created by some domain administrator and derived from w, the new process has no chance of modifying other domain information although it inherits w’s capability. We can solve this problem by defining the constraint dim,dic,dia∈R.
In order to prevent any subject from implicitly bypassing these constraints, EILCM does not entitle any subject to delete those tags that exist inR from its level.
Further, we introduce the relations_sat for Definition 3. Given an object or subject p in an EILCM system, we say ps_satR if and only if ∀r∈R, r∩Cp+∩DS>1⟶r∩Sp=1.
Before defining the information flow rule, we reconsider the example of covert channels mentioned inSection 1. The former models assume that if Bi tries to receive a message from A when A does not send anything, Bi should not be contaminated. However, no transmitting data actually should be regarded as a kind of implicit communication without formal sending and receiving behavior if planned by adversaries. Therefore, in the EILCM, if it can be contaminated within its capability and tries to receive a message from A, Bi will be contaminated automatically whether or not A sends a message to it. In addition, HiStar and Flume introduce the explicit change label method, in which each process must make a decision itself about whether to adjust its level if it wants to communicate with other process successfully. We will formally analyze the reason why these methods can close the known covert channels in Section 3.1. Compared with our method, the explicit change label method increases the process’s interventions, which results in unsmooth communication and introduces overhead for system calls.Definition 3.
(secure information flow and implicit change label). The information flow fromp to q is safe iff(1)Sp−Cp±⊆Sq∪Cq+,Ip∪Cp±⊇Iq−Cq−,qs_satR.
When the flow is finished,q’s level is implicitly changed, that is:(2)Sq←Sq∪Sp−Cp±,Iq←Iq−Iq−Ip∪Cp±.
Definition3 demands that secure information flow is from low secrecy-level and high integrity-level objects or subjects to high secrecy-level and low integrity-level objects or subjects, where both party’s capabilities of adjusting their own level are considered adequate. For different types of concrete operations, its operational semantics are as follows:(i)
Subjectp can receive message from subject q, iff(a)
ps_satR(b)
q exists(c)
Sq−Cq±⊆Sp∪Cp+andIq∪Cq±⊇Ip−Cp−(d)
Sp∪Sq−Cq±satR (e) q has sent message to p.Whenp triggers the related receive system call, p’s level will be adjusted according toIf (a)–(e) hold, then(3)Sp←Sp∪Sq−Cq±,Ip←Ip−Ip−Iq∪Cq±.If (a) holds and (b) or (c) or (d) does not hold, then(4)Sp←Sp∪Cp+∩DS−R,Ip←Ip−Cp−.Otherwise,p’s level will remain unchanged.(ii)
Subjectp can write/delete object q, iff(a)
q exists(b)
Sp−Cp±⊆SqandIp∪Cp±⊇Iq(iii)
Subjectp can read/load object q, iff(a)
ps_satR(b)
q exists(c)
Sq⊆Sp∪Cp+andIq⊇Ip−Cp−(d)
Sp∪SqsatRWhenp triggers the related read/load system call, p’s level will be adjusted according toIf (a)–(d) hold, then(5)Sp←Sp∪Sq,Ip←Ip−Ip−Iq.If (a) holds and (b) or (c) or (d) does not hold, then(6)Sp←Sp∪Cp+∩DS−R,Ip←Ip−Cp−.Otherwise,p’s level will remain unchanged.(iv)
Subjectp can create object q with its secrecy/integrity levels being Sq/Iq, iff(a)
q does not exist(b)
Sp−Cp±⊆SqandIp−Cp−⊇Iq(v)
Subjectp can execute object o, and create a new subject, iff(a)
ps_satR(b)
o exists(c)
So⊆Sp∪Cp+andIo⊇Ip−Cp−(d)
Sp∪SosatR(e)
Sp−Cp±⊆So∪Cq+andIp∪Cp±⊇Io−Cq−,where q is the id that the system allocates for the new subject and q’s capability is derived from the properties of o.
Whenp triggers the execute system call, p’s level will be adjusted according to
If (a)–(e) hold, then(7)Sp←Sp∪So,Ip←Ip−Ip−Io.
If (a) holds and (b) or (c) or (d) or (e) does not hold, then(8)Sp←Sp∪Cp+∩DS−R,Ip←Ip−Cp−.
Otherwise,p’s level will remain unchanged.
Whenq is born, its level will be set according to(9)Sq←Sp−Cp±∪So,Iq←Ip∩Io,and its capability will be set according to(10)Cq+←Cp+∩Co+,Cq−←Cp−∩Co−.
This process can be broken down into the process ofp “reading” o and of p “writing” q. In the former process, p can know, at least, whether o exists. In the latter process, the parameters are the information p directly tells q if p starts q with parameters. Without parameters, p starting q is just the sensitive information that p tells q if only p can start q.Definition 4.
(secure explicit change label). For a subjectp, let X be Sp or Ip and let X′ be the new value that p requests about X. The change from X to X′ is safe if and only if(11)X′−X⊆Cs+,X−X′⊆Cs−,X′satR.
Correspondingly, for an objecto and a subject p, let Y be So or Io and let Y′ be the new value that p requests about Y. The change from Y to Y′ is safe iff(12)X−Cs±⊆Y⊆X∪Cs±,X−Cs±⊆Y′.
The subject can adjust their own level within their capacity. For example, a word-processing process can produce the first confidential documents in the system by raising its own secrecy level, and PGP software can reduce its own secrecy level in order to send the encrypted document. The explicit label change is an effective supplement to implicit label change. Now, the condition of secure information flow can be relaxed and becomesSp−Cp−⊆Sq∪Cq+ and Ip−Cp−⊆Iq∪Cq+.
The requirement for a subject adjusting an object’s level is consistent with that of the subject adjusting its own level and Definition3. In the same condition, a subject p can finish adjusting an object o’s level through the following process: p reads the contents of o ⟶ s writes content to a temp file f ⟶ p deletes o ⟶ p creates o with level being Y′ ⟶ p reads f ⟶ p writes o ⟶ p deletes f. We specify this requirement to simplify the system processes.
Based on the above definition, the next section gives the precise semantics of the model.


### 2.2. Formal Specifications of EILCM

In order to formally analyze the security of EILCM and the known covert channels, we describe EILCM’s formal specifications using communicating sequential processes (CSP) [25]. CSP can capture effectively the required or expected behaviors of a concurrency system or component, and this is suitable for analyzing the security properties of the information flow model [26]. These specifications involve file operation, program execution, inter-process communication, etc. Since they are primary, a real EILCM system might not be constructed from them. For example, the specifications do not capture how to reliably obtain the object label but assume that all object labels have been stored in the object manager; the specifications do not capture the reliable communication but simply make the new message cover the old message that has not be taken away when the message buffer is full; the specifications do not capture the fairness scheduling of processes but permit any interleaving of processes. However, our specification is fundamental. It expresses the essential safety requirements of EILCM and is easy to expand, refine, and adjust in its nonsecurity aspects.Figure1 depicts the composition and control principles of EILCM. We refer to the ISO general access control framework, which isolates access control policy decisions and enforcement to provide flexibility in access control. Our framework mainly consists of Access Control Enforcement Function (AEF), Access Control Decision Function (ADF), and Object Management (OM). Each subject i calls the system service via channel apii, which is captured by AEF. AEF will get a variety of Access Decision Information (ADI) about this system call from OM via the channel qstate and then sends ADI to ADF via the channel qpolicy. Based on ADI and information flow rules, ADF makes a decision and returns it to ADF. Finally, AEF enforces this decision. The AEF and OM constitute the security kernel. The security kernel should be small enough to ensure efficiency and facilitate security analysis.Figure 1
Composition and control principles of EILCM.


#### 2.2.1. User Processes

In general, the user processes access system resources through system calls. There is no direct interaction between them, so we use the interleaving operator to express their relations. The notationUSERi denotes the user process i. The behaviors of all user processes are specified as follows:(13)USERS=|||i:P−1@USERi|||USER_LIVE1,where P denotes the set of all process identifiers and USER_LIVE1 denotes the first process with CUSER_LIVE1=DS∪DI×+,− at the system startup, which can execute any object to create a new process for the startup needs. There is no deriving operator in CSP, but the actual systems usually restrict the maximum size of a process; thus, we can prebuild all the possible user processes. Any processes will be in an idle state before they receive the signal. The signal born makes it transition into the live state, and the exit signal makes it return to the idle state again. The behaviors of a single user process are specified as follows:(14)USERi=borni?msg⟶USER_LIVEi.In the live state,USERi can issue a system call:(15)USER_LIVEi=SENDi|RECVi|WRITEi|READi|CREATEi|DELi|EXECi|EXITi|CHANGELABELi.The subprocessSENDi describes sending a message msg to user process USERto:(16)SENDi=apii!send,to,msg…⟶USER_LIVEi.The subprocessRECVi describes receiving a message from USERfrom, where msg is the receive buffer and result=ok,error returns the success/failure result of this system call.(17)RECVi=apii!recv,from⟶apii?result,msg..⟶USER_LIVE.The subprocessEXECi describes executing an object which, where OM allocates randomly the PID of the new process.(18)EXECi=apii!exec,which,msg⟶USER_LIVEi.The subprocessEXITi describes process’s state transition from live to idle.(19)EXITi=apii!exit⟶USERi.The subprocessesWRITEi, READi, CREATEi, DELi, and CHANGELABELi have similar behaviors, and we omit the description of their behaviors.


#### 2.2.2. AEF

AEF receives and processes concurrently system calls from different users, each subprocess AEF_ITEMi listening to the corresponding USERi’s calls via channel apii and controlling access to the system. The process SYN_SO guarantees the state consistency of the security kernel when more than two system calls involve the same subject or object simultaneously.(20)AEF=|||i:P@AEF_ITEMi||aSYNSYN_SO.Each system call gets its own dedicated subprocess, andAEF_ITEMi consists of these subprocesses through the choice operator.(21)AEF_ITEMi=AEF_SENDi|AEF_RECVi|AEF_EXECi|.......The processSYN implements the “mutex” lock by virtue of the parallel operator in order to serialize the access to the same subject or object. In order to prevent deadlock in locking the multiple subject or object involved in a system call, the priority of locking is set by subject first, and from small id to large id.(22)SYN=SYN_S|||SYN_O.The alphabet of processSYN is aSYN=enterS,leaveS,enterO,leaveO.The subject-access-synchronism process isSYN_S=|||i:P@SYN_Si, where SYN_Si=enterS.i⟶leaveS.i⟶SYN_Si.Similarly, the object-access-synchronism process isSYN_O=|||i:O@SYN_Oi, where SYN_Oj=enterO.jj⟶leaveO.j⟶SYN_O, and O is the set of all possible object ids.We set the buffer to cache and forward the messages in process communication. IfUSERi wants to send msg to USERj, AEF_SENDi will first set the msg level in terms of the current level of USERi and store it in the message slot BUFF_2i,j,full,msg, whose specifications are given in the following descriptions of OM. Subsequently, if USERj tries to obtain themsg, AEF_RECVj will collect the related ADI and send it to ADF for control policy. Only when a request is permitted by ADF, AEF_RECVj will return msg to USERj. Moreover, AEF_RECVj might adjust USERi’s level in terms of AEF’s requirements.(23)AEF_SENDi=apii?send,j,msg⟶ifi==jthen AEF_ITEMielse enterS.i⟶qstateSi.getlabel?Si,Ii,Ci,existi,s_sati⟶qstatei,j.buf_.in!msg,Si−Ci±,Ii∪Ci±⟶leaveS.i⟶AEF_ITEMiAEF_RECVi=apii?recv,j⟶ifi==jthenapii!error,null⟶AEF_ITEMielse locki,j⟶qstateSi.getlabel?Si,Ii,Ci,existi⟶AEF_ITEMielse locki,j⟶qstateSi.getlabel?Si,Ii,Ci,existi⟶qstatej,i.buff_test?full,Sj,Ij⟶qstateSj.getlabel?Sj′,Ij′,Cj,existj⟶qpolicyi!irecv,Si,Ii,Ci,full,Sj,Ij,existj,Sj′,Ij′⟶qpolicyi?policy,Sj′,Ij′,renew⟶if policy==accept thenqstatej,i.buff_out?msg⟶apii!ok,msg⟶if renew thenqstateSi.setlabel!Si′,Ii′,Ci,1⟶unlocki,j⟶AEF_ITEMielse unlocki,j⟶AEF_ITEMielseapii!error,empty⟶if renew thenqstateSi.setlabel!Si′,Ii′,Ci,1⟶unlocki,j⟶AEF_ITEMielse unlocki,j⟶AEF_ITEMi,where locki,j=enterS.mini,j⟶enterS.maxi,j and unlocki,j = leaveS.mini,j⟶leaveS.maxi,j.WhenUSERi has permission to access object j, AEF expresses the related object operation using the event in channel io, e.g.,(24)AEF_WRITEi=……⟶if policy==accept then io!writefile,j,msg⟶…….IfUSERi requests creating a new subject, AEF will first request the new pid from OM and OM will select the new pid randomly from the set of available process identifiers. Then AEF will adjust the levels of USERi and USERnewid and give off the born signal to activate the process USERnewid.(25)AEF_EXECi=apii?exec,j,msg⟶enterO.j⟶enterS.i⟶qstateSi.getlabel?Si,Ii,Ci,existi⟶qstateOj.getlabel?Sj,Ij,Cj,existj⟶qpolicyi!iexec,Si,Ii,Ci,Sj,Ij,Cj,existj⟶qpolicyi?policy,Si′,Ii′,Sj′,Ij′,Cj′,renew⟶if¬renew thenEXEC_RETi,j,errorelseqstateSi.setlabel!Si′,Ii′,Ci,1⟶ifpolicy==accept thenqstatePID.getpid⟶qstatePID.choose?result.newid⟶ifresult thenqstateSnewid.setlabel?Sj′,Ij′,Cj′,1⟶bornnewid!msg⟶EXEC_RETi,j,okelse EXEC_RETi,j,errorelse EXEC_RETi,j,error,where EXEC_RETi,j,result=leaveS.i⟶leaveO.j⟶AEF_ITEMi.When a subject exits,AEF will clear its label information in OM and update the set of available subject identifiers. In addition, it clears its send buffer.(26)AEF_EXITi=apii?exit⟶enterS.i⟶RM_eEXITi,PRM_eEXITfrom,to=if to==0then⟶qstateSi.setlabel!,,,0⟶qstatePID.delpid!i⟶leaveS.from⟶RM_ITEMfromelsebufffrom,to.out?msg⟶RM_eEXITfrom,to−1.The system calls for changing level are mainly used to update the label information inOM.


#### 2.2.3. OM

The processOM manages the system states information, i.e., the labels and existence of all the subjects and objects, the set of available process identifiers, and the messages in process communication.We have introduced its subprocesses one by one.OM_S_LIVEpid,s,i,c,exist provides the query and modification service for the label and existence of all the subjects, where pid denotes the process id, s, i, and c, respectively, denote USERpid’s secrecy level, integrity level, and capabilities, and exist denotes whether the subject exists.(27)OM_S_LIVEpid,s,i,c,exist=qstateSpid.getlabel!s,i,c,exist⟶OM_S_LIVEpid,s,i,c,exist|qstateSpid.setlabel?s′,i′,c′,exist′⟶OM_S_LIVEpid,s′,i′,c′,exist′,s_sat.OM_S is an interleaving of all the OM_S_LIVEpid,s,i,c,exist. We assume that the USER1 with C1=DS∪DI×+,− is the only live user process at system startup. Therefore, we can set up any initial state of the system, for any type of process and object can be created by USER1.(28)OM_S=|||pid:P−1@OM_S_LIVEpid,,,,0|||OM_S_LIVE1,,,DS∪DI×+,−,1.Similarly,OM_O_LIVEoid,s,i,c,exist,exe provides the query and set service about the label and existence of all the objects, and OM_O is an interleaving of all the OM_O_LIVEoid,s,i,c,exist. The “capability” attributes of the object are set by authority administrator, and we model it as a random event in the channel nonce.SIC.(29)OM_O_LIVEoid,s,i,c,exist=qstateOoid.getlabel!s,i,c,exist⟶OM_O_LIVEoid,s,i,c,exist|qstateOoid.setlabel?s′,i′,c′,exist′⟶OM_O_LIVEoid,s′,i′,c′,exist′OM_O=|||oid:O@nonce.SIC?s,i,c,exist⟶OM_O_LIVEoid,s,i,c,exist.OM_ID_MGR provides the management of available process identifiers via channel qstatePID, which allocates a new id when a new process is created and reclaims the id when a process exits. In our specifications, access to channel qstatePID is mutually exclusive.(30)OM_ID_MGRoccupy,free=qstatePIDgetpidi⟶if emptyfreethenqstatePID.choose!1,0⟶OM_ID_MGRoccupy,freeelse nonce.Pid?i:free⟶qstatePID.choose!0,i⟶OM_ID_MGRoccupy∪i,free−i|qstatePID.delpid?i⟶OM_ID_MGRoccupy−i,free∪i.BUFF describes the behaviors of the message buffer in process communication, which caches and forwards the message. For simplicity, a message slot is set for each pair of sender and receiver.The processOM_BUFF specifies the behavior of the process communication buffers.(31)OM_BUFF=|||from:P@BUFF_1from,BUFF_1from=|||to:P@BUFF_2from,to,0,msg,,.The message slot provides the storage and removal of information. We specify simply that the new message will cover the old message that has not been taken away when the message buffer is full. The stored information also includes the current level of the sender. Its transition is as follows:(32)BUFF_2from,to,full,msg,S,I=qstatefrom,to.buff_in?msg′,S′,I′⟶BUFF_2from,to,1,msg′,S′,I′|qstatefrom,to.buff_out!msg⟶BUFF_2from,to,0,null,,|qstatefrom,to.buff_test!full,S,I⟶BUFF_2from,to,full,msg,S,I.Finally, the OM is an interleaving of these service subprocesses:(33)OM=OM_S|||OM_O|||OM_ID_MGR1,P−1|||OM_BUFF.


#### 2.2.4. ADF

ADF also concurrently deals with the request of each of the subprocesses of AEF. According to the ADI and the rules, ADF returns its decision and requirements for state transition. Its behaviors are specified as follows:(34)ADF=|||i:P@ADF_ITEMi|||ADF_SATR,pidwhere ADF_ITEMi=ADF_RECVi|ADF_WRITEi|ADF_READi|….The process communication is controlled when the receiver tries to receive the message. For the request ofapii.recv,j, SS_RECVi will determine whether to permit it and develop the policy of adjusting the USERi’s level in terms of Definition 3. Since the system will clear the corresponding buffer when any subject exits, the message existing in the buffer must be fresh to guarantee the data consistency.(35)ADF_RECVi=qpolicyi?irecv,Si,Ii,Ci,full,Sj,Ij,existj,Sj′,Ij′⟶constratinSSATiquery!Si,Ci⟶constrainSSATpidquery?s_sati⟶if¬s_satithenqpolicyi!reject,,,0⟶ADF_ITEMielseconstratinSATiquery!Si∪Sj,,Ci⟶constrainSSATpidquery?sati⟶ifexistj∧Sj⊆Si∪Ci+∧Ij⊆Ii−Ci−∧sati∧full thenqpolicyi!accept,Si∪Sj,Ii−Ii−Ij,1⟶ADF_ITEMielse ifexistj∧¬full∧Sj′⊆Si∪Ci+∧Ij′⊆Ii−Ci−∧satithenqpolicyi!reject,Si∪Sj,Ii−Ii−Ij,1⟶ADF_ITEMielseqpolicyi!reject,Si∪Ci+∩DS−R,Ii−Ci−,1⟶ADF_ITEMi.The decision process for a request to read/write/create/delete/execute an object is similar toADF_RECVi mentioned above. The “capability” attributes of new object are set by authority administrator, and we model it as a random event in the channel nonce.C. We omit the unnecessary details.(36)ADF_CREATEi=qstatei?icreate,j,Sj,Ij⟶…⟶nonceC?Cj⟶…qstatei!Sj,Ij,Cj.ADF_SATR,pid stores the mutually exclusive tag constraints R and provides the service to verify whether a given label is sat or s_satR.(37)ADF_SATR,pid=constrainSAT pid.query?s,i,c⟶SATR,pid,s,i,c|constrainSSAT pid.query?s,c⟶SSATR,pid,s,cSATremain,pid,s,i,c=if emptyremainthenconstrainSAT pid.query!true⟶ADF_SATR,pidelse ifheadremain∩s>1∨headremain∩i>1thenconstrainSAT pid.query!false⟶ADF_SATR,pidelseSATtailremain,pid,s,i,cSSATremain,pid,s,c=if emptyremainthenconstrainSSAT pid.query!true⟶ADF_SATR,pidelse ifheadremain∩c+∩DS>1∧headremain∩s=0thenconstrainSSAT pid.query!false⟶ADF_SATR,pidelseSSATtailremain,pid,s,c.


#### 2.2.5. Abstract EILCM System

Based on the components above, the security kernel can be described as the concurrent implementation ofAEF, OM, and ADF.(38)KERNEL=AEFOMqstate‖qpolicyADF.The overall system is the concurrent implementation of security kernel and user processes.(39)SYSTEMEILCM=USERKERNELapiaKERNEL,where aKERNEL=qstate,qpolicy,nonce,io,aSYN,....We use the hide operator inSYSTEMEILCM to hide the inner transitions, e.g., the communication between AEF and ADF. In fact, the inner implementation of the system is a black box to user, and the user can at most see other user’s behaviors, other than the inner traces [18].


### 2.3. Application of EILCM

The application case is a desktop system, as shown in Figure2. Typically, the system includes an instant messaging tool IM, a map navigation software MN, a data encryption and transmission software EMail, an antivirus tool Killer, a web browser UC, and a Shell Explorer.Figure 2
A typical application scenario of a desktop operating system.The user’s chat information is stored inIM data. The daily operations of a user include communicating with contacts via IM, sending encrypted important IM files or MN data to his/her colleagues via EMail, and assisting driving via MN. The important configuration information of this system is stored in OS config file. Killer can detect and kill viruses, but it needs to update its own virus database online regularly. The security requirements of this system are as follows:(1)
IM and MN are untrusted. They are forbidden to read each other’s data.(2)
Killer is allowed to readIM data, MN data, and OS config file in order to detect and kill potential viruses in time. However, it is forbidden to disclose these private data when updating the virus database.(3)
Secret IM data and MN data can be encrypted and sent out byEMail. Since a program can make an aggregation analysis of IM data and MN data and thus obtain more privacy information of users, the system requires privilege constraint about simultaneous reading of IM data and MN data.(4)
Explorer can no longer modify OS config files after it loads the insecure libraries that are downloaded from network by UC.(5)
The updated OS packages that are downloaded from network byUC cannot modify the configuration files unless they have been already checked by Killer.(6)
IM sets the label of IM data. MN sets the label of MN data.The label and capability scheme for building EILCM is as follows. In order to protect the secrecy of IM data and MN data, secrecy tagsdsIM and dsMN are created, respectively, to track and control the propagation flow of these secret information. In order to protect the important data integrity of the operating system, an integrity label diOS is established. The network is considered to have the lowest integrity level and secrecy level. Establish secrecy/least privilege rule: {dsMN, dsIM} ε R. The initial settings of each label are shown in Table 1.Table 1
Setting of initial labels and capabilities of subject and object by EILCM system.
SubjectsSecrecy labelIntegrity labelCapabilitiesObjectsSecrecy labelIntegrity labelIMdiIMdsIM±IM datadsIMMNdsMN±MN datadsMNEmaildsIM±,dsMN±ETP dataKillerdsIM+,dsMN+,dios±OS config filesdiosUCdios−Download dataExplorerdios−OS Updated packagesdiosIn Table1, since IM process is the owner of IM data, and its ability is set to dsIM±, indicating that it can manage these data. Similarly, the ability of MN process is set to dsMN±. The ability of EMail process is set to dsIM±,dsMN±, so that it can read IM and MN data and encrypt them before sending. The ability of Killer is set to dsIM+,dsMN+,dios±, which means that it can read any secret information, but it does not have the ability to release secret information to network. Killer can lower the integrity level to scan any entity or add diOS tags to itself or the data that are considered safe after scanning. The ability of UC process and Explorer process is set to dios−. They are not given the ability to add integrity tag diOS, so they cannot destroy the integrity of system data even if they are infected. It can be seen that EILCM system can better meet these security requirements. At the same time, because it belongs to the taint propagation model and supports the implicit change of tags, the system can reasonably automatically adjust the subject and object tags according to the access requirements. In addition, it also supports the explicit change of labels, which makes the system more flexible and improves the availability.


## 2.1. Informal Descriptions of EILCM

In an EILCM protection system, letO be the set of all objects (e.g., files) and U be the set of all subjects (e.g., processes). Let DS be the set of secrecy (export) protection tags, with each tag denoting a secrecy domain type. It is with its secrecy level containing the same tag x that a requestor can observe the information in an x-type secrecy domain. Correspondingly, let DI be the set of integrity (import) protection tags, with each tag denoting an integrity domain type. A requestor whose integrity level does not contain the same y cannot alter the information in a y-type integrity domain.Definition 1.
(label). For each object or subjectp∈O∪U, its label Lp is a triple Sp,Ip,Cp, where Lp⊆DS denotes its secrecy level, Ip⊆DI denotes its integrity level, and Cp⊆DS∪DI×+,− denotes its management capability for its own label.
Secrecy levels and integrity levels, respectively, form a lattice under the partial order of the set relation⊆, such that Sp≥Sq if and only if Sp⊇Sq, and Ip≥Iq if and only if Iq⊇Ip. In EILCM, information can flow from low secrecy-level and high integrity-level objects or subjects to high secrecy-level and low integrity-level objects or subjects.
A subjectp with d+∈Cp can add a tag d to its own Sp if d∈DS or to its own Ip if d∈DI, while with d−∈Cs, it can remove d from its own Sp or Ip. Generally speaking, for a secrecy tag d1, an untrustworthy process p with d1+∈Cp and d1−∉Cp can read a secret file f with Sf=d1 by raising its own to Sp∪d1 without the ability to reveal it. If d1−∈Cp, the system conservatively assumes that p has declassification ability and it does not propagate f’s data. If there are multiple tags in Sf, then p requires independent consent for each tag before reading f. Similarly, for a integrity tag d2, a system-level process q with d2−∈Cq and d2+∉Cq can receive network data by reducing its own Iq to Iq−d2; however, once it reads this unsafe data, it loses the ability to modify the system configurations. If d2+∈Cq, the system conservatively assumes q has decontamination ability and it can still modify the system configurations.
The subject’s capability is derived from the properties of the executable object where it was born, which is set by the authority administrator. We defineCo=φ, o∈O, which means that an object cannot change its level itself.
To simplify notation, a subjectp’s “add-tag” capability is given by Cp+=d|d+∈Cp, and its “remove-tag” capability is given by Cp−=d|d−∈Cp. The notation Cp±=d|d+∈Cp∧d−∈Cp represents p’s dual-privilege capability.Definition 2.
(constraints).R⊆2DS∪2DI is a set of mutually exclusive tag constraints with the property that for each d1,d2,…,dm∈R, the secrecy/integrity level X of any object or subject satisfies X∩d1,d2,…,dm<2, which we call “XsatR.”
We introduce mutually exclusive tag constraints to solve the contradictions between users’ sharing of common software and authorization constraints for separation of duty or least privilege.Example 1.
(secrecy/least privilege). Alice and Bob share the word-processing programw to, respectively, edit their private documents with their secrecy levels dsA and dsB. Then, w’s capability should involve dsA+ and dsB+ in order to read these documents. Assume that Alice executes w to generate a new process wA with dsA∈SwA using her shell process, and wA inherits w’s capability. In order to prevent Alice from reading Bob’s document by means of wA, wA should be deprived of dsB+ capability at that time, which means that the process should run with as few privileges as possible. We can solve this problem by defining constraint dsA,dsB∈R.Example 2.
(integrity/separation of duty). General information systems emphasize the separation of powers and do not allow any individual to have sufficient authority within the system to single handedly perpetrate fraud. The normal division of authority is into security management, system configurations, and audit management. Assume these management domains are denoted, respectively, by integrity tags ofdim, dic, and dia, and the domain administrators are used to using same program w to modify their domain information, which requires that w’s capability should contain dim, dic, and dia together. However, we need be assured that when it is created by some domain administrator and derived from w, the new process has no chance of modifying other domain information although it inherits w’s capability. We can solve this problem by defining the constraint dim,dic,dia∈R.
In order to prevent any subject from implicitly bypassing these constraints, EILCM does not entitle any subject to delete those tags that exist inR from its level.
Further, we introduce the relations_sat for Definition 3. Given an object or subject p in an EILCM system, we say ps_satR if and only if ∀r∈R, r∩Cp+∩DS>1⟶r∩Sp=1.
Before defining the information flow rule, we reconsider the example of covert channels mentioned inSection 1. The former models assume that if Bi tries to receive a message from A when A does not send anything, Bi should not be contaminated. However, no transmitting data actually should be regarded as a kind of implicit communication without formal sending and receiving behavior if planned by adversaries. Therefore, in the EILCM, if it can be contaminated within its capability and tries to receive a message from A, Bi will be contaminated automatically whether or not A sends a message to it. In addition, HiStar and Flume introduce the explicit change label method, in which each process must make a decision itself about whether to adjust its level if it wants to communicate with other process successfully. We will formally analyze the reason why these methods can close the known covert channels in Section 3.1. Compared with our method, the explicit change label method increases the process’s interventions, which results in unsmooth communication and introduces overhead for system calls.Definition 3.
(secure information flow and implicit change label). The information flow fromp to q is safe iff(1)Sp−Cp±⊆Sq∪Cq+,Ip∪Cp±⊇Iq−Cq−,qs_satR.
When the flow is finished,q’s level is implicitly changed, that is:(2)Sq←Sq∪Sp−Cp±,Iq←Iq−Iq−Ip∪Cp±.
Definition3 demands that secure information flow is from low secrecy-level and high integrity-level objects or subjects to high secrecy-level and low integrity-level objects or subjects, where both party’s capabilities of adjusting their own level are considered adequate. For different types of concrete operations, its operational semantics are as follows:(i)
Subjectp can receive message from subject q, iff(a)
ps_satR(b)
q exists(c)
Sq−Cq±⊆Sp∪Cp+andIq∪Cq±⊇Ip−Cp−(d)
Sp∪Sq−Cq±satR (e) q has sent message to p.Whenp triggers the related receive system call, p’s level will be adjusted according toIf (a)–(e) hold, then(3)Sp←Sp∪Sq−Cq±,Ip←Ip−Ip−Iq∪Cq±.If (a) holds and (b) or (c) or (d) does not hold, then(4)Sp←Sp∪Cp+∩DS−R,Ip←Ip−Cp−.Otherwise,p’s level will remain unchanged.(ii)
Subjectp can write/delete object q, iff(a)
q exists(b)
Sp−Cp±⊆SqandIp∪Cp±⊇Iq(iii)
Subjectp can read/load object q, iff(a)
ps_satR(b)
q exists(c)
Sq⊆Sp∪Cp+andIq⊇Ip−Cp−(d)
Sp∪SqsatRWhenp triggers the related read/load system call, p’s level will be adjusted according toIf (a)–(d) hold, then(5)Sp←Sp∪Sq,Ip←Ip−Ip−Iq.If (a) holds and (b) or (c) or (d) does not hold, then(6)Sp←Sp∪Cp+∩DS−R,Ip←Ip−Cp−.Otherwise,p’s level will remain unchanged.(iv)
Subjectp can create object q with its secrecy/integrity levels being Sq/Iq, iff(a)
q does not exist(b)
Sp−Cp±⊆SqandIp−Cp−⊇Iq(v)
Subjectp can execute object o, and create a new subject, iff(a)
ps_satR(b)
o exists(c)
So⊆Sp∪Cp+andIo⊇Ip−Cp−(d)
Sp∪SosatR(e)
Sp−Cp±⊆So∪Cq+andIp∪Cp±⊇Io−Cq−,where q is the id that the system allocates for the new subject and q’s capability is derived from the properties of o.
Whenp triggers the execute system call, p’s level will be adjusted according to
If (a)–(e) hold, then(7)Sp←Sp∪So,Ip←Ip−Ip−Io.
If (a) holds and (b) or (c) or (d) or (e) does not hold, then(8)Sp←Sp∪Cp+∩DS−R,Ip←Ip−Cp−.
Otherwise,p’s level will remain unchanged.
Whenq is born, its level will be set according to(9)Sq←Sp−Cp±∪So,Iq←Ip∩Io,and its capability will be set according to(10)Cq+←Cp+∩Co+,Cq−←Cp−∩Co−.
This process can be broken down into the process ofp “reading” o and of p “writing” q. In the former process, p can know, at least, whether o exists. In the latter process, the parameters are the information p directly tells q if p starts q with parameters. Without parameters, p starting q is just the sensitive information that p tells q if only p can start q.Definition 4.
(secure explicit change label). For a subjectp, let X be Sp or Ip and let X′ be the new value that p requests about X. The change from X to X′ is safe if and only if(11)X′−X⊆Cs+,X−X′⊆Cs−,X′satR.
Correspondingly, for an objecto and a subject p, let Y be So or Io and let Y′ be the new value that p requests about Y. The change from Y to Y′ is safe iff(12)X−Cs±⊆Y⊆X∪Cs±,X−Cs±⊆Y′.
The subject can adjust their own level within their capacity. For example, a word-processing process can produce the first confidential documents in the system by raising its own secrecy level, and PGP software can reduce its own secrecy level in order to send the encrypted document. The explicit label change is an effective supplement to implicit label change. Now, the condition of secure information flow can be relaxed and becomesSp−Cp−⊆Sq∪Cq+ and Ip−Cp−⊆Iq∪Cq+.
The requirement for a subject adjusting an object’s level is consistent with that of the subject adjusting its own level and Definition3. In the same condition, a subject p can finish adjusting an object o’s level through the following process: p reads the contents of o ⟶ s writes content to a temp file f ⟶ p deletes o ⟶ p creates o with level being Y′ ⟶ p reads f ⟶ p writes o ⟶ p deletes f. We specify this requirement to simplify the system processes.
Based on the above definition, the next section gives the precise semantics of the model.


## 2.2. Formal Specifications of EILCM

In order to formally analyze the security of EILCM and the known covert channels, we describe EILCM’s formal specifications using communicating sequential processes (CSP) [25]. CSP can capture effectively the required or expected behaviors of a concurrency system or component, and this is suitable for analyzing the security properties of the information flow model [26]. These specifications involve file operation, program execution, inter-process communication, etc. Since they are primary, a real EILCM system might not be constructed from them. For example, the specifications do not capture how to reliably obtain the object label but assume that all object labels have been stored in the object manager; the specifications do not capture the reliable communication but simply make the new message cover the old message that has not be taken away when the message buffer is full; the specifications do not capture the fairness scheduling of processes but permit any interleaving of processes. However, our specification is fundamental. It expresses the essential safety requirements of EILCM and is easy to expand, refine, and adjust in its nonsecurity aspects.Figure1 depicts the composition and control principles of EILCM. We refer to the ISO general access control framework, which isolates access control policy decisions and enforcement to provide flexibility in access control. Our framework mainly consists of Access Control Enforcement Function (AEF), Access Control Decision Function (ADF), and Object Management (OM). Each subject i calls the system service via channel apii, which is captured by AEF. AEF will get a variety of Access Decision Information (ADI) about this system call from OM via the channel qstate and then sends ADI to ADF via the channel qpolicy. Based on ADI and information flow rules, ADF makes a decision and returns it to ADF. Finally, AEF enforces this decision. The AEF and OM constitute the security kernel. The security kernel should be small enough to ensure efficiency and facilitate security analysis.Figure 1
Composition and control principles of EILCM.


### 2.2.1. User Processes

In general, the user processes access system resources through system calls. There is no direct interaction between them, so we use the interleaving operator to express their relations. The notationUSERi denotes the user process i. The behaviors of all user processes are specified as follows:(13)USERS=|||i:P−1@USERi|||USER_LIVE1,where P denotes the set of all process identifiers and USER_LIVE1 denotes the first process with CUSER_LIVE1=DS∪DI×+,− at the system startup, which can execute any object to create a new process for the startup needs. There is no deriving operator in CSP, but the actual systems usually restrict the maximum size of a process; thus, we can prebuild all the possible user processes. Any processes will be in an idle state before they receive the signal. The signal born makes it transition into the live state, and the exit signal makes it return to the idle state again. The behaviors of a single user process are specified as follows:(14)USERi=borni?msg⟶USER_LIVEi.In the live state,USERi can issue a system call:(15)USER_LIVEi=SENDi|RECVi|WRITEi|READi|CREATEi|DELi|EXECi|EXITi|CHANGELABELi.The subprocessSENDi describes sending a message msg to user process USERto:(16)SENDi=apii!send,to,msg…⟶USER_LIVEi.The subprocessRECVi describes receiving a message from USERfrom, where msg is the receive buffer and result=ok,error returns the success/failure result of this system call.(17)RECVi=apii!recv,from⟶apii?result,msg..⟶USER_LIVE.The subprocessEXECi describes executing an object which, where OM allocates randomly the PID of the new process.(18)EXECi=apii!exec,which,msg⟶USER_LIVEi.The subprocessEXITi describes process’s state transition from live to idle.(19)EXITi=apii!exit⟶USERi.The subprocessesWRITEi, READi, CREATEi, DELi, and CHANGELABELi have similar behaviors, and we omit the description of their behaviors.


### 2.2.2. AEF

AEF receives and processes concurrently system calls from different users, each subprocess AEF_ITEMi listening to the corresponding USERi’s calls via channel apii and controlling access to the system. The process SYN_SO guarantees the state consistency of the security kernel when more than two system calls involve the same subject or object simultaneously.(20)AEF=|||i:P@AEF_ITEMi||aSYNSYN_SO.Each system call gets its own dedicated subprocess, andAEF_ITEMi consists of these subprocesses through the choice operator.(21)AEF_ITEMi=AEF_SENDi|AEF_RECVi|AEF_EXECi|.......The processSYN implements the “mutex” lock by virtue of the parallel operator in order to serialize the access to the same subject or object. In order to prevent deadlock in locking the multiple subject or object involved in a system call, the priority of locking is set by subject first, and from small id to large id.(22)SYN=SYN_S|||SYN_O.The alphabet of processSYN is aSYN=enterS,leaveS,enterO,leaveO.The subject-access-synchronism process isSYN_S=|||i:P@SYN_Si, where SYN_Si=enterS.i⟶leaveS.i⟶SYN_Si.Similarly, the object-access-synchronism process isSYN_O=|||i:O@SYN_Oi, where SYN_Oj=enterO.jj⟶leaveO.j⟶SYN_O, and O is the set of all possible object ids.We set the buffer to cache and forward the messages in process communication. IfUSERi wants to send msg to USERj, AEF_SENDi will first set the msg level in terms of the current level of USERi and store it in the message slot BUFF_2i,j,full,msg, whose specifications are given in the following descriptions of OM. Subsequently, if USERj tries to obtain themsg, AEF_RECVj will collect the related ADI and send it to ADF for control policy. Only when a request is permitted by ADF, AEF_RECVj will return msg to USERj. Moreover, AEF_RECVj might adjust USERi’s level in terms of AEF’s requirements.(23)AEF_SENDi=apii?send,j,msg⟶ifi==jthen AEF_ITEMielse enterS.i⟶qstateSi.getlabel?Si,Ii,Ci,existi,s_sati⟶qstatei,j.buf_.in!msg,Si−Ci±,Ii∪Ci±⟶leaveS.i⟶AEF_ITEMiAEF_RECVi=apii?recv,j⟶ifi==jthenapii!error,null⟶AEF_ITEMielse locki,j⟶qstateSi.getlabel?Si,Ii,Ci,existi⟶AEF_ITEMielse locki,j⟶qstateSi.getlabel?Si,Ii,Ci,existi⟶qstatej,i.buff_test?full,Sj,Ij⟶qstateSj.getlabel?Sj′,Ij′,Cj,existj⟶qpolicyi!irecv,Si,Ii,Ci,full,Sj,Ij,existj,Sj′,Ij′⟶qpolicyi?policy,Sj′,Ij′,renew⟶if policy==accept thenqstatej,i.buff_out?msg⟶apii!ok,msg⟶if renew thenqstateSi.setlabel!Si′,Ii′,Ci,1⟶unlocki,j⟶AEF_ITEMielse unlocki,j⟶AEF_ITEMielseapii!error,empty⟶if renew thenqstateSi.setlabel!Si′,Ii′,Ci,1⟶unlocki,j⟶AEF_ITEMielse unlocki,j⟶AEF_ITEMi,where locki,j=enterS.mini,j⟶enterS.maxi,j and unlocki,j = leaveS.mini,j⟶leaveS.maxi,j.WhenUSERi has permission to access object j, AEF expresses the related object operation using the event in channel io, e.g.,(24)AEF_WRITEi=……⟶if policy==accept then io!writefile,j,msg⟶…….IfUSERi requests creating a new subject, AEF will first request the new pid from OM and OM will select the new pid randomly from the set of available process identifiers. Then AEF will adjust the levels of USERi and USERnewid and give off the born signal to activate the process USERnewid.(25)AEF_EXECi=apii?exec,j,msg⟶enterO.j⟶enterS.i⟶qstateSi.getlabel?Si,Ii,Ci,existi⟶qstateOj.getlabel?Sj,Ij,Cj,existj⟶qpolicyi!iexec,Si,Ii,Ci,Sj,Ij,Cj,existj⟶qpolicyi?policy,Si′,Ii′,Sj′,Ij′,Cj′,renew⟶if¬renew thenEXEC_RETi,j,errorelseqstateSi.setlabel!Si′,Ii′,Ci,1⟶ifpolicy==accept thenqstatePID.getpid⟶qstatePID.choose?result.newid⟶ifresult thenqstateSnewid.setlabel?Sj′,Ij′,Cj′,1⟶bornnewid!msg⟶EXEC_RETi,j,okelse EXEC_RETi,j,errorelse EXEC_RETi,j,error,where EXEC_RETi,j,result=leaveS.i⟶leaveO.j⟶AEF_ITEMi.When a subject exits,AEF will clear its label information in OM and update the set of available subject identifiers. In addition, it clears its send buffer.(26)AEF_EXITi=apii?exit⟶enterS.i⟶RM_eEXITi,PRM_eEXITfrom,to=if to==0then⟶qstateSi.setlabel!,,,0⟶qstatePID.delpid!i⟶leaveS.from⟶RM_ITEMfromelsebufffrom,to.out?msg⟶RM_eEXITfrom,to−1.The system calls for changing level are mainly used to update the label information inOM.


### 2.2.3. OM

The processOM manages the system states information, i.e., the labels and existence of all the subjects and objects, the set of available process identifiers, and the messages in process communication.We have introduced its subprocesses one by one.OM_S_LIVEpid,s,i,c,exist provides the query and modification service for the label and existence of all the subjects, where pid denotes the process id, s, i, and c, respectively, denote USERpid’s secrecy level, integrity level, and capabilities, and exist denotes whether the subject exists.(27)OM_S_LIVEpid,s,i,c,exist=qstateSpid.getlabel!s,i,c,exist⟶OM_S_LIVEpid,s,i,c,exist|qstateSpid.setlabel?s′,i′,c′,exist′⟶OM_S_LIVEpid,s′,i′,c′,exist′,s_sat.OM_S is an interleaving of all the OM_S_LIVEpid,s,i,c,exist. We assume that the USER1 with C1=DS∪DI×+,− is the only live user process at system startup. Therefore, we can set up any initial state of the system, for any type of process and object can be created by USER1.(28)OM_S=|||pid:P−1@OM_S_LIVEpid,,,,0|||OM_S_LIVE1,,,DS∪DI×+,−,1.Similarly,OM_O_LIVEoid,s,i,c,exist,exe provides the query and set service about the label and existence of all the objects, and OM_O is an interleaving of all the OM_O_LIVEoid,s,i,c,exist. The “capability” attributes of the object are set by authority administrator, and we model it as a random event in the channel nonce.SIC.(29)OM_O_LIVEoid,s,i,c,exist=qstateOoid.getlabel!s,i,c,exist⟶OM_O_LIVEoid,s,i,c,exist|qstateOoid.setlabel?s′,i′,c′,exist′⟶OM_O_LIVEoid,s′,i′,c′,exist′OM_O=|||oid:O@nonce.SIC?s,i,c,exist⟶OM_O_LIVEoid,s,i,c,exist.OM_ID_MGR provides the management of available process identifiers via channel qstatePID, which allocates a new id when a new process is created and reclaims the id when a process exits. In our specifications, access to channel qstatePID is mutually exclusive.(30)OM_ID_MGRoccupy,free=qstatePIDgetpidi⟶if emptyfreethenqstatePID.choose!1,0⟶OM_ID_MGRoccupy,freeelse nonce.Pid?i:free⟶qstatePID.choose!0,i⟶OM_ID_MGRoccupy∪i,free−i|qstatePID.delpid?i⟶OM_ID_MGRoccupy−i,free∪i.BUFF describes the behaviors of the message buffer in process communication, which caches and forwards the message. For simplicity, a message slot is set for each pair of sender and receiver.The processOM_BUFF specifies the behavior of the process communication buffers.(31)OM_BUFF=|||from:P@BUFF_1from,BUFF_1from=|||to:P@BUFF_2from,to,0,msg,,.The message slot provides the storage and removal of information. We specify simply that the new message will cover the old message that has not been taken away when the message buffer is full. The stored information also includes the current level of the sender. Its transition is as follows:(32)BUFF_2from,to,full,msg,S,I=qstatefrom,to.buff_in?msg′,S′,I′⟶BUFF_2from,to,1,msg′,S′,I′|qstatefrom,to.buff_out!msg⟶BUFF_2from,to,0,null,,|qstatefrom,to.buff_test!full,S,I⟶BUFF_2from,to,full,msg,S,I.Finally, the OM is an interleaving of these service subprocesses:(33)OM=OM_S|||OM_O|||OM_ID_MGR1,P−1|||OM_BUFF.


### 2.2.4. ADF

ADF also concurrently deals with the request of each of the subprocesses of AEF. According to the ADI and the rules, ADF returns its decision and requirements for state transition. Its behaviors are specified as follows:(34)ADF=|||i:P@ADF_ITEMi|||ADF_SATR,pidwhere ADF_ITEMi=ADF_RECVi|ADF_WRITEi|ADF_READi|….The process communication is controlled when the receiver tries to receive the message. For the request ofapii.recv,j, SS_RECVi will determine whether to permit it and develop the policy of adjusting the USERi’s level in terms of Definition 3. Since the system will clear the corresponding buffer when any subject exits, the message existing in the buffer must be fresh to guarantee the data consistency.(35)ADF_RECVi=qpolicyi?irecv,Si,Ii,Ci,full,Sj,Ij,existj,Sj′,Ij′⟶constratinSSATiquery!Si,Ci⟶constrainSSATpidquery?s_sati⟶if¬s_satithenqpolicyi!reject,,,0⟶ADF_ITEMielseconstratinSATiquery!Si∪Sj,,Ci⟶constrainSSATpidquery?sati⟶ifexistj∧Sj⊆Si∪Ci+∧Ij⊆Ii−Ci−∧sati∧full thenqpolicyi!accept,Si∪Sj,Ii−Ii−Ij,1⟶ADF_ITEMielse ifexistj∧¬full∧Sj′⊆Si∪Ci+∧Ij′⊆Ii−Ci−∧satithenqpolicyi!reject,Si∪Sj,Ii−Ii−Ij,1⟶ADF_ITEMielseqpolicyi!reject,Si∪Ci+∩DS−R,Ii−Ci−,1⟶ADF_ITEMi.The decision process for a request to read/write/create/delete/execute an object is similar toADF_RECVi mentioned above. The “capability” attributes of new object are set by authority administrator, and we model it as a random event in the channel nonce.C. We omit the unnecessary details.(36)ADF_CREATEi=qstatei?icreate,j,Sj,Ij⟶…⟶nonceC?Cj⟶…qstatei!Sj,Ij,Cj.ADF_SATR,pid stores the mutually exclusive tag constraints R and provides the service to verify whether a given label is sat or s_satR.(37)ADF_SATR,pid=constrainSAT pid.query?s,i,c⟶SATR,pid,s,i,c|constrainSSAT pid.query?s,c⟶SSATR,pid,s,cSATremain,pid,s,i,c=if emptyremainthenconstrainSAT pid.query!true⟶ADF_SATR,pidelse ifheadremain∩s>1∨headremain∩i>1thenconstrainSAT pid.query!false⟶ADF_SATR,pidelseSATtailremain,pid,s,i,cSSATremain,pid,s,c=if emptyremainthenconstrainSSAT pid.query!true⟶ADF_SATR,pidelse ifheadremain∩c+∩DS>1∧headremain∩s=0thenconstrainSSAT pid.query!false⟶ADF_SATR,pidelseSSATtailremain,pid,s,c.


### 2.2.5. Abstract EILCM System

Based on the components above, the security kernel can be described as the concurrent implementation ofAEF, OM, and ADF.(38)KERNEL=AEFOMqstate‖qpolicyADF.The overall system is the concurrent implementation of security kernel and user processes.(39)SYSTEMEILCM=USERKERNELapiaKERNEL,where aKERNEL=qstate,qpolicy,nonce,io,aSYN,....We use the hide operator inSYSTEMEILCM to hide the inner transitions, e.g., the communication between AEF and ADF. In fact, the inner implementation of the system is a black box to user, and the user can at most see other user’s behaviors, other than the inner traces [18].


## 2.2.1. User Processes

In general, the user processes access system resources through system calls. There is no direct interaction between them, so we use the interleaving operator to express their relations. The notationUSERi denotes the user process i. The behaviors of all user processes are specified as follows:(13)USERS=|||i:P−1@USERi|||USER_LIVE1,where P denotes the set of all process identifiers and USER_LIVE1 denotes the first process with CUSER_LIVE1=DS∪DI×+,− at the system startup, which can execute any object to create a new process for the startup needs. There is no deriving operator in CSP, but the actual systems usually restrict the maximum size of a process; thus, we can prebuild all the possible user processes. Any processes will be in an idle state before they receive the signal. The signal born makes it transition into the live state, and the exit signal makes it return to the idle state again. The behaviors of a single user process are specified as follows:(14)USERi=borni?msg⟶USER_LIVEi.In the live state,USERi can issue a system call:(15)USER_LIVEi=SENDi|RECVi|WRITEi|READi|CREATEi|DELi|EXECi|EXITi|CHANGELABELi.The subprocessSENDi describes sending a message msg to user process USERto:(16)SENDi=apii!send,to,msg…⟶USER_LIVEi.The subprocessRECVi describes receiving a message from USERfrom, where msg is the receive buffer and result=ok,error returns the success/failure result of this system call.(17)RECVi=apii!recv,from⟶apii?result,msg..⟶USER_LIVE.The subprocessEXECi describes executing an object which, where OM allocates randomly the PID of the new process.(18)EXECi=apii!exec,which,msg⟶USER_LIVEi.The subprocessEXITi describes process’s state transition from live to idle.(19)EXITi=apii!exit⟶USERi.The subprocessesWRITEi, READi, CREATEi, DELi, and CHANGELABELi have similar behaviors, and we omit the description of their behaviors.


## 2.2.2. AEF

AEF receives and processes concurrently system calls from different users, each subprocess AEF_ITEMi listening to the corresponding USERi’s calls via channel apii and controlling access to the system. The process SYN_SO guarantees the state consistency of the security kernel when more than two system calls involve the same subject or object simultaneously.(20)AEF=|||i:P@AEF_ITEMi||aSYNSYN_SO.Each system call gets its own dedicated subprocess, andAEF_ITEMi consists of these subprocesses through the choice operator.(21)AEF_ITEMi=AEF_SENDi|AEF_RECVi|AEF_EXECi|.......The processSYN implements the “mutex” lock by virtue of the parallel operator in order to serialize the access to the same subject or object. In order to prevent deadlock in locking the multiple subject or object involved in a system call, the priority of locking is set by subject first, and from small id to large id.(22)SYN=SYN_S|||SYN_O.The alphabet of processSYN is aSYN=enterS,leaveS,enterO,leaveO.The subject-access-synchronism process isSYN_S=|||i:P@SYN_Si, where SYN_Si=enterS.i⟶leaveS.i⟶SYN_Si.Similarly, the object-access-synchronism process isSYN_O=|||i:O@SYN_Oi, where SYN_Oj=enterO.jj⟶leaveO.j⟶SYN_O, and O is the set of all possible object ids.We set the buffer to cache and forward the messages in process communication. IfUSERi wants to send msg to USERj, AEF_SENDi will first set the msg level in terms of the current level of USERi and store it in the message slot BUFF_2i,j,full,msg, whose specifications are given in the following descriptions of OM. Subsequently, if USERj tries to obtain themsg, AEF_RECVj will collect the related ADI and send it to ADF for control policy. Only when a request is permitted by ADF, AEF_RECVj will return msg to USERj. Moreover, AEF_RECVj might adjust USERi’s level in terms of AEF’s requirements.(23)AEF_SENDi=apii?send,j,msg⟶ifi==jthen AEF_ITEMielse enterS.i⟶qstateSi.getlabel?Si,Ii,Ci,existi,s_sati⟶qstatei,j.buf_.in!msg,Si−Ci±,Ii∪Ci±⟶leaveS.i⟶AEF_ITEMiAEF_RECVi=apii?recv,j⟶ifi==jthenapii!error,null⟶AEF_ITEMielse locki,j⟶qstateSi.getlabel?Si,Ii,Ci,existi⟶AEF_ITEMielse locki,j⟶qstateSi.getlabel?Si,Ii,Ci,existi⟶qstatej,i.buff_test?full,Sj,Ij⟶qstateSj.getlabel?Sj′,Ij′,Cj,existj⟶qpolicyi!irecv,Si,Ii,Ci,full,Sj,Ij,existj,Sj′,Ij′⟶qpolicyi?policy,Sj′,Ij′,renew⟶if policy==accept thenqstatej,i.buff_out?msg⟶apii!ok,msg⟶if renew thenqstateSi.setlabel!Si′,Ii′,Ci,1⟶unlocki,j⟶AEF_ITEMielse unlocki,j⟶AEF_ITEMielseapii!error,empty⟶if renew thenqstateSi.setlabel!Si′,Ii′,Ci,1⟶unlocki,j⟶AEF_ITEMielse unlocki,j⟶AEF_ITEMi,where locki,j=enterS.mini,j⟶enterS.maxi,j and unlocki,j = leaveS.mini,j⟶leaveS.maxi,j.WhenUSERi has permission to access object j, AEF expresses the related object operation using the event in channel io, e.g.,(24)AEF_WRITEi=……⟶if policy==accept then io!writefile,j,msg⟶…….IfUSERi requests creating a new subject, AEF will first request the new pid from OM and OM will select the new pid randomly from the set of available process identifiers. Then AEF will adjust the levels of USERi and USERnewid and give off the born signal to activate the process USERnewid.(25)AEF_EXECi=apii?exec,j,msg⟶enterO.j⟶enterS.i⟶qstateSi.getlabel?Si,Ii,Ci,existi⟶qstateOj.getlabel?Sj,Ij,Cj,existj⟶qpolicyi!iexec,Si,Ii,Ci,Sj,Ij,Cj,existj⟶qpolicyi?policy,Si′,Ii′,Sj′,Ij′,Cj′,renew⟶if¬renew thenEXEC_RETi,j,errorelseqstateSi.setlabel!Si′,Ii′,Ci,1⟶ifpolicy==accept thenqstatePID.getpid⟶qstatePID.choose?result.newid⟶ifresult thenqstateSnewid.setlabel?Sj′,Ij′,Cj′,1⟶bornnewid!msg⟶EXEC_RETi,j,okelse EXEC_RETi,j,errorelse EXEC_RETi,j,error,where EXEC_RETi,j,result=leaveS.i⟶leaveO.j⟶AEF_ITEMi.When a subject exits,AEF will clear its label information in OM and update the set of available subject identifiers. In addition, it clears its send buffer.(26)AEF_EXITi=apii?exit⟶enterS.i⟶RM_eEXITi,PRM_eEXITfrom,to=if to==0then⟶qstateSi.setlabel!,,,0⟶qstatePID.delpid!i⟶leaveS.from⟶RM_ITEMfromelsebufffrom,to.out?msg⟶RM_eEXITfrom,to−1.The system calls for changing level are mainly used to update the label information inOM.


## 2.2.3. OM

The processOM manages the system states information, i.e., the labels and existence of all the subjects and objects, the set of available process identifiers, and the messages in process communication.We have introduced its subprocesses one by one.OM_S_LIVEpid,s,i,c,exist provides the query and modification service for the label and existence of all the subjects, where pid denotes the process id, s, i, and c, respectively, denote USERpid’s secrecy level, integrity level, and capabilities, and exist denotes whether the subject exists.(27)OM_S_LIVEpid,s,i,c,exist=qstateSpid.getlabel!s,i,c,exist⟶OM_S_LIVEpid,s,i,c,exist|qstateSpid.setlabel?s′,i′,c′,exist′⟶OM_S_LIVEpid,s′,i′,c′,exist′,s_sat.OM_S is an interleaving of all the OM_S_LIVEpid,s,i,c,exist. We assume that the USER1 with C1=DS∪DI×+,− is the only live user process at system startup. Therefore, we can set up any initial state of the system, for any type of process and object can be created by USER1.(28)OM_S=|||pid:P−1@OM_S_LIVEpid,,,,0|||OM_S_LIVE1,,,DS∪DI×+,−,1.Similarly,OM_O_LIVEoid,s,i,c,exist,exe provides the query and set service about the label and existence of all the objects, and OM_O is an interleaving of all the OM_O_LIVEoid,s,i,c,exist. The “capability” attributes of the object are set by authority administrator, and we model it as a random event in the channel nonce.SIC.(29)OM_O_LIVEoid,s,i,c,exist=qstateOoid.getlabel!s,i,c,exist⟶OM_O_LIVEoid,s,i,c,exist|qstateOoid.setlabel?s′,i′,c′,exist′⟶OM_O_LIVEoid,s′,i′,c′,exist′OM_O=|||oid:O@nonce.SIC?s,i,c,exist⟶OM_O_LIVEoid,s,i,c,exist.OM_ID_MGR provides the management of available process identifiers via channel qstatePID, which allocates a new id when a new process is created and reclaims the id when a process exits. In our specifications, access to channel qstatePID is mutually exclusive.(30)OM_ID_MGRoccupy,free=qstatePIDgetpidi⟶if emptyfreethenqstatePID.choose!1,0⟶OM_ID_MGRoccupy,freeelse nonce.Pid?i:free⟶qstatePID.choose!0,i⟶OM_ID_MGRoccupy∪i,free−i|qstatePID.delpid?i⟶OM_ID_MGRoccupy−i,free∪i.BUFF describes the behaviors of the message buffer in process communication, which caches and forwards the message. For simplicity, a message slot is set for each pair of sender and receiver.The processOM_BUFF specifies the behavior of the process communication buffers.(31)OM_BUFF=|||from:P@BUFF_1from,BUFF_1from=|||to:P@BUFF_2from,to,0,msg,,.The message slot provides the storage and removal of information. We specify simply that the new message will cover the old message that has not been taken away when the message buffer is full. The stored information also includes the current level of the sender. Its transition is as follows:(32)BUFF_2from,to,full,msg,S,I=qstatefrom,to.buff_in?msg′,S′,I′⟶BUFF_2from,to,1,msg′,S′,I′|qstatefrom,to.buff_out!msg⟶BUFF_2from,to,0,null,,|qstatefrom,to.buff_test!full,S,I⟶BUFF_2from,to,full,msg,S,I.Finally, the OM is an interleaving of these service subprocesses:(33)OM=OM_S|||OM_O|||OM_ID_MGR1,P−1|||OM_BUFF.


## 2.2.4. ADF

ADF also concurrently deals with the request of each of the subprocesses of AEF. According to the ADI and the rules, ADF returns its decision and requirements for state transition. Its behaviors are specified as follows:(34)ADF=|||i:P@ADF_ITEMi|||ADF_SATR,pidwhere ADF_ITEMi=ADF_RECVi|ADF_WRITEi|ADF_READi|….The process communication is controlled when the receiver tries to receive the message. For the request ofapii.recv,j, SS_RECVi will determine whether to permit it and develop the policy of adjusting the USERi’s level in terms of Definition 3. Since the system will clear the corresponding buffer when any subject exits, the message existing in the buffer must be fresh to guarantee the data consistency.(35)ADF_RECVi=qpolicyi?irecv,Si,Ii,Ci,full,Sj,Ij,existj,Sj′,Ij′⟶constratinSSATiquery!Si,Ci⟶constrainSSATpidquery?s_sati⟶if¬s_satithenqpolicyi!reject,,,0⟶ADF_ITEMielseconstratinSATiquery!Si∪Sj,,Ci⟶constrainSSATpidquery?sati⟶ifexistj∧Sj⊆Si∪Ci+∧Ij⊆Ii−Ci−∧sati∧full thenqpolicyi!accept,Si∪Sj,Ii−Ii−Ij,1⟶ADF_ITEMielse ifexistj∧¬full∧Sj′⊆Si∪Ci+∧Ij′⊆Ii−Ci−∧satithenqpolicyi!reject,Si∪Sj,Ii−Ii−Ij,1⟶ADF_ITEMielseqpolicyi!reject,Si∪Ci+∩DS−R,Ii−Ci−,1⟶ADF_ITEMi.The decision process for a request to read/write/create/delete/execute an object is similar toADF_RECVi mentioned above. The “capability” attributes of new object are set by authority administrator, and we model it as a random event in the channel nonce.C. We omit the unnecessary details.(36)ADF_CREATEi=qstatei?icreate,j,Sj,Ij⟶…⟶nonceC?Cj⟶…qstatei!Sj,Ij,Cj.ADF_SATR,pid stores the mutually exclusive tag constraints R and provides the service to verify whether a given label is sat or s_satR.(37)ADF_SATR,pid=constrainSAT pid.query?s,i,c⟶SATR,pid,s,i,c|constrainSSAT pid.query?s,c⟶SSATR,pid,s,cSATremain,pid,s,i,c=if emptyremainthenconstrainSAT pid.query!true⟶ADF_SATR,pidelse ifheadremain∩s>1∨headremain∩i>1thenconstrainSAT pid.query!false⟶ADF_SATR,pidelseSATtailremain,pid,s,i,cSSATremain,pid,s,c=if emptyremainthenconstrainSSAT pid.query!true⟶ADF_SATR,pidelse ifheadremain∩c+∩DS>1∧headremain∩s=0thenconstrainSSAT pid.query!false⟶ADF_SATR,pidelseSSATtailremain,pid,s,c.


## 2.2.5. Abstract EILCM System

Based on the components above, the security kernel can be described as the concurrent implementation ofAEF, OM, and ADF.(38)KERNEL=AEFOMqstate‖qpolicyADF.The overall system is the concurrent implementation of security kernel and user processes.(39)SYSTEMEILCM=USERKERNELapiaKERNEL,where aKERNEL=qstate,qpolicy,nonce,io,aSYN,....We use the hide operator inSYSTEMEILCM to hide the inner transitions, e.g., the communication between AEF and ADF. In fact, the inner implementation of the system is a black box to user, and the user can at most see other user’s behaviors, other than the inner traces [18].


## 2.3. Application of EILCM

The application case is a desktop system, as shown in Figure2. Typically, the system includes an instant messaging tool IM, a map navigation software MN, a data encryption and transmission software EMail, an antivirus tool Killer, a web browser UC, and a Shell Explorer.Figure 2
A typical application scenario of a desktop operating system.The user’s chat information is stored inIM data. The daily operations of a user include communicating with contacts via IM, sending encrypted important IM files or MN data to his/her colleagues via EMail, and assisting driving via MN. The important configuration information of this system is stored in OS config file. Killer can detect and kill viruses, but it needs to update its own virus database online regularly. The security requirements of this system are as follows:(1)
IM and MN are untrusted. They are forbidden to read each other’s data.(2)
Killer is allowed to readIM data, MN data, and OS config file in order to detect and kill potential viruses in time. However, it is forbidden to disclose these private data when updating the virus database.(3)
Secret IM data and MN data can be encrypted and sent out byEMail. Since a program can make an aggregation analysis of IM data and MN data and thus obtain more privacy information of users, the system requires privilege constraint about simultaneous reading of IM data and MN data.(4)
Explorer can no longer modify OS config files after it loads the insecure libraries that are downloaded from network by UC.(5)
The updated OS packages that are downloaded from network byUC cannot modify the configuration files unless they have been already checked by Killer.(6)
IM sets the label of IM data. MN sets the label of MN data.The label and capability scheme for building EILCM is as follows. In order to protect the secrecy of IM data and MN data, secrecy tagsdsIM and dsMN are created, respectively, to track and control the propagation flow of these secret information. In order to protect the important data integrity of the operating system, an integrity label diOS is established. The network is considered to have the lowest integrity level and secrecy level. Establish secrecy/least privilege rule: {dsMN, dsIM} ε R. The initial settings of each label are shown in Table 1.Table 1
Setting of initial labels and capabilities of subject and object by EILCM system.
SubjectsSecrecy labelIntegrity labelCapabilitiesObjectsSecrecy labelIntegrity labelIMdiIMdsIM±IM datadsIMMNdsMN±MN datadsMNEmaildsIM±,dsMN±ETP dataKillerdsIM+,dsMN+,dios±OS config filesdiosUCdios−Download dataExplorerdios−OS Updated packagesdiosIn Table1, since IM process is the owner of IM data, and its ability is set to dsIM±, indicating that it can manage these data. Similarly, the ability of MN process is set to dsMN±. The ability of EMail process is set to dsIM±,dsMN±, so that it can read IM and MN data and encrypt them before sending. The ability of Killer is set to dsIM+,dsMN+,dios±, which means that it can read any secret information, but it does not have the ability to release secret information to network. Killer can lower the integrity level to scan any entity or add diOS tags to itself or the data that are considered safe after scanning. The ability of UC process and Explorer process is set to dios−. They are not given the ability to add integrity tag diOS, so they cannot destroy the integrity of system data even if they are infected. It can be seen that EILCM system can better meet these security requirements. At the same time, because it belongs to the taint propagation model and supports the implicit change of tags, the system can reasonably automatically adjust the subject and object tags according to the access requirements. In addition, it also supports the explicit change of labels, which makes the system more flexible and improves the availability.


## 3. Noninterference Analysis for EILCM

We will analyze the security properties ofSYSTEMEILCM in this section. Goguen and Meseguer [27] took an important step towards a formal specification and analysis of information flow with the concept of noninterference. Intuitively, user A not interfering with user B means that that A’s behavior has no effect on what B can observe, that is, B’s view of the system is independent of A’s behavior. It is usually assumed that a system satisfying noninterference security has no covert channels.Many variants of Goguen and Meseguer’s definition [27] of noninterference were proposed with finite-state automaton [28], relational Hoare-type theory [29], Petri nets [30], game theory [26], etc. Ryan and Schneider [26] redefined the noninterference concept using CSP verification model [31] based on process equivalence. Bossi et al. [32] and Krohn and Tromer [18] partitioned the space of symbols into three sets: high, low, and declassify, and we also adopt similar idea. Krohn and Tromer and Bossi et al. [18, 32] presented the formula of noninterference with declassification in CSP property-oriented specifications, which lacks the effective support of CSP tools for automated analysis when compared with standard CSP process-oriented specification [31]. In this section, we first use the definition of noninterference from [26] to formally detect the known covert channels and analyze the reasons why EILCM can close them; secondly, we propose our definition of noninterference with declassification and prove that the abstract SYSTEMEILCM fulfills the noninterference.


### 3.1. Analysis of Covert Channel in EILCM System

We used Ryan and Schneider’s definition [26] of noninterference to detect the known cover channels above. We called their definition basic noninterference. In this section, we used the concept of CSP model and equivalence [31].Definition 5.
(basic noninterference). Assume that high-level users interact with the systemSYS via the high events (aHIGH) and low-level users do so via the low events (aLOW). Further assume that these two types of events partition the full range of events (alphabet) of SYS. Then, the high-level user is said to be noninterfering with the low-level user via S if and only if(40)∀tr,tr′∈tracesSYS,tr↑aLOW=tr′↑aLOW⇒S/traLOW=failureS/tr′aLOW.
That is, after being advanced bytr and tr′, the two processes must accept all of the same traces (projected to low) and refuse all of the same refusal sets (projected to low) [18].The definition above is a property-oriented specification. In order to avoid the need to explicitly quantify over traces, Ryan and Schneider expressed a characterization directly as a standard CSP equivalence:(41)SYSSTOPaHIGHaHIGH=failureSYSaHIGH.
Nevertheless, equation (40) is strictly stronger than equation (41) [26] because the latter does not consider the divergences in terms of semantics of the stable failure model. An alternative is not to hide the high events but to camouflage them [26]:(42)SYSSTOPaHIGH|||RUNaHIGH=failureSYS|||RUNaHIGH.
Obviously, this will greatly increase the state space for verification. In our view, when selecting the equivalence semantics from traces, failures, and divergences, we should consider safety, efficiency, and the characteristics of the actual verified system simultaneously. In general, based on the restriction of these models, we order these models from weak to strong and the complexity from low to high as follows: trace model, stable failure model, and failures/divergences. The trace model checks all the possible traces of process. This is appropriate for verifying safety properties [31], which are generally of the form “something bad will not happen.” However, it cannot verify liveliness properties, generally in the form of “something good will happen.” This is because the internal and external choice operators have the same trace semantics. The stable failure model solves the problem through increasing the failure check, but it does not capture the divergence behaviors. In general, adding the hide operator to a process expression might result in process divergence behaviors for the process. The failure/divergence model will check both failure and divergences, which are usually taken as the standard model. Of course, it can add some considerable overhead to the state space exploration. We think that if not for the existing divergence behavior of the actual system SYS but for the virtual system SYS/aHIGH, a divergence attack does not exist and thus we need not require the equivalence of divergences.
According to Definition5, for each event, we need to know the current levels of its sponsors and its properties in order to analyze the noninterference of the system. While the levels of all subjects and objects are stored in OM, the events themselves have no state information. Therefore, we explicitly label each system call apii.… with the caller’s current levels and capability. Now these system calls apii.… have the form apii,S,I,C.…, where S, I, and C denote, respectively, its secrecy level, integrity level, and the caller’s capability. The user process USERi gets its label once born:(43)USERi=borni?S,I,C,msg⟶USER_LIVEi,S,I,C,USER_LIVEi,S,I,C=SENDi,S,I,C|RECVi,S,I,C|WRITEi,S,I,C|READi,S,I,C|CREATEi,S,I,O|DELi,S,I,O|…….
In an EILCM system, the system calls that might cause the changing of caller’s levels includeapii,S,I,C.recv,…, apii,S,I,C.read,…,apii,S,I,Cchangelabel,…, and apii,S,I,C.exec,…. Our implicit labeling for the system calls should reflect these changes in time. We introduce the virtual system call apii,S,I,C.getlabel,… and its kernel response to know the latest state of caller. The involved user subprocesses include RECVi,S,I,C, READi,S,I,C, CHANGELABELi, and EXECi,S,I,C. We take RECVi,S,I,C as an example.(44)RECVi,S,I,C=apii,S,I,C!recv,from⟶apii,S,I,C?getlabel,S′,I′⟶apii,S′,I′,C′?result,msg⟶USER_LIVEi,S′,I′,C.
Other subprocesses need not update their label state; we takeSENDi,S,I,C as an example.(45)SENDi,S,I,C=apii,S,I,C!send,to,msg…⟶USER_LIVEi,S,I,C.
The modifiedSYSTEMEILCM is notated SYSEILCM. Evidently, the label query call cannot change the secure states and state transitions, and the ADI used for ADF ’s decision is still derived from OM. The explicit label for system calls only aids in the verification, and the implementation of SYSTEMEILCM need not consider it. SYSEILCM is equivalent to SYSTEMEILCM in security properties.
We use Krohn and Tromer’s definition [18] to classify the SYSEILCM user-level events in terms of their labels.Definition 6.
(high event/low event). Given a systemSYSEILCM, for each secrecy protection tag d, define the high and low alphabets as follows.
The high events are(46)aHIGHd=apii,S,I,C......|d∈S,i∈P∪borni.S,I,C…|d∈S,i∈P.
The low events are the complement sets:(47)aLOWd=apii,S,I,C......|d∉S,i∈P∪borni.S,I,C…|d∉S,i∈P.
Next, we can analyze the known covert channels mentioned inSection 1 by virtue of Definitions 5 and 6.Example 3.
Detecting the known covert channels: let the attack instance mentioned inSection 1 run in SYS based on our EILCM specifications. Firstly, assume that the ADF implements the information flow rules similar to Asbestos’s, rather than rules of EILCM. For secrecy protection, a contaminated process A is a high process and the other uncontaminated processes are low processes.
LetSYS′ denote SYS‖STOPaHIGH. Assume Bi is not contaminated in its initial state. If it is permitted for a contaminated process to change the labels of a less contaminated process implicitly, consider the trace send,C,m1,apiBi,LOW.recv,A,msg,apiC,LOW.recv,Bi,msg〉, and the trace apiA,HIGH.send,Bi,m2s∧, where each event is labeled with the sponsor’s secrecy level. It is easy to conclude that s∈tracesSYS′, t∈tracesSYS, and s↑aLOW=t↑aLOW. When the event apiC,LOW.recv,Bi,msg is triggered, we have s∧apiC,LOW.ok,msg∈traceSYS′/aHIGH and t∧apiC,LOW.ok,msg∉traceSYS/aHIGH, which fails to satisfy equation (41), that is, the HIGH event apiA.send,B1,msg interferes with the low process. Thus, we find a covert channel.
Secondly, assume that theADF implements the rules of EILCM and continues to analyze the attack. When the event apiC,LOW.recv,Bi,msg is triggered, we have s∧apiC,LOW.ok,msg∉tracesSYS′/aHIGH and t∧<apiC,LOW.ok,msg>∉traceSYS/aHIGH, which means that the trace will not occur in SYS and SYS′. Thus, we do not find a covert channel in EILCM system.
Thirdly, assumeADF denies implicit label change but permits explicit label change. Since the event u=apiBi,LOWchangelabel,self,high does not exist in trace s and t, Bi will not be raised to the high level, then both traceSYS and traceSYS′ do not involve the trace s∧apiC,LOW.ok,msg; in addition, if s′=us∧ and t′=ut∧, we have s↑aLOW=t↑aLOW=u∧apiC,LOWrecv,Bi,msg, which make C unable to receive the message from Bi, that is, both refusalSYS′/s′/aHIGH and refusalSYS/t′/aHIGH involve apiC,LOW.ok,msg. Therefore, there is no difference in this case and we do not find a covert channel in the situation of explicit label change.


### 3.2. Proof of Noninterference Property of EILCM

Definition5 strictly prohibits the high events from interfering with the low processes, but this might not reflect the actual secure requirement, e.g., the conditional downgrading. Many information flow models permit conditional information flows from high processes to low processes.For example, these flows are required to be carried out through trusted agents. EILCM permits these flows traversing the appropriate declassifiers. For a secrecy tag d, the declassifiers are the processes owning the ability to delete d from its secrecy level itself. Nevertheless, declassification makes the permitted information flow in EILCM system violate basic noninterference. For instance, consider a process p with Sp=d, Cp=d+,d−, a process q with Sq=d, Cq=d−, and a process r with Sr=, Cr=. Comparing the case where p has called apip,HIGHsend,r,m1 with the case where p has not, we find that if it calls apir,LOW.recv,p,msg, the process r will obtain the information m1 in the former case and will not obtain it in the latter case; similarly, comparing the case where q has triggered the event sequence apiq,HIGHsend,r,m1,apiq,HIGH.changelabel,self,0,,I with the case where q has not, we find that if it calls apir,LOWrecv,q,msg, the process r will obtain the information m1 in the former case and will not obtain it in the latter case. Therefore, we need a reasonable explanation and definition of noninterference for these cases. The new definition should permit the declassifier and low processes to interfere with any other processes and also permit the high processes to interfere with the other high processes but prohibit the high processes interfering with the low processes. This is called intransitive noninterference [33] or noninterference with declassification [18, 29, 30, 34].Some works analyzed formally Android programs [35], Java programs [36], and microkernel [37] with noninterference theory, while their analyses are not automated. Egger et al. [38] proved that the verification of intransitive noninterference can be solved in polynomial time. We will use a model checker tool FDR to make an automated analysis.Before we analyze theSYSEILCM’s property of noninterference with declassification, we need to specify the declassifying event, also called the mid event.Definition 7.
(mid event). Given a systemSYSEILCM, for each secrecy protection tag d, define the mid alphabets as follows:(48)aMIDd=apii,S,I,C......|d∈C−,i∈P∪borni.S,I,C…|d∈C−,i∈P.
Definition7 permits the intersection between aMID and aHIGH (or aLOW) not to be empty. In fact, aMID includes all the events the declassifiers can trigger whether they are in high state or in low state. The aMID might include events irrelevant to declassification, e.g., the declassifier sending a message to a high process or receiving a message from a low process. It is easy to conclude that these events neither change the current security state of the system nor interfere with the low process.
Now, we propose our definition of noninterference with declassification based on CSP equivalence.Definition 8.
(noninterference with declassification). Given a systemSYSEILCM, we say that SYSEILCM is secure for noninterference with declassification if and only if for each secrecy protection tag d, the following equation holds:(49)SYSEILCMSTOPaHIGHd−aMIDdaHIGHd∪aMIDd≡SYSEILCMaHIGHd∪aMIDd,where aSYS=aHIGHd∪aLOWd, aHIGHd∩aLOWd=φ, aMIDd⊆aSYS, and ≡ denotes an appropriate process equivalence.
Our definition of noninterference with declassification demands that the original system permitting all kinds of events to happen and the derived system prohibiting the events inaHIGH−aMID to happen are equivalent if they all hide the events in aMID∪aHIGH. That is, the set of events aMID has the same influence on the low processes with aMID∪aHIGH; put differently, the low processes cannot interfere with what the high processes do via the declassifiers; likewise, the high processes cannot interfere with the low processes via the declassifiers. Note that this extended definition is equivalent to basic noninterference if aMID=, where no declassifiers exist.
Next, we can review the declassification example mentioned at the beginning ofSection 1 in light of Definitions 7 and 8. The events of apiq.changelabel,self,0,,I, apipsend,r,m1, and apiqsend,r,m1 are not only high but also mid. They can occur in SYS′=SYS‖STOPaHIGH−aMID. Therefore, both SYS/aHIGH∪aMID and SYS′/aHIGH∪aMID involve the trace apir,LOW.recv,p,msg,apir,LOW.okerror,msg, permitting p or q to interfere with r. That is, r can deduce the behaviors of the declassifiers p and q, but it cannot interfere with the behaviors of high processes.
The security property of noninterference with declassification requires that there is no explicit and implicit information flow from a domain to outside, excluding all the information flows produced by subjects with declassification abilities to write entities outside the domain. The property of noninterference with declassification is weaker than that of basic noninterference, since the latter requires that in any case there is no information flow from a domain to outside. Therefore, there are limitations of the security property of noninterference with declassification because it needs to assume that a subject with declassification ability of a certain domain will not leak the information of this domain. When it is untrusted and sends the information in the domain to the outside of the domain, the secret information is leaked, and the confidentiality is damaged.Theorem 1.
SYSEILCM is secure for noninterference with declassification.Proof.
According to Definition8, we need prove that for each secrecy protection tag d, the claim SYSEILCM‖STOPaHIGHd−aMIDd/aHIGHd∪aMIDd≡SYSEILCM/aHIGHd∪aMIDd holds. Since the internal operator is not used in the specifications of SYSEILCM, the trace model and the stable failures model have the same equivalence semantics; in addition, the secure kernel KERNEL=AEF‖OMqstate‖ADFqpolicy just triggers the related inner event for the user’s system call. There are no inner loop processes; moreover, the priority of locking is set to prevent deadlock in terms of conventional methods. Therefore, KERNEL will not consecutively and infinitely execute the inner event, that is, KERNEL will not be divergent. Taking all the factors above into account, we use the trace model to verify process equivalence.
InSYSEILCM, given a secrecy tag d, firstly consider d∉R, that is, d is not mutually exclusive to any other tag. In this case, according to different combinations of a subject’s levels and capability, the subjects have eight states with respect to protecting the secrecy domain d. These states are as follows: d,, d,d+, d,d−, d,d+,d−, ,, ,d+, ,d−, ,d+,d−, where each state is a 2-tuple S,C, with S representing the subject’ secrecy level and C representing the subject’s capability. During the system state transitions, consider two subjects A and B that have the same state at some moment. We have the following knowledge. Firstly, it is easy to know that A and B have the same influence on the other subjects and objects, that is, A can do anything B does, and vice versa. Secondly, the influence of other parts of systems on A and B is also the same, that is, whether or not it is permitted that any other part’s operation sequence on A is the same as that on B. Thirdly, since both of them are contaminated or uncontaminated subjects simultaneously, their own interaction will not change their level. Finally, the subject’s capability remains unchangeable. On the other hand, as for the object’s states, since the label of a new subject has a reference to the levels and “capability” attribute of the object from whom it is derived, the objects have eight states in this case. If two objects have the same state, any traces related to them can happen when they are replaced by each other.
InSYSEILCM, let P be the set of all subject identifiers and let O be the set of all object identifiers. Assume P = 8 and O = 8. Assume that in the initial state of the system there is only a subject with its capabilities being d+,d−, so it can create any type of object and further any type of subject; therefore, during the system state transitions, it is legal that there are eight subjects with different subject states. Assuming the claim holds on the condition that P = 8 and O = 8, we analyze whether the claim holds when P = 9 and O = 8. If it does not hold on this condition, the interference must appear at some point after nine subjects start existing simultaneously and be relevant to the behavior of the ninth-born subject because the claim holds on condition that P = 8.
Meanwhile, the ninth-born subject’s state must be the same as one of the top-eight-born subjects because all subjects have at most eight states. Nevertheless, according to the analysis in the previous paragraph, two subjects that have the same states have the same influence on systems, and the influence of other parts on them is also the same, and their own interaction does not change the system state. So, we get the following paradox: given two subjects with the same state, one subject causes the occurrence of interference, while the other does not.
Therefore, the assumption that the claim does not hold atP = 9 and O = 8 is wrong. So, if it holds on the condition that P = 8 and O = 8, then the claims must hold at P = 9 and O = 8. Moreover, we can deduce that if it holds on condition that P = 9 and O = 8, then the claim must hold on the condition that P > 9 and O = 8, and so on. We can use the same method to analyze the situation of P = 8, O = 9. If there are nine objects existing together, it must mean that two subjects among them must have same states, which means that any other part’s operation sequence on them has the same result, i.e., permission or rejection. So, if it holds at P = 8 and O = 8, then the claim must hold on condition that P = 8 and O = 9, and so on.
Therefore, if we can prove that the claim holds on the condition thatp = 8, O = 8, R=φ and there is a subject with its capabilities d+,d− in the system initial state, inductively, we can prove that the claim holds on the condition that p > 8, O > 8, R=φ, with the initial state of system being arbitrary. Thus, we prove that it holds on the condition that p ≥ 0, O ≥ 0, R=φ, with the initial state of system being arbitrary. Actually, the eight states of the subjects can be divided into five categories, and the states of each categoryare equivalent: (1) d,d,d+. (2) d,d−. (3) ,d+,d−d,d+,d−. (4) ,d+. (5) ,,d−. For instance, each subject whose state is in class (3) can freely adjust its own level between  and d and its behavior consisting of mid events entirely. So, we only need to analyze whether the claim holds on the condition that p = 5, O = 5, R=φ and there is a subject with its capabilities d+,d−.
We use FDR2 to verify the claim on the condition thatp = 5, O = 5, R=φ, and there is a subject with the capabilities d+,d− in the system initial state. FDR is a model-checking tool for state machines, with foundations in the theory of concurrency-based CSP. It can establish whether a property holds for a refined transition system. FDR2 improves verification efficiency through compressing the states. It is easy to conclude that the trace collection of SYSEILCM‖STOPaHIGHd−aMIDd/aHIGHd∪aMIDd is a subset of SYSEILCM/aHIGHd∪aMIDd.
We need to verify whether or not the latter is a subset of the former. The verification problem can be expressed in FDR2 using the following assertion:(50)assertSYSEILCMSTOPaHIGHd−aMIDdaHIGHd∪aMIDdTSYSEILCMaHIGHd∪aMIDd.
The previous section considered the case thatd∉R. As for the case that d∈R, we know that no subject has the ability to delete tag d from its own level in terms of our EILCM. In this case, the subjects have eight states with respect to protecting the secrecy domain d. Having been compressed, these states are as follows: , , ,d+, e+,e+, ,d+,e+, d,, e,, d,e,, where each state is a 2-tuple S,C, S represents the subject’s secrecy level, C represents the subject’s capability, and e represents some tag mutually exclusive to tag d. In this case, we use FDR2 to verify the claim on the condition that p = 10, O = 1, R=d,e, and there is a subject with its capabilities ,d+,d−,e+,e− in the system initial state.
The experiments were performed using FDR2.83 on Ubuntu 9.10 with an Intel P4 2.8 G CPU and 2 GB of memory. Both of the results of verification for the two cases above are true. The runtime verification time is 1680 seconds in the case ofd∉R and 2580 seconds in the case of d∈R.
Taking into account all of the results of the analysis and automatic verification, we conclude thatSYSEILCM is secure for noninterference with declassification.
Though our noninterference ofSYSEILCM was deduced from secrecy protection, the same argument holds for integrity protection. For integrity tag d, the high events are the events with integrity level involving the tag d, the low events are the events with its integrity level not involving the tag d, the contaminated subjects are regarded as high subjects, and the uncontaminated subjects are regarded as low processes. We can use the same methods to prove that the contaminated subjects do not interfere with uncontaminated subjects.
The covert channel mentioned in the paper can also be found by using Definition8 as a property. Our modeling of the system in the proof process has depicted the possible utilization behavior of the covert channel, and there are subjects with different labels and capabilities in the initial state of the system, so whether this covert channel can occur has been verified by the FDR tool. The participating entities of this covert channel do not contain declassifiers, so Definitions 8 and 5 are equivalent for detecting this covert channel. In order to explain more clearly, the noninterference analysis of this covert channel is also analyzed by using basic noninterference in Definition 5.


## 3.1. Analysis of Covert Channel in EILCM System

We used Ryan and Schneider’s definition [26] of noninterference to detect the known cover channels above. We called their definition basic noninterference. In this section, we used the concept of CSP model and equivalence [31].Definition 5.
(basic noninterference). Assume that high-level users interact with the systemSYS via the high events (aHIGH) and low-level users do so via the low events (aLOW). Further assume that these two types of events partition the full range of events (alphabet) of SYS. Then, the high-level user is said to be noninterfering with the low-level user via S if and only if(40)∀tr,tr′∈tracesSYS,tr↑aLOW=tr′↑aLOW⇒S/traLOW=failureS/tr′aLOW.
That is, after being advanced bytr and tr′, the two processes must accept all of the same traces (projected to low) and refuse all of the same refusal sets (projected to low) [18].The definition above is a property-oriented specification. In order to avoid the need to explicitly quantify over traces, Ryan and Schneider expressed a characterization directly as a standard CSP equivalence:(41)SYSSTOPaHIGHaHIGH=failureSYSaHIGH.
Nevertheless, equation (40) is strictly stronger than equation (41) [26] because the latter does not consider the divergences in terms of semantics of the stable failure model. An alternative is not to hide the high events but to camouflage them [26]:(42)SYSSTOPaHIGH|||RUNaHIGH=failureSYS|||RUNaHIGH.
Obviously, this will greatly increase the state space for verification. In our view, when selecting the equivalence semantics from traces, failures, and divergences, we should consider safety, efficiency, and the characteristics of the actual verified system simultaneously. In general, based on the restriction of these models, we order these models from weak to strong and the complexity from low to high as follows: trace model, stable failure model, and failures/divergences. The trace model checks all the possible traces of process. This is appropriate for verifying safety properties [31], which are generally of the form “something bad will not happen.” However, it cannot verify liveliness properties, generally in the form of “something good will happen.” This is because the internal and external choice operators have the same trace semantics. The stable failure model solves the problem through increasing the failure check, but it does not capture the divergence behaviors. In general, adding the hide operator to a process expression might result in process divergence behaviors for the process. The failure/divergence model will check both failure and divergences, which are usually taken as the standard model. Of course, it can add some considerable overhead to the state space exploration. We think that if not for the existing divergence behavior of the actual system SYS but for the virtual system SYS/aHIGH, a divergence attack does not exist and thus we need not require the equivalence of divergences.
According to Definition5, for each event, we need to know the current levels of its sponsors and its properties in order to analyze the noninterference of the system. While the levels of all subjects and objects are stored in OM, the events themselves have no state information. Therefore, we explicitly label each system call apii.… with the caller’s current levels and capability. Now these system calls apii.… have the form apii,S,I,C.…, where S, I, and C denote, respectively, its secrecy level, integrity level, and the caller’s capability. The user process USERi gets its label once born:(43)USERi=borni?S,I,C,msg⟶USER_LIVEi,S,I,C,USER_LIVEi,S,I,C=SENDi,S,I,C|RECVi,S,I,C|WRITEi,S,I,C|READi,S,I,C|CREATEi,S,I,O|DELi,S,I,O|…….
In an EILCM system, the system calls that might cause the changing of caller’s levels includeapii,S,I,C.recv,…, apii,S,I,C.read,…,apii,S,I,Cchangelabel,…, and apii,S,I,C.exec,…. Our implicit labeling for the system calls should reflect these changes in time. We introduce the virtual system call apii,S,I,C.getlabel,… and its kernel response to know the latest state of caller. The involved user subprocesses include RECVi,S,I,C, READi,S,I,C, CHANGELABELi, and EXECi,S,I,C. We take RECVi,S,I,C as an example.(44)RECVi,S,I,C=apii,S,I,C!recv,from⟶apii,S,I,C?getlabel,S′,I′⟶apii,S′,I′,C′?result,msg⟶USER_LIVEi,S′,I′,C.
Other subprocesses need not update their label state; we takeSENDi,S,I,C as an example.(45)SENDi,S,I,C=apii,S,I,C!send,to,msg…⟶USER_LIVEi,S,I,C.
The modifiedSYSTEMEILCM is notated SYSEILCM. Evidently, the label query call cannot change the secure states and state transitions, and the ADI used for ADF ’s decision is still derived from OM. The explicit label for system calls only aids in the verification, and the implementation of SYSTEMEILCM need not consider it. SYSEILCM is equivalent to SYSTEMEILCM in security properties.
We use Krohn and Tromer’s definition [18] to classify the SYSEILCM user-level events in terms of their labels.Definition 6.
(high event/low event). Given a systemSYSEILCM, for each secrecy protection tag d, define the high and low alphabets as follows.
The high events are(46)aHIGHd=apii,S,I,C......|d∈S,i∈P∪borni.S,I,C…|d∈S,i∈P.
The low events are the complement sets:(47)aLOWd=apii,S,I,C......|d∉S,i∈P∪borni.S,I,C…|d∉S,i∈P.
Next, we can analyze the known covert channels mentioned inSection 1 by virtue of Definitions 5 and 6.Example 3.
Detecting the known covert channels: let the attack instance mentioned inSection 1 run in SYS based on our EILCM specifications. Firstly, assume that the ADF implements the information flow rules similar to Asbestos’s, rather than rules of EILCM. For secrecy protection, a contaminated process A is a high process and the other uncontaminated processes are low processes.
LetSYS′ denote SYS‖STOPaHIGH. Assume Bi is not contaminated in its initial state. If it is permitted for a contaminated process to change the labels of a less contaminated process implicitly, consider the trace send,C,m1,apiBi,LOW.recv,A,msg,apiC,LOW.recv,Bi,msg〉, and the trace apiA,HIGH.send,Bi,m2s∧, where each event is labeled with the sponsor’s secrecy level. It is easy to conclude that s∈tracesSYS′, t∈tracesSYS, and s↑aLOW=t↑aLOW. When the event apiC,LOW.recv,Bi,msg is triggered, we have s∧apiC,LOW.ok,msg∈traceSYS′/aHIGH and t∧apiC,LOW.ok,msg∉traceSYS/aHIGH, which fails to satisfy equation (41), that is, the HIGH event apiA.send,B1,msg interferes with the low process. Thus, we find a covert channel.
Secondly, assume that theADF implements the rules of EILCM and continues to analyze the attack. When the event apiC,LOW.recv,Bi,msg is triggered, we have s∧apiC,LOW.ok,msg∉tracesSYS′/aHIGH and t∧<apiC,LOW.ok,msg>∉traceSYS/aHIGH, which means that the trace will not occur in SYS and SYS′. Thus, we do not find a covert channel in EILCM system.
Thirdly, assumeADF denies implicit label change but permits explicit label change. Since the event u=apiBi,LOWchangelabel,self,high does not exist in trace s and t, Bi will not be raised to the high level, then both traceSYS and traceSYS′ do not involve the trace s∧apiC,LOW.ok,msg; in addition, if s′=us∧ and t′=ut∧, we have s↑aLOW=t↑aLOW=u∧apiC,LOWrecv,Bi,msg, which make C unable to receive the message from Bi, that is, both refusalSYS′/s′/aHIGH and refusalSYS/t′/aHIGH involve apiC,LOW.ok,msg. Therefore, there is no difference in this case and we do not find a covert channel in the situation of explicit label change.


## 3.2. Proof of Noninterference Property of EILCM

Definition5 strictly prohibits the high events from interfering with the low processes, but this might not reflect the actual secure requirement, e.g., the conditional downgrading. Many information flow models permit conditional information flows from high processes to low processes.For example, these flows are required to be carried out through trusted agents. EILCM permits these flows traversing the appropriate declassifiers. For a secrecy tag d, the declassifiers are the processes owning the ability to delete d from its secrecy level itself. Nevertheless, declassification makes the permitted information flow in EILCM system violate basic noninterference. For instance, consider a process p with Sp=d, Cp=d+,d−, a process q with Sq=d, Cq=d−, and a process r with Sr=, Cr=. Comparing the case where p has called apip,HIGHsend,r,m1 with the case where p has not, we find that if it calls apir,LOW.recv,p,msg, the process r will obtain the information m1 in the former case and will not obtain it in the latter case; similarly, comparing the case where q has triggered the event sequence apiq,HIGHsend,r,m1,apiq,HIGH.changelabel,self,0,,I with the case where q has not, we find that if it calls apir,LOWrecv,q,msg, the process r will obtain the information m1 in the former case and will not obtain it in the latter case. Therefore, we need a reasonable explanation and definition of noninterference for these cases. The new definition should permit the declassifier and low processes to interfere with any other processes and also permit the high processes to interfere with the other high processes but prohibit the high processes interfering with the low processes. This is called intransitive noninterference [33] or noninterference with declassification [18, 29, 30, 34].Some works analyzed formally Android programs [35], Java programs [36], and microkernel [37] with noninterference theory, while their analyses are not automated. Egger et al. [38] proved that the verification of intransitive noninterference can be solved in polynomial time. We will use a model checker tool FDR to make an automated analysis.Before we analyze theSYSEILCM’s property of noninterference with declassification, we need to specify the declassifying event, also called the mid event.Definition 7.
(mid event). Given a systemSYSEILCM, for each secrecy protection tag d, define the mid alphabets as follows:(48)aMIDd=apii,S,I,C......|d∈C−,i∈P∪borni.S,I,C…|d∈C−,i∈P.
Definition7 permits the intersection between aMID and aHIGH (or aLOW) not to be empty. In fact, aMID includes all the events the declassifiers can trigger whether they are in high state or in low state. The aMID might include events irrelevant to declassification, e.g., the declassifier sending a message to a high process or receiving a message from a low process. It is easy to conclude that these events neither change the current security state of the system nor interfere with the low process.
Now, we propose our definition of noninterference with declassification based on CSP equivalence.Definition 8.
(noninterference with declassification). Given a systemSYSEILCM, we say that SYSEILCM is secure for noninterference with declassification if and only if for each secrecy protection tag d, the following equation holds:(49)SYSEILCMSTOPaHIGHd−aMIDdaHIGHd∪aMIDd≡SYSEILCMaHIGHd∪aMIDd,where aSYS=aHIGHd∪aLOWd, aHIGHd∩aLOWd=φ, aMIDd⊆aSYS, and ≡ denotes an appropriate process equivalence.
Our definition of noninterference with declassification demands that the original system permitting all kinds of events to happen and the derived system prohibiting the events inaHIGH−aMID to happen are equivalent if they all hide the events in aMID∪aHIGH. That is, the set of events aMID has the same influence on the low processes with aMID∪aHIGH; put differently, the low processes cannot interfere with what the high processes do via the declassifiers; likewise, the high processes cannot interfere with the low processes via the declassifiers. Note that this extended definition is equivalent to basic noninterference if aMID=, where no declassifiers exist.
Next, we can review the declassification example mentioned at the beginning ofSection 1 in light of Definitions 7 and 8. The events of apiq.changelabel,self,0,,I, apipsend,r,m1, and apiqsend,r,m1 are not only high but also mid. They can occur in SYS′=SYS‖STOPaHIGH−aMID. Therefore, both SYS/aHIGH∪aMID and SYS′/aHIGH∪aMID involve the trace apir,LOW.recv,p,msg,apir,LOW.okerror,msg, permitting p or q to interfere with r. That is, r can deduce the behaviors of the declassifiers p and q, but it cannot interfere with the behaviors of high processes.
The security property of noninterference with declassification requires that there is no explicit and implicit information flow from a domain to outside, excluding all the information flows produced by subjects with declassification abilities to write entities outside the domain. The property of noninterference with declassification is weaker than that of basic noninterference, since the latter requires that in any case there is no information flow from a domain to outside. Therefore, there are limitations of the security property of noninterference with declassification because it needs to assume that a subject with declassification ability of a certain domain will not leak the information of this domain. When it is untrusted and sends the information in the domain to the outside of the domain, the secret information is leaked, and the confidentiality is damaged.Theorem 1.
SYSEILCM is secure for noninterference with declassification.Proof.
According to Definition8, we need prove that for each secrecy protection tag d, the claim SYSEILCM‖STOPaHIGHd−aMIDd/aHIGHd∪aMIDd≡SYSEILCM/aHIGHd∪aMIDd holds. Since the internal operator is not used in the specifications of SYSEILCM, the trace model and the stable failures model have the same equivalence semantics; in addition, the secure kernel KERNEL=AEF‖OMqstate‖ADFqpolicy just triggers the related inner event for the user’s system call. There are no inner loop processes; moreover, the priority of locking is set to prevent deadlock in terms of conventional methods. Therefore, KERNEL will not consecutively and infinitely execute the inner event, that is, KERNEL will not be divergent. Taking all the factors above into account, we use the trace model to verify process equivalence.
InSYSEILCM, given a secrecy tag d, firstly consider d∉R, that is, d is not mutually exclusive to any other tag. In this case, according to different combinations of a subject’s levels and capability, the subjects have eight states with respect to protecting the secrecy domain d. These states are as follows: d,, d,d+, d,d−, d,d+,d−, ,, ,d+, ,d−, ,d+,d−, where each state is a 2-tuple S,C, with S representing the subject’ secrecy level and C representing the subject’s capability. During the system state transitions, consider two subjects A and B that have the same state at some moment. We have the following knowledge. Firstly, it is easy to know that A and B have the same influence on the other subjects and objects, that is, A can do anything B does, and vice versa. Secondly, the influence of other parts of systems on A and B is also the same, that is, whether or not it is permitted that any other part’s operation sequence on A is the same as that on B. Thirdly, since both of them are contaminated or uncontaminated subjects simultaneously, their own interaction will not change their level. Finally, the subject’s capability remains unchangeable. On the other hand, as for the object’s states, since the label of a new subject has a reference to the levels and “capability” attribute of the object from whom it is derived, the objects have eight states in this case. If two objects have the same state, any traces related to them can happen when they are replaced by each other.
InSYSEILCM, let P be the set of all subject identifiers and let O be the set of all object identifiers. Assume P = 8 and O = 8. Assume that in the initial state of the system there is only a subject with its capabilities being d+,d−, so it can create any type of object and further any type of subject; therefore, during the system state transitions, it is legal that there are eight subjects with different subject states. Assuming the claim holds on the condition that P = 8 and O = 8, we analyze whether the claim holds when P = 9 and O = 8. If it does not hold on this condition, the interference must appear at some point after nine subjects start existing simultaneously and be relevant to the behavior of the ninth-born subject because the claim holds on condition that P = 8.
Meanwhile, the ninth-born subject’s state must be the same as one of the top-eight-born subjects because all subjects have at most eight states. Nevertheless, according to the analysis in the previous paragraph, two subjects that have the same states have the same influence on systems, and the influence of other parts on them is also the same, and their own interaction does not change the system state. So, we get the following paradox: given two subjects with the same state, one subject causes the occurrence of interference, while the other does not.
Therefore, the assumption that the claim does not hold atP = 9 and O = 8 is wrong. So, if it holds on the condition that P = 8 and O = 8, then the claims must hold at P = 9 and O = 8. Moreover, we can deduce that if it holds on condition that P = 9 and O = 8, then the claim must hold on the condition that P > 9 and O = 8, and so on. We can use the same method to analyze the situation of P = 8, O = 9. If there are nine objects existing together, it must mean that two subjects among them must have same states, which means that any other part’s operation sequence on them has the same result, i.e., permission or rejection. So, if it holds at P = 8 and O = 8, then the claim must hold on condition that P = 8 and O = 9, and so on.
Therefore, if we can prove that the claim holds on the condition thatp = 8, O = 8, R=φ and there is a subject with its capabilities d+,d− in the system initial state, inductively, we can prove that the claim holds on the condition that p > 8, O > 8, R=φ, with the initial state of system being arbitrary. Thus, we prove that it holds on the condition that p ≥ 0, O ≥ 0, R=φ, with the initial state of system being arbitrary. Actually, the eight states of the subjects can be divided into five categories, and the states of each categoryare equivalent: (1) d,d,d+. (2) d,d−. (3) ,d+,d−d,d+,d−. (4) ,d+. (5) ,,d−. For instance, each subject whose state is in class (3) can freely adjust its own level between  and d and its behavior consisting of mid events entirely. So, we only need to analyze whether the claim holds on the condition that p = 5, O = 5, R=φ and there is a subject with its capabilities d+,d−.
We use FDR2 to verify the claim on the condition thatp = 5, O = 5, R=φ, and there is a subject with the capabilities d+,d− in the system initial state. FDR is a model-checking tool for state machines, with foundations in the theory of concurrency-based CSP. It can establish whether a property holds for a refined transition system. FDR2 improves verification efficiency through compressing the states. It is easy to conclude that the trace collection of SYSEILCM‖STOPaHIGHd−aMIDd/aHIGHd∪aMIDd is a subset of SYSEILCM/aHIGHd∪aMIDd.
We need to verify whether or not the latter is a subset of the former. The verification problem can be expressed in FDR2 using the following assertion:(50)assertSYSEILCMSTOPaHIGHd−aMIDdaHIGHd∪aMIDdTSYSEILCMaHIGHd∪aMIDd.
The previous section considered the case thatd∉R. As for the case that d∈R, we know that no subject has the ability to delete tag d from its own level in terms of our EILCM. In this case, the subjects have eight states with respect to protecting the secrecy domain d. Having been compressed, these states are as follows: , , ,d+, e+,e+, ,d+,e+, d,, e,, d,e,, where each state is a 2-tuple S,C, S represents the subject’s secrecy level, C represents the subject’s capability, and e represents some tag mutually exclusive to tag d. In this case, we use FDR2 to verify the claim on the condition that p = 10, O = 1, R=d,e, and there is a subject with its capabilities ,d+,d−,e+,e− in the system initial state.
The experiments were performed using FDR2.83 on Ubuntu 9.10 with an Intel P4 2.8 G CPU and 2 GB of memory. Both of the results of verification for the two cases above are true. The runtime verification time is 1680 seconds in the case ofd∉R and 2580 seconds in the case of d∈R.
Taking into account all of the results of the analysis and automatic verification, we conclude thatSYSEILCM is secure for noninterference with declassification.
Though our noninterference ofSYSEILCM was deduced from secrecy protection, the same argument holds for integrity protection. For integrity tag d, the high events are the events with integrity level involving the tag d, the low events are the events with its integrity level not involving the tag d, the contaminated subjects are regarded as high subjects, and the uncontaminated subjects are regarded as low processes. We can use the same methods to prove that the contaminated subjects do not interfere with uncontaminated subjects.
The covert channel mentioned in the paper can also be found by using Definition8 as a property. Our modeling of the system in the proof process has depicted the possible utilization behavior of the covert channel, and there are subjects with different labels and capabilities in the initial state of the system, so whether this covert channel can occur has been verified by the FDR tool. The participating entities of this covert channel do not contain declassifiers, so Definitions 8 and 5 are equivalent for detecting this covert channel. In order to explain more clearly, the noninterference analysis of this covert channel is also analyzed by using basic noninterference in Definition 5.


## 4. Policy Verification for EILCM System

### 4.1. Problem Definition and Complexity

The purpose of noninterference analysis is to verify whether the EILCM system implements the information flow control according to the information flow policies and whether there are covert channels in which there are information flows that violate the security policy, including explicit and implicit information flows. If the system is secure without interference, it means that the implementation of the system strictly adheres to the security policy and there is no covert channels.The purpose of policy verification is to verify the information flow reachability problem under a given tag and capability allocation scheme. The EILCM model is highly flexible, often with thousands of entities whose capabilities and tags are varied. Also, the EILCM model is dynamic, and its information flow accessibility is complicated. Then, the burden on administrators is large, which can easily lead to policy mismatches and mismatches. Automated policy verification can assist administrators in managing policies and thus is required.In EILCM, although the subject’s capabilities for deleting secrecy tags or adding integrity tags from its own levels have good semantics, these capabilities complicate the information flow analysis. We need to verify whether information can flow from one subject/object to another subject/object in the system state transitions. For instance, a subjectA with SA=ds1, IA=di1, and CA= cannot send messages directly to a subject B with SB=ds2, IB=di2, and CA=, but A can indirectly achieve its goals through forwarding a subject M with SM=ds1, IM=, and MC=ds1−,di2+.In our model, the secrecy submodel is the dual of the integrity submodel. Their problems of policy analysis are equivalent and can be transformed into each other. A conversion method is as follows: given an integrity tagd, for each subject/object x, we use the notation Ixd: a1,a2,a3 denoting its integrity level on d, where a1,a2,a3∈0,1, a1 denotes whether x’s level involves d, a2 denotes whether x has the capability of adding d to its own integrity level, and a3 denotes whether x has the capability of deleting d from its own integrity level. We can give its dual form of secrecy level on d: Sxda1¯,a3,a2. Similarly, if we let Iyd: b1,b2,b3 be y’s integrity level on d, then we have Syd: b1¯,b3,b2 as y’s secrecy level on d. By enumerating all possible cases, we can determine that the integrity constraint of Ixd and Iyd and the secrecy constraint of Sxd and Syd have the same effect on communication. Therefore, in order to simplify the analysis, we only consider the constraints of secrecy protection on the information flow.Moreover, there are two aspects that can simplify the analysis. Firstly, it is easy to determine that the remaining part of a legal path after deleting all the object-type nodes is still a legal path because the object’s capability is empty. For instance, if a pathp⟶o⟶q is legal, where p,q are subjects and o is an object, then p⟶q is legal. So, we need not consider objects being nodes in a legal path. Secondly, in terms of Definition 3, the new-born subject’s capabilities are the subset of its parent subject’s capabilities, while its secrecy/integrity levels are lower than its parent’s. That is, any legal path remains legal if we replace some subject node with the subject’s parent. So we need not consider generating subjects.To facilitate its description, an EILCM system instanceSys is a 9-tuple Sys=U,O,DS,DI,S,I,C,CO,A, where U denotes the set of all the users, O denotes the set of all the objects, DS denotes the set of all the secrecy(export) protection tags, DI denotes the set of integrity(import) protection tags. Let V=U∪O; then, S:V⟶2DS maps the each subject/object onto secrecy levels, I:V⟶2DI maps the each subject/object onto integrity levels, C:S⟶2DS∪DI×+,− maps each subject/object onto capabilities, R is the set of mutually exclusive tags constraints, and A:O⟶2DS∪DI×+,− maps each object onto “capability” attributes. According to the analysis of the object’s influence, our policy verifications ignore new process generation, any objects occurring in the path, and integrity protection. Therefore, Sys can be simplified as U,DS,S,C,CO . Next, we can define the problem of policy verifications of EILCM systems.Definition 9.
(policy verification problem of EILCM systems). Given an EILCM system instanceSys=U,DS,S,C,CO, for ∀p,q∈U, we say p can reach q if and only if there is a path v1,v2,…,vn, where v1=p, vn=q, vi∈U, 1≤i≤n, and the information can legally flow in terms of requirement of EILCM. Let Sinitialvi be the initial secrecy level of vi before the query. Let Sinvi be the secrecy levels of vi just when vi has received the information from vi−1. Let Soutvi be the secrecy levels of vi when vi is sending the information to vi+1. That is, the path needs to satisfy two constraints: (1) information flow constraints: Soutvi−1⊆Sinvi, 1<i≤n; Soutvi⊆Sinvi+1, 1≤i<n; (2) level adjusting constraints: Sinitialvi⊆Sinvi⊆Sinitialvi∪C+vi, SinvisatCO, Sinvi−C−vi⊆Soutvi⊆Sinvi.
The problem of reachability analysis is a decision problem. We use the notationQEILCMp,q,Sys to represent the instance judging whether p can reach q in an EILCM system Sys. Next, we use the reduction method to analyze the complexity of this problem. The problem used to reduce from is the 3SAT problem defined below:Definition 10.
(monotone 3SAT). Given a setX of Boolean variables and a collection L of clauses over X, each l∈L having l=3 and containing either all positive variables or all negative variables, is there a satisfying truth assignment on X for L? This problem is notated as M3SATL,X. Monotone 3SAT is a special case of 3SAT.Theorem 2.
The problem of policy verifications of EILCM system isNP-complete.Proof.
We first reduce monotone 3SAT to the problem in polynomial time, that is, MSAT∝P QEILCM. Given a monotone 3SAT instance M3SATL,X, assume X=x1,x2,…,xK and L=a1∧a2∧…∧aM∧b1∧b2∧…∧bN, where each clause ai=xi1∨xi2∨xi3 and each clause bj=xj1¯∨xj2¯∨xj3¯. We produce the corresponding QEILCM instance QEILCMp,q,Sys, Sys=U,DS,S,C,CO as follows.
Constructing the tags: for each clauseai, 1≤i≤M, we introduce a secrecy protection tag di into S. For each clause bj, 1≤j≤N, we introduce three secrecy protection tags dj′1,dj′2,dj′3.
Constructing the first part of subject: for each Boolean variablexi∈X, 1≤i≤K, we introduce a subject ui into U with its initial secrecy level Sui=φ and its capabilities Cui=dj+|1≤j∈M∪dj′w+|1≤j≤N,1≤w≤3. Then, for each clause ai=xi1∨xi2∨xi3, let Cui1=Cui1∪di−, Cui2=Cui2∪di−, Cui3=Cui3∪di−; for each clause bj=xj1¯∨xj2¯∨xj3¯, let Sujw=Sujw∪dj′w, where 1≤w≤3.
Constructing the second part of subject: for each clausebj=xj1¯∨xj2¯∨xj3¯, 1≤j≤N, we introduce three subjects: uj′1,uj′2,uj′3 into U, let each subject’s secrecy level Suj′w=φ, and let each subject’s capabilities Cuj′w=di′y+|1≤i≤N,1≤y≤3,i≠j∪dj′z±|1≤z≤3,z≠w.
Constructingp, q, and CO: let Sp=di|1≤i≤M. Let Sq=φ. Let CO=φ.
Clearly the construction process can be finished in polynomial time. Next, we prove thatM3SATL,X is true if and only if QEILCMp,q,Sys is true.
Equivalence of the two problems: in problemM3SATL,X, if there exist true/false assignments to the variables such that formula L is satisfiable, let set X′=xs1,xs2,…,xsw be the variables assigned to true. Then, in problem QEILCMp,q,Sys, we can prove that the path p,us1,us2,…,usw,1in3u1′1,u1′2,u1′3,1in3u2′1,u3′2,u4′3,…,1in3un′1,un′2,un′3,q is legal, where 1in3uj′1,uj′2,uj′3, 1≤j≤n, denotes choosing one subject as the current node from subjects uj′1,uj′2,uj′3 that can legally forward the information from the previous node. Here, we can reasonably assume that each node x in the path will delete every tag it has the right to delete from its current level when it receives the information from previous node, that is, Soutx=Sinx−C−x. Now, since each clause ai=xi1∨xi2∨xi3 is true, 1≤i≤m, X′ includes at least one variant of xi1,xi2,xi3. Therefore, corresponding to each tag di in p’s levels, 1≤i≤m, there is at least one subject of us1,us2,…,usw that can delete di from its own contaminated level when the information flow from p passes the path p,us1,us2,…,usw. And since bj=xj1¯∨xj2¯∨xj3¯ is true, X′ includes at most two variables of xj1,xj2,xj3. Correspondingly, for each group of tags dj′1,dj′2,dj′3, \1≤j≤n, after the information flow passes the path p,us1,us2,…,usw, Soutusw includes at most two tags of this group. This means that the path 1in3u1′1,u1′2,u1′3,1in3u2′1,u3′2,u4′3,...,1in3un′1,un′2,un′3 can delete all the tags that are bound with the information level and contaminated by us1,us2,…,usw. Therefore, if the formula L is satisfiable, p can reach q.
For the “only if” part, assume that there exists a legal pathp,v1,v2,…,vw,q, where vi∈uy|1≤y≤K∪uz′|1≤z≤N,1≤i≤w. We first simplify the path. Let the node vr be the first one whose Soutvr does not include the tags di, 1≤i≤M. According to our transformation, for each vj where j≤r, we have vi∈uy|1≤y≤K, that is, another form of the path is p,uλ1,uλ2,…,uλy,vr+1,vr+2…,vwq. Moreover, it is easy to determine that the path remains legal after deleting arbitrary node vj where j>r and vj∈uz′|1≤z≤N, and we use p,uλ1,uλ2,…,uλr,uγr+1′,uγr+2′,…,uγw′q to denote the remains of the path. From the path, we pick up the subjects that belong to ui|1≤i≤K to constitute set U′. Each variable in X that corresponds to each user in U′ constitutes the set X′. If the variables in X′ are assigned to true and the variables in X−X′ are assigned to false, we can prove L is true. In fact, for each tag di involved in p’s levels, there must be at least a subject vz that has the ability to delete di from its own level. Correspondingly, for each ai=xi1∨xi2∨xi3, X′ involves at least one of xi1,xi2,xi3. Meanwhile, for each bj=xj1¯∨xj2¯∨xj3¯, it is impossible that X′ simultaneously involves xj1,xj2,xj3; otherwise, before the information that comes from p and flows down the path arrived uγr+1′, the information has been contaminated by dj1′1,dj1′2,dj1′3 simultaneously, that is, dj1′1,dj1′2,dj1′3 ∈ Soutuλy. However, according to our transformation, no subject among uj′1,uj′2,uj′3 has the abilities to delete all the three tags simultaneously, and the path does not exist, which is contradictory to our assumption, so each bj=xj1¯∨xj2¯∨xj3¯ holds. Therefore, if p can reach q, then formula L is satisfiable. Now we can prove MSAT ∝P QEILCM, that is, QEILCM is NP-hard.
Next, we show the QEILCM in NP. Given an instanceQEILCMp,q,Sys with a solution in form of a path, the verification algorithm can get the answers in linear time On, where n is the length of path. Now we prove that the problem of policy verifications of EILCM system is NP-complete.
Theorem2 shows that in the worst case, the policy verification problem in EILCM system cannot be solved in polynomial time. It reflects that the EILCM policy with the rich expressive ability can provide management solutions for complex fine-grained information flow control. The high complexity of EILCM is attributed to the mechanisms of decentralized declassification and taint-tracking. According to this conclusion, the complexity of the verification algorithm is exponential, and a good verification algorithm should solve fewer instances over long time periods while solving most EILCM instances in short time periods. With some search optimization strategies, the backtracking algorithm can guarantee a low computational overhead in most cases.


### 4.2. Algorithms for QEILCM

The backtracking algorithm searches the solution in the tree of candidate solutions, which starts from the root node and does not search the subtree that must not include the solution. The process of searching is systematic and jumping. In our problem, ifp is a source node and q is a destination node, then p is regarded as the root node, the leaf nodes are the subjects who can send information to q, and the middle nodes are the subjects that can receive information from their parent nodes. Therefore, the path from root node to leaf node is an information flow path from p to q. The tree is an arrangement of subjects. In our algorithm, the variable curpath records the current searched path, and pathlen records the length of current searched path. The backtracking function searches all the possible paths’ depth recursively.We adopt two policies to decrease the search space. We firstly introduce a pruning functionprunecurpathpathlen to prune the subtree where there must not be solutions, and its root node is curpathpathlen. That is, if the node curpathpathlen has a tag in its levels that no subject on its extending subtree has the ability to delete, the function returns 0. The pruning function avoids the ineffective search. In order to decrease the computation amount, we introduce the integer array allsub, with each item in it corresponding to a tag and recording the sum of subjects that do not exist in current path and have abilities to delete the tag. Each recursion only does the incremental computation rather than the overall computation again. Secondly, we adjust the search order and search preferentially the subjects that have greater benefits and smaller expense, which can efficiently select the next node to extend. We define a subject i’s priority PRIi=tainti/subtracti, where tainti is the sum of tags it has no ability to delete from its levels, that is, tainti=Si−Ci−, and subtracti is the size of Ci−. PRI considers the influence of the subject i’s contaminated situation (expenses) and its abilities of deleting tags (benefits). In the preprocess stage, function SortbyPRI arranges the search priority from the subjects having small priority to subjects having great priority. Algorithm 1 is as follows.Algorithm 1:QEILCM (u0..n−1co0,k−1).
Input: array u0..n−1: each item records a subject’s levels and capabilities. n: sum of the subjects. co: set of mutually exclusive tags constraints.Output: if u0 can reach un−1, then print the path; else print “unreachable.”QEILCM (u){u=SortbyPRIu;curpath0=u0;ifBacktrack1,u,curpath,pathlenthenoutputcurpath;elseoutput″cannot find path″; }Backtrack (depth, u, curpath, pathlen){ifdepth=n−1 return 0;if not canflowcurpathpathlen,un−1return 1;ifprunecurpathpathlen,allsubcapabilityreturn 0;fori=depth,…,n−2{ifcanflowcurpathpathlen,uicontinue;ifnot flowsuccesscurpathpathlen,ui,curpathpathlen+1continue;pathlen++; swapudepth,uiremove capabilityall sub,curpathpathlen;.ifBacktrackdepth+1,u,curpath,pathlen=1return 1;addcapabilityallsub,curpathpathlen;.pathlen++; swapudepth,ui}return 0; }In our algorithm, functioncanflowsubject1,subject2 judges whether subject1 can send information to subject2. Function flowsuccesssubject1,subject2,curpathpathlen+1 judges whether subject 2’s levels change violates the constraints CO if subject1 can send information to subject2; moreover it will store the newly adjusted subject 1’s levels into curpathpathlen+1 if subjects have sent information to subject2. Functions addcapabilityallsub,curpathpathlen and removecapabilityallsub,curpathpathlen, respectively, add/subtract 1 to the value of each allsub item if the node curpathpathlen has the ability to delete the tag corresponding to the item. The algorithm’s computational complexity is On!. Nevertheless, because of the requirement of partial relation between the sender’s level and the receiver’s level, in general, the algorithm can get the answer in a shorter time, which can be demonstrated by the following experiments.In order to validate QEILCM algorithm, we first create a test data generator. It performs as follows: givenn subjects and m tags, for each tag d and each subject p, whether p’s levels include d depends on the random choice based on 0,1, and p’s capabilities concerning d depend on the random choice based on {0, 1,…, 5}, in which 0, 1, 2, and others denote, respectively, the following capabilities: adding d, subtracting d, both adding and subtracting d, and no capabilities. We implement the QEILCM algorithm using Visual C++. Our experiments are run on Windows2003 with an Intel P4 2.8 G CPU and 2 GB of memory.Firstly, we present our results about the algorithm’s performance under different parameter values. These parameters are as follows: subject sum (n), tag sum (m), and the size of mutually exclusive set (k). Each group with constant parameter values repeats the test 20 times. The evaluation index includes average runtime (st) and average path length (l) in case that there exists a path, average runtime (ut) in case that there does not exist a path, successful times (sc),unsuccessful times (uc), and times (N/A) in case that all the tests do not work out the result in 30 minutes. The results are shown in Table 2.Table 2
Algorithm performance under different parameter values.
nmklscucN/Ast (ms)ut (ms)30152310100<13601525.512811412015281550141201547.51460131202041081112712030472180462003048.2514110274400304209832500730020005083531522200113005000508824610171505.2∗ 105Table2 shows that although its complexity is exponential time, we can get the answers in most cases. If m and k are constants, the increase of runtime the algorithm takes will not be proportional to the increase of n at all, and even st has no distinct change, possibly because the scale of the arranging tree is not increased in proportion to the increase of subject sum under the constraints of partial relation of levels between the subjects. If the parameter k is constant, with the increase of m, the runtime will decrease remarkably because the subject’s levels are generated randomly and the probability that a pair of subject’s levels satisfying partial relations will decrease when m is bigger. If n and m are constants, with the increase of k, the success rate will appreciably decrease with the increase in k, while the runtime has no distinct change.Secondly, we present our results about the functionsprune and SortbyPRI influencing algorithm performance. Letting k = 2, for different combinations of n/m, we test eight times to compare the runtime in the case of using them with the runtime in the case of not using them. As shown in Figure 3, functions prune and SortbyPRI improve the search efficiency remarkably.Figure 3
Influence of functionprune and SortbyPRI on performance.


## 4.1. Problem Definition and Complexity

The purpose of noninterference analysis is to verify whether the EILCM system implements the information flow control according to the information flow policies and whether there are covert channels in which there are information flows that violate the security policy, including explicit and implicit information flows. If the system is secure without interference, it means that the implementation of the system strictly adheres to the security policy and there is no covert channels.The purpose of policy verification is to verify the information flow reachability problem under a given tag and capability allocation scheme. The EILCM model is highly flexible, often with thousands of entities whose capabilities and tags are varied. Also, the EILCM model is dynamic, and its information flow accessibility is complicated. Then, the burden on administrators is large, which can easily lead to policy mismatches and mismatches. Automated policy verification can assist administrators in managing policies and thus is required.In EILCM, although the subject’s capabilities for deleting secrecy tags or adding integrity tags from its own levels have good semantics, these capabilities complicate the information flow analysis. We need to verify whether information can flow from one subject/object to another subject/object in the system state transitions. For instance, a subjectA with SA=ds1, IA=di1, and CA= cannot send messages directly to a subject B with SB=ds2, IB=di2, and CA=, but A can indirectly achieve its goals through forwarding a subject M with SM=ds1, IM=, and MC=ds1−,di2+.In our model, the secrecy submodel is the dual of the integrity submodel. Their problems of policy analysis are equivalent and can be transformed into each other. A conversion method is as follows: given an integrity tagd, for each subject/object x, we use the notation Ixd: a1,a2,a3 denoting its integrity level on d, where a1,a2,a3∈0,1, a1 denotes whether x’s level involves d, a2 denotes whether x has the capability of adding d to its own integrity level, and a3 denotes whether x has the capability of deleting d from its own integrity level. We can give its dual form of secrecy level on d: Sxda1¯,a3,a2. Similarly, if we let Iyd: b1,b2,b3 be y’s integrity level on d, then we have Syd: b1¯,b3,b2 as y’s secrecy level on d. By enumerating all possible cases, we can determine that the integrity constraint of Ixd and Iyd and the secrecy constraint of Sxd and Syd have the same effect on communication. Therefore, in order to simplify the analysis, we only consider the constraints of secrecy protection on the information flow.Moreover, there are two aspects that can simplify the analysis. Firstly, it is easy to determine that the remaining part of a legal path after deleting all the object-type nodes is still a legal path because the object’s capability is empty. For instance, if a pathp⟶o⟶q is legal, where p,q are subjects and o is an object, then p⟶q is legal. So, we need not consider objects being nodes in a legal path. Secondly, in terms of Definition 3, the new-born subject’s capabilities are the subset of its parent subject’s capabilities, while its secrecy/integrity levels are lower than its parent’s. That is, any legal path remains legal if we replace some subject node with the subject’s parent. So we need not consider generating subjects.To facilitate its description, an EILCM system instanceSys is a 9-tuple Sys=U,O,DS,DI,S,I,C,CO,A, where U denotes the set of all the users, O denotes the set of all the objects, DS denotes the set of all the secrecy(export) protection tags, DI denotes the set of integrity(import) protection tags. Let V=U∪O; then, S:V⟶2DS maps the each subject/object onto secrecy levels, I:V⟶2DI maps the each subject/object onto integrity levels, C:S⟶2DS∪DI×+,− maps each subject/object onto capabilities, R is the set of mutually exclusive tags constraints, and A:O⟶2DS∪DI×+,− maps each object onto “capability” attributes. According to the analysis of the object’s influence, our policy verifications ignore new process generation, any objects occurring in the path, and integrity protection. Therefore, Sys can be simplified as U,DS,S,C,CO . Next, we can define the problem of policy verifications of EILCM systems.Definition 9.
(policy verification problem of EILCM systems). Given an EILCM system instanceSys=U,DS,S,C,CO, for ∀p,q∈U, we say p can reach q if and only if there is a path v1,v2,…,vn, where v1=p, vn=q, vi∈U, 1≤i≤n, and the information can legally flow in terms of requirement of EILCM. Let Sinitialvi be the initial secrecy level of vi before the query. Let Sinvi be the secrecy levels of vi just when vi has received the information from vi−1. Let Soutvi be the secrecy levels of vi when vi is sending the information to vi+1. That is, the path needs to satisfy two constraints: (1) information flow constraints: Soutvi−1⊆Sinvi, 1<i≤n; Soutvi⊆Sinvi+1, 1≤i<n; (2) level adjusting constraints: Sinitialvi⊆Sinvi⊆Sinitialvi∪C+vi, SinvisatCO, Sinvi−C−vi⊆Soutvi⊆Sinvi.
The problem of reachability analysis is a decision problem. We use the notationQEILCMp,q,Sys to represent the instance judging whether p can reach q in an EILCM system Sys. Next, we use the reduction method to analyze the complexity of this problem. The problem used to reduce from is the 3SAT problem defined below:Definition 10.
(monotone 3SAT). Given a setX of Boolean variables and a collection L of clauses over X, each l∈L having l=3 and containing either all positive variables or all negative variables, is there a satisfying truth assignment on X for L? This problem is notated as M3SATL,X. Monotone 3SAT is a special case of 3SAT.Theorem 2.
The problem of policy verifications of EILCM system isNP-complete.Proof.
We first reduce monotone 3SAT to the problem in polynomial time, that is, MSAT∝P QEILCM. Given a monotone 3SAT instance M3SATL,X, assume X=x1,x2,…,xK and L=a1∧a2∧…∧aM∧b1∧b2∧…∧bN, where each clause ai=xi1∨xi2∨xi3 and each clause bj=xj1¯∨xj2¯∨xj3¯. We produce the corresponding QEILCM instance QEILCMp,q,Sys, Sys=U,DS,S,C,CO as follows.
Constructing the tags: for each clauseai, 1≤i≤M, we introduce a secrecy protection tag di into S. For each clause bj, 1≤j≤N, we introduce three secrecy protection tags dj′1,dj′2,dj′3.
Constructing the first part of subject: for each Boolean variablexi∈X, 1≤i≤K, we introduce a subject ui into U with its initial secrecy level Sui=φ and its capabilities Cui=dj+|1≤j∈M∪dj′w+|1≤j≤N,1≤w≤3. Then, for each clause ai=xi1∨xi2∨xi3, let Cui1=Cui1∪di−, Cui2=Cui2∪di−, Cui3=Cui3∪di−; for each clause bj=xj1¯∨xj2¯∨xj3¯, let Sujw=Sujw∪dj′w, where 1≤w≤3.
Constructing the second part of subject: for each clausebj=xj1¯∨xj2¯∨xj3¯, 1≤j≤N, we introduce three subjects: uj′1,uj′2,uj′3 into U, let each subject’s secrecy level Suj′w=φ, and let each subject’s capabilities Cuj′w=di′y+|1≤i≤N,1≤y≤3,i≠j∪dj′z±|1≤z≤3,z≠w.
Constructingp, q, and CO: let Sp=di|1≤i≤M. Let Sq=φ. Let CO=φ.
Clearly the construction process can be finished in polynomial time. Next, we prove thatM3SATL,X is true if and only if QEILCMp,q,Sys is true.
Equivalence of the two problems: in problemM3SATL,X, if there exist true/false assignments to the variables such that formula L is satisfiable, let set X′=xs1,xs2,…,xsw be the variables assigned to true. Then, in problem QEILCMp,q,Sys, we can prove that the path p,us1,us2,…,usw,1in3u1′1,u1′2,u1′3,1in3u2′1,u3′2,u4′3,…,1in3un′1,un′2,un′3,q is legal, where 1in3uj′1,uj′2,uj′3, 1≤j≤n, denotes choosing one subject as the current node from subjects uj′1,uj′2,uj′3 that can legally forward the information from the previous node. Here, we can reasonably assume that each node x in the path will delete every tag it has the right to delete from its current level when it receives the information from previous node, that is, Soutx=Sinx−C−x. Now, since each clause ai=xi1∨xi2∨xi3 is true, 1≤i≤m, X′ includes at least one variant of xi1,xi2,xi3. Therefore, corresponding to each tag di in p’s levels, 1≤i≤m, there is at least one subject of us1,us2,…,usw that can delete di from its own contaminated level when the information flow from p passes the path p,us1,us2,…,usw. And since bj=xj1¯∨xj2¯∨xj3¯ is true, X′ includes at most two variables of xj1,xj2,xj3. Correspondingly, for each group of tags dj′1,dj′2,dj′3, \1≤j≤n, after the information flow passes the path p,us1,us2,…,usw, Soutusw includes at most two tags of this group. This means that the path 1in3u1′1,u1′2,u1′3,1in3u2′1,u3′2,u4′3,...,1in3un′1,un′2,un′3 can delete all the tags that are bound with the information level and contaminated by us1,us2,…,usw. Therefore, if the formula L is satisfiable, p can reach q.
For the “only if” part, assume that there exists a legal pathp,v1,v2,…,vw,q, where vi∈uy|1≤y≤K∪uz′|1≤z≤N,1≤i≤w. We first simplify the path. Let the node vr be the first one whose Soutvr does not include the tags di, 1≤i≤M. According to our transformation, for each vj where j≤r, we have vi∈uy|1≤y≤K, that is, another form of the path is p,uλ1,uλ2,…,uλy,vr+1,vr+2…,vwq. Moreover, it is easy to determine that the path remains legal after deleting arbitrary node vj where j>r and vj∈uz′|1≤z≤N, and we use p,uλ1,uλ2,…,uλr,uγr+1′,uγr+2′,…,uγw′q to denote the remains of the path. From the path, we pick up the subjects that belong to ui|1≤i≤K to constitute set U′. Each variable in X that corresponds to each user in U′ constitutes the set X′. If the variables in X′ are assigned to true and the variables in X−X′ are assigned to false, we can prove L is true. In fact, for each tag di involved in p’s levels, there must be at least a subject vz that has the ability to delete di from its own level. Correspondingly, for each ai=xi1∨xi2∨xi3, X′ involves at least one of xi1,xi2,xi3. Meanwhile, for each bj=xj1¯∨xj2¯∨xj3¯, it is impossible that X′ simultaneously involves xj1,xj2,xj3; otherwise, before the information that comes from p and flows down the path arrived uγr+1′, the information has been contaminated by dj1′1,dj1′2,dj1′3 simultaneously, that is, dj1′1,dj1′2,dj1′3 ∈ Soutuλy. However, according to our transformation, no subject among uj′1,uj′2,uj′3 has the abilities to delete all the three tags simultaneously, and the path does not exist, which is contradictory to our assumption, so each bj=xj1¯∨xj2¯∨xj3¯ holds. Therefore, if p can reach q, then formula L is satisfiable. Now we can prove MSAT ∝P QEILCM, that is, QEILCM is NP-hard.
Next, we show the QEILCM in NP. Given an instanceQEILCMp,q,Sys with a solution in form of a path, the verification algorithm can get the answers in linear time On, where n is the length of path. Now we prove that the problem of policy verifications of EILCM system is NP-complete.
Theorem2 shows that in the worst case, the policy verification problem in EILCM system cannot be solved in polynomial time. It reflects that the EILCM policy with the rich expressive ability can provide management solutions for complex fine-grained information flow control. The high complexity of EILCM is attributed to the mechanisms of decentralized declassification and taint-tracking. According to this conclusion, the complexity of the verification algorithm is exponential, and a good verification algorithm should solve fewer instances over long time periods while solving most EILCM instances in short time periods. With some search optimization strategies, the backtracking algorithm can guarantee a low computational overhead in most cases.


## 4.2. Algorithms for QEILCM

The backtracking algorithm searches the solution in the tree of candidate solutions, which starts from the root node and does not search the subtree that must not include the solution. The process of searching is systematic and jumping. In our problem, ifp is a source node and q is a destination node, then p is regarded as the root node, the leaf nodes are the subjects who can send information to q, and the middle nodes are the subjects that can receive information from their parent nodes. Therefore, the path from root node to leaf node is an information flow path from p to q. The tree is an arrangement of subjects. In our algorithm, the variable curpath records the current searched path, and pathlen records the length of current searched path. The backtracking function searches all the possible paths’ depth recursively.We adopt two policies to decrease the search space. We firstly introduce a pruning functionprunecurpathpathlen to prune the subtree where there must not be solutions, and its root node is curpathpathlen. That is, if the node curpathpathlen has a tag in its levels that no subject on its extending subtree has the ability to delete, the function returns 0. The pruning function avoids the ineffective search. In order to decrease the computation amount, we introduce the integer array allsub, with each item in it corresponding to a tag and recording the sum of subjects that do not exist in current path and have abilities to delete the tag. Each recursion only does the incremental computation rather than the overall computation again. Secondly, we adjust the search order and search preferentially the subjects that have greater benefits and smaller expense, which can efficiently select the next node to extend. We define a subject i’s priority PRIi=tainti/subtracti, where tainti is the sum of tags it has no ability to delete from its levels, that is, tainti=Si−Ci−, and subtracti is the size of Ci−. PRI considers the influence of the subject i’s contaminated situation (expenses) and its abilities of deleting tags (benefits). In the preprocess stage, function SortbyPRI arranges the search priority from the subjects having small priority to subjects having great priority. Algorithm 1 is as follows.Algorithm 1:QEILCM (u0..n−1co0,k−1).
Input: array u0..n−1: each item records a subject’s levels and capabilities. n: sum of the subjects. co: set of mutually exclusive tags constraints.Output: if u0 can reach un−1, then print the path; else print “unreachable.”QEILCM (u){u=SortbyPRIu;curpath0=u0;ifBacktrack1,u,curpath,pathlenthenoutputcurpath;elseoutput″cannot find path″; }Backtrack (depth, u, curpath, pathlen){ifdepth=n−1 return 0;if not canflowcurpathpathlen,un−1return 1;ifprunecurpathpathlen,allsubcapabilityreturn 0;fori=depth,…,n−2{ifcanflowcurpathpathlen,uicontinue;ifnot flowsuccesscurpathpathlen,ui,curpathpathlen+1continue;pathlen++; swapudepth,uiremove capabilityall sub,curpathpathlen;.ifBacktrackdepth+1,u,curpath,pathlen=1return 1;addcapabilityallsub,curpathpathlen;.pathlen++; swapudepth,ui}return 0; }In our algorithm, functioncanflowsubject1,subject2 judges whether subject1 can send information to subject2. Function flowsuccesssubject1,subject2,curpathpathlen+1 judges whether subject 2’s levels change violates the constraints CO if subject1 can send information to subject2; moreover it will store the newly adjusted subject 1’s levels into curpathpathlen+1 if subjects have sent information to subject2. Functions addcapabilityallsub,curpathpathlen and removecapabilityallsub,curpathpathlen, respectively, add/subtract 1 to the value of each allsub item if the node curpathpathlen has the ability to delete the tag corresponding to the item. The algorithm’s computational complexity is On!. Nevertheless, because of the requirement of partial relation between the sender’s level and the receiver’s level, in general, the algorithm can get the answer in a shorter time, which can be demonstrated by the following experiments.In order to validate QEILCM algorithm, we first create a test data generator. It performs as follows: givenn subjects and m tags, for each tag d and each subject p, whether p’s levels include d depends on the random choice based on 0,1, and p’s capabilities concerning d depend on the random choice based on {0, 1,…, 5}, in which 0, 1, 2, and others denote, respectively, the following capabilities: adding d, subtracting d, both adding and subtracting d, and no capabilities. We implement the QEILCM algorithm using Visual C++. Our experiments are run on Windows2003 with an Intel P4 2.8 G CPU and 2 GB of memory.Firstly, we present our results about the algorithm’s performance under different parameter values. These parameters are as follows: subject sum (n), tag sum (m), and the size of mutually exclusive set (k). Each group with constant parameter values repeats the test 20 times. The evaluation index includes average runtime (st) and average path length (l) in case that there exists a path, average runtime (ut) in case that there does not exist a path, successful times (sc),unsuccessful times (uc), and times (N/A) in case that all the tests do not work out the result in 30 minutes. The results are shown in Table 2.Table 2
Algorithm performance under different parameter values.
nmklscucN/Ast (ms)ut (ms)30152310100<13601525.512811412015281550141201547.51460131202041081112712030472180462003048.2514110274400304209832500730020005083531522200113005000508824610171505.2∗ 105Table2 shows that although its complexity is exponential time, we can get the answers in most cases. If m and k are constants, the increase of runtime the algorithm takes will not be proportional to the increase of n at all, and even st has no distinct change, possibly because the scale of the arranging tree is not increased in proportion to the increase of subject sum under the constraints of partial relation of levels between the subjects. If the parameter k is constant, with the increase of m, the runtime will decrease remarkably because the subject’s levels are generated randomly and the probability that a pair of subject’s levels satisfying partial relations will decrease when m is bigger. If n and m are constants, with the increase of k, the success rate will appreciably decrease with the increase in k, while the runtime has no distinct change.Secondly, we present our results about the functionsprune and SortbyPRI influencing algorithm performance. Letting k = 2, for different combinations of n/m, we test eight times to compare the runtime in the case of using them with the runtime in the case of not using them. As shown in Figure 3, functions prune and SortbyPRI improve the search efficiency remarkably.Figure 3
Influence of functionprune and SortbyPRI on performance.


## 5. Related Work

Information flow models can effectively control information propagation to protect the secrecy and integrity of the operating system. The traditional one-directional information flow model is too rigid to use. Much work adopts the technique of taint-tracking to capture the more precise characterization of information flow. IX [39], an experimental MLS variant of Unix, has a “drop-on-exec” feature, in which a process will rise to cover the labels of code that the process executes and data that it reads. For integrity protection, the Low-Water Mark Policy of the Biba model permits subjects to “read down” objects, but adjusts the current level of a subject to the lowest level of the object it has read. LOMAC [40] is a dynamically loadable extension for COTS Linux kernels based on the Low-Water Mark model. UMIP [41] uses only high and low integrity levels to preserve system integrity in the face of network-based attacks, where a high-integrity process may drop its integrity to low when it receives remote network traffic, and a low-integrity subject cannot perform key operations. IFEDAC [42] improves UMIP to provide strong user separation, where the integrity labels of a subject are the ID set of users who have contaminated the subject, and a process integrity level will be contaminated by the object it executes or reads. In IFEDAC, each object has read/write/manage protect classes, which are the sets of users who are authorized to read/write/manage it and originated from system DAC policy. Each subject can read/write/manage it when its level is no less than the object’s read/write/manage protect class. Mao et al. [42] developed several techniques to automate the generation of low-level policies of the taint-tracking model from data contained in software package managers and logs that capture normal usage of these systems. However, these studies do not involve the problem of the covert channel in implicit label change model and some of them might not uphold noninterference.Meanwhile, specifying and managing information flow model policies is a challenging problem. Much work develops verification techniques for access control policies. Such analysis on traditional access control models has been done well. In their landmark paper, Harrison et al. [43] first showed that in general, the safety analysis problem in the access control matrix model is undecidable. Jha et al. [44] proved that the problems of security analysis in ARBAC97 model are PSPACE-complete; further, a number of special cases of the problems are NP-complete. When it comes to policy verifications of information flow models, Chaudhuri et al. [23] presented a logic-programming language and tool, called EON, to model and analyze dynamic access control models of the Asbestos and Windows Vista systems. Query evaluation in EON can be reduced to decidable query satisfiability in a fragment of Datalog. Harris et al. [24] presented a method of abstraction that allows a model checker to verify policy soundly for DIFC programs that manipulate potentially unbounded sets of processes, principals, and communication channels. Harris et al. [20] also presented a technique that automatically turns a DIFC-unaware application with information flow requirements into a Flume application. Guttman et al. [45] presented a systematic way based on model checking to determine the information flow security properties of SELinux systems. Hicks et al. [46] modeled the SELinux MLS model, using a logical specification and implemented that specification in the Prolog language. Nevertheless, few of these studies in information flow policy analyze the computational complexity of policy verification.


## 6. Conclusions and Future Work

Aiming at the vulnerability and potential security risks of mobile operating systems, this paper proposes a flexible dynamic fine-grained security model. It can effectively protect the security of private data in untrusted operating system environments. In particular, our model can close the known covert channels because EILCM regards potential information flow situation as a possible information flow and expands the semantics of information propagation. It also solves the contradictions between users’ sharing of common software and authorization constraints for separation of duty or least privilege through mutually exclusive tags constraints.We use two ways to formally analyze its safety. Firstly, in terms of Ryan and Schneider’s definition of noninterference [26], we verify that a known covert channel in the traditional implicit label change models does not exist in EILCM. Secondly, we used an automated checker to prove that abstract EILCM systems have the security property of noninterference with declassification due to our definition of noninterference with declassification based on standard CSP-oriented specification.We prove that the problem of EILCM policy verification is an NP-complete problem through reducing the 3SAT problem to it. We also present a backtrack-based search algorithm to solve the problem. Experiments show that the algorithm is effective. This conclusion can reflect to some extent the computational complexity of the problem of Flume policy verification due to their partial similarity.In the future, we plan to use our analysis method to verify the safety of other relevant models.



---

*Source: 2481818-2021-08-25.xml*