Alessandra Di Pierro, Chris Hankin, Igor Siveroni and Herbert Wiklicky. Tempus Fugit: How to Plug it. To appear in the special issue of the Journal of Logic and Algebraic Programming on Information Flow and Dependency, Elsevier 2006.
Igor Siveroni. Filling out the gaps: a padding algorithm for transforming out timing leaks. In Proceedings of the 3rd Workshop on Quantitative Aspects of Programming Languauges , ETAPS 05, Edinburgh 2005.
Rene Rydhof Hansen and Igor Siveroni. Towards verification of well-formed transactions in Java Card bytecode. To be published as part of the proceedings for the 1st Workshop on Bytecode Semantics, Verification, Analysis and Transformation , ETAPS 05, Edinburgh 2005.
Igor Siveroni. Operational Semantics of the Java Card Virtual Machine. Journal of Logic and Algebraic Programming Volume 58, Issues 1-2 , January-March 2004, Pages 3-25. Formal Methods for Smart Cards.
Abstract: We present the operational semantics of Carmel, a language that models the Java Card Virtual Machine Language. We define a small-step relation between program configurations, including rules for exception handling, array objects and subroutines. We also include the basic structures needed to model object ownership and the Java Card firewall. The main goal of this work is to present a readable and complete specification of the JCVM that can be used as a component of the specification of the whole Java Card system which takes into account the JCRE and API.
Igor Siveroni, Thomas Jensen and Marc Eluard. A Formal Specification of the Java Card Firewall. In Hane Riis Nielson (ed.): Proceedings NordSec 2001, Sixth Nordic Workshop on Secure IT-Systems , 1-2 November 2001, Technical University of Denmark. Technical Report IMM-TR-2001-14.
Abstract: Secure processing is fundamental for Java Card applications. The Java Card platform supports a subset of the Java programming language features including the security mechanisms associated to the supported language subset. Due to the nature of the Java Card system and its applications, Java language-level security mechanisms are insufficient to provide a satisfactory security level. Additional runtime security mechanisms are needed. The aim of this paper is to provide a formal specification of the Java Card firewall, a mechanism designed to protect the security and integrity of the Java Card runtime environment (JCRE) and of each applet. In the Java Card firewall scheme, applets can only access objects that were created by applets defined in the same package or through special object sharing mechanisms such as shareable interfaces. We present a precise specification of the Java Card Firewall for a small subset of the Java Card virtual machine language. We define the operational semantics of the language subset and include the firewall security checks as part of the evaluation rules.
Mitchell Wand and Igor Siveroni. Constraint Systems for Useless Variable Elimination. In Proceedings 26th ACM Symposium on Programming Languages, 1999.
Abstract: A useless variable is one whose value contributes nothing to the final outcome of a computation. Such variables are unlikely to occur in human-produced code, but may be introduced by various program transformations. We would like to eliminate useless parameters from procedures and eliminate the corresponding actual parameters from their call sites. This transformation is the extension to higher-order programming of a variety of dead-code elimination optimizations that are important in compilers for first-order imperative languages. Shivers has presented such a transformation. We reformulate the transformation and prove its correctness. We believe that this correctness proof can be a model for proofs of other analysis-based transformations.
Rene Rydhof Hansen and Igor Siveroni. Java Card Safety and Security through Static Analysis . October 2003. SECSAFE-IMM-011.
Abstract: This report presents the flow logic specification of a context-sensitive control and data flow analysis of JCVM programs, based on object ownership information, that includes exception handling and tracking of variable dependencies. The analysis is used to verify a number of desirable safety and security properties of Java Card programs, e.g. that no firewall violations will occur or that transactions are well-formed.
Igor Siveroni. Formalisation of the Semantics of Java Card. October 2003. SECSAFE-ICSTM-014.
Abstract: Java Card is a reactive system: activity in the card is triggered by the occurrence of events generated by the host. An event is generated and sent to the card every time the card is placed into the card acceptance device, the host sends a command, a card tear-off occurs or when the host resets the card. We present a formal specification of the semantics of Java Card that formalises the interactions between the card's components - JCVM, JCRE and API - with the host. We define the semantics of Java Card as a small-step transition system that takes as input events sent by the host. This document also includes the formalisation of the main JCRE features (defined as JCRE components) and the specification of the java.lang and javacard.framework packages.
Igor Siveroni and Luke Jackson. Prototype Implementation of an Integrated Interpreter and Analyser of Carmel Programs. October 2003. SECSAFE-ICSTM-015.
Abstract: We present a prototype implementation of an integrated interpreter and analyser of Java Card virtual machine programs. The program is made of three components: loader, interpreter and analyser. Programs are written in Carmel, a language that abstracts away some of the low-level elements of the JCVML while retaining the main features of Java Card. The loader is in charge of the parsing, linking and verification of Carmel programs. The interpreter implements the operational semantics of Carmel and provides a step-by-step visualisation of the execution of Carmel programs. The analyser performs control and data flow analysis on selected Carmel programs based on the Flow Logic specification given in SECSAFE-IMM-001-1.5 and later extended in SECSAFE-IMM-011. The analysis specification is encoded into ALFP formulas which are solved by the SML/NJ implementation of the Succint Solver. The solutions generated by the solver are parsed by the program, displayed by the GUI and used to provide information about basic safety and security property violations such as ill-formed transactions, unauthorized access and uncaught exceptions.
Igor Siveroni. Correctness of Analysis-based Program Transformations of Functional Programming Languages. PhD Thesis, Northeastern University . January 2002.