Semantics This task has two-subparts: modularising semantic specifications and correctness proofs; and semantic specification of security-specific aspects of Java and Java Card. Key technical challenges involve developing good semantics accounts of visibility and shareable interfaces.

Documents

	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. 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)