Aug 31, 2010: Minh Tri Ngo: Verification of Noninterference

August 31, 2010Verification of Noninterference
Room: Zi 5126Minh Tri Ngo

Our project is about developing a uniform verification framework for the protection of data. Key innovation on which the proposal is based is the notion of self-composition. This gives a different view on classical security properties, recasting them into safety properties of a single program. It allows to use the program verification techniques, which have an advantage that the verification is automatic and precise. We believe that this approach can handle a wide range of data-related security properties, such as confidentiality, integrity and availability. In the first part of the project, we work with the definitions of observational determinism, a generalization of noninterference for multi-threaded programs, and probabilistic noninterference, which arise from a probabilistic scheduler. We rephrase these definitions in terms of temporal logics. This allows to use model checking tools, e.g. Prism, to verify them.