This book constitutes the refereed proceedings of the 22nd International Static Analysis Symposium, SAS 2015, held in Saint-Malo, France, in September 2015. The 18 papers presented in this volume were carefully reviewed and selected from 44 submissions. All fields of static analysis as a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance are addressed, featuring theoretical, practical, and application advances in the area

This book constitutes the refereed proceedings of the Second International Conference on Research in Smart Cards, E-smart 2001, held in Cannes, France, in September 2001. The 20 revised full papers presented were carefully reviewed and selected from 38 submissions. Among the topics addressed are biometrics, cryptography and electronic signatures on smart card security, formal methods for smart card evaluation and certification, architectures for multi-applications and secure open platforms, and middleware for smart cards and novel applications of smart cards.

Smart cards are playing an increasingly important role in areas such as ban- 1 king,electroniccommerce,andtelecommunications. TheJavaCard language hasbeenproposedasahigh-levellanguageforprogrammingmulti-application smartcards. Theuseofahigh-levellanguagecanfacilitatethedevelopmentand veri?cation of software for smart cards. The modest code size and the imp- tanceoftheapplicationareasimpliesthatitisbothpossibleanddesirableto developandapplyformalmethodsintheconstructionofsafeandsecureJava Cardsoftware. ThepresentvolumeconstitutestheproceedingsoftheJavaCardworkshop heldinCannes,14September2000. TheworkshopgrewoutoftheINRIAAction deRechercheCoop'erative"JavaCard"andwasorganizedincollaborationwith the Java Card Forum. A call for papers resulted in 14 submissions of which theprogramcommitteeselected11papersforpresentationattheworkshop. In addition,theworkshopfeaturedaninvitedtalkbyDanielLeM'etayer,Trusted Logic,onformalmethodsandsmartcardsecurity. WewishtothankCatherine Godest and Maryse Renaud for their help with preparing the proceedings for thisworkshop. February2001IsabelleAttali ThomasJensen 1 ItshouldbenotedthatJavaCardisatrademarkofSunMicrosystems. Organization ProgramCommittee ProgramChair: IsabelleAttali(INRIA,France) ThomasJensen(IRISA/CNRS,France) Committeemembers: ChristianGoire(BullCP8,France) SebastianHans(SunMicrosystems,USA) PieterHartel(UniversityofSouthampton,UK) PeterHoneyman(UniversityofMichigan,USA) PierreParadinas(Gemplus,France) JoachimPosegga(SAPCorporateResearch,Germany) TableofContents InvitedTalk FormalMethodsinContext:SecurityandJavaCard ...1 D. Bolignano,D. LeM'etayer,C. Loiseaux ContributedPapers ADynamicLogicfortheFormalVeri?cationofJavaCardPrograms ...6 BernhardBeckert ThePACAPPrototype:AToolforDetectingJavaCardIllegalFlow ...25 P. Bieber,J. Cazin,A. ElMarouani,P. Girard,J. -L. Lanet,V. Wiels, G. Zanon CardKt:AutomatedMulti-modalDeductiononJavaCardsfor Multi-applicationSecurity...38 RajeevGor'e,LanDuyNguyen A Programming and a Modelling Perspective on the Evaluation of Java CardImplementations...52 PieterH. Hartel,EduarddeJong SecureInternetSmartcards...73 NaomaruItoi,TomokoFukuzawa,PeterHoneyman IssuesinSmartcardMiddleware...90 RogerKehr,MichaelRohs,HaraldVogt OpenPlatfomSecurity ...98 MarcKekiche?,ForoughKashef,DavidBrewer ASimple(r)InterfaceDistributionMechanismforJavaCard ...1 14 KsheerabdhiKrishna,MichaelMontgomery AutomaticTestGenerationforJavaCardApplets ...121 HuguesMartin,LydieduBousquet FormalSpeci?cationandVeri?cationofJavaCard'sApplicationIdenti?er Class...137 JoachimvandenBerg,BartJacobs,ErikPoll X TableofContents Security on Your Hand: Secure Filesystems with a "Non-cryptographic" JAVA-Ring...151 R..udigerWeis,BastiaanBakker,StefanLucks AuthorIndex ...163 Formal Methods in Context: Security and Java Card D. Bolignano, D. Le Metayer, and C. Loiseaux Trusted Logic www. trusted-logic. fr 1. Security and Java Card: An Ideal Application Area for Formal Methods The benefits of formal methods for software engineering have been described at length in many research papers. They include among others: Better understanding and improved communication through unambiguous descriptions. Early bug detection thanks to the formalisation of specifications.

Erstmals liegt eine systematische Untersuchung zum Themenkomplex der Planungsstabilitat vor. Sie beschaftigt sich mit dem Problem der Instabilitat der im Rahmen einer rollierenden Planungsumgebung im Zeitablauf generierten Planungsvorgaben. Anhand operationaler Masse fur unterschiedliche Stabilitatsaspekte werden als Beispiel die strukturellen Stabilitatseigenschaften stochastischer Lagerdispositionsregeln analysiert. Es zeigt sich, dass die erreichbare Stabilitat vom Typ der Bestellregel und von den verwendeten Politikparametern abhangt, wobei vorgeschlagene modifizierte Dispositionsregeln zu deutlich stabileren Planungsergebnissen fuhren. Mit den gewonnenen Erkenntnissen erschliessen sich dem Leser neue Moeglichkeiten, um Problemen der Planungsnervositat gezielt und wissenschaftlich fundiert begegnen zu koennen

This is a reproduction of a book published before 1923. This book may have occasional imperfections such as missing or blurred pages, poor pictures, errant marks, etc. that were either part of the original artifact, or were introduced by the scanning process. We believe this work is culturally important, and despite the imperfections, have elected to bring it back into print as part of our continuing commitment to the preservation of printed works worldwide. We appreciate your understanding of the imperfections in the preservation process, and hope you enjoy this valuable book.