Malicious code on Java Card smartcards: Attacks and countermeasures (2009)
Abstract. When it comes to security, an interesting difference between Java Card and regular Java is the absence of an on-card bytecode verifier on most Java Cards. In principle this opens up the...
Fingerprinting Passports (2009)
Henning Richter, Wojciech Mostowski, Erik Poll
Abstract. Passports issued nowadays have an embedded RFID chip that carries digitally signed biometric information. Access to this chip is wireless, which introduces a security risk, in that an...
Fingerprinting Passports (2008)
Henning Richter, Wojciech Mostowski, Erik Poll
Abstract. Passports issued nowadays have an embedded RFID chip that carries digitally signed biometric information. Access to this chip is wireless, which introduces a security risk, in that an...
Fingerprinting Passports (2008)
Henning Richter, Wojciech Mostowski, Erik Poll
Abstract. Passports issued nowadays have an embedded RFID chip that carries digitally signed biometric information. Access to this chip is wireless, which introduces a security risk, in that an...
Malicious code on Java Card smartcards: Attacks and countermeasures (2008)
Abstract. When it comes to security, an interesting difference between Java Card and regular Java is the absence of an on-card bytecode verifier on most Java Cards. In principle this opens up the...
JAVA CARD Tools for Together Control Center webpage. http://www.cs.chalmers.se/~woj/javacard (2008)
This is a description of the JAVA CARD Tools package for Together Control Center. The package supports the development of JAVA CARD applets (writing, compiling, installing, testing, etc.) inside the...
A Comparison of Java Cards: State-of-Affairs 2006 ∗ (2008)
Wojciech Mostowski, Jing Pan, Srikanth Akkiraju, Erik Vink, Erik Poll, Jerry Hartog
This document presents the results of a comparative study of some popular Java Cards on the market. Eight different cards from four manufacturers have been considered. The analysis has been done at...
◮ Full specification and implementation for the verification of
John Boyland, Alex Buckley, Patrice Chalin, Dave Clarke, Paola Giannini, Marieke Huisman, ...
This report contains the papers presented at FTfJP ’07: 9th workshop on Formal
John Boyland, Alex Buckley, Patrice Chalin, Dave Clarke, Paola Giannini, Marieke Huisman, ...
This report contains the papers presented at FTfJP ’07: 9th workshop on Formal
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...
Abstract OCL 2.0- UML 2003 Preliminary Version Specifying JAVA CARD API in OCL (2008)
Daniel Larsson, Wojciech Mostowski
We discuss the development of an OCL specification for the JAVA CARD API. The main purpose of this specification is to support and aid the verification of JAVA CARD programs in the KeY system. The...
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, ...
Abstract KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal...
UNU/IIST and UNU/IIST Reports (2007)
Tomasz Janowski, Wojciech Mostowski
the governments of the People's Republic of China and Portugal through a contribution to the UNU Endownment Fund. As well as providing two-thirds of the endownment fund, the Macau authorities...
FASE System Description The System: Integrating Object-Oriented Design and Formal Methods ⋆ (2007)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, ...
Abstract. This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1, which is aimed at bridging the gap between (a) OO software engineering methods...
Bernhard Beckert, Wojciech Mostowski
Abstract. In this paper we extend a program logic for verifying JAVA CARD applications by introducing a \throughout " operator that allows us to prove \strong " invariants. Strong...
Technical Report no. 2003-05 The KeY Tool 1 (2007)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, ...
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and...
Testing the Java Card Applet Firewall (2007)
Abstract. In this paper we discuss the methodology and results of testing the Java Card applet firewall mechanism. The main motivation for this work is the complexity of the firewall. Given the...
Testing the Java Card Applet Firewall (2007)
Abstract. In this paper we discuss the methodology and results of testing the Java Card applet firewall mechanism. The main motivation for this work is the complexity of the firewall. Given the...
Fully verified Java Card API reference implementation (2007)
Abstract. We present a formally verified reference implementation of the JAVA CARD API. This case study has been developed with the KeY verification system. The KeY system allows us to symbolically...
Fully verified Java Card API reference implementation (2007)
Abstract. We present a formally verified reference implementation of the JAVA CARD API. This case study has been developed with the KeY verification system. The KeY system allows us to symbolically...
Formal reasoning about non-atomic JAVA CARD methods in Dynamic Logic (2006)
Abstract. We present an extension to JAVA CARD Dynamic Logic, a program logic for reasoning about JAVA CARD programs, to handle JAVA CARD’s so-called non-atomic methods. Although JAVA CARD DL...
Engelbert Hubbers, Wojciech Mostowski, Erik Poll
Abstract. This paper reports on investigations into the JAVA CARD transaction mechanism, especially on the interaction with so-called nonatomic methods in the JAVA CARD API. This work started with...
Abstract We present an approach to systematic, toolsupported design and development of JAVA CARD applets. We employ the Unified Modeling Language (UML) and formal methods for object-oriented software...
Engelbert Hubbers, Wojciech Mostowski, Erik Poll
Abstract. This paper reports on investigations into the JAVA CARD transaction mechanism, especially on the interaction with so-called nonatomic methods in the JAVA CARD API. This work started with...
Formal reasoning about non-atomic JAVA CARD methods in Dynamic Logic (2006)
Abstract. We present an extension to JAVA CARD Dynamic Logic, a program logic for reasoning about JAVA CARD programs, to handle JAVA CARD’s so-called non-atomic methods. Although JAVA CARD DL...
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Bubel, Richard, Giese, Martin, Hähnle, Reiner, ...
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and...
Formalisation and verification of Java Card security properties in dynamic logic (2005)
Abstract. 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...
Formal Development of Safe and Secure Java Card Applets (2005)
Wojciech Mostowski, Wojciech Mostowski, C Wojciech Mostowski
This thesis is concerned with different aspects of JAVA CARD application development and use of formal methods in the JAVA CARD world. JAVA CARD is a technology that provides means to program smart...
Verification of safety properties in the presence of transactions (2005)
1 Introduction As JAVA CARD technology is picking up speed it becomes more and more inter-esting to employ formal analysis techniques in order to ensure that J AVA CARDapplications work as intended....
Formal Development of Safe and Secure Java Card Applets (2005)
Wojciech Mostowski, Wojciech Mostowski, Doktorsavhandlingar Chalmers, Tekniska Högskola, Chalmers Reproservice, Wojciech Mostowski
This thesis is concerned with formal development of JAVA CARD applets. JAVA CARD is a technology that provides a means to program smart cards with (a subset of) the JAVA language. In recent years...
Formal Development of Safe and Secure Java Card Applets (2005)
Abstract This thesis is concerned with different aspects of JAVA CARD application de-velopment and use of formal methods in the J AVA CARD world. JAVA CARD is atechnology that provides means to...
Verification of safety properties in the presence of transactions (2005)
Reiner Hähnle, Wojciech Mostowski
Abstract. The JAVA CARD transaction mechanism can ensure that a sequence of statements either is executed to completion or is not executed at all. Transactions make verification of JAVA CARD programs...
Verification of safety properties in the presence of transactions (2005)
Reiner Hähnle, Wojciech Mostowski
Abstract. The JAVA CARD transaction mechanism can ensure that a sequence of statements either is executed to completion or is not executed at all. Transactions make verification of JAVA CARD programs...
Formalisation and verification of Java Card security properties in dynamic logic (2005)
Abstract. 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...
A program logic for handling Java Card’s transaction mechanism (2003)
Bernhard Beckert, Wojciech Mostowski
Abstract. In this paper we extend a program logic for verifying JAVA CARD applications by introducing a “throughout ” operator that allows us to prove “strong ” invariants. Strong invariants...
A program logic for handling Java Card’s transaction mechanism (2003)
Bernhard Beckert, Wojciech Mostowski
Abstract. In this paper we extend a program logic for verifying JAVA CARD applications by introducing a “throughout ” operator that allows us to prove “strong ” invariants. Strong invariants...
OCL Specifications for the Java Card API (2003)
Daniel Larsson, Wojciech Mostowski, Wolfgang Ahrendt
This Master's thesis discusses the development of OCL specifications for Java Card API, and is part of the KeY project. OCL is a specification language, i.e. it is used to express formally the...
The KeY system: Integrating object-oriented design and formal methods (2002)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Elmar Habermalz, Wolfram Menzel, Wojciech Mostowski, ...
Abstract. This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1, which is aimed at bridging the gap between (a) OO software engineering methods...
Rigorous development of JAVA CARD applications (2002)
We present an approach to rigorous, tool supported design and development of JavaCard applications. We employ the Unied Modelling Language (UML) and formal methods for object oriented software...
Rigorous development of JAVA CARD applications (2002)
We present an approach to rigorous, tool supported design and development of Java Card applications. We employ the Unified Modelling Language (UML) and formal methods for object oriented software...
Fail-Stop Software Components by Pattern Matching (1999)
Tomasz Janowski, Wojciech Mostowski
China and Portugal through contribution to the UNU Endowment Fund. The mission of UNU/IIST is to assist developing countries in the application and development of software technology. UNU/IIST...