1.College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China; 2.Jiangsu Automation Research Institute,Lianyungang 222061,China

Analysis ofsystem trustworthiness based on information fl ow noninterference theory

Xiangying Kong1,2,*,YanhuiChen2,and YiZhuang1

1.College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China; 2.Jiangsu Automation Research Institute,Lianyungang 222061,China

The trustworthiness analysis and evaluation are the bases of the trust chain transfer.In this paper the formalmethod of trustworthiness analysis of a system based on the noninterference(NI)theory of the information fl ow is studied.Firstly,existing methods cannot analyze the impact of the system states on the trustworthiness ofsoftware during the process oftrustchain transfer.To solve this problem,the impact of the system state on trustworthiness ofsoftware is investigated,the run-time mutualinterference behaviorofsoftware entities is described and an interference modelofthe access controlautomaton ofa system is established. Secondly,based on the intransitive noninterference(INI)theory,a formalanalytic method of trustworthiness for trustchain transfer is proposed,providing a theoreticalbasis for the analysis ofdynamic trustworthiness ofsoftware during the trustchain transfer process. Thirdly,a prototype system with dynamic trustworthiness on a platform with dual core architecture is constructed and a veri fi cation algorithm of the system trustworthiness is provided.Finally,the monitor hypothesis is extended to the dynamic monitor hypothesis,a theorem of static judgment rule of system trustworthiness is provided,which is usefulto prove dynamic trustworthiness of a system at the beginning of system construction.Compared with previous work in this fi eld,this research proposes notonly a formal analytic method for the determination of system trustworthiness, but also a modeling method and an analysis algorithm that are feasible for practicalimplementation.

trusted computing,trustchain,intransitive noninterference(INI),dynamic trustworthiness,access control.

1.Introduction

Trusted computing proposed by the trusted computing group(TCG)is regarded as an effective method forsolving the security problem of information systems,and the core idea is to use a hardware module called trusted platform module(TPM)which is independentof CPUcontrolas the source of trust.A chain of trustis established on the basis ofthe trusted TPM,which means thatallthe software must be veri fi ed to be trustable before running[1].Software is the soul of a modern computer system because the functionality of a modern computer system is implemented in the form of software programs.Trustworthiness of a computer system is based on trustworthiness of allits running software.

The concept of trustworthiness of a software program originates from social science[2].Trust in society is defi ned as“a social behavior that prefers those who behave according to societal rules”[3].The trust relationship between two parties may vary with time and situations,so trust relationships between groups or people are dynamic [4,5].In[4],trust is characterized as a social relationship that is dynamically developed and spirally reinforced.In [6],trust is viewed as a quantity that gradually changes rather than a binary choice between trust and distrust.In fact,the trust relationship between people varies as time and situation change.For example,the trust relationship between group members varies according to the nature of their tasks and the progress of these tasks.Similar to that in social science,the trust relationship between software entities also possesses this dynamic nature.Trustworthiness of a software entity depends on both internal and externalcauses.The internalcauses are dynamic changes of the software entity itself,and the external causes are the dynamic environmentin which the software entity is executed,i.e.changes of the state of a computersystem.However,the impact of the system state on trustworthiness of software is largely overlooked in mostexisting researches.

Currently,there are many research achievements in the measurementmodelofsoftware trustworthiness.Pateland Beth use the probabilistic approach to model and measure trustworthiness ofsoftware entities running in an open network environment,but their approach emphasizes the“trust and reputation”of a software entity[7,8].In orderto re fl ect the fuzzy nature of the trust relationship,Tang and Mo employ the fuzzy set theory to model and assess the management of trustworthiness of software entities in an open network environment[9-11].There are some other approaches to modelsoftware trustworthiness. In[12,13],trust models based on the process algebra and evidence theory were proposed,and in[14],a trustmodel based on software behaviorism was presented.All these models representthe authors’own understanding and definition of the concept of trust,but they do not re fl ect the nature of the run-time interaction between software entities.The TCG proposed a TPM-based binary attestation (TBA)[1].IBM proposed integrity measurementarchitecture(IMA)based on the TBA,which is capable of doing an integrity measurementbefore loading modules into the system[15],but the integrity of modules is only one of many trustworthiness-related properties of a software entity.In[16],the limitations of trustworthiness measurementbefore TCG loading was analyzed and a conclusion was made that load-time trustworthiness does not imply run-time trustworthiness,the integrity and trustworthiness are notequivalentand static trustworthinessdoes notimply run-time trustworthiness.

To solve the problem of software run-time trustworthiness,some researchers take approaches based on the noninterference(NI)theory ofinformation fl ow.In[17],the NI theory of information fl ows into the fi eld of trusted computing.Their approach instantiates the abstract term entities in the TCG’s de fi nition oftrustworthiness in processes, maps processes to the security domain of the NI theory, establishes a trust chain transfer model based on the NI theory,and provides a formal description and validation of this model,but the forms of interference are not analyzed in their papers,and the trust chain transfer function needs further studies.Base on their work,in[18,19],an abstraction was made that a running system is composed of processes/modules,actions and state outputs.They employed the intransitive noninterference(INI)theory and reference monitor assumptions(RMA)to present a formal de fi nition,description and analysis of the conditions of a trusted running process/module.They also provided the judgment method of trust chain transfer of the trusted computing platform and proved it.A prototype of trusted computing using the virtualmachine separation technique was also constructed.

