Computer Science – Cryptography and Security
Scientific paper
2011-08-21
Computer Science
Cryptography and Security
7 pages, this is a full version of the work presented on 2011 IEEE INFOCOM Workshops
Scientific paper
Language-based information flow security aims to decide whether an action-observable program can unintentionally leak confidential information if it has the authority to access confidential data. Recent concerns about declassification polices have provided many choices for practical intended information release, but more precise enforcement mechanism for these policies is insufficiently studied. In this paper, we propose a security property on the where-dimension of declassification and present an enforcement based on automated verification. The approach automatically transforms the abstract model with a variant of self-composition, and checks the reachability of illegal-flow state of the model after transformation. The self-composition is equipped with a store-match pattern to reduce the state space and to model the equivalence of declassified expressions in the premise of property. The evaluation shows that our approach is more precise than type-based enforcement.
Chen Zhong
Sun Cong
Tang Liyong
No associations
LandOfFree
A New Enforcement on Declassification with Reachability Analysis 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 A New Enforcement on Declassification with Reachability Analysis, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A New Enforcement on Declassification with Reachability Analysis will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-537670