HAL - INRIA :: [inria-00130210, version 1] Automata-based Confidentiality Monitoring

inria-00130210, version 1

%% inria-00130210, version 1
%% http://hal.inria.fr/inria-00130210/en/
@inproceedings{LEGUERNIC:2006:INRIA-00130210:1,
	title = { {A}utomata-based {C}onfidentiality {M}onitoring},
	author = {{L}e {G}uernic, {G}urvan and {B}anerjee, {A}nindya and {J}ensen, {T}homas and {S}chmidt, {D}avid},
	abstract = {{N}on-interference is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. {I}n contrast to static checking of non-interference, this paper considers dynamic, automaton-based, monitoring of information flow for a single execution of a sequential program. {T}he monitoring mechanism is based on a combination of dynamic and static analyses. {D}uring program execution, abstractions of program events are sent to the automaton, which uses the abstractions to track information flows and to control the execution by forbidding or editing dangerous actions. {T}he mechanism proposed is proved to be sound, to preserve executions of well-typed programs (in the security type system of {V}olpano, {S}mith and {I}rvine), and to preserve some safe executions of ill-typed programs.},
	keywords = {{L}anguage-based security; {M}onitoring; {A}utomata; {I}nformation flow; {C}onfidentiality; {N}on-interference},
	language = {{E}nglish},
	affiliation = {{D}epartment of {C}omputing and {I}nformation {S}ciences - {K}ansas {S}tate {U}niversity - {LANDE} - {INRIA} - {IRISA} - {CNRS} : {UMR}6074 - {INRIA} - {I}nstitut {N}ational des {S}ciences {A}ppliqu{\'e}es de {R}ennes - {U}niversit{\'e} de {R}ennes 1 },
	booktitle = {{ASIAN}'06: 11th {A}nnual {A}sian {C}omputing {S}cience {C}onference },
	address = {{T}okyo/{J}apan },
	organization = {{N}ational {I}nstitute of {I}nformatics },
	note = {{F}.: {T}heory of {C}omputation/{F}.3: {LOGICS} {AND} {MEANINGS} {OF} {PROGRAMS}/{F}.3.1: {S}pecifying and {V}erifying and {R}easoning about {P}rograms, {F}.: {T}heory of {C}omputation/{F}.3: {LOGICS} {AND} {MEANINGS} {OF} {PROGRAMS}/{F}.3.2: {S}emantics of {P}rogramming {L}anguages/{F}.3.2.2: {O}perational semantics, {F}.: {T}heory of {C}omputation/{F}.3: {LOGICS} {AND} {MEANINGS} {OF} {PROGRAMS}/{F}.3.2: {S}emantics of {P}rogramming {L}anguages/{F}.3.2.5: {P}rogram analysis, {D}.: {S}oftware/{D}.1: {PROGRAMMING} {TECHNIQUES}/{D}.1.4: {S}equential {P}rogramming, {D}.: {S}oftware/{D}.2: {SOFTWARE} {ENGINEERING}/{D}.2.5: {T}esting and {D}ebugging/{D}.2.5.6: {M}onitors, {D}.: {S}oftware/{D}.2: {SOFTWARE} {ENGINEERING}/{D}.2.4: {S}oftware/{P}rogram {V}erification/{D}.2.4.2: {C}orrectness proofs, {D}.: {S}oftware/{D}.2: {SOFTWARE} {ENGINEERING}/{D}.2.4: {S}oftware/{P}rogram {V}erification/{D}.2.4.8: {V}alidation, {D}.: {S}oftware/{D}.2: {SOFTWARE} {ENGINEERING}/{D}.2.1: {R}equirements/{S}pecifications/{D}.2.1.1: {L}anguages, {D}.: {S}oftware/{D}.3: {PROGRAMMING} {LANGUAGES}/{D}.3.1: {F}ormal {D}efinitions and {T}heory/{D}.3.1.0: {S}emantics, {D}.: {S}oftware/{D}.4: {OPERATING} {SYSTEMS}/{D}.4.6: {S}ecurity and {P}rotection/{D}.4.6.3: {I}nformation flow controls {B}anerjee and {L}e {G}uernic were partially supported by {NSF} grants {CNS}-0627748, {CNS}-0209205, {CCF}-0296182 and {ITR}-0326577. {S}chmidt was partially supported by {NSF} grants {ITR}-0326577 and {ITR}-0086154. {L}e {G}uernic was also partially supported by the {P}o{T}est{AT} project ({ACI} {S}{\'e}curit{\'e}). },
	audience = {not specified },
    day = {06},
    month = {12},
    year = {2006},
    URL = {http://hal.inria.fr/inria-00130210/en/},
    URL = {http://hal.inria.fr/inria-00130210/PDF/automatonBasedNiMonitoring.pdf},
}

%F inria-00130210, version 1
%0 Conference Proceedings
%U http://hal.inria.fr/inria-00130210/en/
%2 INFO:INFO_PL;INFO:INFO_CR;INFO:INFO_SE
%T Automata-based Confidentiality Monitoring
%A Le Guernic, Gurvan
%A Banerjee, Anindya
%A Jensen, Thomas
%A Schmidt, David
%A Le Guernic, G.
%A Banerjee, A.
%A Jensen, T.
%A Schmidt, D.
%A Le Guernic G. et al
%+ Department of Computing and Information Sciences - Kansas State University - LANDE - INRIA - IRISA - CNRS : UMR6074 - INRIA - Institut National des Sciences Appliquées de Rennes - Université de Rennes 1
%X Non-interference is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. In contrast to static checking of non-interference, this paper considers dynamic, automaton-based, monitoring of information flow for a single execution of a sequential program. The monitoring mechanism is based on a combination of dynamic and static analyses. During program execution, abstractions of program events are sent to the automaton, which uses the abstractions to track information flows and to control the execution by forbidding or editing dangerous actions. The mechanism proposed is proved to be sound, to preserve executions of well-typed programs (in the security type system of Volpano, Smith and Irvine), and to preserve some safe executions of ill-typed programs.
%2 F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs, F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.2: Semantics of Programming Languages/F.3.2.2: Operational semantics, F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.2: Semantics of Programming Languages/F.3.2.5: Program analysis, D.: Software/D.1: PROGRAMMING TECHNIQUES/D.1.4: Sequential Programming, D.: Software/D.2: SOFTWARE ENGINEERING/D.2.5: Testing and Debugging/D.2.5.6: Monitors, D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.2: Correctness proofs, D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.8: Validation, D.: Software/D.2: SOFTWARE ENGINEERING/D.2.1: Requirements/Specifications/D.2.1.1: Languages, D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.1: Formal Definitions and Theory/D.3.1.0: Semantics, D.: Software/D.4: OPERATING SYSTEMS/D.4.6: Security and Protection/D.4.6.3: Information flow controls
%G English
%8 2006-12-06
%2 not specified
%B ASIAN'06: 11th Annual Asian Computing Science Conference
%2 Tokyo/Japan
%8 2006-12-06
%2 National Institute of Informatics
%K Language-based security; Monitoring; Automata; Information flow; Confidentiality; Non-interference
%Z Banerjee and Le Guernic were partially supported by NSF grants CNS-0627748, CNS-0209205, CCF-0296182 and ITR-0326577. Schmidt was partially supported by NSF grants ITR-0326577 and ITR-0086154. Le Guernic was also partially supported by the PoTestAT project (ACI Sécurité).

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="inria-00130210"><analytic>
<author><persName><forename>Gurvan</forename><surname>Le Guernic</surname></persName>
<affiliation>
<orgName type="team">Department of Computing and Information Sciences</orgName>
<country>US</country>
<orgName type="institution">Kansas State University</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">LANDE</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Institut National des Sciences Appliquées de Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Anindya</forename><surname>Banerjee</surname></persName>
<affiliation>
<orgName type="team">Department of Computing and Information Sciences</orgName>
<country>US</country>
<orgName type="institution">Kansas State University</orgName>
</affiliation>
</author>
<author><persName><forename>Thomas</forename><surname>Jensen</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">LANDE</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Institut National des Sciences Appliquées de Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>David</forename><surname>Schmidt</surname></persName>
<affiliation>
<orgName type="team">Department of Computing and Information Sciences</orgName>
<country>US</country>
<orgName type="institution">Kansas State University</orgName>
</affiliation>
</author>
<title type="main" level="a">Automata-based Confidentiality Monitoring</title></analytic><monogr><meeting>ASIAN'06: 11th Annual Asian Computing Science Conference</meeting><imprint><pubPlace><settlement>Tokyo</settlement><country>Japan</country></pubPlace><biblScope type="publicationDate">2006-12-06</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00130210/en/</idno><idno type="HALFile">http://hal.inria.fr/inria-00130210/PDF/automatonBasedNiMonitoring.pdf</idno></biblStruct>
</listBibl>
</listBibl>

Automata-based Confidentiality Monitoring

Gurvan Le Guernic (

) ^1, 2, Anindya Banerjee (

) ¹, Thomas Jensen (

)^a^, 2, David Schmidt (

http://www.cis.ksu.edu/~schmidt/home.html

) ¹

(2006)

Access to full text
PDF

ASIAN'06: 11th Annual Asian Computing Science Conference (2006)

Abstract: Non-interference is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. In contrast to static checking of non-interference, this paper considers dynamic, automaton-based, monitoring of information flow for a single execution of a sequential program. The monitoring mechanism is based on a combination of dynamic and static analyses. During program execution, abstractions of program events are sent to the automaton, which uses the abstractions to track information flows and to control the execution by forbidding or editing dangerous actions. The mechanism proposed is proved to be sound, to preserve executions of well-typed programs (in the security type system of Volpano, Smith and Irvine), and to preserve some safe executions of ill-typed programs.

a –	CNRS
1:	Department of Computing and Information Sciences
	Kansas State University
2:	LANDE (INRIA - IRISA)
	CNRS : UMR6074 – INRIA – Institut National des Sciences Appliquées de Rennes – Université de Rennes 1

Domain

Computer Science/Programming Languages

Computer Science/Cryptography and Security

Computer Science/Software Engineering

Keywords : Language-based security – Monitoring – Automata – Information flow – Confidentiality – Non-interference


inria-00130210, version 1
http://hal.inria.fr/inria-00130210/en/
oai:hal.inria.fr:inria-00130210_v1
From: Gurvan Le Guernic <>
Submitted on: Friday, 9 February 2007 18:09:24
Updated on: Saturday, 10 February 2007 18:41:32