There are two problems left[18,19]:(i)The prototype system is implemented using the virtual machine which uses a very coarse trustable unit.Trustworthiness within the virtualmachine itself and how the trustchain transfers are not discussed.(ii)Any details about the implementation of the trustable communication channelare notgiven. The software dynamic trustworthiness based on process algebra is modelled,and a method of analyzing software dynamic trustworthiness is proposed[20].The method is applied to analyze the interference relationship between information fl ow within a single process and information fl ow among multiple processes based on the INI theory. These results provide a novel idea for using the INI theory to analyze the software trustworthiness during loadtime and run-time.However,researches mentioned above do nottake into accountthe impactof system state on software dynamic trustworthiness,and system trustworthiness is notstudied either.

NI of information fl ow was proposed fi rst by Goguen and Meseguer[21],which is a method for analyzing system security from the perspective of information fl ow.After that,Rushby improved it by proposing the INI model of information fl ow[22].The core idea of the INI model is thatfor a particular access operation,if the system state after a sequence of access actions are executed is identical to the state after all actions that do not interfere with a particular domain are removed from the sequence of actions with the ipurge function,then the access operation is considered to be secure,otherwise,there must be a potential access operation that could interfere with the execution of the access operation,which results in an unsafe operation.The INI model divides the system entity into several different security domains according to the prede fi ned security levels.If actions of a security domain u have no effect on the outputs of another security domain v,then it can be considered that domain u does not interfere with domain v.The interference rules of an INImodel are considered to be static,so the INI theory cannot describe changes ofthe interference relationship among software entities caused by changes of the system states and the INI theory cannot help to analyze the impact of the system state on the transfer of the trustchain.

To re fl ect the impact of the system state on interference rules,Leslie proposed a dynamic intransitive noninterference(DINI)model[23],which uses the automaton to modela system.An action willcause the state transition of the system,and generate some outputs.To re fl ect the dynamic characters of security rules of the system which changes with time,the DINI model associates rules with the state.That is to say,the system state is a dependent variable of the interference relationship.In different system states,the interference relationship between domain u and domain v is also different,so DINIis able to describe the interference relationship among security domains in differentsystem states.

In this paper,the impactofthe system state on trustworthiness of software is analyzed,the access control tech-nique is employed to model the run-time states of software,a formalanalysis method to evaluate trustworthiness of the software entity in the process of trust chain transfer and the de fi nition of trustworthiness of trust chain transfer are proposed and a judgment rule of the system dynamic trustworthiness is provided.The main innovations are:(i)we discuss the impact of system state on software trustworthiness and establish an automaton model of the dynamic systems;(ii)we propose a formal analysis method for analyzing trustworthiness of software entities and systems,and give a judgment theorem;(iii)we extend the RMA to the dynamic reference monitor assumptions(DRMA)and give a judgmenttheorem of trustworthiness of a system.

The rest of this paper is organized as follows.In Section 2,the access control technique is used to model the run-time state of software systems.Section 3 fi rst introduces the DINI model based on which a formal analytic model of run-time software trustworthiness is provided and a DINI-based system dynamic judgment theorem is proved.Section 4 uses examples to illustrate the process of analyzing the software dynamic trustworthiness with the DINI model,and presents a prototype system with dynamic trustworthiness.Section 5 is a conclusion of this paper with a summary of all work in the previous sections and gives a future research plan.

2.Modeling of the dynamic behavior of

a system

In a modern computersystem,a software program is stored in a data storage device in the form of a binary executable image before it is loaded into the system.To run the software program,the operating system(OS)will load the binary image into memory,allocate all necessary resources, create a corresponding process and start it,so a process is the form of a run-time software program.At the program loading stage,trust chain transfer is carried out with the software module as the basic unit of a transfer,so at this stage the software entity is composed of all the independently loadable modules.At the run-time stage when all the processes are scheduled to run by the OS scheduler, transfer of the system trust chain is carried out with the process as the basic unit of a transfer,so at this stage the process is the object of this study of dynamic trustworthiness of systems.

2.1 Impact of the system state on trustworthiness of processes

In[17-19],the assumption is made thatthe basic entity of trusted computing is the process.In[19],a trusted computing environment using the virtualization technology is constructed.The entity of the trustchain transfer is called a component,which is also a process from the perspective ofthe hypervisor.Allthese researches are based on the INI model,which assume that interferences among processes are invariant,and do not take into account the impacts of the system state on software trustworthiness.

In a practical system,trustworthiness of a software entity is closely related to the system state in which itis running.Consider the following two cases.

Case 1Assume there are two users Hu and Li in a system and they belong to two differentsecurity levels(security domains).Normally information is only allowed to fl ow from Li to Hu rather than the reverse direction ofinformation fl ow,but under some particular conditions,the system will temporarily upgrade the security level of Li, and allow information fl ow from Hu to Li.For example, Li obtains a temporary secret key,and is allowed to have access to a fi le thatbelongs to Hu.

