Abstract: With the development of the Internet,the status of cyberspace has risen,and the importance of information is increasing.To ensure the security of information,it is particularly important for the control of illegal information flow.This paper analyzed the security of information flow in a lattice model of information flow,and classified the information flow inside the model better.Firstly,the linear analysis is done for the lattice model of the information flow,which is called a linear lattice model of information flow.Then,the Markov chain is introduced,the state attribute of the Markov chain is used,and the probability variation of the two states in the Markov chain is used to quantify the representation between the subject and the object in the model.Further,the security state of each information flow is analyzed by comparing the probability of the normal return state and the transient state corresponding to the internal body and the object respectively.That is to say,when two constant return states occur simultaneously in the model detection,the security model is violated,and an illegal information flow occurs.Due to the identity of the change in probability,the method produces errors and affects its detection results.In order to overcome this shortcoming,this paper introduced the SPA language,then described the SPA language of the linear information flow model,and used the non-interference method in formalization to make the lack of probability identity in the Markov chain model.Finally,the illegal information flow hidden in it is detected,the security state of each information flow with error is judged,and it is concluded that the information flow that conforms to the security model but violates the security policy does not satisfy the non-interference attribute.This is a major significance on software design and hardware application.

Key words: Covert channel, Information flow, Markov chain, Non-interference, SPA