NDLI: Enforcing Reactive Noninterference with Reachability Analysis

Content Provider	IEEE Xplore Digital Library
Author	Cong Sun Liyong Tang Zhong Chen
Copyright Year	2011
Abstract	The reactive computational model is pervasively used as a proper abstraction of web-based applications which receive inputs and generate outputs throughout execution. The present static enforcements of information flow security on reactive program are either based on type system or abstract interpretation. In this work we first propose an approach using automated verification to check conformance with information flow policy for reactive program. This approach utilizes our previous idea to incorporate self-composition with reach ability analysis. In order to reduce the state space of model, we propose the Store-Match Self-Composition (SMSC) to avoid duplicating the low channels. The result of preliminary experiments shows that our approach is more precise and efficient than existing work and also more efficient than our previous reach ability analysis.
Starting Page	321
Ending Page	326
File Size	261780
Page Count	6
File Format	PDF
ISBN	9781612844275
DOI	10.1109/ITNG.2011.63
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2011-04-11
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	information flow Computational modeling Semantics Motorcycles pushdown system program analysis noninterference reactive program Data structures Software Security Reachability analysis
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Enforcing Relaxed Declassifications with Reference Points

Secure Information Flow in Java via Reachability Analysis of Pushdown System

Secure Information Flow by Model Checking Pushdown System

Distributed Noninterference

A new enforcement on declassification with reachability analysis

Using Dynamic Pushdown Networks to Automate a Modular Information-flow Analysis

Type-Driven Gradual Security with References

Colored Petri Nets Based Modeling of Information Flow Security

Automated enforcement for relaxed information release with reference points

Enforcing Reactive Noninterference with Reachability Analysis

Similar Documents

Enforcing Relaxed Declassifications with Reference Points

Secure Information Flow in Java via Reachability Analysis of Pushdown System

Secure Information Flow by Model Checking Pushdown System

Distributed Noninterference

A new enforcement on declassification with reachability analysis

Using Dynamic Pushdown Networks to Automate a Modular Information-flow Analysis

Type-Driven Gradual Security with References

Colored Petri Nets Based Modeling of Information Flow Security

Automated enforcement for relaxed information release with reference points

Enforcing Reactive Noninterference with Reachability Analysis