A Formal Connection between Security Automata and JML Annotations

Marieke Huisman, A. Tamalet

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)

Abstract

Security automata are a convenient way to describe security policies. Their typical use is to monitor the execution of an application, and to interrupt it as soon as the security policy is violated. However, run-time adherence checking is not always convenient. Instead, we aim at developing a technique to verify adherence to a security policy statically. To do this, we consider a security automaton as specification, and we generate JML annotations that inline the monitor~--~as a specification~--~into the application. We describe this translation and prove preservation of program behaviour, i.e., if monitoring does not reveal a security violation, the generated annotations are respected by the program. The correctness proofs are formalised using the PVS theorem prover. This reveals several subtleties to be considered in the definition of the translation algorithm and in the program requirements.
Original languageUndefined
Title of host publicationFundamental Approaches to Software Engineering
EditorsM. Checkik, M. Wirsing
Place of PublicationBerlin
PublisherSpringer
Pages340-354
Number of pages15
ISBN (Print)978-3-642-00592-3
DOIs
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume5503
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • EWI-15336
  • IR-62803
  • METIS-263839

Cite this

Huisman, M., & Tamalet, A. (2009). A Formal Connection between Security Automata and JML Annotations. In M. Checkik, & M. Wirsing (Eds.), Fundamental Approaches to Software Engineering (pp. 340-354). [10.1007/978-3-642-00593-0_23] (Lecture Notes in Computer Science; Vol. 5503). Berlin: Springer. https://doi.org/10.1007/978-3-642-00593-0_23
Huisman, Marieke ; Tamalet, A. / A Formal Connection between Security Automata and JML Annotations. Fundamental Approaches to Software Engineering. editor / M. Checkik ; M. Wirsing. Berlin : Springer, 2009. pp. 340-354 (Lecture Notes in Computer Science).
@inproceedings{705ae5b5ece647bc9c5f9c02d4b37dda,
title = "A Formal Connection between Security Automata and JML Annotations",
abstract = "Security automata are a convenient way to describe security policies. Their typical use is to monitor the execution of an application, and to interrupt it as soon as the security policy is violated. However, run-time adherence checking is not always convenient. Instead, we aim at developing a technique to verify adherence to a security policy statically. To do this, we consider a security automaton as specification, and we generate JML annotations that inline the monitor~--~as a specification~--~into the application. We describe this translation and prove preservation of program behaviour, i.e., if monitoring does not reveal a security violation, the generated annotations are respected by the program. The correctness proofs are formalised using the PVS theorem prover. This reveals several subtleties to be considered in the definition of the translation algorithm and in the program requirements.",
keywords = "EWI-15336, IR-62803, METIS-263839",
author = "Marieke Huisman and A. Tamalet",
note = "10.1007/978-3-642-00593-0_23",
year = "2009",
doi = "10.1007/978-3-642-00593-0_23",
language = "Undefined",
isbn = "978-3-642-00592-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "340--354",
editor = "M. Checkik and M. Wirsing",
booktitle = "Fundamental Approaches to Software Engineering",

}

Huisman, M & Tamalet, A 2009, A Formal Connection between Security Automata and JML Annotations. in M Checkik & M Wirsing (eds), Fundamental Approaches to Software Engineering., 10.1007/978-3-642-00593-0_23, Lecture Notes in Computer Science, vol. 5503, Springer, Berlin, pp. 340-354. https://doi.org/10.1007/978-3-642-00593-0_23

A Formal Connection between Security Automata and JML Annotations. / Huisman, Marieke; Tamalet, A.

Fundamental Approaches to Software Engineering. ed. / M. Checkik; M. Wirsing. Berlin : Springer, 2009. p. 340-354 10.1007/978-3-642-00593-0_23 (Lecture Notes in Computer Science; Vol. 5503).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - A Formal Connection between Security Automata and JML Annotations

AU - Huisman, Marieke

AU - Tamalet, A.

N1 - 10.1007/978-3-642-00593-0_23

PY - 2009

Y1 - 2009

N2 - Security automata are a convenient way to describe security policies. Their typical use is to monitor the execution of an application, and to interrupt it as soon as the security policy is violated. However, run-time adherence checking is not always convenient. Instead, we aim at developing a technique to verify adherence to a security policy statically. To do this, we consider a security automaton as specification, and we generate JML annotations that inline the monitor~--~as a specification~--~into the application. We describe this translation and prove preservation of program behaviour, i.e., if monitoring does not reveal a security violation, the generated annotations are respected by the program. The correctness proofs are formalised using the PVS theorem prover. This reveals several subtleties to be considered in the definition of the translation algorithm and in the program requirements.

AB - Security automata are a convenient way to describe security policies. Their typical use is to monitor the execution of an application, and to interrupt it as soon as the security policy is violated. However, run-time adherence checking is not always convenient. Instead, we aim at developing a technique to verify adherence to a security policy statically. To do this, we consider a security automaton as specification, and we generate JML annotations that inline the monitor~--~as a specification~--~into the application. We describe this translation and prove preservation of program behaviour, i.e., if monitoring does not reveal a security violation, the generated annotations are respected by the program. The correctness proofs are formalised using the PVS theorem prover. This reveals several subtleties to be considered in the definition of the translation algorithm and in the program requirements.

KW - EWI-15336

KW - IR-62803

KW - METIS-263839

U2 - 10.1007/978-3-642-00593-0_23

DO - 10.1007/978-3-642-00593-0_23

M3 - Conference contribution

SN - 978-3-642-00592-3

T3 - Lecture Notes in Computer Science

SP - 340

EP - 354

BT - Fundamental Approaches to Software Engineering

A2 - Checkik, M.

A2 - Wirsing, M.

PB - Springer

CY - Berlin

ER -

Huisman M, Tamalet A. A Formal Connection between Security Automata and JML Annotations. In Checkik M, Wirsing M, editors, Fundamental Approaches to Software Engineering. Berlin: Springer. 2009. p. 340-354. 10.1007/978-3-642-00593-0_23. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-00593-0_23