Case 2The INI system constructed with the virtual machine in[19]is shown in Fig.1.The arrows represent the direction of information fl ow,i.e.the interference relationship.Due to the characteristics of software,updates are unavoidable.Assume virtualmachine A with a high security level needs to be updated,and then the system has to do this via the update module of the HyperVisor.A new domain A＇is introduced to minimize impacts ofthe updating process on the running system A.In the HyperVisor, another new domain H should be introduced,which creates the domain A＇,and copies information of A to A＇. The interference rule is A～＞H,H～＞A＇(A～＞H means domain A is allowed to interfere with domain H, i.e.information is allowed to fl ow from domain A to domain H).When domain H is copying information to confi gure domain A＇,domain A can still be communicating with virtualmachine C via a trusted channel B,as shown in Fig 2.Once A＇is properly con fi gured,A＇willreplace A to communicate with C via the trusted channel B and the system rule now is changed to A/～＞H(A/～＞H means domain A cannot interfere with domain H,i.e.information fl ow from domain A to domain H is notallowed),but domain H stillkeeps high levelsecurity information itobtains while itis con fi guring domain A＇,as shown in Fig.3. Since the system needs domain H to update domain C,a new domain C＇has to be created,which introduces rules C～＞H and H～＞C＇,and then an insecure channelis formed which allows information with a high security level to fl ow to domains with a low security level,as shown in Fig.4.As a result,as the system state changes,trustworthiness of modules which are used to update the virtual ma-chine in domain H also changes.

From the cases above,it can be seen that the interference relationship among processes changes with the system state,and trustworthiness of software at a particular time and in a particular system environmentdoes not imply its trustworthiness when it is scheduled to run for the second time in a differentsystem environment.

Fig.1 Trusted computing system constructed in[19]based on virtualmachine

Fig.2 An illustration of the process ofupdating domain A

Fig.3 Process after the upgrade

Fig.4 An illustration of the process ofupdating domain C

2.2 Definition of trustworthiness of a software entityTrustworthiness of a software entity RAincludes notonly module-integrity trustworthiness,but also run-time dynamic trustworthiness.To make it simple,in this paper it is assumed that each software entity has only one corresponding process in the system.The following is the formalde fi nition of trustworthiness of a software entity.

Definition 1Trustworthiness ofsoftware entity RAcan be formally described as

where MAdenotes the binary module before RAis loaded into the system memory.Load Trusted(MA)means MAis trusted atthe module loading stage,PAdenotes the runtime process of RA,and Run Trusted(PA)means PAis trusted during the run-time.

The TCG speci fi cation gives a measurementmethod for integrity trustworthiness[1].In this paper,trustworthiness of run-time processes is discussed.

In most computer systems,an independently loadable software module MAis an object fi le such as a binary executable or a dynamic loadable library stored on a storage device like a disk.Such a software module can be loaded into the system memory through a system loading function (data exchange between the primary memory and the sec-ondary memory could happen when processes are rescheduled and memory pages are swapped in and out),and will possess codes and data thatare used to perform a particular functionality,which is the same for OS kernels.These software modules possess the independenttext(code)segmentand data segment,and existin the form ofone process or a group of processes during the run-time.Each process possesses a group of registers,stacks/heaps and other necessary software and hardware recourses,such as CPU,I/O ports,fi le/device descriptors(handles).

According to the de fi nition of a trusted software entity by the TCG,in a trusted system,an entity is considered to be trusted if it behaves as the system expects.In other words,it does not violate the prede fi ned conventions of the system and has no adverse effect on other entities in the same system.In computer systems,during the trust chain transfer process,a software entity is loaded into the system memory,and is allowed to use system resources such as CPU and I/O devices,which implies that the direct control of registers,memory and I/O is handed over to the software entity.This type of state changes in a computer system could become the basis for a vicious process to attack the system and cause critical information leakage.To be speci fi c,the main ways a malicious process can take to adversely affect other entities are:(i)violating CPU usage conventions,and occupying the CPU completely;(ii)using the system memory illegally,obtaining information unauthorized for the malicious software entity and viciously altering the contents in the memory of storage devices;(iii)illegally accessing fi les and devices.CPU usage is determined by the OS kernel,so this kind ofattack can be avoided with the improvementof the security of the OS kernel.Attacks through(ii)and(iii)essentially take advantage of the information fl ow in the system.When a process has the CPUtime,itwillexecute a series ofactions to obtain or revise the permissions,operations or information of other software entities.These actions and outputs willviolate the prede fi ned rules of the system,and have an adverse effect on other entities.From this point of view, software attacks and information leakage can be viewed as an unexpected information fl ow in the system,which can be analyzed with the NItheory of information fl ow.

Software and hardware resources such as system memories,fi les and devices can be viewed abstractly as independently accessible(observable and changeable)objects. Each objectis given a name and an associated value.The name of each object is fi xed,but the corresponding value changes with the system state.The rule of access to an object of a process in the system is determined by a prede fi ned access control function.The access control function determines whether a given process has the right to observe(read)or change(write)a given object’s value in a particular state.A process in the system is composed of a sequence of actions.Each action accesses the setof names according to the access controlrules,and generates some outputs.Operation of the system is driven by actions,and execution of each action will drive the system into a new state.The system state is determined by allthe name-value pairs in the system.The following is the de fi nition of the dynamic behaviormodelof computersystems.

