Statically checking confidentiality via dynamic labels

B.P.F. Jacobs; Wolter Pieters; M. Warnier

doi:10.1145/1045405.1045411

Statically checking confidentiality via dynamic labels

B.P.F. Jacobs, Wolter Pieters, M. Warnier

Research output: Contribution to conference › Paper › peer-review

10 Citations (Scopus)

122 Downloads (Pure)

Abstract

This paper presents a new approach for verifying confidentiality for programs, based on abstract interpretation. The framework is formally developed and proved correct in the theorem prover PVS. We use dynamic labeling functions to abstractly interpret a simple programming language via modification of security levels of variables. Our approach is sound and compositional and results in an algorithm for statically checking confidentiality.

Original language	Undefined
Pages	50-56
Number of pages	7
DOIs	https://doi.org/10.1145/1045405.1045411
Publication status	Published - 2005
Event	WITS '05: 2005 workshop on Issues in the theory of security - Long Beach, CA Duration: 10 Jan 2005 → 11 Jan 2005

Workshop

Workshop	WITS '05: 2005 workshop on Issues in the theory of security
Period	10/01/05 → 11/01/05
Other	10-11 Jan 2005

Keywords

SCS-Cybersecurity
IR-65097
EWI-14062

Access to Document

10.1145/1045405.1045411

http://doi.acm.org/10.1145/1045405.1045411

Cite this

@conference{a02afc3991f64c6fa0ec47bc8b69e23a,

title = "Statically checking confidentiality via dynamic labels",

abstract = "This paper presents a new approach for verifying confidentiality for programs, based on abstract interpretation. The framework is formally developed and proved correct in the theorem prover PVS. We use dynamic labeling functions to abstractly interpret a simple programming language via modification of security levels of variables. Our approach is sound and compositional and results in an algorithm for statically checking confidentiality.",

keywords = "SCS-Cybersecurity, IR-65097, EWI-14062",

author = "B.P.F. Jacobs and Wolter Pieters and M. Warnier",

year = "2005",

doi = "10.1145/1045405.1045411",

language = "Undefined",

pages = "50--56",

note = "null ; Conference date: 10-01-2005 Through 11-01-2005",

}

TY - CONF

T1 - Statically checking confidentiality via dynamic labels

AU - Jacobs, B.P.F.

AU - Pieters, Wolter

AU - Warnier, M.

PY - 2005

Y1 - 2005

N2 - This paper presents a new approach for verifying confidentiality for programs, based on abstract interpretation. The framework is formally developed and proved correct in the theorem prover PVS. We use dynamic labeling functions to abstractly interpret a simple programming language via modification of security levels of variables. Our approach is sound and compositional and results in an algorithm for statically checking confidentiality.

AB - This paper presents a new approach for verifying confidentiality for programs, based on abstract interpretation. The framework is formally developed and proved correct in the theorem prover PVS. We use dynamic labeling functions to abstractly interpret a simple programming language via modification of security levels of variables. Our approach is sound and compositional and results in an algorithm for statically checking confidentiality.

KW - SCS-Cybersecurity

KW - IR-65097

KW - EWI-14062

U2 - 10.1145/1045405.1045411

DO - 10.1145/1045405.1045411

M3 - Paper

SP - 50

EP - 56

Y2 - 10 January 2005 through 11 January 2005

ER -