JACK - A Tool for Validation of Security and Behaviour of Java Applications

Gilles Barthe; Lilian Burdy; Julien Charles; Benjamin Grégoire; Marieke Huisman; Jean-Louis Lanet; Mariela Pavlova; Antoine Requet

doi:10.1007/978-3-540-74792-5_7

JACK - A Tool for Validation of Security and Behaviour of Java Applications

Gilles Barthe, Lilian Burdy, Julien Charles, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet, Mariela Pavlova, Antoine Requet

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

21 Citations (Scopus)

Abstract

We describe the main features of JACK (Java Applet Correctness Kit), a tool for the validation of Java applications, annotated with JML specifications. JACK has been especially designed to improve the quality of trusted personal device applications. JACK is fully integrated with the IDE Eclipse, and provides an easily accessible user interface. In particular, it allows to inspect the generated proof obligations in a Java syntax, and to trace them back to the source code that gave rise to them. Further, JACK provides support for annotation generation, and for interactive verification. The whole platform works both for source code and for bytecode, which makes it particularly suitable for a proof carrying code scenario.

Original language	English
Title of host publication	Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures
Editors	Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, Willem P. de Roever
Publisher	Springer
Pages	152-174
Number of pages	23
DOIs	https://doi.org/10.1007/978-3-540-74792-5_7
Publication status	Published - 2006
Externally published	Yes
Event	5th International Symposium on Formal Methods for Components and Objects, FMCO 2006 - Amsterdam, Netherlands Duration: 7 Nov 2006 → 10 Nov 2006 Conference number: 5

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	4709

Conference

Conference	5th International Symposium on Formal Methods for Components and Objects, FMCO 2006
Abbreviated title	FMCO 2006
Country/Territory	Netherlands
City	Amsterdam
Period	7/11/06 → 10/11/06

Access to Document

10.1007/978-3-540-74792-5_7

Cite this

Barthe, G., Burdy, L., Charles, J., Grégoire, B., Huisman, M., Lanet, J.-L., Pavlova, M., & Requet, A. (2006). JACK - A Tool for Validation of Security and Behaviour of Java Applications. In F. S. D. Boer, M. M. Bonsangue, S. Graf, & W. P. D. Roever (Eds.), Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures (pp. 152-174). (Lecture Notes in Computer Science; Vol. 4709). Springer. https://doi.org/10.1007/978-3-540-74792-5_7

Barthe, Gilles ; Burdy, Lilian ; Charles, Julien et al. / JACK - A Tool for Validation of Security and Behaviour of Java Applications. Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures. editor / Frank S. de Boer ; Marcello M. Bonsangue ; Susanne Graf ; Willem P. de Roever. Springer, 2006. pp. 152-174 (Lecture Notes in Computer Science).

@inproceedings{5566b9d8f0b84d3abb6d3494664c3bd5,

title = "JACK - A Tool for Validation of Security and Behaviour of Java Applications",

abstract = "We describe the main features of JACK (Java Applet Correctness Kit), a tool for the validation of Java applications, annotated with JML specifications. JACK has been especially designed to improve the quality of trusted personal device applications. JACK is fully integrated with the IDE Eclipse, and provides an easily accessible user interface. In particular, it allows to inspect the generated proof obligations in a Java syntax, and to trace them back to the source code that gave rise to them. Further, JACK provides support for annotation generation, and for interactive verification. The whole platform works both for source code and for bytecode, which makes it particularly suitable for a proof carrying code scenario.",

author = "Gilles Barthe and Lilian Burdy and Julien Charles and Benjamin Gr{\'e}goire and Marieke Huisman and Jean-Louis Lanet and Mariela Pavlova and Antoine Requet",

year = "2006",

doi = "10.1007/978-3-540-74792-5_7",

language = "English",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "152--174",

editor = "Boer, {Frank S. de} and Bonsangue, {Marcello M.} and Susanne Graf and Roever, {Willem P. de}",

booktitle = "Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures",

address = "Germany",

note = "5th International Symposium on Formal Methods for Components and Objects, FMCO 2006, FMCO 2006 ; Conference date: 07-11-2006 Through 10-11-2006",

}

Barthe, G, Burdy, L, Charles, J, Grégoire, B, Huisman, M, Lanet, J-L, Pavlova, M & Requet, A 2006, JACK - A Tool for Validation of Security and Behaviour of Java Applications. in FSD Boer, MM Bonsangue, S Graf & WPD Roever (eds), Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures. Lecture Notes in Computer Science, vol. 4709, Springer, pp. 152-174, 5th International Symposium on Formal Methods for Components and Objects, FMCO 2006, Amsterdam, Netherlands, 7/11/06. https://doi.org/10.1007/978-3-540-74792-5_7

JACK - A Tool for Validation of Security and Behaviour of Java Applications. / Barthe, Gilles; Burdy, Lilian; Charles, Julien et al.
Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures. ed. / Frank S. de Boer; Marcello M. Bonsangue; Susanne Graf; Willem P. de Roever. Springer, 2006. p. 152-174 (Lecture Notes in Computer Science; Vol. 4709).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - JACK - A Tool for Validation of Security and Behaviour of Java Applications

AU - Barthe, Gilles

AU - Burdy, Lilian

AU - Charles, Julien

AU - Grégoire, Benjamin

AU - Huisman, Marieke

AU - Lanet, Jean-Louis

AU - Pavlova, Mariela

AU - Requet, Antoine

N1 - Conference code: 5

PY - 2006

Y1 - 2006

N2 - We describe the main features of JACK (Java Applet Correctness Kit), a tool for the validation of Java applications, annotated with JML specifications. JACK has been especially designed to improve the quality of trusted personal device applications. JACK is fully integrated with the IDE Eclipse, and provides an easily accessible user interface. In particular, it allows to inspect the generated proof obligations in a Java syntax, and to trace them back to the source code that gave rise to them. Further, JACK provides support for annotation generation, and for interactive verification. The whole platform works both for source code and for bytecode, which makes it particularly suitable for a proof carrying code scenario.

AB - We describe the main features of JACK (Java Applet Correctness Kit), a tool for the validation of Java applications, annotated with JML specifications. JACK has been especially designed to improve the quality of trusted personal device applications. JACK is fully integrated with the IDE Eclipse, and provides an easily accessible user interface. In particular, it allows to inspect the generated proof obligations in a Java syntax, and to trace them back to the source code that gave rise to them. Further, JACK provides support for annotation generation, and for interactive verification. The whole platform works both for source code and for bytecode, which makes it particularly suitable for a proof carrying code scenario.

U2 - 10.1007/978-3-540-74792-5_7

DO - 10.1007/978-3-540-74792-5_7

M3 - Conference contribution

T3 - Lecture Notes in Computer Science

SP - 152

EP - 174

BT - Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures

A2 - Boer, Frank S. de

A2 - Bonsangue, Marcello M.

A2 - Graf, Susanne

A2 - Roever, Willem P. de

PB - Springer

T2 - 5th International Symposium on Formal Methods for Components and Objects, FMCO 2006

Y2 - 7 November 2006 through 10 November 2006

ER -

Barthe G, Burdy L, Charles J, Grégoire B, Huisman M, Lanet JL et al. JACK - A Tool for Validation of Security and Behaviour of Java Applications. In Boer FSD, Bonsangue MM, Graf S, Roever WPD, editors, Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures. Springer. 2006. p. 152-174. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-74792-5_7

JACK - A Tool for Validation of Security and Behaviour of Java Applications

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this