Definition 2A computer system M is an octuple{N, V,A,S,s0,O,D,F}.

N is the setofnames,representing the setofallthe alterable resources in the system,such as memory space,variables,fi les,I/O ports etc.Italic letter m is used to represent names in the set.

V is the setof values,which is allthe possible values of allthe names.Greek letterνrepresents the values.

A is the setofactions.Each action can be viewed as“input”,“command”or“instruction”thatthe automaton executes,and italic letter a and b are used to denote actions. Greek lettersαandβdenote a sequence ofactions.

S is the setof states,which is denoted using italic letters s or t.

s0is the initialstate,s0∈S.

O is the setof outputs,which is de fi ned as allthe values corresponding to the names in N in states S.

D is the setofprocesses.Each process has a corresponding security domain,and itis a one-to-one correspondence between a domain and a process.The rest of this paper makes no distinction between the security domain and its corresponding process.u and v are used to denote the security domain(process).Each process sends outoperational instructions to the system to interactwith otherparts ofthe system,and the corresponding results can be observed.

F is the set of functions,which includes the following six functions:

contents:S×N→V,contents(s,m)is the value corresponding to the name m in the state s.

observer:D×S→P(N),where P(N)is the power setof the setof names,observer(u,s)is the set of names whose values can be observed by process u in the state s.

alter:D×S→P(N),alter(u,s)is the setof names whose values can be altered by process u in the state s.

dom:A→D,a mapping from an action to a process. dom(a)denotes the associated process of action a.

step:S×A→S,the single-step state transferfunction step(s,a)=t means when an action a takes place in the state s,the system willtransfer from state s to state t.

output:S×A→O,the outputfunction output(s,a) is the returned resultof an action a in the state s.

The fi rst three functions determine the access matrix, which can be used to dynamically describe the access controlrules ofthe system.Notice thatthe state is a dependent variable of the access matrix.

The lastthree functions are used in the DINImodel.

Definition 3In system M and state s,running a process u is composed of executing a sequence of actionsthatbelong to this process,where 0≤i≤n,The system goes through a sequence of state transfersis called the state trace of process u produced when u begins to run in state s,which is denoted byis called the action trace, which is denoted by

Since programsmightjump to severaldifferentbranches according to differentconditions,so in differentstates,the externalinput mightbe different,and the action sequence executed by the process is also different,resulting in differenttraces.

To make it simple,it is assumed that the length of the action trace I is the set of non-negative integers,n∈I,i∈I and 0≤i＜n.

The functions head,tail and one are de fi ned as

A?denotes the setof action sequences.

The functions head,tail and one can be used respectively to obtain the pre fi x,suf fi x of the given length and the action of the given position in an action trace.

3.Trustworthiness modeling ofa process based on DINI theory

In[19],the DINImodelproposed by Leslie inherits many basic thoughts of Rushby,and it views a computer system as an automaton.An action will cause the transition of the system state,and generate some outputs.The main improvementof the DINI model includes the revised de fi nitions of the sources function,the ipurge function and local interference.

Functions run,do and test de fi ned in[18]are applied to the computer system modelde fi ned above in this paper.

For a system M,the system running function S× A?→S is an extension of the function step.

Λdenotes the empty sequence,?denotes concatenation and a?αmeans a is the action before the action sequence α.

Functions do and test are de fi ned as follows:

To re fl ect the dynamics of rules,the system state is introduced into the interference relationship.

It denotes the interference relationship among security domains in state s.us～＞v means domain u interferences with domain v in state s,i.e.in state s,information is allowed to fl ow from u to v,and v is able to observe the result of the execution of actions of the process u.s～＞means there is no interference relationship.

Similarly,the system state into sources and ipurge functions is introduced as a parameterto re fl ectsystem dynamics.

In order to differentiate the function sources from ipurge in the INI model and re fl ect the dynamic nature of the system model,these two functions are renamed as dsources and dipurge respectively in this paper.

Definition 4Function dsources:A?×D×S→P(D) where P(D)is the power setof D.

For a non-empty action sequence a?αs executed in a given state s,dsources checks whether a can directly interfere with a domain in dsources(αs,u,step(s,a))under the rules of state s.

Defintion 5Function dipurge:A?×D×S→A?is de fi ned as

In short,the result of performing the function dipurge(α,u,s)is to remove those actions in the sequence αwhich have no inference effect on u,and leave actions in the sequence thatdirectly orindirectly interfere with domain u.

Definition 6The dynamic security property of a system.A system with dynamic rules is secure if an arbitrary action sequenceαand action a satisfy

