CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Formalisation and Verification of Java Card Security Properties in Dynamic Logic

Wojciech Mostowski (Institutionen för datavetenskap)
Göteborg : Chalmers University of Technology, 2004.
[Rapport]

We present how common Java Card security properties can be formalised in Dynamic Logic and verified, mostly automatically, with the KeY system. The properties we consider, are a large subset of properties that are of importance to the smart card industry. We discuss the properties one by one, illustrate them with examples of real-life, industrial size, Java Card applications, and show how the properties are verified with the KeY Prover - an interactive theorem prover for Java Card source code based on a version of Dynamic Logic that models the full Java Card standard. We report on the experience related to formal verification of Java Card programs we gained during the course of this work. Thereafter, we present the current state of the art of formal verification techniques offered by the KeY system and give an assessment of interactive theorem proving as an alternative to static analysis.

Nyckelord: formal specification, formal verification, object oriented programs, interactive theorem proving, Dynamic Logic, Java Card, security properties



Denna post skapades 2006-08-25. Senast ändrad 2013-08-12.
CPL Pubid: 2067

 

Institutioner (Chalmers)

Institutionen för datavetenskap (2002-2004)

Ämnesområden

Information Technology

Chalmers infrastruktur

Ingår i serie

Technical report - Department of Computing Science, Chalmers University of Technology and Göteborg University 2004-08