Safety and Security

  • Renaud Marlet and Daniel Le Metayer. First note on industrial needs in terms of language, API and security properties of Java Card. SECSAFE-TL-002.
  • Renaud Marlet. Typical code Patterns Found in Java Card Applets to be used as Targets for Program Analysis. SECSAFE-TL-003.
  • Renaud Marlet. Proposition of a Hierarchy of Languages to be studied in Secsafe. SECSAFE-TL-004.
  • Renaud Marlet. Syntax of the JCVM Language to be studied in the SecSafe Project. May 16, 2001. SECSAFE-TL-005. ( .pdf)
  • Renaud Marlet and Daniel Le Metayer. Security Properties and Java Card Specificities to be Studied in the SecSafe Project. August 23, 2001. SECSAFE-TL-006. ( .pdf)
  • Rene Rydhof Hansen. Computer Security Bibliography. July 5, 2001. SECSAFE-DAIMI-003. ( .ps)
  • Rene Rydhof Hansen. Java Bibliography. January 22, 2001. SECSAFE-DAIMI-004. ( .pdf)
  • Renaud Marlet and Cedric Mesnil. Demoney: A Demonstrative Electronic Purse - Card specification . November 22, 2002. SECSAFE-TL-007. ( .pdf)

    Static Analysis

  • Hanne Riis Nielson and Flemming Nielson. Flow Logic: a multi-paradigmatic approach to static analysis. SECSAFE-DAIMI-001.
  • Flemming Nielson and Hanne Riis Nielson. Flow Logic for Imperative Objects. SECSAFE-DAIMI-002.
  • Rene Rydhof Hansen. Flow Logic for Carmel. June 28, 2002. SECSAFE-IMM-001. ( .pdf)
  • Rene Rydhof Hansen. Extending the Flow Logic for Carmel. June 28, 2002. SECSAFE-IMM-003. Internal.
  • Marc Eluard and Thomas Jensen. Constraint-based security analysis for the Java Card firewall. SECSAFE-IRISA-002. ( .ps)
  • Thomas Jensen and Fausto Spoto. Class Analysis of Object-Oriented Programs through Abstract Interpretation. SECSAFE-IRISA-005.
  • David Clark, Chris Hankin, and Sebastian Hunt. Information Flow for Algol-like Languages . SECSAFE-ICSTM-002. ( .ps)
  • Alessandra Di Pierro, Herbert Wiklicky and Chris Hankin. Approximate Non-Interference . SECSAFE-ICSTM-007. ( .pdf)
  • Mikael Buchholtz, Hanne Riis Nielson and Flemming Nielson. Experiments with Succint Solvers . February 12, 2002. SECSAFE-IMM-002. ( .pdf)
  • Rene Rydhof Hansen. Implementing the Flow Logic for Carmel. November 13, 2002. SECSAFE-IMM-004. ( .pdf)
  • Hongyan Sun, Hanne Riis Nielson and Flemming Nielson. Data Structures in the Succint Solver . November 11, 2002. SECSAFE-IMM-005. ( .pdf)
  • Rene Rydhof Hansen. A Prototype Tool for JavaCard Firewall Analysis. November 13, 2002. SECSAFE-IMM-006. ( .pdf)
  • Frederic Besson, Thomas de Grenier de Latour and Thomas Jensen. Secure Calling Contexts for Stack Inspection . November 15, 2002. SECSAFE-IRISA-006. ( .pdf)
  • C. Bodei, M. Buchholtz, P. Degano, F. Nielson and H. Riis Nielson. Automatic Validation of Protocol Narration . August 12, 2003. SECSAFE-IMM-007. Internal.
  • Flemming Nielson, Hanne Riis Nielson and Hongyan Sun. Observation Predicates in Flow Logic September 3, 2003. SECSAFE-IMM-010. Internal.

    Semantics

  • Igor Siveroni and Chris Hankin. A Proposal for the JCVMLe Operational Semantics. October 18, 2001. SECSAFE-ICSTM-001. ( .ps)
  • Igor Siveroni, Thomas Jensen and Marc Eluard. A Formal Specification of the Java Card Firewall . October 12, 2001. SECSAFE-ICSTM-003. ( .ps)
  • Chris Hankin, Rajagopal Nagarajan, and Prahladavaradan Sampath. Flow Analysis: Games and Nets. SECSAFE-ICSTM-004. ( .ps)
  • Alessandra Di Pierro, Chris Hankin and Herbert Wiklicky. Approximate Probabilistic Confinement. November 2002. SECSAFE-ICSTM-005. ( .ps)
  • Igor Siveroni. Formalisation of the Java Card Runtime Environment and API . November 2002. SECSAFE-ICSTM-006. ( .pdf)
  • Alessandra Di Pierro, Chris Hankin and Herbert Wiklicky. Analysing Approximate Confinement under Uniform Attacks. September 2002. SECSAFE-ICSTM-008. ( .pdf)
  • Alessandra Di Pierro, Chris Hankin and Herbert Wiklicky. Process Equivalences and Probabilistic Abstract Interpretation. SECSAFE-ICSTM-009.
  • Igor Siveroni. Operational Semantics of the Java Card Virtual machine . November 2002. SECSAFE-ICSTM-010. ( .pdf)
  • Igor Siveroni. Operational Semantics of the Java Card Virtual Machine October 2003. SECSAFE-ICSTM-011. This is a revision of SECSAFE-ICSTM-010. Accepted for publication in a special issue of the Journal of Logic and Algebraic Programming on Smart Cards, Elsevier Science. ( .ps)
  • Igor Siveroni. Formalisation of the Semantics of Java Card. October 2003. SECSAFE-ICSTM-014. Replaces SECSAFE-ICSTM-006. ( .ps)

    Algorithms

  • Thomas Jensen. Iteration-based fixed point algorithms. SECSAFE-IRISA-003.
  • Mikael Buchholtz, Hanne Riis Nielson and Flemming Nielson. Experiments with Succint Solvers. SECSAFE-IMM-002. ( .pdf)
  • Henrik Pilegaard. Flow-Logic based Program Analysis - The Succint Solver v2.0 vs. XSB Prolog v2.6. SECSAFE-IMM-008. Internal.
  • Hongyan Sun, Hanne Riis Nielson and Flemming Nielson. Extended Features of the Succint Solver (V2.0). SECSAFE-IMM-009. ( .pdf)

    Tools

  • A Web-based Carmel Interpreter by Luke Jackson .
  • Renaud Marlet. Demoney: Java Card Implementation . SECSAFE-TL-008. November 21. 2002. ( .pdf)
  • Igor Siveroni and Luke Jackson. Prototype Implementation of an Integrated Interpreter and Analyser of Carmel Programs. SECSAFE-ICSTM-015. October 2003. (Report .pdf)