The security property of the system dynamic rules can be explained as follows:the system starts from the initial state s0,executes a series of actionsα∈A?,and produces a series of state transitions.Each state transition generates some outputs,and the system fi nally reaches the state s=do(α).In this state,action a of domain u(where u=dom(a))is executed,an output test(α,a)is generated.Actions a and its output u are used in a test to obtain some information about action sequenceα.If u is able to differentiate action sequenceαfrom dipurge(α,u,do(α)) by their different outputs through this test,then in state do(α),some domains v(vs～＞u)which are supposed to have no interference relationship with domain u contain actions that interfere with u,which contradicts with the prede fi ned rule vs～＞u,so the conclusion is thatthis system is insecure.

In system M,processes are mapped to security domains and the trustchain transfer of the system(module loading and process scheduling)is equivalentto performing corresponding actions belonging to differentsecurity domains, so a given trustchain transfer process can be viewed as the execution procedure of the corresponding action sequence. If the interference relationship between the mapped domains satis fi es the conditions of DINI,then the information fl ow between processes willobey the prede fi ned security rules and violations of security rules will not happen. Thatmeans scheduling and execution of the processes are performed according to the prede fi ned ways and rules with no illegal mutualinterference,and then the corresponding loading procedure is trustable.

The following is the de fi nition oftrustworthiness ofprocess execution in state s.

Definition 7A system M performs a sequence of actionsα∈A?,and reaches state s=run(s0,α).u∈D is

are the action trace and the state trace of process u in state s,respectively.allsatis fi es(14),then itcan be said thatprocess u is trusted in state s.

Next is the de fi nition of trusted transfer of the system trustchain.

Definition 8The initial state of system M is s0.s0is the root of the trust chain.Processes u0,u1,...,un∈D are sequentially scheduled and executed in the system. State siis the system state at the beginning of the execution of process ui.If on the scheduling list of the OS scheduler,the execution of each process uiis trusted in its corresponding state si,then the trust chain transfer is trusted.

4.Decision theorem of system dynamic trustworthiness based on DINI

The process dynamic trustworthiness modeland its analysis method have been provided and the decision theorem of computer system dynamic trustworthiness,which can decide trustworthiness ofthe designed system,willbe proposed in the following part.

In order to give the decision theorem of system dynamic trustworthiness,de fi nitions of output consistency,weak single step consistency and dynamic partialinterference of the computersystem M are given as follows.

Definition 9View partition and outputconsistency.The system M is view partitioned.If every process u∈D has an equivalentrelationshipu～on S,and those equivalentrelationships are consistent,then itshallmeet(15).

Outputconsistency means if the two states s and t in the system are the same for process u,then in these two states, the execution of process u and the outputresult generated by the system are also the same.

Definition 10Weak single step consistency.M is weak single step consistentif itmeets(16).

Weak single step consistency means for processes u and v,if the two states s and t in the system are different,then in these two states,the execution of one process is transparentto the other,i.e.they cannotnotice the execution of each other.

Definition 11Dynamic partial interference.For one rule,if M is a view-partitioned outputconsistency system, then itcan be said that M is dynamic partialinterfered,if itmeets(17).

Namely,if the process v does notinterfere with the process u in the state s,then the activity effectof v in the states cannotbe noticed by u.From the perspective of state s,u cannotdifferentiate the result of state s before it executes action a from the resultof state s after itexecutes action a in process v.

Definition 12Regulation interference.A system meets regulation interference.If the two states are equivalent from the perspective of process u,then under the regulations of state s and t,the aggregates of the process thatinterfere the process u are also the same.Then,(18)is valid.

Theorem 1Expansion theorem ofdynamic regulation. M is a view-partitioned dynamic regulation system.If it meets allthe following conditions:

(i)outputconsistency;

(ii)weak single step consistency;

(iii)dynamic partialinterference;

(iv)regulation interference,

then M is safe relative to the dynamic regulation,which means(12)is valid.

In order to apply the expansion theorem of the dynamic regulation to the model system just established,it is necessary to introduce the DRMA,which is different from Rushby’s RMA.It introduces dynamic characters that refl ectthe operation of the system.

First,the de fi nition of equivalentrelationshipof state aggregation S is given.

Definition 13Equivalentrelationshipof state aggregation S.and meets(19).

In state s,if acts of the system match the explanation of functions observer(u,s)and alter(u,s),the corresponding query control regulation can be executed and is regarded as safe.It needs to meet the following three assumptions.

Definition 14Dynamic reference monitorassumptions.

Assumption 1In orderto make the outputofact a only rely on the value observed by domain dom(a),(20)needs to be valid.

Assumption 2If act a transforms the system from one state to another,allnew values thatchange the objectmust only rely on the value thatcan be observed and inquired by dom(a),namely itshould meet(21).

Assumption 3In state s,if act a changes the value of object m,then dom(a)should be able to alter and access m.

In the above DRMA,the difference between DRMA and RMAis thatAssumption 1 and Assumption 3 introduce the state restriction.This improvementdirectly re fl ects the information fl ow interference relationship between the system state change and the software entity,which means the trustworthiness restriction.

The following is the dynamic trustworthiness judgment theorem based on the DINIsystem.

Theorem 2System dynamic trustworthiness judgment theorem.If a system meets the requirementof DRMA and (23),then the system is trustworthy.

Proofthe system should meetfour requirements ofthe dynamic regulation expansion theorem(Theorem 1).

