Computer Science – Cryptography and Security
Scientific paper
2010-06-22
Computer Science
Cryptography and Security
26 pages. ACM class (full): D.2.4 [Software Engineering]: Software/Program Verification---Formal Methods; F.3.2 [Logics and Me
Scientific paper
Non-interference is a semantic program property that assigns confidentiality levels to data objects and prevents illicit information flows from occurring from high to low security levels. In this paper, we present a novel security model for global non-interference which approximates non-interference as a safety property. We also propose a certification technique for global non-interference of complete Java classes based on rewriting logic, a very general logical and semantic framework that is efficiently implemented in the high-level programming language Maude. Starting from an existing Java semantics specification written in Maude, we develop an extended, information-flow Java semantics that allows us to correctly observe global non-interference policies. In order to achieve a finite state transition system, we develop an abstract Java semantics that we use for secure and effective non-interference Java analysis. The analysis produces certificates that are independently checkable and are small enough to be used in practice.
Alba-Castro Mauricio
Alpuente María
Escobar Santiago
No associations
LandOfFree
Abstract Certification of Global Non-Interference in Rewriting Logic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Abstract Certification of Global Non-Interference in Rewriting Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Abstract Certification of Global Non-Interference in Rewriting Logic will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-108407