Research On Programming Language-based Secure Declassification Model

Nowadays,due to our country and society抯widespread dependence on computer and network technology,information security is more and more valued.Standard security mechanisms such as access control and encryption are essential components for protecting the confidentiality and integrity of data.But they do not provide end-to-end guarantees.Information flow control can provide such guarantees.Recently,a promising approach has been developed:the use of programming-language techniques such as process algebra and type system for enforcing information flow policies and identifying covert channels.In language-based information flow control,the security policy is often formalized as noninterference polices,which requires that confidential inputs not affect the publicly visible outputs.However,noninterference is too strong to express security properties useful in practice.Realistic computing systems do release some confidential information as part of their intended function.In this respect,our thesis uses programming-language techniques to control information declassification,and focus on the following four interrelated aspects.Firstly,addressing to dynamic information release control,we propose a dynamic robust declassification security model.We build a security lattice which is a product of confidentiality and integrity lattices,and then specify integrity endorsing policies controlling integrity level upgrading according to搘 here? and搘 hen? dimensions.An endorsing policy specifies a sequence of integrity levels through which a given data may be endorsed.Each step in the sequence is annotated with a condition that must be satisfied in order to perform the endorsing.Although declassification can only occur in a high-integrity context,we are able to upgrade the integrity of untrusted code in a controlled way to grant the code an ability to affect declassification.In addition,we show an efficient type system parameterized by a static condition analysis that can determine whether conditions are true at the time of endorsement.Developer can choose an appropriate static condition analysis(e.g.dataflow analysis and abstract interpreta- tion) according to application requirement and the characteristics of programs.Secondly,aiming at information flow control in multithreaded programs,we define a security model in the style of strong bisimulation equivalence,which can handle both information declassification and erasure.This model is robust for any choice of a particular scheduler.It accurately controls what information is released and guarantees that attackers cannot exploit declassification mechanisms to reveal more sensitive data then intended.Moreover,data after erasure cannot be abused by attackers.In order to determine whether a given program is secure or not,we present a non-transforming type system and a transforming type system which enforce the same security policy. The former simply checks whether a program is well-typed,while the latter uses the cross-copying technique to eliminate internal timing covert channels resulting from the interplay between different threads.If a program is not accepted by the non-transforming type system,we use the transforming type system to try to transform it into a secure one.The resulting program has the same semantics as the original program. If no such transforming rules can be applied,the program is rejected.Thirdly,considering declassification in probabilistic systems,we extend the intransitive noninterference information flow security model from deterministic systems to probabilistic systems.To model trusted parts of real systems,the concept of trust domain is introduced into Probabilistic Secure Process Algebra(PSPA).Then we present Intransitive Bisimulation Strong Probabilistic Noninterference(I_BSPNI) and Intransitive Probabilistic Bisimulation-based Nondeducibility on Composition(I_PBNDC) based on probabilistic weak bisimulation equivalence.In order to expose the potential secure problem that I_PBNDC cannot discover in dynamic context,the persistent I_PBNDC property is proposed,which requires that every reachable state of the system must satisfy I_PBNDC.The strong I_PBNDC property,which is easy to verify,is defined in terms of unwinding conditions demanding properties of individual actions. Furthermore,we analyze intransitive information flow security properties of a real probabilistic routing system.Finally,considering declassification in probabilistic timed systems,we use probabilistic timed automata to model probabilistic timed systems,and then extend the in- transitive noninterference security model to probabilistic timed systems.Thus intransitive noninterference model can be applied to information flow analysis for timed systems such as real-time systems.The set of possible actions of the automata is partitioned into high level actions,low level actions and trusted actions.Then we propose Intransitive Probabilistic Timed Noninterference(I_PTNI) and Intransitive Probabilistic Timed Nondeducibility on Composition(I_PTNDC).These properties can be used to analyze intransitive information flow for probabilistic timed systems.Moreover,we can use them to detect both probabilistic and timing covert channels.In sum,this thesis make language-based secure declassification model more practical in development and secure verification of real systems.