(i)Requirement1:outputconsistency.

Make the view-partitioned relationshipof the dynamic intransitive expansion theorem equivalentto the corresponding relationshipof the DRMA.Assumption 1 of DRMA willdirectly getthe outputconsistency.

(ii)Requirement2:weak single step consistency.

In order to prove the weak single step consistency,it’s necessary to prove

The above formula can be rewritten as

Itcan be divided into the following three cases:Case 1

Assumption 2 of DRMA can directly getthe conclusion based on sCase 2Case 3

(iii)Requirement3:dynamic partialinterference. Prove

Through the proof by contradiction,the de fi nition ofcan be extended,namely

If contents(step(s,a),m)/=contents(s,m),through Assumption 3 of DRMA,it can be seen that m∈alter(dom(a),s)and thenu can be extrapolated through the conditions given by the theorem.

(iv)Requirement 4:regulation interference,namely to attest

In consideration ofthe orderliness of s and t,itis necessary to prove only

And then,the theorem is proved.

5.Example analysis and realization of prototype system

5.1 Example analysis

For case 1 mentioned above,the system is modeled as follows:

Security policies:

Namely,in state(h,l),the system allows information to fl ow from Hu to Li.

step and output functions:

For system actseries

The initial state of the system is s0=(h,l).Pay attention thatthe initialstate can be any trustworthy state of the system.According to De fi nition 8,check whether the transmission of the system trustworthiness chain is trustworthy or not.

(i)From initial state s0=(h,l),the system executesα sequentially.System states are

(ii)Fortwo safe domains,calculate dipurge(α,L,(h,l)), and dipurge(α,H,(h,l)).

For safe domain L

