NDLI: Runtime verification of declassification for imperative programs: Formal foundations

Please wait, while we are loading the content...

2013 International Conference on Risks and Security of Internet and Systems (CRiSIS)

2012 7th International Conference on Risks and Security of Internet and Systems (CRiSIS)

2011 6th International Conference on Risks and Security of Internet and Systems (CRiSIS)

2010 Fifth International Conference on Risks and Security of Internet and Systems (CRiSIS)

2009 Fourth International Conference on Risks and Security of Internet and Systems (CRiSIS 2009)

Title page

Foreword

Blank page

Conference committees

Blank page

Table of contents

A logical framework for reasoning about policies with trust negotiations and workflows in a distributed environment

A secured delegation of remote services on IPv6 home networks

CryptoNET: Secure federation protocol and authorization policies for SMI

Formal analysis of attacks for e-voting system

Data disclosure risk evaluation

Runtime verification of declassification for imperative programs: Formal foundations

SIDAN: A tool dedicated to software instrumentation for detecting attacks on non-control-data

Re-inforced stealth breakpoints

Permutation-based steganographic channels

A formal methodology for detection of vulnerabilities in an enterprise information system

A reference model for risk-aware business process management

Risk analysis via heterogeneous models of SCADA interconnecting Power Grids and Telco networks

Greylisting — long term analysis of anti-SPAM effect

Experiments and data analysis of electronic voting system

Modeling dependencies in security risk management

A quantitative approach to assess information security related risks

Untrustworthiness: A trust-based security metric

Honeypot router for routing protocols protection

A formal design of secure information systems by using a Formal Secure Data Flow Diagram (FSDFD)

Author index

2008 Third International Conference on Risks and Security of Internet and Systems

Runtime verification of declassification for imperative programs: Formal foundations

Content Provider	IEEE Xplore Digital Library
Author	Demongeot, T. Mallet, J. Le Traon, Y.
Copyright Year	2009
Description	Author affiliation: DGA/DET/CELAR, Bruz - France (Demongeot, T.) \|\| Telecom Bretagne, Cesson-Se¿vigne¿ - France (Le Traon, Y.) \|\| Telecom Bretagne, Brest - France (Mallet, J.)
Abstract	Declassification is required for most programs which manipulate protected data to process their results. In highly-secure programs, the declassification decision must be taken explicitly, which means that data or operations which are being declassified are known. This decision is critical and must be supported by automated verifications, which determine the risk of information leakage related to a given declassification. Currently, the available techniques are based on static analysis, which perform an over-approximation of this risk. In this paper, we study how dynamic approaches can perform more precise analysis on what is declassified and where, and finally ensure the security property, which allows declassification, at runtime. The notion of dynamic analysis w.r.t. to non-leakage properties is studied from a theoretical point of view and this proof of concept is illustrated using a ”While” language.
Starting Page	43
Ending Page	50
File Size	389421
Page Count	8
File Format	PDF
ISBN	9781424444984
ISSN	2151478X
DOI	10.1109/CRISIS.2009.5411980
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2009-10-19
Publisher Place	France
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Data security Interference dynamic analysis Telecommunications Risk analysis Information analysis Connectors Runtime declassification Information flow Information security security policies noninterference Performance analysis Protection
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

Security policies for downgrading

End-to-End Enforcement of Erasure and Declassification

Noninterference for mobile code with dynamic security domains.

A lattice-based approach to mashup security

Securing web application code by static analysis and runtime protection

Expressive Declassification Policies and Modular Static Enforcement

Epistemic temporal logic for information flow security

JSLINQ: Building Secure Applications across Tiers

Runtime protecting system for java applications with dynamic data flow analyzing

Runtime verification of declassification for imperative programs: Formal foundations

Similar Documents

Security policies for downgrading

End-to-End Enforcement of Erasure and Declassification

Noninterference for mobile code with dynamic security domains.

A lattice-based approach to mashup security

Securing web application code by static analysis and runtime protection

Expressive Declassification Policies and Modular Static Enforcement

Epistemic temporal logic for information flow security

JSLINQ: Building Secure Applications across Tiers

Runtime protecting system for java applications with dynamic data flow analyzing

Runtime verification of declassification for imperative programs: Formal foundations