Because dom(Li,f lip)=L,and dsource((Li,flip),

Because dom(Hu,f lip)=H,and dsources(α,L, (h,l))={L}and H/∈{L},

Namely,

For safe domain H,

Because dom((Li,f lip))=L∈dsources((Li,f lip),

Because dom((Hu,f lip))=H∈dsources(α,H, (h,l))={L,H},

Namely,dipurge(α,H,(h,l))=α.

(iii)

Therefore,according to De fi nition 8,for the given safe rule,the transmission of this trustworthiness chain is untrustworthy,because the act(Hu,f lip)in the safe domain H interferes with the safe domain L.

For Case 2,the modelis: State aggregate:

φmeans empty,sAand sCmean A and C have not been updated respectively,and sA,sCmean A and C have been updated respectively.Forsimplifying the process,the updating here is regarded as an atom act which is completed instantly.Communication between A and C willnot change the state.

Act aggregate:A={aA,aC},which means both virtual machines A and C are updated.To make it simple, communication between A and C is notconsidered.

Safe domain:D={uH,uA,uC}.

To make it simple,the domain in which the trustworthy channelis located is notconsidered.

Output aggregate:O={φ,{oA},{oC},{oA,oC}} means the information left in HyperVisor by the updating act.

This means thatwhen the virtualmachine A is updated, the system does notallow the information to fl ow from uHto uC.

Functions step and output:

For system actseriesα=aAaC,the initialstate of the system is s0=φ.Note that the initial state can be any trustworthy state in the system.Through analysis,it can be found thatthe process is similar to circumstance 1.According to De fi nition 8,it can be judged that the system has information leakage.Therefore,the transmission ofthe trustworthiness chain corresponding to the act is untrustworthy.

5.2 Realization of the prototype system

This paper has provided an analysis method for processing dynamic trustworthiness.According to this method,a prototype system that supports the certi fi cation of system dynamic trustworthiness is designed and realized.

The prototype system adopts bi-kernel trustworthy architecture(bi-kernelTRA).Itis composed ofthe superkernel and the user kernel.The super kernel is an unchangeable part.Itcan access alldata in the user-kernelwhich is regarded as a process operation.In orderto supportthe certi fi cation of system dynamic trustworthiness,the bi-kernel TRA is improved and the improved prototype is called the dynamic trustworthiness system based on bi-kernel(DT-biK).The structure is shown in Fig.5.

Fig.5 Dynamic trustworthiness system based on bi-kernel

The lowest level of the DT-biK is the hardware level including TPM.The upper one of it is the super-kernel level,and the topmostlevelis the application system level user-kernel.There is a TruMonitor module embedded in the user-kernel.Itcan monitor and interceptthe operations of all the application programs.The super-kernel level includes a security policies database of application systems and other data structures thatneed to be maintained. The user-kernelcan access virtual TPM(vTPM)provided by the super-kernel level through the virtual TPM driver (vTPM Drv)and the vTPM of the super-kernel level can access the real TPMthrough vTPMDrv.

To make it simple,in the prototype system,the focus is only on acts that are related to the process and documentaccess,concentrating on Case 1.The system needs tomaintain the following three data structures.

SPDB:A security policy database used to describe the dynamic interference relationship among processes;

SSD:Asystem state descriptorused to record the current state of the system;

SAS:A system actsequence used to record executed act series of the system.

According to De fi nition 1,the trustworthiness certi fication algorithm of Trusted(RA)of the software entity RAcan be divided into two phases.The fi rst phase is to test Load Trusted(MA)and the second phase is to test Run T rusted(PA).

During the loading process of software entity,measures and tests the completeness of MAby adopting the method given by reference [11],so as to ensure static trustworthiness of RA.testopportunity happenswhen the currentdocumentexecutes the fi les.The TruMonitorintercepts the system’s scheduling and tests the trustworthiness of the wait-to-be scheduling process curProc.The testalgorithm is as follows.

Step 1Record the act of curProc as Act.P is the current system process line and p is the head of P.Make the currentprocess in a trustworthy state.

Step 2Calculate O1:=test(SAS,Act).

Step 3If p is empty,leap to Step 8.

Step 4Calculate dipurge(SAS,P,SSD).

Step 5Calculate O2:=test(dipurge(SAS,P,SSD), Act).

Step 6If O1＜＞O2,make the process in an untrustworthy state and leap to Step 8.

Step 7p:=p-＞next,leap to Step 3.

Step 8If the process is in a trustworthy state,then SAS:=SAS?Act,modify SSD:=step(SSD,Act).

Step 9Return to the state of the process.

With the realization thought of RTLinux[24,25],the DT-biK on Loongson 2F is designed and realized.As Fig.6 shows,the super-kernel is modi fi ed by adopting GDB-STUB.Itis a super kernel.The user-kernelis modi fi ed on Linux core 2.6.18.Since the super-kernelis modi fi ed by GDB-STUB,it can be independent of the userkernel code that is modi fi ed based on the standard Linux core.They can be independently stored physically and trustworthiness of the module increases.

Fig.6 Realization structure of DT-biK based on Loongson 2F platform

For the interruption management,the super-kerneluses the hardware interruption of Loongson IP2-IP7 and isolates the user-kernel from the interruption controller through softinterruption.This is realized by replacing the interruption switch function(cli and sti),interruption return functioninterruption processing function and interruption vector table of Linux.Interruption processing of the user-kernel is replaced by soft interruption,which means using a group of variables to record the interruption switch and happening conditions.However,all hardware interruptions are intercepted by the super-kernel and whether it is necessary to conductinterruption groups to the user-kernel is decided by the interruption type and mark.

On task scheduling,the super-kernel rede fi nes the scheduling function.The user-kernelis regarded as the low priority of the super-kernel,while the normaluser process can stilloperate on the user-kerneland use allkinds of services provided by the user-kernel.

As the“real process”running in the super-kernel,the communication between the measurementmodule and the user-kernelstill adopts the Mbuff communication mechanism of RTLinux.

In the prototype system of DT-biK,a simulation testfor Case 1 is conducted.The simulation result shows that Algorithm 1 can identify dynamic trustworthiness of the currentprocess operation.

6.Conclusions

Focusing on the analysis of software trustworthiness during the transmission of the trustworthiness chain,the paper analyzes the impact of the system state on process trustworthiness.It adopts access control to establish the software operation state mutual interference act model.Theaccess controlmatrix of the mutual interference act of the trustworthy entity caused by the memory,fi le/equipment handle can be directly transformed to codes so as to provide software analysis tools for system dynamic trustworthiness.It can be further used for collection/analysis of software operation state acts.Based on the DINI theory, the paper puts forward a system dynamic trustworthy form judgment theorem,which provides theoretic support for trustworthiness calculation.In addition,suf fi cient conditions of the judgment theorem in this paper are too strict for the entity trustworthiness judgment,and[26]gives a suf fi cient requisite condition which is used to check whether a system meets the INI model and provides the corresponding algorithm.The algorithm is divided into two phases.First of all,introduce an iP-observability attribute into the INI system and prove that the system will meet the INI only when it is regarded as iP-observability.And then,through the automaton transformation,a relationship between iP-observability and P-observability is tested.IP-observability is transformed to P-observability in the automaton so as to check whether the corresponding system meets INI[26]through the judgement of P-observability in the automaton.This provides a thoughtand basis about how to check whethera system meets DINI.The following plan of the research is to study the transformation method between DINIand the automaton and provide the requisite condition and the corresponding algorithm with which the system will meet the dynamic trustworthiness judgment theorem.

[1]TCG Group.TCG speci fi cation architecture overview.TCG Speci fi cation Revision.http://www.trustedcomputinggroup.org.

[2]H.G.Zhang,J.Luo,G.Jing,et al.Trusted computing research.Wuhan University:Natural Science Edition,2006, 52(5):513-518.(in Chinese)

[3]C.S.Dong.A sociological study of credibility and its typology.Journal of Hebei Normal University(Philosophy and Social Science),2004,27(1):40-43.(in Chinese)

[4]D.E.Zand.Trust and managerial problem solving.Administrative Science Quarterly,1972,17(2):229-239.

[5]H.H.Brower,F.D.Schoorman,H.Tan.A model of relational leadership:the integration of trust and leader-member exchange.Leadership Quarterly,2000,(11):227-250.

[6]R.C.Mayer,F.D.Schoorman,J.H.Davis.An integrative model of organizational trust.Academy of Management Review,1995,20(3):709-734.

[7]T.Beth,M.Borcherding,B.Klein.Valuation of thustin open network.Proc.of the European Symposium on Research in Computer Security,1994:3-18.

[8]J.Patel,T.W.T.Luke,N.R.Jennings,etal.A probabilistic trust model for handling inaccurate reputation sources.Proc. of the Third International Conference on Trust Management, 2005:193-209.

[9]W.Tang,Z.Chen.Research of subjective trust management model based on the fuzzy set theory.Journal of Software, 2003,14(9):1401-1408.(in Chinese)

[10]W.Tang,J.B.Hu,Z.Chen.Research on a fuzzy logic-based subjective trust management model.Journal of Computer Research and Development,2005,42(10):1654-1659.(in Chinese)

[11]J.Q.Mo,Z.W.Hu,X.L.Ye.Research of trust assessment method in trust computing based on fuzzy theory.Journal of Computer Application,2013,33(1):142-145.(in Chinese)

[12]X.X.Wang,X.Y.Kong,X.B.Chen.A dynamic noninterference trust chain model based on security process algebra.TELKOMNIKA Indonesian Journal of Electrical Engineering,2014,12(1):747-752.

[13]L.L.Yuan,G.S.Zeng,W.Wang.Trust evaluation model based on dempster-shafer evidence theory.Journal of Wuhan University(Natural Science Edition),2006,52(5):627-630. (in Chinese)

[14]Y.W.Qu.Software Behavior.Beijing:Electronic Industry Press,2004.(in Chinese)

[15]R.Sailer,X.Zhang,T.Jaeger,et al.Design and implementation of a TCG-based integrigty measurement architecture. Proc.of the 13th USENIX Security Symposium,2004:223-238.

[16]T.Jaeger,R.Sailer,U.Shankar.PRIMA:Policy reduced integrity measurementarchitecture.Proc.of the 11th ACM Symposium on Access Control Models and Technologies(SACMAT2006),2006:134-143.

[17]J.Zhao,C.X.Shen,J.Q.Liu,etal.A noninterference-based trusted chain model.Journal of Computer Research and Development,2008,45(6):974-980.(in Chinese)

[18]X.Zhang,Y.L.Chen,C.X.Shen.Non-interference trusted modelbased on processes.Journal on Communications,2009, 30(3):6-11.(in Chinese)

[19]X.Zhang,Q.Huang,C.X.Shen.A formal method based on noninterference foranalyzing trustchain of trusted computing platform.Chinese Journal of Computers,2010,33(1):74-81. (in Chinese)

[20]F.Zhang,M.Jiang,H.G.Wu,et al.Approach for trust analysis of software dynamic behavior based on noninterference. Computer Science,2012,39(1):101-103.(in Chinese)

[21]J.Goguen and J.Meseguer.Security policies and security models.Proc.of IEEE Symposium on Security and Privacy, 1982:11-20.

[22]J.Rushby.Noninterference,transitivity,and channel-control security policies.Menlo Park Stanford Research Institute, 1992.

[23]L.Rebekah.Dynamic intransitive noninterference.Proc.of the IEEE International Symposium on Secure Software Engineering,2006,65-74.

[24]X.Y.Kong,X.B.Chen,Y.Zhuang.A dynamic trustworthiness attestation method based on dualkernelarchitecture.InternationalJournalofHybrid Information Technology,2013,16(5): 237-248.

[25]C.E.All.A real-time Linux system for autonomous navigation and fl ight attitude controlof an uninhabit edaerial vehicle.Proc.ofthe 20th Conference on DigitalAvionics Systems, 2001:1A11-1A19.

[26]N.Ben Hadj Alouane,S.Lafrance,F.Lin,et al.Characterizing intransitive noninterference for 3-domain security policies with observability.IEEE Trans.on Automatic Control,2005, 50(6):920-925.

Biographies

Xiangying Kong was born in 1972.He received his B.S.degree in Xi’an Jiaotong University in 1995.He is currently a Ph.D.candiadate of Nanjing University of Aeronautics and Astronautics and a professor of Jiangsu Automation Research Institute.He presided over the development of multi-type electronic equipment and national defense pre-research project.His research interests include software engineering,information security and real-time operating system.

E-mail:kongxy716@aliyun.com

Yanhui Chen was born in 1973.She received her B.S.degree from Departmentof Computer Science, Southeast University.She is currently a senior engineer of Jiangsu Automation Research Institute.She presided over the development of multi-type automatic control system and C3Isystem.Her research interests include software engineering,information security and system engineering.

E-mail:chenyh@jari.cn

Yi Zhuang graduated from Department of Computer Science,Nanjing University of Aeronautics and Astronautics in 1981.She is now a Ph.D.supervisor in Nanjing University of Aeronautics and Astronautics.She has published over 50 papers in core journals or academic conferences at home and abroad.Besides,she has presided more than thirty state orprovincial projects,or scienti fi c and technological cooperation projects.Her research interests include network and distributed computing,and information security.

E-mail:zhuangyi@nuaa.edu.cn

10.1109/JSEE.2015.00043

Manuscriptreceived April25,2014.

*Corresponding author.

This work was supported by the NaturalScience Foundation of Jiangsu Province(BK2012237).